--- /dev/null
+\documentclass[11pt]{article}\r
+\newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}\r
+\usepackage{amsthm}\r
+\newtheorem{theorem}{Theorem}\r
+\newtheorem{defn}{Definition}\r
+\r
+\begin{document}\r
+\section{Approach}\r
+\r
+\subsection{Keys}\r
+\r
+Each device has: user id + password\r
+\r
+Server login is:\r
+hash1(user id), hash1(password)...\r
+\r
+Symmetric Crypto keys is:\r
+hash2(user id | password)\r
+\r
+Server has finite length queue of entries + max\_entry\_identifier +\r
+server login key\r
+\r
+\subsection{Entry layout}\r
+Each entry has:\r
+\begin{enumerate}\r
+\item Sequence identifier\r
+\item Random IV (if needed by crypto algorithm)\r
+\item Encrypted payload\r
+\end{enumerate}\r
+\r
+Payload has:\r
+\begin{enumerate}\r
+\item Sequence identifier\r
+\item Machine id\r
+\item Hash of previous slot\r
+\item Data entries\r
+\item HMAC of current slot\r
+\end{enumerate}\r
+\r
+Data entry can be:\r
+\begin{enumerate}\r
+\item All or part of a Key-value entry,\r
+\item Slot sequence entry: Machine id + last message identifier, or\r
+\item Queue state entry: Includes queue size\r
+\end{enumerate}\r
+\r
+\subsection{Live status}\r
+\r
+Live status of entries:\r
+\begin{enumerate}\r
+\item Key-Value Entry is dead if either (a) there is a newer key-value pair or (b) it is incomplete.\r
+ \r
+\item Slot sequence number is dead if (of either a message version data\r
+or user-level data) is dead if there is a newer slot from the same machine\r
+\r
+\item Queue state entry is dead if there is a newer queue state entry\r
+\end{enumerate}\r
+\r
+When data is at the end of the queue ready to expunge, if:\r
+\begin{enumerate}\r
+\item The key-value entry is not dead, it must be reinserted at the\r
+beginning of the queue.\r
+\r
+\item If the slot sequence number is not dead, then a message sequence\r
+entry must be inserted\r
+\r
+\item If the queue state entry is not dead, it must be reinserted at the\r
+beginning of the queue\r
+\end{enumerate}\r
+\r
+\r
+\paragraph{Reads:}\r
+Client sends a sequence number. Server replies with either: all data\r
+entries or all newer data entries.\r
+\r
+\paragraph{Writes:}\r
+Client sends slot, server verifies that sequence number is valid,\r
+checks entry hash, and replies with an accept message if all checks\r
+pass. On success, client updates its sequence number.\r
+\r
+\paragraph{Local state on each client:}\r
+A list of machines and the corresponding latest sequence numbers\r
+\r
+\paragraph{Validation procedure on client:}\r
+\begin{enumerate}\r
+\item Decrypt each new slot in order\r
+\item For each slot:\r
+ (a) check its HMAC\r
+ (b) check that the previous entry HMAC field matches the previous\r
+ entry\r
+\item Check that the last message version for our machine matches our\r
+last message sent\r
+\item For all other machines, check that the latest sequence number is\r
+at least as large (never goes backwards)\r
+\item That the queue has a current queue state entry\r
+\item That the number of entries received is consistent with the size\r
+specified in the queue state entry\r
+\end{enumerate}\r
+\r
+Key-value entries can span multiple slots. They aren't valid until\r
+they are complete.\r
+\r
+\subsection{Resizing Queue}\r
+Client can make a request to resize the queue... This is done as a write that combines:\r
+ (a) a slot with the message\r
+ (b) a request to the server\r
+\r
+\subsection{Formal Guarantees}\r
+\r
+Rahmadi should clean this section up.\r
+\r
+\begin{defn}[System Execution]\r
+Formalize a system execution as a sequence of slot updates... There\r
+is a total order of all slot updates.\r
+\end{defn}\r
+\r
+\begin{defn}[Transitive Closure]\r
+Define transitive closure relation for slot updates... There is an\r
+edge from a slot update to a slot receive event if the receive event\r
+reads from the update event.\r
+\end{defn}\r
+\r
+\r
+\begin{defn}[Suborder]\r
+Define suborder of total order. It is a sequence of contiguous slots\r
+updates (as observed by a given device).\r
+\end{defn}\r
+\r
+\begin{defn}[Prefix of a suborder]\r
+Given a sub order $o=u_{i},u_{i+1},...,u_j, u_{j+i},..., u', ...$ and\r
+a slot update $u'$ in $o$, the prefix of $o$ is a sequence of all\r
+updates that occur before $u'$ and $u'$.\r
+\end{defn}\r
+\r
+\begin{defn}[Consistency between a suborder and a total order]\r
+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
+\end{defn}\r
+\r
+\begin{defn}[Consistency between suborders]\r
+Define notion of consistency between suborders... Two suborders U,V\r
+are consistent if there exist a total order T such that both U and V\r
+are suborders of T.\r
+\end{defn}\r
+\r
+\begin{defn}[Error-free execution]\r
+Define error-free execution --- execution for which the client does\r
+not flag any errors...\r
+\end{defn}\r
+\r
+\begin{theorem} Error-free execution of algorithm ensures that the suborder\r
+for node n is consistent with the prefix suborder for all other nodes\r
+that are in the transitive closure.\r
+\end{theorem}\r
+\begin{proof}\r
+Exercise for Rahmadi.\r
+\end{proof}\r
+\r
+\begin{defn}[State of Data Structure]\r
+Define in terms of playing all updates sequentially onto local data\r
+structure.\r
+\end{defn}\r
+\r
+\begin{theorem}\r
+Algorithm gives consistent view of data structure.\r
+\end{theorem}\r
+\begin{proof}\r
+Exercise for Rahmadi.\r
+\end{proof}\r
+\r
+\subsection{Future Work}\r
+\paragraph{Support Messages}\r
+ A message is dead once receiving machine sends an entry with a newer\r
+ sequence identifier\r
+\r
+\paragraph{Persistent data structures}\r
+ Root object w/ fields\r
+ Other objects can be reachable from root\r
+ Each object has its own entries\r
+ Dead objects correspond to dead \r
+\r
+\paragraph{Multiple App Sharing}\r
+\r
+Idea is to separate subspace of entries... Shared with other cloud...\r
+\end{document}\r
projects / iotcloud.git / commitdiff