doc/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{algpseudocode}% http://ctan.org/pkg/algorithmicx\r
   6 \newtheorem{theorem}{Theorem}\r
   7 \newtheorem{defn}{Definition}\r
   8 \newcommand{\note}[1]{{\color{red} \bf [[#1]]}}\r
   9 \newcommand{\push}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax}\r
  10 \begin{document}\r
  11 \section{Approach}\r
  12 \r
  13 \subsection{Keys}\r
  14 \r
  15 Each device has: user id + password\r
  16 \r
  17 Server login is:\r
  18 hash1(user id), hash1(password)\r
  19 \r
  20 Symmetric Crypto keys is:\r
  21 hash2(user id | password)\r
  22 \r
  23 Server has finite length queue of entries + max\_entry\_identifier +\r
  24 server login key\r
  25 \r
  26 \subsection{Entry layout}\r
  27 Each entry has:\r
  28 \begin{enumerate}\r
  29 \item Sequence identifier\r
  30 \item Random IV (if needed by crypto algorithm)\r
  31 \item Encrypted payload\r
  32 \end{enumerate}\r
  33 \r
  34 Payload has:\r
  35 \begin{enumerate}\r
  36 \item Sequence identifier\r
  37 \item Machine id (most probably something like a 64-bit random number \r
  38 that is self-generated by client)\r
  39 \item HMAC of previous slot\r
  40 \item Data entries\r
  41 \item HMAC of current slot\r
  42 \end{enumerate}\r
  43 \r
  44 A data entry can be one of these:\r
  45 \begin{enumerate}\r
  46 \item All or part of a Key-value entry\r
  47 \item Slot sequence entry: Machine id + last message identifier \r
  48 \newline {The purpose of this is to keep the record of the last slot \r
  49 from a certain client if a client's update has to expunge that other \r
  50 client's last entry from the queue. This is kept in the slot until \r
  51 the entry owner inserts a newer update into the queue.}\r
  52 \item Queue state entry: Includes queue size \newline {The purpose \r
  53 of this is for the client to tell if the server lies about the number \r
  54 of slots in the queue, e.g. if there are 2 queue state entry in the queue, \r
  55 e.g. 50 and 70, the client knows that when it sees 50, it should expect \r
  56 at most 50 slots in the queue and after it sees 70, it should expect \r
  57 50 slots before that queue state entry slot 50 and at most 70 slots. \r
  58 The queue state entry slot 70 is counted as slot number 51 in the queue.}\r
  59 \item Collision resolution entry: message identifier + machine id of a\r
  60 collision winner\r
  61 \newline {The purpose of this is to keep keep track of the winner of \r
  62 all the collisions until all clients have seen the particular entry.}\r
  63 \end{enumerate}\r
  64 \r
  65 \subsection{Live status}\r
  66 \r
  67 Live status of entries:\r
  68 \begin{enumerate}\r
  69 \item Key-Value Entry is dead if either (a) there is a newer key-value pair or (b) it is incomplete.\r
  70         \r
  71 \item Slot sequence number (of either a message version data\r
  72 or user-level data) is dead if there is a newer slot from the same machine.\r
  73 \r
  74 \item Queue state entry is dead if there is a newer queue state entry.\r
  75 {In the case of queue state entries 50 and 70, this means that queue state \r
  76 entry 50 is dead and 70 is live. However, not until the number of slots reaches \r
  77 70 that queue state entry 50 will be expunged from the queue.}\r
  78 \r
  79 \item Collision resolution entry is dead if this entry has been seen\r
  80 by all clients after a collision happens.\r
  81 \end{enumerate}\r
  82 \r
  83 When data is at the end of the queue ready to expunge, if:\r
  84 \begin{enumerate}\r
  85 \item The key-value entry is not dead, it must be reinserted at the\r
  86 beginning of the queue.\r
  87 \r
  88 \item If the slot sequence number is not dead, then a message sequence\r
  89 entry must be inserted.\r
  90 \r
  91 \item If the queue state entry is not dead, it must be reinserted at the\r
  92 beginning of the queue.\r
  93 \end{enumerate}\r
  94 \r
  95 \r
  96 \paragraph{Reads:}\r
  97 Client sends a sequence number.  Server replies with either: all data\r
  98 entries or all newer data entries.\r
  99 \r
 100 \paragraph{Writes:}\r
 101 Client sends slot, server verifies that sequence number is valid,\r
 102 checks entry hash, and replies with an accept message if all checks\r
 103 pass.  On success, client updates its sequence number.  On failure,\r
 104 server sends updates slots to client and client validates those slots.\r
 105 \r
 106 \paragraph{Local state on each client:}\r
 107 A list of machines and the corresponding latest sequence numbers.\r
 108 \r
 109 \paragraph{Validation procedure on client:}\r
 110 \begin{enumerate}\r
 111 \item Decrypt each new slot in order.\r
 112 \item For each slot:\r
 113     (a) check its HMAC, and\r
 114     (b) check that the previous entry HMAC field matches the previous\r
 115     entry.\r
 116 \item Check that the last message version for our machine matches our\r
 117 last message sent.\r
 118 \item For all other machines, check that the latest sequence number is\r
 119 at least as large (never goes backwards).\r
 120 \item That the queue has a current queue state entry.\r
 121 \item That the number of entries received is consistent with the size\r
 122 specified in the queue state entry.\r
 123 \end{enumerate}\r
 124 \r
 125 Key-value entries can span multiple slots.  They aren't valid until\r
 126 they are complete.\r
 127 \r
 128 \subsection{Resizing Queue}\r
 129 Client can make a request to resize the queue. This is done as a write that combines:\r
 130   (a) a slot with the message, and\r
 131         (b) a request to the server\r
 132 \r
 133 \subsection{Server Algorithm}\r
 134 $s \in SN$ is a sequence number set\\\r
 135 $sv \in SV$ is a slot's value\\\r
 136 $slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\\r
 137 \r
 138 \textbf{State} \\\r
 139 \textit{SL = set of live slots on server} \\\r
 140 \textit{max = maximum number of slots (input only for resize message)} \\\r
 141 \textit{n = number of slots} \\ \\\r
 142 \textbf{Helper Function} \\\r
 143 $MaxSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv}\r
 144 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \geq s_s$ \\\r
 145 $MinSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv} \r
 146 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \leq s_s$ \\\r
 147 $SeqN(\tuple{s, sv})=s$ \\\r
 148 $SlotVal(\tuple{s, sv})=sv$ \\\r
 149 \r
 150 \begin{algorithmic}[1]\r
 151 \Function{GetSlot}{$s_g$}\r
 152 \State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$}\r
 153 \EndFunction\r
 154 \end{algorithmic}\r
 155 \r
 156 \begin{algorithmic}[1]\r
 157 \Function{PutSlot}{$s_p,sv_p,max'$}\r
 158 \If{$(max' \neq \emptyset)$}\Comment{Resize}\r
 159 \State $max \gets max'$\r
 160 \EndIf\r
 161 \State $\tuple{s_n,sv_n} \gets MaxSlot(SL)$\Comment{Last sv}\r
 162 \State $s_n \gets SeqN(\tuple{s_n,sv_n})$\r
 163 \If{$(s_p = s_n + 1)$}\r
 164         \If{$n = max$}\r
 165         \State $\tuple{s_m,sv_m} \gets MinSlot(SL)$\Comment{First sv}\r
 166                 \State $SL \gets SL - \{\tuple{s_m,sv_m}\}$\r
 167         \Else \Comment{$n < max$}\r
 168                 \State $n \gets n + 1$\r
 169         \EndIf\r
 170     \State $SL \gets SL \cup \{\tuple{s_p,sv_p}\}$\r
 171         \State \Return{$(true,\emptyset)$}\r
 172 \Else\r
 173         \State \Return{$(false,\{\tuple{s,sv}\in SL \mid \r
 174     s \geq s_p\})$}\r
 175 \EndIf\r
 176 \EndFunction\r
 177 \end{algorithmic}\r
 178 \r
 179 \subsection{Client Algorithm}\r
 180 \subsubsection{Reading Slots}\r
 181 \textbf{Data Entry} \\\r
 182 $de$ is a data entry \\\r
 183 $k$ is key of entry \\\r
 184 $v$ is value of entry \\\r
 185 $kv$ is a key-value entry $\tuple{k,v}$, $kv \in D$ \\\r
 186 $ss$ is a slot sequence entry $\tuple{id,s_{last}}$, \r
 187 id + last s of a machine, $ss \in D$ \\\r
 188 $qs$ is a queue state entry, $qs \in D$ \\\r
 189 $cr$ is a collision resolution entry $\tuple{s_{col},id_{col}}$, \r
 190 s + id of a machine that wins a collision, $cr \in D$ \\\r
 191 $D = \{kv,ss,qs,cr\}$ \\\r
 192 $DE = \{de \mid de \in D\}$ \\ \\\r
 193 $s \in SN$ is a sequence number set\\\r
 194 $id$ is a machine ID\\\r
 195 $hmac_p$ is the HMAC value of the previous slot \\\r
 196 $hmac_c$ is the HMAC value of the current slot \\\r
 197 $Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
 198 $sv_s = \tuple{s, E(Dat_s)} = \r
 199 \tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\\r
 200 \r
 201 \textbf{States} \\\r
 202 \textit{DT = set of $\tuple{k,v}$ on client} \\\r
 203 \textit{MS = set of $\tuple{id, s_{last}}$ of all clients on client \r
 204 (initially empty)} \\\r
 205 \textit{$MS_g$ = set MS to save all $\tuple{id, s_{last}}$ pairs while\r
 206 traversing DT after a request to server (initially empty)} \\\r
 207 \textit{$SM$ = set of $\tuple{s, id}$ of all slots in a previous read\r
 208 (initially empty)} \\\r
 209 \textit{$max_g$ = maximum number of slots (initially $max_c > 0$)} \\\r
 210 \textit{m = number of slots on client (initially $m = 0 and m \leq n$)} \\\r
 211 \textit{$hmac_{p_g}$ = the HMAC value of the previous slot \r
 212 ($hmac_{p_g} = \emptyset$ for the first slot)} \\\r
 213 \textit{$id_{self}$ = machine Id of this client} \\\r
 214 \textit{SK = Secret Key} \\ \\\r
 215 \textbf{Helper Functions} \\\r
 216 $MaxSlot(SL_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}\r
 217 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \geq s_s$ \\\r
 218 $MinSlot(SL_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv} \r
 219 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \leq s_s$ \\\r
 220 $Slot(SL_s,s_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv} \r
 221 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s = s_s$ \\\r
 222 $SeqN(\tuple{s, sv})=s$ \\\r
 223 $SlotVal(\tuple{s, sv})=sv$ \\\r
 224 $Decrypt(SK_s,sv_s)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
 225 $GetSeqN(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=s$ \\\r
 226 $GetMacId(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=id$ \\\r
 227 $GetPrevHmac(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=hmac_p$ \\\r
 228 $GetCurrHmac(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=hmac_c$ \\\r
 229 $GetDatEnt(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=DE$ \\\r
 230 $GetKV(de_s$ \textit{such that} $de_s \in D \land de_s = kv)=\tuple{k_s,v_s}$ \\\r
 231 $GetSS(de_s$ \textit{such that} $de_s \in D \land de_s = ss)=\tuple{id,s_{last}}$ \\\r
 232 $GetQS(de_s$ \textit{such that} $de_s \in D \land de_s = qs)=qs_s$ \\\r
 233 $GetCR(de_s$ \textit{such that} $de_s \in D \land de_s = cr)=\tuple{s_s,id_s}$ \\\r
 234 $GetLastSeqN(MS_s,id_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}}\r
 235 \in MS_s \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, id = id_s$ \\\r
 236 $GetMachineId(SM_s,s_s)= id$ \textit{such that} $\tuple{s, id}\r
 237 \in SM_s \wedge \forall \tuple{s_s, id_s} \in SM_s, s = s_s$ \\\r
 238 $GetS(\tuple{s, id})=s$ \\\r
 239 $GetId(\tuple{s, id})=id$ \\\r
 240 $GetKey(\tuple{k, v})=k$ \\\r
 241 $GetVal(\tuple{k, v})=v$ \\\r
 242 $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v} \r
 243 \in DT_s \wedge \forall \tuple{k_s, v_s} \in DT_s, k = k_s$ \\\r
 244 \r
 245 \begin{algorithmic}[1]\r
 246 \Procedure{ReportError}{$msg$}\r
 247 \State $Print(msg)$\r
 248 \State $Halt()$\r
 249 \EndProcedure\r
 250 \end{algorithmic}\r
 251 \r
 252 \begin{algorithmic}[1]\r
 253 \Function{ValidHmac}{$DE_s,SK_s,hmac_{stored}$}\r
 254 \State $hmac_{computed} \gets Hmac(DE_s,SK_s)$\r
 255 \If{$hmac_{stored} = hmac_{computed}$}\r
 256         \State $valid \gets true$\r
 257 \Else\r
 258         \State $valid \gets false$\r
 259 \EndIf\r
 260 \State \Return{$valid$}\r
 261 \EndFunction\r
 262 \end{algorithmic}\r
 263 \r
 264 \begin{algorithmic}[1]\r
 265 \Function{ValidPrevHmac}{$DE_s,hmac_{p_s},hmac_{p_{sto}}$}\r
 266 \If{$hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC}\r
 267         \State $valid \gets true$\r
 268 \Else\r
 269         \If{$hmac_{p_{sto}} = hmac_{p_s}$}\r
 270                 \State $valid \gets true$\r
 271         \Else\r
 272                 \State $valid \gets false$\r
 273         \EndIf\r
 274 \EndIf\r
 275 \State \Return{$valid$}\r
 276 \EndFunction\r
 277 \end{algorithmic}\r
 278 \r
 279 \begin{algorithmic}[1]\r
 280 \Function{GetQueSta}{$Dat_s$}\r
 281 \State $DE_s \gets GetDatEnt(DE_s)$\r
 282 \State $de_{qs} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
 283         de_s \in D \land de_s = qs$\r
 284 \If{$de_{qs} \neq \emptyset$}\r
 285         \State $qs_{ret} \gets GetQS(de_{qs})$\r
 286 \Else\r
 287         \State $qs_{ret} \gets \emptyset$\r
 288 \EndIf\r
 289 \State \Return{$qs_{ret}$}\r
 290 \EndFunction\r
 291 \end{algorithmic}\r
 292 \r
 293 \begin{algorithmic}[1]\r
 294 \Function{GetSlotSeq}{$Dat_s$}\r
 295 \State $DE_s \gets GetDatEnt(Dat_s)$\r
 296 \State $de_{ss} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
 297         de_s \in D \land de_s = ss$\r
 298 \If{$de_{ss} \neq \emptyset$}\r
 299         \State $\tuple{id_{ret},s_{last_{ret}}} \gets GetSS(de_{ss})$\r
 300 \Else\r
 301         \State $\tuple{id_{ret},s_{last_{ret}}} \gets \emptyset$\r
 302 \EndIf\r
 303 \State \Return{$\tuple{id_{ret},s_{last_{ret}}}$}\r
 304 \EndFunction\r
 305 \end{algorithmic}\r
 306 \r
 307 \begin{algorithmic}[1]\r
 308 \Function{GetColRes}{$Dat_s$}\r
 309 \State $DE_s \gets GetDatEnt(Dat_s)$\r
 310 \State $de_{cr} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
 311         de_s \in D \land de_s = cr$\r
 312 \If{$de_{cr} \neq \emptyset$}\r
 313         \State $\tuple{s_{ret},id_{ret}} \gets GetCR(de_{cr})$\r
 314 \Else\r
 315         \State $\tuple{s_{ret},id_{ret}} \r
 316         \gets \emptyset$\r
 317 \EndIf\r
 318 \State \Return{$\tuple{s_{ret},id_{ret}}$}\r
 319 \EndFunction\r
 320 \end{algorithmic}\r
 321 \r
 322 \begin{algorithmic}[1]\r
 323 \Function{UpdateLastSeqN}{$id_s,s_s,MS_s$}\r
 324 \State $s_t \gets GetLastSeqN(MS_s,id_s)$\r
 325 \If{$s_t = \emptyset$}\r
 326         \State $MS_s \gets MS_s \cup \{\tuple{id_s,s_s}\}$\Comment{First occurrence}\r
 327 \Else\r
 328         \If{$s_s > s_t$}\Comment{Update entry with a later s}\r
 329         \State $MS_s \gets (MS_s - \{\tuple{id_s,s_t}\}) \cup \r
 330                 \{\tuple{id_s,s_s}\}$\r
 331     \EndIf\r
 332 \EndIf\r
 333 \State \Return{$MS_s$}\r
 334 \EndFunction\r
 335 \end{algorithmic}\r
 336 \r
 337 \begin{algorithmic}[1]\r
 338 \Procedure{CheckLastSeqN}{$MS_s,MS_t$}\Comment{Check $MS_t$ based on $MS_s$}\r
 339 \ForAll{$\tuple{id_t,s_{t_{last}}} \in MS_t$}\r
 340         \State $s_{s_{last}} \gets GetLastSeqN(MS_s,id_t)$\r
 341         \If{$s_{s_{last}} \neq \emptyset$}\r
 342                 \If{$id_t = id_{self}$}\r
 343                 \If{$s_{s_{last}} \neq s_{t_{last}}$}\r
 344                                 \State \Call{ReportError}{'Invalid last $s$ for this machine'}\r
 345                         \EndIf\r
 346                 \Else\r
 347                         \If{$s_{s_{last}} \geq s_{t_{last}}$}\r
 348                                 \State $MS_s \gets (MS_s - \{\tuple{id_t,s_{t_{last}}}\}) \cup \r
 349                                 \{\tuple{id_t,s_{s_{last}}}\}$\r
 350                         \Else\r
 351                                 \State \Call{ReportError}{'Invalid last $s$ for machine $id_t$'}\r
 352                         \EndIf\r
 353                 \EndIf\r
 354         \EndIf\r
 355 \EndFor\r
 356 \EndProcedure\r
 357 \end{algorithmic}\r
 358 \r
 359 \begin{algorithmic}[1]\r
 360 \Procedure{CheckColRes}{$SM_s,\tuple{s_t,id_t}$}\Comment{Check $id_s$ in $SM_s$}\r
 361 \State $s_t \gets GetS(\tuple{s_t,id_t})$\r
 362 \State $id_t \gets GetId(\tuple{s_t,id_t})$\r
 363 \State $id_s \gets GetMachineId(SM_s,s_t)$\r
 364 \If{$id_s \neq id_t$}\r
 365         \State \Call{ReportError}{'Invalid $id_s$ for this slot update'}\r
 366 \EndIf\r
 367 \EndProcedure\r
 368 \end{algorithmic}\r
 369 \r
 370 \begin{algorithmic}[1]\r
 371 \Function{UpdateDT}{$DT_s,Dat_s$}\r
 372 \State $DE_s \gets GetDatEnt(Dat_s)$\r
 373 \ForAll{$de_s \in DE_s$}\r
 374         \If{$de_s$ \textit{such that} $de_s \in D \land de_s = kv$}\r
 375                 \State $\tuple{k_s,v_s} \gets GetKV(de_s)$\r
 376                 \State $k_s \gets GetKey(\tuple{k_s,v_s})$\r
 377                 \State $\tuple{k_s,v_t} \gets GetKeyVal(DT_s,k_s)$\r
 378                 \If{$\tuple{k_s,v_t} = \emptyset$}\r
 379                         \State $DT_s \gets DT_s \cup \{\tuple{k_s,v_s}\}$\r
 380                 \Else\r
 381                 \State $DT_s \gets (DT_s - \{\tuple{k_s,v_t}\}) \cup \r
 382                         \{\tuple{k_s,v_s}\}$\r
 383                 \EndIf\r
 384     \EndIf\r
 385 \EndFor\r
 386 \State \Return{$DT_s$}\r
 387 \EndFunction\r
 388 \end{algorithmic}\r
 389 \r
 390 \begin{algorithmic}[1]\r
 391 \Procedure{ProcessSL}{$SL_g$}\r
 392 \State $MS_g \gets \emptyset$\r
 393 \State $SM_{curr} \gets \emptyset$\r
 394 \State $\tuple{s_{g_{max}},sv_{g_{max}}} \gets MaxSlot(SL_g)$\r
 395 \State $s_{g_{max}} \gets SeqN(\tuple{s_{g_{max}},sv_{g_{max}}})$\r
 396 \State $\tuple{s_{g_{min}},sv_{g_{min}}} \gets MinSlot(SL_g)$\r
 397 \State $s_{g_{min}} \gets SeqN(\tuple{s_{g_{min}},sv_{g_{min}}})$\r
 398 \For{$s_g \gets s_{g_{min}}$ \textbf{to} $s_{g_{max}}$}\Comment{Process slots \r
 399         in $SL_g$ in order}\r
 400         \State $\tuple{s_g,sv_g} \gets Slot(SL_g,s_g)$\r
 401         \State $SM_{curr} \gets SM_{curr} \cup \{\tuple{s_g,sv_g}\}$\r
 402     \State $s_g \gets SeqN(\tuple{s_g,sv_g})$\r
 403         \State $sv_g \gets SlotVal(\tuple{s_g,sv_g})$\r
 404         \State $Dat_g \gets Decrypt(SK,sv_g)$\r
 405         \State $s_{g_{in}} \gets GetSeqN(Dat_g)$\r
 406     \If{$s_g \neq s_{g_{in}}$}\r
 407                 \State \Call{ReportError}{'Invalid sequence number'}\r
 408         \EndIf\r
 409         \State $DE_g \gets GetDatEnt(Dat_g)$\r
 410         \State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_g)$\r
 411         \If{$\neg \Call{ValidPrevHmac}{DE_g,hmac_{p_g},hmac_{p_{stored}}}$}\r
 412                 \State \Call{ReportError}{'Invalid previous HMAC value'}\r
 413         \EndIf\r
 414         \State $hmac_{c_g} \gets GetCurrHmac(Dat_g)$\r
 415         \If{$\neg \Call{ValidHmac}{DE_g,SK,hmac_{c_g}}$}\r
 416                 \State \Call{ReportError}{'Invalid current HMAC value'}\r
 417         \EndIf\r
 418         \State $hmac_{p_g} \gets Hmac(Dat_g,SK)$\Comment{Update $hmac_{p_g}$ for next check}\r
 419         \State $qs_g \gets \Call{GetQueSta}{Dat_g}$\Comment{Handle qs}\r
 420         \If{$qs_g \neq \emptyset \land qs_g > max_g$}\r
 421                 \State $max_g \gets qs_g$\r
 422         \EndIf\r
 423     %Check for last s in Dat\r
 424         \State $id_g \gets GetMacId(Dat_g)$\Comment{Handle last s}\r
 425         \State $MS_g \gets \Call{UpdateLastSeqN}{id_g,s_g,MS_g}$\r
 426     %Check for last s in DE in Dat\r
 427     \State $\tuple{id_d,s_{d_{last}}} \gets \Call{GetSlotSeq}{Dat_g}$\Comment{Handle ss}\r
 428         \If{$\tuple{id_d,s_{d_{last}}} \neq \emptyset$}\r
 429         \State $MS_g \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_g}$\r
 430         \EndIf\r
 431         \State $\tuple{s_e,id_e} \gets \r
 432         \Call{GetColRes}{Dat_g}$\Comment{Handle cr}\r
 433         \If{$\tuple{s_e,id_e} \neq \emptyset$}\r
 434                 \State $s_e \gets GetS(\tuple{s_e,id_e})$\r
 435                 \State $id_e \gets GetId(\tuple{s_e,id_e})$\r
 436                 \State $s_{c_{last}} \gets GetLastSeqN(MS,id_e)$\r
 437                 \If{$s_{c_{last}} < s_e$}\r
 438                         \State $\Call{CheckColRes}{SM,\tuple{s_e,id_e}}$\r
 439                 \EndIf\r
 440     \EndIf\r
 441         \State $DT \gets \Call{UpdateDT}{DT,Dat_g}$\r
 442 \EndFor\r
 443 \State $SM \gets SM_{curr}$\r
 444 \If{$m + |SL_g| \leq max_g$}\Comment{Check actual size against $max_g$}\r
 445         \State $m \gets m + |SL_g|$\r
 446 \Else\r
 447         \State \Call{ReportError}{'Actual queue size exceeds $max_g$'}\r
 448 \EndIf\r
 449 \State $\Call{CheckLastSeqN}{MS_g,MS}$\r
 450 \EndProcedure\r
 451 \end{algorithmic}\r
 452 \r
 453 \begin{algorithmic}[1]\r
 454 \Procedure{GetKVPairs}{}\r
 455 \State $s_g \gets GetLastSeqN(MS,id_{self}) + 1$\r
 456 \State $SL_c \gets \Call{GetSlot}{s_g}$\r
 457 \State $\Call{ProcessSL}{SL_c}$\Comment{Process slots and update DT}\r
 458 \EndProcedure\r
 459 \end{algorithmic}\r
 460 \r
 461 \begin{algorithmic}[1]\r
 462 \Function{GetValFromKey}{$k_g$}\r
 463 \State $\tuple{k_s,v_s} \gets \tuple{k,v}$ \textit{such that} $\tuple{k,v} \r
 464         \in DT \land k = k_g$\r
 465 \State $v_s \gets GetVal(\tuple{k_s,v_s})$\r
 466 \State \Return{$v_s$}\r
 467 \EndFunction\r
 468 \end{algorithmic}\r
 469 \r
 470 \subsubsection{Writing Slots}\r
 471 \textbf{Data Entry} \\\r
 472 $k$ is key of entry \\\r
 473 $v$ is value of entry \\\r
 474 $kv$ is a key-value entry $\tuple{k,v}$\\\r
 475 $D = \{kv,ss,qs,cr\}$ \\\r
 476 $DE = \{de \mid de \in D\}$ \\\r
 477 $Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
 478 $sv_s = \tuple{s, E(Dat_s)} = \r
 479 \tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\\r
 480 \r
 481 \textbf{States} \\\r
 482 \textit{$cp$ = data entry $DE$ maximum size/capacity} \\\r
 483 \textit{$cr_p$ = saved cr entry $\tuple{s,id}$ on client if there is a collision\r
 484 (sent in the following slot)} \\\r
 485 \textit{$ck_p$ = counter of $kv \in KV$ for putting pairs (initially 0)} \\\r
 486 \textit{$ck_g$ = counter of $kv \in KV$ for getting pairs (initially 0)} \\\r
 487 \textit{$id_{self}$ = machine Id of this client} \\\r
 488 \textit{$hmac_{c_p}$ = the HMAC value of the current slot} \\\r
 489 \textit{$hmac_{p_p}$ = the HMAC value of the previous slot \r
 490 ($hmac_{p_p} = \emptyset$ for the first slot)} \\\r
 491 \textit{$KV$ = set of $\tuple{ck, \tuple{k,v}}$ of kv entries on client} \\\r
 492 \textit{$ST$ = set of $DE$ objects on client} \\\r
 493 \textit{$SL_p$ = set of returned slots on client} \\\r
 494 \textit{SK = Secret Key} \\\r
 495 \r
 496 \textbf{Helper Functions} \\\r
 497 $CreateDat(s,id,hmac_p,DE,hmac_c)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
 498 $Encrypt(Dat_s,SK_s)=sv_s$ \\\r
 499 $GetStatus(\tuple{status,SL})=status$ \\\r
 500 $GetSL(\tuple{status,SL})=SL$ \\\r
 501 $GetColSeqN(SL_s,s_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}\r
 502 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s = s_s$ \\\r
 503 $CreateCR(s,id)=\tuple{s,id}$ \\\r
 504 $GetKV(KV_s,k_s)= \tuple{ck,\tuple{k, v}}$ \textit{such that} \r
 505 $\tuple{ck,\tuple{k, v}} \in KV_s \wedge\r
 506 \forall \tuple{ck_s,\tuple{k_s, v_s}} \in KV_s, k = k_s$ \\\r
 507 $MaxLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \r
 508 \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \geq s_{s_{last}}$ \\\r
 509 \r
 510 \begin{algorithmic}[1]\r
 511 \Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$}\r
 512 \State $k_s \gets GetKey(\tuple{k_s,v_s})$\r
 513 \State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKV(KV_s,k_s)$\r
 514 \If{$\tuple{ck_s,\tuple{k_s,v_t}} = \emptyset$}\r
 515         \State $KV_s \gets KV_s \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
 516         \State $ck_p \gets ck_p + 1$\r
 517 \Else\r
 518         \State $KV_s \gets (KV_s - \{\tuple{ck_s, \tuple{k_s,v_t}}\}) \cup \r
 519         \{\tuple{ck_s, \tuple{k_s,v_s}}\}$\r
 520 \EndIf\r
 521 \State \Return{$KV_s$}\r
 522 \EndFunction\r
 523 \end{algorithmic}\r
 524 \r
 525 \begin{algorithmic}[1]\r
 526 \Function{GetDEPairs}{$KV_s$}\r
 527 \State $DE_{ret} \gets \emptyset$\r
 528 \State $cp_s \gets cp$\r
 529 \If{$cr_p \neq \emptyset$}\r
 530         \State $DE_{ret} \gets DE_{ret} \cup cr_p$\r
 531         \State $cp_s \gets cp_s - 1$\r
 532 \EndIf\r
 533 \If{$|KV_s| \leq cp$}\Comment{KV set can extend multiple slots based on $cp$}\r
 534         \State $DE_{ret} \gets DE_{ret} \cup\r
 535         \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s\}$\r
 536 \Else\r
 537         \State $DE_{ret} \gets DE_{ret} \cup\r
 538         \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s,\r
 539                 ck_g \leq ck_s < ck_g + cp_s\}$\r
 540         \If{$|DE_{ret}| = cp$}\r
 541                 \State $ck_g \gets ck_g + cp_s$\Comment{Middle of KV set}\r
 542         \Else\r
 543                 \State $ck_g \gets 0$\Comment{End of KV set}\r
 544         \EndIf\r
 545 \EndIf\r
 546 \State \Return{$DE_{ret}$}\r
 547 \EndFunction\r
 548 \end{algorithmic}\r
 549 \r
 550 \begin{algorithmic}[1]\r
 551 \Function{PutDataEntries}{$max'_p$}\r
 552 \State $s_p \gets MaxLastSeqN(MS)$\r
 553 \State $DE_p \gets GetDEPairs(KV)$\r
 554 \State $hmac_{c_p} \gets Hmac(DE_p,SK)$\r
 555 \State $Dat_p \gets CreateSlot(s_p,id_{self},hmac_{p_p},DE_p,hmac_{c_p})$\r
 556 \State $hmac_{p_p} \gets hmac_{c_p}$\r
 557 \State $sv_p \gets Encrypt(Dat_p,SK)$\r
 558 \State $\tuple{stat_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$\r
 559 \State $stat_p \gets GetStatus(\tuple{stat_p,SL_p})$\r
 560 \State $SL_p \gets GetSL(\tuple{stat_p,SL_p})$\r
 561 \If{$\neg stat_p$}\Comment{Handle collision}\r
 562         \State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_p,s_p)$\r
 563         \State $s_{col} \gets SeqN(\tuple{s_{col},sv_{col}})$\r
 564         \State $sv_{col} \gets SlotVal(\tuple{s_{col},sv_{col}})$\r
 565         \State $Dat_{col} \gets Decrypt(SK,sv_{col})$\r
 566         \State $id_{col} \gets GetMacId(Dat_{col})$\r
 567         \State $\tuple{s_{col},id_{col}} \gets CreateCR(s_{col},id_{col})$\r
 568         \State $cr_p \gets \tuple{s_{col},id_{col}}$\r
 569 \Else\r
 570         \State $cr_p \gets \emptyset$\r
 571 \EndIf\r
 572 \State $\Call{ProcessSL}{SL_p}$\r
 573 \State \Return{$ST$}\r
 574 \EndFunction\r
 575 \end{algorithmic}\r
 576 \r
 577 \subsection{Formal Guarantees}\r
 578 \r
 579 \textit{To be completed ...}\r
 580 \r
 581 \begin{defn}[System Execution]\r
 582 Let \\\r
 583 \begin{center}\r
 584 $Q = \{slot_{sn_1}, slot_{sn_2}, \dots, Slot_{sn_n}\}$, \\\r
 585 $SN = \{sn_1, sn_2, \dots, sn_n\}$ \\\r
 586 \end{center}\r
 587 denote a queue $Q$ of $n$ slots, with each slot entry being denoted by a\r
 588 valid sequence number $sn_i \in SN$. $Q$ represents a total order of all \r
 589 slot updates from all corresponding machines.\r
 590 %\textit{Formalize a system execution as a sequence of slot updates...\r
 591 %There is a total order of all slot updates.}\r
 592 \end{defn}\r
 593 \r
 594 \begin{defn}[Transitive Closure]\r
 595 A transitive closure $\tau : \tau = \epsilon_{update(slot_i)} R $\r
 596 $\epsilon_{receive(slot_i)}$ is a relation from slot update event\r
 597 $\epsilon$ to a slot receive event $\epsilon$ for $slot_i$.\r
 598 %Define transitive closure relation for slot updates...  There is an\r
 599 %edge from a slot update to a slot receive event if the receive event\r
 600 %reads from the update event.\r
 601 \end{defn}\r
 602 \r
 603 \begin{defn}[Suborder]\r
 604 Let \\\r
 605 \begin{center}\r
 606 $q = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\}, \r
 607 sn_1 \leq i \leq j \leq sn_n \Longrightarrow q \subseteq Q$\r
 608 \end{center}\r
 609 denote a suborder of the total order. Set q is a sequence of contiguous\r
 610 slot updates that is a subset of a total order of all slot updates in Q.\r
 611 %Define suborder of total order.  It is a sequence of contiguous slots\r
 612 %updates (as observed by a given device).\r
 613 \end{defn}\r
 614 \r
 615 \begin{defn}[Prefix of a suborder]\r
 616 Given a suborder \\ \r
 617 \begin{center}\r
 618 $q' = \{slot_{i}, slot_{i+1}, \dots, slot_{j}, \dots\}, \r
 619 sn_1 \leq i \leq j \leq sn_n \Longrightarrow \r
 620 q' \subseteq Q$\r
 621 \end{center}\r
 622 with $slot_{j}$ as a slot update in $q'$, the prefix of $q'$ is a sequence \r
 623 of all slot updates $\{slot_{i}, slot_{i+1}, \dots, slot_{j-1}\} \cup\r
 624 slot_{j}$.\r
 625 %Given a sub order $o=u_{i},u_{i+1},...,u_j, u_{j+i},..., u', ...$ and\r
 626 %a slot update $u'$ in $o$, the prefix of $o$ is a sequence of all\r
 627 %updates that occur before $u'$ and $u'$.\r
 628 \end{defn}\r
 629 \r
 630 \begin{defn}[Consistency between a suborder and a total order]\r
 631 A suborder $q'$ is consistent with a total order $T$ of $Q$, if all\r
 632 updates in $q'$ appear in $T$ and they appear in the same order, as \r
 633 the following:\r
 634 \begin{center}\r
 635 $q' = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\},$\r
 636 $T = \{slot_{sn_1}, \dots, slot_{i}, slot_{i+1}, \dots, slot_{j}, \dots,\r
 637 slot_{sn_n}\},$ \\ $sn_1 \leq i \leq j \leq sn_n \Longrightarrow\r
 638 q' \subseteq T$\r
 639 \end{center}\r
 640 %A suborder $o$ is consistent with a total order $t$, if all updates in $o$ %appear in $t$ and they appear in the same order.\r
 641 \end{defn}\r
 642 \r
 643 \begin{defn}[Consistency between suborders]\r
 644 Two suborders U and V are consistent if there exist a total order T \r
 645 such that both U and V are suborders of T.\r
 646 \begin{center}\r
 647 $U = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\},$ \\\r
 648 $V = \{slot_{k}, slot_{k+1}, \dots, slot_{l}\},$ \\\r
 649 $sn_1 \leq i \leq j \leq k \leq l \leq sn_n,$ \\\r
 650 $U \subset T \land V \subset T$ \\\r
 651 $T = \{slot_{sn_1}, \dots, slot_{i}, slot_{i+1}, \dots, slot_{j}, $\\\r
 652 $\dots, slot_{k}, slot_{k+1}, \dots, slot_{l}, \dots, slot_{sn_n}\}$\r
 653 \end{center}\r
 654 %Define notion of consistency between suborders...  Two suborders U,V\r
 655 %are consistent if there exist a total order T such that both U and V\r
 656 %are suborders of T.\r
 657 \end{defn}\r
 658 \r
 659 \begin{defn}[Error-free execution]\r
 660 An error-free execution, for which the client does not flag any errors\r
 661 is defined by the following criteria:\r
 662 \begin{enumerate}\r
 663 \item Item 1\r
 664 \item Item 2\r
 665 \end{enumerate}\r
 666 %not flag any errors...\r
 667 %Define error-free execution --- execution for which the client does\r
 668 %not flag any errors...\r
 669 \end{defn}\r
 670 \r
 671 \begin{theorem} Error-free execution of algorithm ensures that the suborder\r
 672 for node n is consistent with the prefix suborder for all other nodes\r
 673 that are in the transitive closure.\r
 674 \end{theorem}\r
 675 \begin{proof}\r
 676 \textit{TODO}\r
 677 \end{proof}\r
 678 \r
 679 \begin{defn}[State of Data Structure]\r
 680 Define in terms of playing all updates sequentially onto local data\r
 681 structure.\r
 682 \end{defn}\r
 683 \r
 684 \begin{theorem}\r
 685 Algorithm gives consistent view of data structure.\r
 686 \end{theorem}\r
 687 \begin{proof}\r
 688 \textit{TODO}\r
 689 \end{proof}\r
 690 \r
 691 \subsection{Future Work}\r
 692 \paragraph{Support Messages}\r
 693   A message is dead once receiving machine sends an entry with a newer\r
 694   sequence identifier\r
 695 \r
 696 \paragraph{Persistent data structures}\r
 697         Root object w/ fields\r
 698         Other objects can be reachable from root\r
 699         Each object has its own entries\r
 700         Dead objects correspond to dead \r
 701 \r
 702 \paragraph{Multiple App Sharing}\r
 703 \r
 704 Idea is to separate subspace of entries...  Shared with other cloud...\r
 705 \end{document}\r
 706 \r