+++ /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 (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 / blobdiff