From 93c2d19a8681bf86fa0d3f8d92266f32c1bf5c7b Mon Sep 17 00:00:00 2001 From: Ali Younis Date: Sat, 15 Oct 2016 15:41:38 -0700 Subject: [PATCH] Added to formal part --- version2/doc/iotcloud_formal/iotcloud.tex | 128 +++++++++++++++++++++- 1 file changed, 123 insertions(+), 5 deletions(-) diff --git a/version2/doc/iotcloud_formal/iotcloud.tex b/version2/doc/iotcloud_formal/iotcloud.tex index 679c218..8239655 100644 --- 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$\\ \ForAll{$payloadItems$ in $payload_s$} - \State $PISSN \gets PISSN \cup \tuple{payloadItem, ssn_s}$ + \State $PISSN \gets PISSN \cup \{\tuple{payloadItem, ssn_s}\}$ \EndFor\\ \State \Return {$PISSN$} @@ -491,7 +491,7 @@ The following helper functions are needed:\\ \EndIf \State $SpaceRemaining \gets SpaceRemaining -$ \Call{GetSize}{$payload'$} - \State $payload_s \gets payload_s \cup payload'$ + \State $payload_s \gets payload_s \cup \{payload'\}$ \EndIf \EndFor\\ \State \Return{$payload_s$} @@ -554,7 +554,7 @@ The following helper functions are needed:\\ \State $rp \gets$ Empty $resize$ payload \State $cs \gets$ \Call{GetDataStrucSize}{ } \State $rp \gets \tuple{cs * 2}$ - \State \Return{$rp$} + \State \Return{$\{rp\}$} \EndFunction \end{algorithmic} \end{varwidth}% @@ -644,7 +644,7 @@ The following helper functions are needed:\\ \State $payload_s \gets$ \Call{RescuePayloadItems}{$payload_s$} \State $payload_s \gets$ \Call{PadPayload}{$payload_s$} \State $vc \gets $ \Call{GenerateVectorClock}{ } - \State $hmac \gets$ \Call{GetHmac}{$mid, vc, payload_s$} + \State $hmac \gets$ \Call{GenerateHmac}{$mid, vc, payload_s$} \State $record \gets \tuple{mid,vc,hmac,payload}$ \State $record \gets $\Call{Encrypt}{$record$} \State \Call{PutSlotServer}{$record$} @@ -653,11 +653,129 @@ The following helper functions are needed:\\ \end{varwidth}% } +%Check Data Structure for Malicious Activity +%\noindent\fbox{% +%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} +\textbf{Check Data Structure for Malicious Activity:} +\begin{algorithmic}[1] +\Function{CheckDataStructForValidity}{ } + \State $API \gets \emptyset$ \Comment{Set of all Payload Items} + \State $ASeq \gets \emptyset$ \Comment{Set of all Payload Items that are sequences} + \State $MID \gets \emptyset$ \Comment{Set of all machine IDs} + \State $midClocks \gets \emptyset$ \Comment{Set of all clocks for the same machine IDs} + \State $oldestDeletedSsn \gets NULL$ + \State $didFindSsn \gets False$ + \State $didFindClock \gets False$ + \State $hmac \gets NULL$\\ + + \State Sort $R$ by $ssn$ from smallest $ssn$ to largest $ssn$\\ + + \ForAll{record in R} + \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$ + \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} + \State $MID \gets MID \cup \{mid'\}$ + \EndFor\\ + + \ForAll{$record$ in $R$} \Comment{Check HMACs are all valid} + \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$ + \State $hmac \gets $ \Call{GenerateHmac}{$mid', vc', payload'$} + \If{$hmac \neq hmac'$} + \State \Call{Error}{HMAC mismatch} + \EndIf + \EndFor\\ + + \ForAll{$record_1$ in $R$} \Comment{Check no SSN duplicates} + \State $\tuple{ssn_1,rData_1} \gets record_1$ + \ForAll{$record_2$ in $R$} + \If{$record_2 \neq record_1$} + \State $\tuple{ssn_2,rData_2} \gets record_2$ + \If{$ssn_2 = ssn_1$} + \State \Call{Error}{Duplicate SSN for different records} + \EndIf + \EndIf + \EndFor + \EndFor\\ + + + \ForAll{$record_1$ in $R[0:-1]$} \Comment{Check for missing SSN} + \State $\tuple{ssn_1,rData_1} \gets record_1$ + \State $didFindSsn \gets False$ + \ForAll{$record_2$ in $R[1:]$} + \State $\tuple{ssn_2,rData_2} \gets record_2$ + \If{$ssn_2 = (ssn_1 + 1)$} + \State $didFindSsn \gets True$ + \State Break + \EndIf + \EndFor + + \If{$\lnot didFindSsn$} + \State \Call{Error}{Missing SSN in SSN sequence.} + \EndIf + \EndFor\\ + + \ForAll{$\tuple{ssn, payload}$ in $API$} + \If{($payload$ is a $delete) \land$ \Call{IsLive}{$payload, ssn$}} + \State $\tuple{ssn'} \gets payload$ + \State $oldestDeleteSsn \gets ssn'$ + \ElsIf{($payload$ is a $sequence) \land$ \Call{IsLive}{$payload, ssn$}} + \State $ASeq \gets ASeq \cup \{payload\}$ + \EndIf + \EndFor\\ + + + \ForAll{$record$ in $R$} \Comment{Check SSN's are all valid} + \State $\tuple{ssn, rData} \gets record$ + \ForAll{$\tuple{rid', ssn'}$ in $ASeq$} + \If{$(rid' =$ \Call{GetRid}{$record$}$) \land ssn' \neq ssn$} + \State \Call{Error}{SSN mismatch} + \EndIf + \EndFor + \EndFor\\ + + + \State $\tuple{ssn, payload} \gets R[0]$ \Comment{Get first record in the sorted R} + \If{$ssn > (oldestDeleteSsn + 1) $} + \State \Call{Error}{Missing records} + \EndIf\\ + + + \ForAll{$mid$ in $MID$} + \State $midClocks \gets \emptyset$ + + \ForAll{record in R} + \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$ + \If{$mid' = mid$} + \State $\tuple{c_{mid_1}, c_{mid_2},...,c_{mid_k}} \gets vc'$ + \State $midClocks \gets midClocks \cup \{c_{mid_n}|mid_n=mid\}$ + \EndIf + \EndFor\\ + + \State Sort $midClocks$ from smallest clock to largest clock\\ + + \ForAll{$c_1$ in $midClocks[0:-1]$} \Comment{Check for missing SSN} + \State $didFindSsn \gets False$ + \ForAll{$c_2$ in $midClocks[1:]$} + \If{$c_2 = (c_1 + 1)$} + \State $didFindClock\gets True$ + \State Break + \EndIf + \EndFor + \EndFor + + \If{$\lnot didFindClock$} + \State \Call{Error}{Missing clock in clock sequence for: $mid$.} + \EndIf + \EndFor\\ + + \State \Comment{If got here then data structure is valid} +\EndFunction +\end{algorithmic} +%\end{varwidth}% +%} -\textbf{Check Data Structure for Malicious Activity:}\\ \textbf{Transaction Live}:\\ \textbf{Commit Live}:\\ \textbf{Key Value Live}:\\ -- 2.34.1