Added to formal part

diff --git a/version2/doc/iotcloud_formal/iotcloud.tex b/version2/doc/iotcloud_formal/iotcloud.tex
index 679c218fe228d7200b070acc53ad7085a085954b..8239655f65380ee177ae9e929805f14e16f3e538 100644 (file)
--- a/version2/doc/iotcloud_formal/iotcloud.tex
+++ b/version2/doc/iotcloud_formal/iotcloud.tex
@@ -199,7 +199,7 @@ The following helper functions are needed:\\
     \State $\tuple{mid_s, vc_s, hmac_s, payload_s} \gets rd_s$\\\r
     \r
     \ForAll{$payloadItems$ in $payload_s$}\r
     \State $\tuple{mid_s, vc_s, hmac_s, payload_s} \gets rd_s$\\\r
     \r
     \ForAll{$payloadItems$ in $payload_s$}\r

-        \State $PISSN \gets PISSN \cup \tuple{payloadItem, ssn_s}$\r
+        \State $PISSN \gets PISSN \cup \{\tuple{payloadItem, ssn_s}\}$\r

     \EndFor\\\r
     \r
     \State \Return {$PISSN$}\r
     \EndFor\\\r
     \r
     \State \Return {$PISSN$}\r


@@ -491,7 +491,7 @@ The following helper functions are needed:\\
             \EndIf\r
             \r
             \State $SpaceRemaining \gets SpaceRemaining -$ \Call{GetSize}{$payload'$}\r
             \EndIf\r
             \r
             \State $SpaceRemaining \gets SpaceRemaining -$ \Call{GetSize}{$payload'$}\r

-            \State $payload_s \gets payload_s \cup payload'$\r
+            \State $payload_s \gets payload_s \cup \{payload'\}$\r

         \EndIf\r
     \EndFor\\\r
     \State \Return{$payload_s$}\r
         \EndIf\r
     \EndFor\\\r
     \State \Return{$payload_s$}\r


@@ -554,7 +554,7 @@ The following helper functions are needed:\\
     \State $rp \gets$ Empty $resize$ payload\r
     \State $cs \gets$ \Call{GetDataStrucSize}{ }\r
     \State $rp \gets \tuple{cs * 2}$\r
     \State $rp \gets$ Empty $resize$ payload\r
     \State $cs \gets$ \Call{GetDataStrucSize}{ }\r
     \State $rp \gets \tuple{cs * 2}$\r

-    \State \Return{$rp$}\r
+    \State \Return{$\{rp\}$}\r

 \EndFunction\r
 \end{algorithmic}\r
 \end{varwidth}% \r
 \EndFunction\r
 \end{algorithmic}\r
 \end{varwidth}% \r


@@ -644,7 +644,7 @@ The following helper functions are needed:\\
     \State $payload_s \gets$ \Call{RescuePayloadItems}{$payload_s$}\r
     \State $payload_s \gets$ \Call{PadPayload}{$payload_s$}\r
     \State $vc \gets $ \Call{GenerateVectorClock}{ }\r
     \State $payload_s \gets$ \Call{RescuePayloadItems}{$payload_s$}\r
     \State $payload_s \gets$ \Call{PadPayload}{$payload_s$}\r
     \State $vc \gets $ \Call{GenerateVectorClock}{ }\r

-    \State $hmac \gets$ \Call{GetHmac}{$mid, vc, payload_s$}\r
+    \State $hmac \gets$ \Call{GenerateHmac}{$mid, vc, payload_s$}\r

     \State $record \gets \tuple{mid,vc,hmac,payload}$\r
     \State $record \gets $\Call{Encrypt}{$record$}\r
     \State \Call{PutSlotServer}{$record$}\r
     \State $record \gets \tuple{mid,vc,hmac,payload}$\r
     \State $record \gets $\Call{Encrypt}{$record$}\r
     \State \Call{PutSlotServer}{$record$}\r


@@ -653,11 +653,129 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
 \end{varwidth}% \r
 }\r
 \r

+%Check Data Structure for Malicious Activity\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Data Structure for Malicious Activity:}\r
+\begin{algorithmic}[1]\r
+\Function{CheckDataStructForValidity}{ }\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $ASeq \gets \emptyset$   \Comment{Set of all Payload Items that are sequences}\r
+    \State $MID \gets \emptyset$   \Comment{Set of all machine IDs}\r
+    \State $midClocks \gets \emptyset$ \Comment{Set of all clocks for the same machine IDs}\r
+    \State $oldestDeletedSsn \gets NULL$\r
+    \State $didFindSsn \gets False$\r
+    \State $didFindClock \gets False$\r
+    \State $hmac \gets NULL$\\\r
+    \r
+    \State Sort $R$ by $ssn$ from smallest $ssn$ to largest $ssn$\\\r
+    \r
+    \ForAll{record in R}\r
+        \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+        \State $MID \gets MID \cup \{mid'\}$\r
+    \EndFor\\\r
+\r
+    \ForAll{$record$ in $R$} \Comment{Check HMACs are all valid}\r
+        \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$\r
+        \State $hmac \gets $ \Call{GenerateHmac}{$mid', vc', payload'$}\r
+        \If{$hmac \neq hmac'$}\r
+            \State \Call{Error}{HMAC mismatch}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \ForAll{$record_1$ in $R$} \Comment{Check no SSN duplicates}\r
+        \State $\tuple{ssn_1,rData_1} \gets record_1$\r
+        \ForAll{$record_2$ in $R$}\r
+            \If{$record_2 \neq record_1$}\r
+               \State $\tuple{ssn_2,rData_2} \gets record_2$\r
+               \If{$ssn_2 = ssn_1$}\r
+                    \State \Call{Error}{Duplicate SSN for different records}\r
+               \EndIf\r
+            \EndIf\r
+        \EndFor\r
+    \EndFor\\\r
+    \r
+    \r
+    \ForAll{$record_1$ in $R[0:-1]$} \Comment{Check for missing SSN}\r
+        \State $\tuple{ssn_1,rData_1} \gets record_1$\r
+        \State $didFindSsn \gets False$\r
+        \ForAll{$record_2$ in $R[1:]$}\r
+            \State $\tuple{ssn_2,rData_2} \gets record_2$\r
+            \If{$ssn_2 = (ssn_1 + 1)$}\r
+                \State $didFindSsn \gets True$\r
+                \State Break\r
+            \EndIf\r
+        \EndFor\r
+        \r
+        \If{$\lnot didFindSsn$}\r
+            \State \Call{Error}{Missing SSN in SSN sequence.}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
+        \If{($payload$ is a $delete) \land$ \Call{IsLive}{$payload, ssn$}}\r
+            \State $\tuple{ssn'} \gets payload$\r
+            \State $oldestDeleteSsn \gets ssn'$\r
+        \ElsIf{($payload$ is a $sequence) \land$ \Call{IsLive}{$payload, ssn$}}\r
+            \State $ASeq \gets ASeq \cup \{payload\}$\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \r
+    \ForAll{$record$ in $R$} \Comment{Check SSN's are all valid}\r
+        \State $\tuple{ssn, rData} \gets record$\r
+        \ForAll{$\tuple{rid', ssn'}$ in $ASeq$}\r
+            \If{$(rid' =$ \Call{GetRid}{$record$}$) \land ssn' \neq ssn$}\r
+                \State \Call{Error}{SSN mismatch}\r
+            \EndIf\r
+        \EndFor\r
+    \EndFor\\\r
+    \r
+    \r
+    \State $\tuple{ssn, payload} \gets R[0]$ \Comment{Get first record in the sorted R}\r
+    \If{$ssn > (oldestDeleteSsn + 1) $}\r
+        \State \Call{Error}{Missing records}\r
+    \EndIf\\\r
+    \r
+    \r
+    \ForAll{$mid$ in $MID$}\r
+        \State $midClocks \gets \emptyset$\r
+        \r
+        \ForAll{record in R}\r
+            \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$\r
+            \If{$mid' = mid$}\r
+                \State $\tuple{c_{mid_1}, c_{mid_2},...,c_{mid_k}} \gets vc'$\r
+                \State $midClocks \gets midClocks \cup \{c_{mid_n}|mid_n=mid\}$\r
+            \EndIf\r
+        \EndFor\\\r
+        \r
+        \State Sort $midClocks$ from smallest clock to largest clock\\\r
+        \r
+        \ForAll{$c_1$ in $midClocks[0:-1]$} \Comment{Check for missing SSN}\r
+            \State $didFindSsn \gets False$\r
+            \ForAll{$c_2$ in $midClocks[1:]$}\r
+                \If{$c_2 = (c_1 + 1)$}\r
+                    \State $didFindClock\gets True$\r
+                    \State Break\r
+                \EndIf\r
+            \EndFor\r
+        \EndFor\r
+        \r
+        \If{$\lnot didFindClock$}\r
+            \State \Call{Error}{Missing clock in clock sequence for: $mid$.}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State \Comment{If got here then data structure is valid}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r

 \r
 \r
 \r
 \r
 \r
 \r
 \r
 \r

-\textbf{Check Data Structure for Malicious Activity:}\\\r

 \textbf{Transaction Live}:\\\r
 \textbf{Commit Live}:\\\r
 \textbf{Key Value Live}:\\\r
 \textbf{Transaction Live}:\\\r
 \textbf{Commit Live}:\\\r
 \textbf{Key Value Live}:\\\r