X-Git-Url: http://plrg.eecs.uci.edu/git/?p=iotcloud.git;a=blobdiff_plain;f=doc%2Fiotcloud.tex;h=5cf8b641b903155b69d442579826f0aeee8c22be;hp=b4dd5886e1430da165b17d84e01c4e2adca09a97;hb=c9193ea7314ed5c542c091cf4058fa4bbdc2e877;hpb=080ae95b19635e6be2eb3001d0d6b642ab8edd4c diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex index b4dd588..5cf8b64 100644 --- a/doc/iotcloud.tex +++ b/doc/iotcloud.tex @@ -1,9 +1,13 @@ \documentclass[11pt]{article} \newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle} +\usepackage{color} \usepackage{amsthm} +\usepackage{amsmath} +\usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx \newtheorem{theorem}{Theorem} \newtheorem{defn}{Definition} - +\newcommand{\note}[1]{{\color{red} \bf [[#1]]}} +\newcommand{\push}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax} \begin{document} \section{Approach} @@ -12,7 +16,7 @@ Each device has: user id + password Server login is: -hash1(user id), hash1(password)... +hash1(user id), hash1(password) Symmetric Crypto keys is: hash2(user id | password) @@ -31,17 +35,28 @@ Each entry has: Payload has: \begin{enumerate} \item Sequence identifier -\item Machine id -\item Hash of previous slot +\item Machine id (most probably something like a 64-bit random number +that is self-generated by client) +\item HMAC of previous slot \item Data entries \item HMAC of current slot \end{enumerate} -Data entry can be: +A data entry can be one of these: \begin{enumerate} -\item All or part of a Key-value entry, -\item Slot sequence entry: Machine id + last message identifier, or -\item Queue state entry: Includes queue size +\item All or part of a Key-value entry +\item Slot sequence entry: Machine id + last message identifier +\newline {The purpose of this is to keep the record of the last slot +from a certain client if a client's update has to expunge that other +client's last entry from the queue. This is kept in the slot until +the entry owner inserts a newer update into the queue.} +\item Queue state entry: Includes queue size \newline {The purpose +of this is for the client to tell if the server lies about the number +of slots in the queue, e.g. if there are 2 queue state entry in the queue, +e.g. 50 and 70, the client knows that when it sees 50, it should expect +at most 50 slots in the queue and after it sees 70, it should expect +50 slots before that queue state entry slot 50 and at most 70 slots. +The queue state entry slot 70 is counted as slot number 51 in the queue.} \end{enumerate} \subsection{Live status} @@ -51,9 +66,12 @@ Live status of entries: \item Key-Value Entry is dead if either (a) there is a newer key-value pair or (b) it is incomplete. \item Slot sequence number (of either a message version data -or user-level data) is dead if there is a newer slot from the same machine +or user-level data) is dead if there is a newer slot from the same machine. -\item Queue state entry is dead if there is a newer queue state entry +\item Queue state entry is dead if there is a newer queue state entry. +{In the case of queue state entries 50 and 70, this means that queue state +entry 50 is dead and 70 is live. However, not until the number of slots reaches +70 that queue state entry 50 will be expunged from the queue.} \end{enumerate} When data is at the end of the queue ready to expunge, if: @@ -62,10 +80,10 @@ When data is at the end of the queue ready to expunge, if: beginning of the queue. \item If the slot sequence number is not dead, then a message sequence -entry must be inserted +entry must be inserted. \item If the queue state entry is not dead, it must be reinserted at the -beginning of the queue +beginning of the queue. \end{enumerate} @@ -80,72 +98,270 @@ pass. On success, client updates its sequence number. On failure, server sends updates slots to client and client validates those slots. \paragraph{Local state on each client:} -A list of machines and the corresponding latest sequence numbers +A list of machines and the corresponding latest sequence numbers. \paragraph{Validation procedure on client:} \begin{enumerate} -\item Decrypt each new slot in order +\item Decrypt each new slot in order. \item For each slot: - (a) check its HMAC + (a) check its HMAC, and (b) check that the previous entry HMAC field matches the previous - entry + entry. \item Check that the last message version for our machine matches our -last message sent +last message sent. \item For all other machines, check that the latest sequence number is -at least as large (never goes backwards) -\item That the queue has a current queue state entry +at least as large (never goes backwards). +\item That the queue has a current queue state entry. \item That the number of entries received is consistent with the size -specified in the queue state entry +specified in the queue state entry. \end{enumerate} Key-value entries can span multiple slots. They aren't valid until they are complete. \subsection{Resizing Queue} -Client can make a request to resize the queue... This is done as a write that combines: - (a) a slot with the message +Client can make a request to resize the queue. This is done as a write that combines: + (a) a slot with the message, and (b) a request to the server +\subsection{Server Algorithm} +$s \in SN$ is a sequence number\\ +$sv \in SV$ is a slot's value\\ +$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\ + +\textbf{State} \\ +\textit{SL = set of live slots on server} \\ +\textit{max = maximum number of slots (input only for resize message)} \\ +\textit{n = number of slots} \\ + +\begin{algorithmic}[1] +\Function{GetSlot}{$s_g$} +\State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$} +\EndFunction +\end{algorithmic} + +\begin{algorithmic}[1] +\Function{PutSlot}{$s_p,sv_p,max'$} +\If{$(max' \neq \emptyset)$}\Comment{Resize} +\State $max \gets max'$ +\EndIf +\State $s_n \gets \{\langle s,sv \rangle \in SL \mid + \forall \langle s_i,sv_i \rangle \in SL, s \geq s_i\}$\Comment{Last s} +\If{$(s_p = s_n + 1)$} + \If{$n = max$} + \State $SL \gets SL - \{\langle s,sv \rangle \in SL \mid + \forall \langle s_i,sv_i \rangle \in SL, s \leq s_i\}$\Comment{First s} + \Else \Comment{$n < max$} + \State $n \gets n + 1$ + \EndIf + \State $SL \gets SL \cup \{\langle s_p,sv_p \rangle\}$ + \State \Return{$true$} +\Else + \State \Return{$(false,\{\langle s,sv \rangle \in SL \mid + s \geq s_p\})$} +\EndIf +\EndFunction +\end{algorithmic} + +\subsection{Client Algorithm} +\begin{algorithmic}[1] +\Function{CallClient}{$uid,pw,d,m,max,s,Data*,Result*$} +\textit{ +\newline{// uid = user identification} +\newline{// pw = password} +\newline{// d = new data for write} +\newline{// m = client message (read/write/resize)} +\newline{// max = maximum number of slots (input only for resize message)} +\newline{// n = number of slots} +\newline{// s = sequence number for server request} +\newline{// t = sequence numbers of slots on server} +\newline{// mid = machine identification} +\newline{// seq = sequence number inside slot} +\newline{// newSlot = new slot} +\newline{// expSlot = expunged/expired slot} +\newline{// slotSeqE = slot sequence entry} +\newline{// M = list of all machines/devices with their respective latest s on client} +\newline{// Data = array of slots written/read (input only for write)} +\newline{// Result = array of decrypted and valid slots after a read} +\newline{// Slot = one data slot)} +\newline{// DSlot = one decrypted data slot)} +} +\State $SK = Hash(uid + pw)$ +\If{$m = read$} + \State $Data \gets CallServer(m,max,s,Data)$ + \If{$Data = \emptyset$} + \State $ReportError(\emptyset,read)$ + \Else + \If{$\neg HasCurrentQueueStateEntry(Data)$} + \State $ReportError(DSlot_i,read)$ + \EndIf + \ForAll{$Slot_i \in Data$} + \State $DSlot_i \gets Decrypt(SK,Slot_i)$\Comment{Check s and HMAC} + \If{$\neg (ValidSeqN(DSlot_i) \land ValidHmac(DSlot_i) \land $\\ + \push[1] $ValidPrevHmac(DSlot_i))$} + \State $ReportError(DSlot_i,read)$ + \Else\Comment{Check only live entries} + \If{$IsLiveSlotSequenceEntry(DSlot_i)$} + \State $lastS \gets LastSeqN(DSlot_i)$ + \State $lastMid \gets LastMachineId(DSlot_i)$ + \If{$lastS \neq LastSeqN(lastMid,M)$} + \State $ReportError(DSlot_i,read)$ + \EndIf + \ElsIf{$IsLiveKeyValueEntry(DSlot_i)$} + \State $mid \gets MachineId(DSlot_i)$ + \State $seq \gets SeqN(DSlot_i)$ + \If{$IsOwnMid(mid)$} + \If{$IsLastS(mid,seq,Data) \land $\\ + \push[1] $(seq \neq LastSeqN(mid,M))$} + \State $ReportError(DSlot_i,read)$ + \EndIf + \Else\Comment{Check s for other machines} + \If{$IsLastS(mid,seq,Data) \land $\\ + \push[1] $(seq < LastSeqN(mid,M))$} + \State $ReportError(DSlot_i,read)$ + \EndIf + \EndIf\Comment{Check queue state entry} + \ElsIf{$IsLiveQueueStateEntry(DSlot_i)$} + \If{$IsCurrentQueueState(DSlot_i)$} + \If{$Length(Data) > QueueLength(DSlot_i)$} + \State $ReportError(DSlot_i,read)$ + \EndIf + \EndIf + \Else + \State $ReportError(DSlot_i,read)$ + \EndIf + \EndIf + \State $Result \gets Concat(Result, DSlot_i)$ + \EndFor + \EndIf + +\ElsIf{$m = write$} + \State $newSlot \gets CreateSlot(d)$ + \State $Data[1] \gets Encrypt(SK,newSlot)$ + \State $Data \gets CallServer(m,max,s,Data)$ + \If{$Data = \emptyset$} + \State $ReportError(\emptyset,write)$ + \Else\Comment Check for valid return value from server + \If{$\neg ValidOldLastEntry(Data[1])$} + \State $ReportError(Data[1],write)$ + \Else\Comment{Check if we need slot sequence entry} + \If{$Length(Data) = 2$} + \State $expSlot \gets Decrypt(SK,Data[2])$ + \State $mid \gets MachineId(expSlot)$ + \State $seq \gets SeqN(expSlot)$ + \If{$seq = LastSeqN(mid,M)$}\Comment{Liveness check} + \State $slotSeqE \gets CreateSlotSeqE(mid,seq)$ + \State $Data[1] \gets Encrypt(SK,slotSeqE)$ + \State $Data \gets CallServer(m,max,s,Data)$ + \EndIf + \Else + \State $ReportError(Data,write)$ + \EndIf + \EndIf + \EndIf + +\ElsIf{$m = resize$} + \State $Data \gets CallServer(m,max,s,Data)$ + \If{$Data = \emptyset$} + \State $ReportError(\emptyset,resize)$ + \EndIf +\EndIf +\State \Return{$Result$} +\EndFunction +\end{algorithmic} + \subsection{Formal Guarantees} -Rahmadi should clean this section up. +\textit{To be completed ...} \begin{defn}[System Execution] -Formalize a system execution as a sequence of slot updates... There -is a total order of all slot updates. +Let \\ +\begin{center} +$Q = \{slot_{sn_1}, slot_{sn_2}, \dots, Slot_{sn_n}\}$, \\ +$SN = \{sn_1, sn_2, \dots, sn_n\}$ \\ +\end{center} +denote a queue $Q$ of $n$ slots, with each slot entry being denoted by a +valid sequence number $sn_i \in SN$. $Q$ represents a total order of all +slot updates from all corresponding machines. +%\textit{Formalize a system execution as a sequence of slot updates... +%There is a total order of all slot updates.} \end{defn} \begin{defn}[Transitive Closure] -Define transitive closure relation for slot updates... There is an -edge from a slot update to a slot receive event if the receive event -reads from the update event. +A transitive closure $\tau : \tau = \epsilon_{update(slot_i)} R $ +$\epsilon_{receive(slot_i)}$ is a relation from slot update event +$\epsilon$ to a slot receive event $\epsilon$ for $slot_i$. +%Define transitive closure relation for slot updates... There is an +%edge from a slot update to a slot receive event if the receive event +%reads from the update event. \end{defn} - \begin{defn}[Suborder] -Define suborder of total order. It is a sequence of contiguous slots -updates (as observed by a given device). +Let \\ +\begin{center} +$q = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\}, +sn_1 \leq i \leq j \leq sn_n \Longrightarrow q \subseteq Q$ +\end{center} +denote a suborder of the total order. Set q is a sequence of contiguous +slot updates that is a subset of a total order of all slot updates in Q. +%Define suborder of total order. It is a sequence of contiguous slots +%updates (as observed by a given device). \end{defn} \begin{defn}[Prefix of a suborder] -Given a sub order $o=u_{i},u_{i+1},...,u_j, u_{j+i},..., u', ...$ and -a slot update $u'$ in $o$, the prefix of $o$ is a sequence of all -updates that occur before $u'$ and $u'$. +Given a suborder \\ +\begin{center} +$q' = \{slot_{i}, slot_{i+1}, \dots, slot_{j}, \dots\}, +sn_1 \leq i \leq j \leq sn_n \Longrightarrow +q' \subseteq Q$ +\end{center} +with $slot_{j}$ as a slot update in $q'$, the prefix of $q'$ is a sequence +of all slot updates $\{slot_{i}, slot_{i+1}, \dots, slot_{j-1}\} \cup +slot_{j}$. +%Given a sub order $o=u_{i},u_{i+1},...,u_j, u_{j+i},..., u', ...$ and +%a slot update $u'$ in $o$, the prefix of $o$ is a sequence of all +%updates that occur before $u'$ and $u'$. \end{defn} \begin{defn}[Consistency between a suborder and a total order] -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. +A suborder $q'$ is consistent with a total order $T$ of $Q$, if all +updates in $q'$ appear in $T$ and they appear in the same order, as +the following: +\begin{center} +$q' = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\},$ +$T = \{slot_{sn_1}, \dots, slot_{i}, slot_{i+1}, \dots, slot_{j}, \dots, +slot_{sn_n}\},$ \\ $sn_1 \leq i \leq j \leq sn_n \Longrightarrow +q' \subseteq T$ +\end{center} +%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. \end{defn} \begin{defn}[Consistency between suborders] -Define notion of consistency between suborders... Two suborders U,V -are consistent if there exist a total order T such that both U and V -are suborders of T. +Two suborders U and V are consistent if there exist a total order T +such that both U and V are suborders of T. +\begin{center} +$U = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\},$ \\ +$V = \{slot_{k}, slot_{k+1}, \dots, slot_{l}\},$ \\ +$sn_1 \leq i \leq j \leq k \leq l \leq sn_n,$ \\ +$U \subset T \land V \subset T$ \\ +$T = \{slot_{sn_1}, \dots, slot_{i}, slot_{i+1}, \dots, slot_{j}, $\\ +$\dots, slot_{k}, slot_{k+1}, \dots, slot_{l}, \dots, slot_{sn_n}\}$ +\end{center} +%Define notion of consistency between suborders... Two suborders U,V +%are consistent if there exist a total order T such that both U and V +%are suborders of T. \end{defn} \begin{defn}[Error-free execution] -Define error-free execution --- execution for which the client does -not flag any errors... +An error-free execution, for which the client does not flag any errors +is defined by the following criteria: +\begin{enumerate} +\item Item 1 +\item Item 2 +\end{enumerate} +%not flag any errors... +%Define error-free execution --- execution for which the client does +%not flag any errors... \end{defn} \begin{theorem} Error-free execution of algorithm ensures that the suborder @@ -153,7 +369,7 @@ for node n is consistent with the prefix suborder for all other nodes that are in the transitive closure. \end{theorem} \begin{proof} -Exercise for Rahmadi. +\textit{TODO} \end{proof} \begin{defn}[State of Data Structure] @@ -165,7 +381,7 @@ structure. Algorithm gives consistent view of data structure. \end{theorem} \begin{proof} -Exercise for Rahmadi. +\textit{TODO} \end{proof} \subsection{Future Work} @@ -183,3 +399,4 @@ Exercise for Rahmadi. Idea is to separate subspace of entries... Shared with other cloud... \end{document} +