f1a472a937897086d7b0aff7f2c32ba471c87e98
[iotcloud.git] / 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 \textbf{Login}\r
24 \begin{enumerate}\r
25 \item In the beginning, there are $d$ devices. Each of the \r
26 devices has a randomly/user-chosen self-generated $m$-bit user \r
27 identification $i$ and $n$-bit password $p$.\r
28 \item Each device registers these $i$ and $p$ with the server. \r
29 The server appends ‘salt’ values, $k$-bit random strings $s1$ \r
30 and $s2$, and generate hash values $j=h(i+s1)$ and \r
31 $o=h(p+s2)$ for each $i$ and $p$. All $s1$, $s2$, $j$ and $o$ \r
32 are then stored in the database.\r
33 \item Device to server validation is done by checking the hash values \r
34 $j\textsc{\char13}$ and $o\textsc{\char13}$ from $i\textsc{\char13}$ and \r
35 $p\textsc{\char13}$ that are given by users at login time against \r
36 $i$ and $p$ that are stored in the database.\r
37 \end{enumerate}\r
38 \r
39 \textbf{Symmetric Keys}\r
40 \begin{enumerate}\r
41 \item In the beginning, there are $d$ devices. Each of the \r
42 devices has a randomly/user-chosen self-generated $m$-bit user \r
43 identification $i$ and $n$-bit password $p$. These $i$ and $p$ \r
44 are used for device login on server.\r
45 \item All of $d$ agree on a hash function $h$ that is not known by \r
46 the server.\r
47 \item A symmetric key for each device is generated by applying $h$\r
48 to the value $(i + p)$ that gives $SK=h(i + p)$.\r
49 \item This value $SK$ is pre-known and pre-stored by all other \r
50 devices prior to operation of the data structure.\r
51 \end{enumerate}\r
52 \r
53 \textbf{Data Structure on Server}\r
54 \begin{enumerate}\r
55 \item Server maintains a finite length $q$-entry FIFO queue \r
56 $Q=\{0, 1, …, q-1\}$. It has a head and a tail pointers that keep track \r
57 of head and tail slots.\r
58 \item Server records a max entry identifier $max$ as a limit for $q$. \r
59 It keeps track that $q \leq max$ at all times. When $q=max$, the queue \r
60 mechanism allows this sequence of events when there is a new slot added:\r
61 \begin{enumerate}\r
62 \item Pointer for entry $0$ now points to entry $1$, making it the new \r
63 entry $0$.\r
64 \item Entry $0$ is expunged from the queue.\r
65 \item New entry is added to the end of the queue, making it entry $q$.\r
66 \item Pointer for entry $q-1$ is advanced to entry $q$, making it the new \r
67 entry $q-1$.\r
68 \end{enumerate}\r
69 \item For client login, server maintains a table with values $i$, $p$,\r
70 $s1$, and $s2$ that are generated when device registers itself on server \r
71 for the first time.\r
72 \end{enumerate}\r
73 \r
74 \subsection{Entry layout}\r
75 Each entry has:\r
76 \begin{enumerate}\r
77 \item Sequence identifier\r
78 \item Random IV (if needed by crypto algorithm)\r
79 \item Encrypted payload\r
80 \end{enumerate}\r
81 \r
82 Payload has:\r
83 \begin{enumerate}\r
84 \item Sequence identifier\r
85 \item Machine id (most probably something like a 64-bit random number \r
86 that is self-generated by client)\r
87 \item HMAC of previous slot\r
88 \item Data entries\r
89 \item HMAC of current slot\r
90 \end{enumerate}\r
91 \r
92 A data entry can be one of these:\r
93 \begin{enumerate}\r
94 \item All or part of a Key-value entry\r
95 \item Slot sequence entry: Machine id + last message identifier \r
96 \newline {The purpose of this is to keep the record of the last slot \r
97 from a certain client if a client's update has to expunge that other \r
98 client's last entry from the queue. This is kept in the slot until \r
99 the entry owner inserts a newer update into the queue.}\r
100 \item Queue state entry: Includes queue size \newline {The purpose \r
101 of this is for the client to tell if the server lies about the number \r
102 of slots in the queue, e.g. if there are 2 queue state entry in the queue, \r
103 e.g. 50 and 70, the client knows that when it sees 50, it should expect \r
104 at most 50 slots in the queue and after it sees 70, it should expect \r
105 50 slots before that queue state entry slot 50 and at most 70 slots. \r
106 The queue state entry slot 70 is counted as slot number 51 in the queue.}\r
107 \end{enumerate}\r
108 \r
109 \subsection{Live status}\r
110 \r
111 Live status of entries:\r
112 \begin{enumerate}\r
113 \item Key-Value Entry is dead if either (a) there is a newer key-value pair or (b) it is incomplete.\r
114         \r
115 \item Slot sequence number (of either a message version data\r
116 or user-level data) is dead if there is a newer slot from the same machine.\r
117 \r
118 \item Queue state entry is dead if there is a newer queue state entry.\r
119 {In the case of queue state entries 50 and 70, this means that queue state \r
120 entry 50 is dead and 70 is live. However, not until the number of slotes reaches \r
121 70 that queue state entry 50 will be expunged from the queue.}\r
122 \end{enumerate}\r
123 \r
124 When data is at the end of the queue ready to expunge, if:\r
125 \begin{enumerate}\r
126 \item The key-value entry is not dead, it must be reinserted at the\r
127 beginning of the queue.\r
128 \r
129 \item If the slot sequence number is not dead, then a message sequence\r
130 entry must be inserted.\r
131 \r
132 \item If the queue state entry is not dead, it must be reinserted at the\r
133 beginning of the queue.\r
134 \end{enumerate}\r
135 \r
136 \r
137 \paragraph{Reads:}\r
138 Client sends a sequence number.  Server replies with either: all data\r
139 entries or all newer data entries.\r
140 \r
141 \paragraph{Writes:}\r
142 Client sends slot, server verifies that sequence number is valid,\r
143 checks entry hash, and replies with an accept message if all checks\r
144 pass.  On success, client updates its sequence number.  On failure,\r
145 server sends updates slots to client and client validates those slots.\r
146 \r
147 \paragraph{Local state on each client:}\r
148 A list of machines and the corresponding latest sequence numbers.\r
149 \r
150 \paragraph{Validation procedure on client:}\r
151 \begin{enumerate}\r
152 \item Decrypt each new slot in order.\r
153 \item For each slot:\r
154     (a) check its HMAC, and\r
155     (b) check that the previous entry HMAC field matches the previous\r
156     entry.\r
157 \item Check that the last message version for our machine matches our\r
158 last message sent.\r
159 \item For all other machines, check that the latest sequence number is\r
160 at least as large (never goes backwards).\r
161 \item That the queue has a current queue state entry.\r
162 \item That the number of entries received is consistent with the size\r
163 specified in the queue state entry.\r
164 \end{enumerate}\r
165 \r
166 Key-value entries can span multiple slots.  They aren't valid until\r
167 they are complete.\r
168 \r
169 \subsection{Resizing Queue}\r
170 Client can make a request to resize the queue. This is done as a write that combines:\r
171   (a) a slot with the message, and\r
172         (b) a request to the server\r
173 \r
174 \subsection{Formal Guarantees}\r
175 \r
176 \textit{To be completed ...}\r
177 \r
178 \begin{defn}[System Execution]\r
179 Formalize a system execution as a sequence of slot updates...  There\r
180 is a total order of all slot updates.\r
181 \end{defn}\r
182 \r
183 \begin{defn}[Transitive Closure]\r
184 Define transitive closure relation for slot updates...  There is an\r
185 edge from a slot update to a slot receive event if the receive event\r
186 reads from the update event.\r
187 \end{defn}\r
188 \r
189 \begin{defn}[Suborder]\r
190 Define suborder of total order.  It is a sequence of contiguous slots\r
191 updates (as observed by a given device).\r
192 \end{defn}\r
193 \r
194 \begin{defn}[Prefix of a suborder]\r
195 Given a sub order $o=u_{i},u_{i+1},...,u_j, u_{j+i},..., u', ...$ and\r
196 a slot update $u'$ in $o$, the prefix of $o$ is a sequence of all\r
197 updates that occur before $u'$ and $u'$.\r
198 \end{defn}\r
199 \r
200 \begin{defn}[Consistency between a suborder and a total order]\r
201 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
202 \end{defn}\r
203 \r
204 \begin{defn}[Consistency between suborders]\r
205 Define notion of consistency between suborders...  Two suborders U,V\r
206 are consistent if there exist a total order T such that both U and V\r
207 are suborders of T.\r
208 \end{defn}\r
209 \r
210 \begin{defn}[Error-free execution]\r
211 Define error-free execution --- execution for which the client does\r
212 not flag any errors...\r
213 \end{defn}\r
214 \r
215 \begin{theorem} Error-free execution of algorithm ensures that the suborder\r
216 for node n is consistent with the prefix suborder for all other nodes\r
217 that are in the transitive closure.\r
218 \end{theorem}\r
219 \begin{proof}\r
220 \textit{TODO}\r
221 \end{proof}\r
222 \r
223 \begin{defn}[State of Data Structure]\r
224 Define in terms of playing all updates sequentially onto local data\r
225 structure.\r
226 \end{defn}\r
227 \r
228 \begin{theorem}\r
229 Algorithm gives consistent view of data structure.\r
230 \end{theorem}\r
231 \begin{proof}\r
232 \textit{TODO}\r
233 \end{proof}\r
234 \r
235 \subsection{Future Work}\r
236 \paragraph{Support Messages}\r
237   A message is dead once receiving machine sends an entry with a newer\r
238   sequence identifier\r
239 \r
240 \paragraph{Persistent data structures}\r
241         Root object w/ fields\r
242         Other objects can be reachable from root\r
243         Each object has its own entries\r
244         Dead objects correspond to dead \r
245 \r
246 \paragraph{Multiple App Sharing}\r
247 \r
248 Idea is to separate subspace of entries...  Shared with other cloud...\r
249 \end{document}\r