doc/iotcloud.tex

   1 \documentclass[11pt]{article}\r
   2 \newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}\r
   3 \usepackage{amsthm}\r
   4 \newtheorem{theorem}{Theorem}\r
   5 \newtheorem{defn}{Definition}\r
   6 \r
   7 \begin{document}\r
   8 \section{Approach}\r
   9 \r
  10 \subsection{Keys}\r
  11 \r
  12 Each device has: user id + password\r
  13 \r
  14 Server login is:\r
  15 hash1(user id), hash1(password)...\r
  16 \r
  17 Symmetric Crypto keys is:\r
  18 hash2(user id | password)\r
  19 \r
  20 Server has finite length queue of entries + max\_entry\_identifier +\r
  21 server login key\r
  22 \r
  23 \subsection{Entry layout}\r
  24 Each entry has:\r
  25 \begin{enumerate}\r
  26 \item Sequence identifier\r
  27 \item Random IV (if needed by crypto algorithm)\r
  28 \item Encrypted payload\r
  29 \end{enumerate}\r
  30 \r
  31 Payload has:\r
  32 \begin{enumerate}\r
  33 \item Sequence identifier\r
  34 \item Machine id\r
  35 \item Hash of previous slot\r
  36 \item Data entries\r
  37 \item HMAC of current slot\r
  38 \end{enumerate}\r
  39 \r
  40 Data entry can be:\r
  41 \begin{enumerate}\r
  42 \item All or part of a Key-value entry,\r
  43 \item Slot sequence entry: Machine id + last message identifier, or\r
  44 \item Queue state entry: Includes queue size\r
  45 \end{enumerate}\r
  46 \r
  47 \subsection{Live status}\r
  48 \r
  49 Live status of entries:\r
  50 \begin{enumerate}\r
  51 \item Key-Value Entry is dead if either (a) there is a newer key-value pair or (b) it is incomplete.\r
  52         \r
  53 \item Slot sequence number (of either a message version data\r
  54 or user-level data) is dead if there is a newer slot from the same machine\r
  55 \r
  56 \item Queue state entry is dead if there is a newer queue state entry\r
  57 \end{enumerate}\r
  58 \r
  59 When data is at the end of the queue ready to expunge, if:\r
  60 \begin{enumerate}\r
  61 \item The key-value entry is not dead, it must be reinserted at the\r
  62 beginning of the queue.\r
  63 \r
  64 \item If the slot sequence number is not dead, then a message sequence\r
  65 entry must be inserted\r
  66 \r
  67 \item If the queue state entry is not dead, it must be reinserted at the\r
  68 beginning of the queue\r
  69 \end{enumerate}\r
  70 \r
  71 \r
  72 \paragraph{Reads:}\r
  73 Client sends a sequence number.  Server replies with either: all data\r
  74 entries or all newer data entries.\r
  75 \r
  76 \paragraph{Writes:}\r
  77 Client sends slot, server verifies that sequence number is valid,\r
  78 checks entry hash, and replies with an accept message if all checks\r
  79 pass.  On success, client updates its sequence number.  On failure,\r
  80 server sends updates slots to client and client validates those slots.\r
  81 \r
  82 \paragraph{Local state on each client:}\r
  83 A list of machines and the corresponding latest sequence numbers\r
  84 \r
  85 \paragraph{Validation procedure on client:}\r
  86 \begin{enumerate}\r
  87 \item Decrypt each new slot in order\r
  88 \item For each slot:\r
  89     (a) check its HMAC\r
  90     (b) check that the previous entry HMAC field matches the previous\r
  91     entry\r
  92 \item Check that the last message version for our machine matches our\r
  93 last message sent\r
  94 \item For all other machines, check that the latest sequence number is\r
  95 at least as large (never goes backwards)\r
  96 \item That the queue has a current queue state entry\r
  97 \item That the number of entries received is consistent with the size\r
  98 specified in the queue state entry\r
  99 \end{enumerate}\r
 100 \r
 101 Key-value entries can span multiple slots.  They aren't valid until\r
 102 they are complete.\r
 103 \r
 104 \subsection{Resizing Queue}\r
 105 Client can make a request to resize the queue...  This is done as a write that combines:\r
 106   (a) a slot with the message\r
 107         (b) a request to the server\r
 108 \r
 109 \subsection{Formal Guarantees}\r
 110 \r
 111 Rahmadi should clean this section up.\r
 112 \r
 113 \begin{defn}[System Execution]\r
 114 Formalize a system execution as a sequence of slot updates...  There\r
 115 is a total order of all slot updates.\r
 116 \end{defn}\r
 117 \r
 118 \begin{defn}[Transitive Closure]\r
 119 Define transitive closure relation for slot updates...  There is an\r
 120 edge from a slot update to a slot receive event if the receive event\r
 121 reads from the update event.\r
 122 \end{defn}\r
 123 \r
 124 \r
 125 \begin{defn}[Suborder]\r
 126 Define suborder of total order.  It is a sequence of contiguous slots\r
 127 updates (as observed by a given device).\r
 128 \end{defn}\r
 129 \r
 130 \begin{defn}[Prefix of a suborder]\r
 131 Given a sub order $o=u_{i},u_{i+1},...,u_j, u_{j+i},..., u', ...$ and\r
 132 a slot update $u'$ in $o$, the prefix of $o$ is a sequence of all\r
 133 updates that occur before $u'$ and $u'$.\r
 134 \end{defn}\r
 135 \r
 136 \begin{defn}[Consistency between a suborder and a total order]\r
 137 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
 138 \end{defn}\r
 139 \r
 140 \begin{defn}[Consistency between suborders]\r
 141 Define notion of consistency between suborders...  Two suborders U,V\r
 142 are consistent if there exist a total order T such that both U and V\r
 143 are suborders of T.\r
 144 \end{defn}\r
 145 \r
 146 \begin{defn}[Error-free execution]\r
 147 Define error-free execution --- execution for which the client does\r
 148 not flag any errors...\r
 149 \end{defn}\r
 150 \r
 151 \begin{theorem} Error-free execution of algorithm ensures that the suborder\r
 152 for node n is consistent with the prefix suborder for all other nodes\r
 153 that are in the transitive closure.\r
 154 \end{theorem}\r
 155 \begin{proof}\r
 156 Exercise for Rahmadi.\r
 157 \end{proof}\r
 158 \r
 159 \begin{defn}[State of Data Structure]\r
 160 Define in terms of playing all updates sequentially onto local data\r
 161 structure.\r
 162 \end{defn}\r
 163 \r
 164 \begin{theorem}\r
 165 Algorithm gives consistent view of data structure.\r
 166 \end{theorem}\r
 167 \begin{proof}\r
 168 Exercise for Rahmadi.\r
 169 \end{proof}\r
 170 \r
 171 \subsection{Future Work}\r
 172 \paragraph{Support Messages}\r
 173   A message is dead once receiving machine sends an entry with a newer\r
 174   sequence identifier\r
 175 \r
 176 \paragraph{Persistent data structures}\r
 177         Root object w/ fields\r
 178         Other objects can be reachable from root\r
 179         Each object has its own entries\r
 180         Dead objects correspond to dead \r
 181 \r
 182 \paragraph{Multiple App Sharing}\r
 183 \r
 184 Idea is to separate subspace of entries...  Shared with other cloud...\r
 185 \end{document}\r