version2/doc/iotcloud_formal/iotcloud.tex

   1 \documentclass[11pt]{article}\r
   2 \newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}\r
   3 \usepackage{color}\r
   4 \usepackage{amsthm}\r
   5 \usepackage{amsmath}\r
   6 \usepackage{graphicx}\r
   7 \usepackage{mathrsfs}\r
   8 \usepackage{amssymb}\r
   9 \usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx\r
  10 \usepackage[all]{xy}\r
  11 \usepackage{varwidth}\r
  12 \r
  13 \newtheorem{theorem}{Theorem}\r
  14 \newtheorem{prop}{Proposition}\r
  15 \newtheorem{lem}{Lemma}\r
  16 \newtheorem{defn}{Definition}\r
  17 \newcommand{\note}[1]{{\color{red} \bf [[#1]]}}\r
  18 \newcommand{\push}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax}\r
  19 \newcommand*\xor{\mathbin{\oplus}}\r
  20 \begin{document}\r
  21 \r
  22 \r
  23 \setlength\parindent{0pt} % Removes all indentation from paragraphs - comment this line for an assignment with lots of text\r
  24 \r
  25 \r
  26 \section{\textbf{Introduction}}\r
  27 \r
  28 \r
  29 \r
  30 \r
  31 \r
  32 \r
  33 \r
  34 \section{\textbf{Server}}\r
  35 The server maintains a collection of slots such that each slot contains some data.\r
  36 The operations on the slot are as follows:\r
  37 \begin{itemize}\r
  38     \item Put slot\r
  39     \item Get slot\r
  40     \item Delete Slot\r
  41 \end{itemize}\r
  42 \r
  43 \subsection{\textbf{Server Notation Conventions}}\r
  44 $s \in SN$ is a server sequence number\\\r
  45 $sv \in SV$ is a slot's value\\\r
  46 $slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$\r
  47 \r
  48 \subsection{\textbf{Server State}}\r
  49 \textit{n = current server sequence number}\\\r
  50 \textit{SL = set of live slots on the server}\\\r
  51 \r
  52 \textbf{Initial Server State}\\\r
  53 $SL = \emptyset$\\\r
  54 $n = 0$\r
  55 \r
  56 \subsection{\textbf{Put Slot}}\r
  57 Put slot is an operation that inserts data into a new slot at the server.\\\r
  58 \r
  59 %Put Function\r
  60 \noindent\fbox{%\r
  61 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
  62 \textbf{Put Function:}\r
  63 \begin{algorithmic}[1]\r
  64 \Function{PutSlotServer}{$sv_p$}\r
  65     \State $s_p \gets n$\r
  66     \State $n \gets n + 1$\r
  67     \State $SL \gets SL \cup \{\tuple{s_p,sv_p}\}$\r
  68 \EndFunction\r
  69 \end{algorithmic}\r
  70 \end{varwidth}% \r
  71 }\r
  72 \r
  73 \subsection{\textbf{Get Slot}}\r
  74 Get slot is an operation that returns all server slots that are greater than some server sequence number.\\\r
  75 \r
  76 % Get Function\r
  77 \noindent\fbox{%\r
  78 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
  79 \textbf{Get Function:}\r
  80 \begin{algorithmic}[1]\r
  81 \Function{GetSlotServer}{$s_g$}\r
  82     \State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$}\r
  83 \EndFunction\r
  84 \end{algorithmic}\r
  85 \end{varwidth}% \r
  86 }\r
  87 \r
  88 \subsection{\textbf{Delete Slot}}\r
  89 Delete slot is an operation that deletes all live slots that have server sequence numbers that are equal to or less than some server sequence number.\\\r
  90 \r
  91 %Delete Function\r
  92 \noindent\fbox{%\r
  93 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
  94 \textbf{Delete Function:}\r
  95 \begin{algorithmic}[1]\r
  96 \Function{DeleteSlotServer}{$s_d$}\r
  97     \State $SD \gets \{\tuple{s, sv} \in SL \mid s \leq s_g\}$\r
  98     \State $SL \gets SL - SD$\r
  99 \EndFunction\r
 100 \end{algorithmic}\r
 101 \end{varwidth}% \r
 102 }\r
 103 \r
 104 \r
 105 \r
 106 \r
 107 \r
 108 \r
 109 \r
 110 \r
 111 \section{\textbf{Client}}\r
 112 The data structure acts as a key store where key-value pairs can be read and set.\r
 113 The data structure exposes the following functions:\r
 114 \begin{itemize}\r
 115     \item Put Transaction\r
 116     \item Get key-value pair\r
 117     \item Create new key\r
 118 \end{itemize}\r
 119 \r
 120 \subsection{\textbf{Client Notation Conventions}}\r
 121 \r
 122 $K$ is the set of all keys.\\\r
 123 $MID$ is the set of the machine IDs of the devices that are in the system.\r
 124 $K_{mid}$ is a set of all keys that have device mid as the arbitrator\\\r
 125 $ssn_s$ is the server sequence number of a record $s$\\\r
 126 $mid_s \in MID$ is the machine ID for the device that created $record_s$.\\\r
 127 $hmac_s$ is the HMAC of $record_s$\\\r
 128 $c_{mid}$ is the latest read clock for a device with machine ID $mid$\\\r
 129 $vc_s = \{c_{mid} | mid \in MID\}$\\\r
 130 $rid_s = \tuple{mid_s, c_{mid_s}}$\r
 131 $k$ is a key entry\\\r
 132 $v$ is a value entry\\\r
 133 $kv_n$ is a key-value entry $\tuple{k_n,v_n} , k \in K$\\\r
 134 \r
 135 $tid_s = \tuple{mid_s,c_{mid_s}}$\\\r
 136 $guard_s = \tuple{\{kv_1, kv_2, ... ,kv_n | \exists mid \in MID, \forall n, kv_n[k] \in K_{mid}\},$ boolean condition using $ \{kv_1, kv_2, ... ,kv_n\}} $\\\r
 137 $transaction_s = \{mid_s,vc_{s_t} ,\{kv_1, kv_2,...kv_n | \exists mid \in MID, mid = guard_s[mid], \forall n, kv_n[k] \in K_{mid}\},guard_s\}$\\\r
 138 $commit_s = \tuple{tid_s,vc_s}$\\\r
 139 $abort_s = \tuple{tid_s,mid_s,vc_s}$\\\r
 140 $sequence_s = \tuple{rid_s, ssn_s}$\\\r
 141 $delete_s = \tuple{ssn_d}$\\\r
 142 $resize_s = \tuple{x | x \in \mathbb{N}}$\\\r
 143 $newkey_s = \tuple{k_s, vc_s, ssn_s$ or $-1, mid_s}$\\\r
 144 \r
 145 $payload_s = \{x_1, x_2,..., x_k | \forall k, x_k \in \{$transaction, commit, abort, resize, newkey, sequence, delete$\}\}$\\\r
 146 $rd_s = \tuple{mid_s, vc_s, hmac_s, payload_s}$ \\\r
 147 $record_s = \tuple{ssn_s,rd_s}$\\\r
 148 \r
 149 \subsection{\textbf{Client State}}\r
 150 \textit{s = largest server sequence number pulled from the server by a device} \\\r
 151 \textit{R = set of records pulled from the server so far with their server sequence numbers} \\\r
 152 \textit{RL = set of records that contain live data} \\\r
 153 \r
 154 \subsection{Helper Functions}\r
 155 The following helper functions are needed:\\\r
 156 \r
 157 %Get Payload Items from Record with SSN\r
 158 \noindent\fbox{%\r
 159 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 160 \textbf{Get Payload Items from Record with SSN}:\r
 161 \begin{algorithmic}[1]\r
 162 \Function{GetPayloadItemsWithSSN}{$record_s$}\r
 163     \State $PISSN \gets \emptyset$ \Comment{Set of Payload Items with ssn}\r
 164     \State $\tuple{ssn_s, rd_s} \gets record_s$\r
 165     \State $\tuple{mid_s, vc_s, hmac_s, payload_s} \gets rd_s$\\\r
 166     \r
 167     \ForAll{$payloadItems$ in $payload_s$}\r
 168         \State $PISSN \gets PISSN \cup \tuple{payloadItem, ssn_s}$\r
 169     \EndFor\\\r
 170     \r
 171     \State \Return {$PISSN$}\r
 172 \EndFunction\r
 173 \end{algorithmic}\r
 174 \end{varwidth}% \r
 175 }\r
 176 \r
 177 %Get rid For Record\r
 178 \noindent\fbox{%\r
 179 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 180 \textbf{Get rid For Record}:\r
 181 \begin{algorithmic}[1]\r
 182 \Function{GetRid}{$record_s$}\r
 183     \State $\tuple{ssn_s, \tuple{mid_s, \{c_{mid_1}, c_{mid_2}, ... , c_{mid_k}\}, hmac_s, payload_s}} \gets record_s$\r
 184     \State \Return {$\tuple{mid_s, c_{mid_s}}$}\r
 185 \EndFunction\r
 186 \end{algorithmic}\r
 187 \end{varwidth}% \r
 188 }\r
 189 \r
 190 \r
 191 \textbf{Get Transaction Arbitrator}:\\\r
 192 \textbf{Transaction Live}:\\\r
 193 \textbf{Commit Live}:\\\r
 194 \r
 195 %Sequence Live\r
 196 \noindent\fbox{%\r
 197 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 198 \textbf{Sequence Live}:\r
 199 \begin{algorithmic}[1]\r
 200 \Function{SequenceLive}{$sequence_s, ssn_{s1}$}\r
 201     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 202     \State $AS \gets \emptyset$    \Comment{Set of all Payload Items that are sequences}\r
 203     \State $StillHasRecord \gets False$\r
 204     \State $\tuple{rid_s, ssn_{s2}} \gets sequence_s$\\\r
 205     \r
 206     \ForAll{$record$ in $R$}\r
 207         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 208         \If{$rid_s = $\Call{GetRid}{$record$}}\r
 209             \State $StillHasRecord \gets True$\r
 210         \EndIf\r
 211     \EndFor\\\r
 212     \r
 213     \If{$\lnot StillHasRecord$}  \Comment{The Record does not exists anymore}\r
 214         \State \Return{False}\r
 215     \EndIf\\\r
 216     \r
 217     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
 218         \If{$payload$ is a $sequence$}\r
 219             \State $AS \gets AS \cup \{\tuple{ssn, payload}\}$   \Comment{Extract all sequence payloads}\r
 220         \EndIf\r
 221     \EndFor\\\r
 222     \r
 223     \ForAll{$\tuple{ssn_1', \tuple{rid', ssn_2'}}$ in $AS$}\r
 224         \If{$(rid'=rid_s) \land (ssn_1' > ssn_{s_1})$}\r
 225             \State \Return{False}\r
 226         \EndIf\r
 227     \EndFor \\\r
 228     \State \Return{True}\r
 229 \EndFunction\r
 230 \end{algorithmic}\r
 231 \end{varwidth}% \r
 232 }\r
 233 \r
 234 % Delete Live\r
 235 \noindent\fbox{%\r
 236 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 237 \textbf{Delete Live}:\r
 238 \begin{algorithmic}[1]\r
 239 \Function{DeleteLive}{$delete_s, ssn_s$}\r
 240     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 241     \State $AD \gets \emptyset$    \Comment{Set of all Payload Items that are deletes}\r
 242     \State $\tuple{ssn_d} \gets delete_s$\\\r
 243     \r
 244     \ForAll{record in R}\r
 245         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 246     \EndFor\\\r
 247     \r
 248     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
 249         \If{$payload$ is a $delete$}\r
 250             \State $AD \gets AD \cup \{\tuple{ssn, payload}\}$   \Comment{Extract all delete payloads}\r
 251         \EndIf\r
 252     \EndFor\\\r
 253     \r
 254     \ForAll{delete in AD}\r
 255         \State $\tuple{{ssn_s}', \tuple{{ssn_d}'}} \gets delete$\r
 256         \If{${ssn_d}' > ssn_d$}    \Comment{More recently deleted record}\r
 257             \State \Return{False}\r
 258         \ElsIf{$({ssn_d}'= ssn_d) \land ({ssn_s}' > ssn_s)$} \Comment{More recent delete of same record}\r
 259             \State \Return{False}\r
 260         \EndIf\r
 261     \EndFor \\\r
 262     \State \Return{True}\r
 263 \EndFunction\r
 264 \end{algorithmic}\r
 265 \end{varwidth}% \r
 266 }\r
 267 \r
 268 %Abort Live\r
 269 \noindent\fbox{%\r
 270 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 271 \textbf{Abort Live}:\r
 272 \begin{algorithmic}[1]\r
 273 \Function{AbortLive}{$abort_s$}\r
 274     \State $\tuple{tid_s,mid_s,vc_s} \gets abort_s$\\\r
 275     \ForAll{record in R}\r
 276         \State $\tuple{ssn_s',\tuple{mid_s', vc_s', hmac_s', payload_s'}} \gets record$\r
 277         \If{$(mid_s'=mid_s) \land (vc_s' > vc_s)$}\r
 278             \State \Return{True}\r
 279         \EndIf\r
 280     \EndFor\\\r
 281     \State \Return{False}\r
 282 \EndFunction\r
 283 \end{algorithmic}\r
 284 \end{varwidth}% \r
 285 }\r
 286 \r
 287 %Resize Live\r
 288 \noindent\fbox{%\r
 289 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 290 \textbf{Resize Live}:\r
 291 \begin{algorithmic}[1]\r
 292 \Function{ResizeLive}{$resize_s, ssn_s$}\r
 293     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 294     \State $AR \gets \emptyset$    \Comment{Set of all Payload Items that are resize}\r
 295     \State $\tuple{size} \gets resize_s$\\\r
 296     \r
 297     \ForAll{record in R}\r
 298         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 299     \EndFor\\\r
 300     \r
 301     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
 302         \If{$payload$ is a $resize$}\r
 303             \State $AR \gets AR \cup \{\tuple{ssn, payload}\}$   \Comment{Extract all resize payloads}\r
 304         \EndIf\r
 305     \EndFor\\\r
 306     \r
 307     \ForAll{$\tuple{ssn', \tuple{size'}}$ in $AR$}\r
 308         \If{$size' > size$}\r
 309             \State \Return{False}\r
 310         \ElsIf{$(size'=size) \land (ssn' > ssn_s)$}\r
 311             \State \Return{False}\r
 312         \EndIf\r
 313     \EndFor \\\r
 314     \State \Return{True}\r
 315 \EndFunction\r
 316 \end{algorithmic}\r
 317 \end{varwidth}% \r
 318 }\r
 319 \r
 320 \r
 321 \r
 322 \textbf{Evaluate Guard Condition:}\\\r
 323 \r
 324 \r
 325 \textbf{Get Latest Data Structure From Server:}\\\r
 326 \textbf{Delete Records:}\\\r
 327 \textbf{Check Data Structure for Malicious Activity:}\r
 328 \r
 329 \r
 330 \subsection{\textbf{Put Transaction}}\r
 331 \r
 332 \r
 333 \r
 334 \subsection{\textbf{Get key-value pair}}\r
 335 \subsection{\textbf{Create new key}}\r
 336 \r
 337 \end{document}\r