From c19662cac3f345b01780137f2eff0fd1be282a30 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 28 Jun 2016 23:02:06 -0700 Subject: [PATCH] Add document --- doc/iotcloud.tex | 184 +++++++++++++++++++++++++++++++++++++++++++++++ doc/makefile | 8 +++ 2 files changed, 192 insertions(+) create mode 100644 doc/iotcloud.tex create mode 100644 doc/makefile diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex new file mode 100644 index 0000000..7d3002b --- /dev/null +++ b/doc/iotcloud.tex @@ -0,0 +1,184 @@ +\documentclass[11pt]{article} +\newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle} +\usepackage{amsthm} +\newtheorem{theorem}{Theorem} +\newtheorem{defn}{Definition} + +\begin{document} +\section{Approach} + +\subsection{Keys} + +Each device has: user id + password + +Server login is: +hash1(user id), hash1(password)... + +Symmetric Crypto keys is: +hash2(user id | password) + +Server has finite length queue of entries + max\_entry\_identifier + +server login key + +\subsection{Entry layout} +Each entry has: +\begin{enumerate} +\item Sequence identifier +\item Random IV (if needed by crypto algorithm) +\item Encrypted payload +\end{enumerate} + +Payload has: +\begin{enumerate} +\item Sequence identifier +\item Machine id +\item Hash of previous slot +\item Data entries +\item HMAC of current slot +\end{enumerate} + +Data entry can be: +\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 +\end{enumerate} + +\subsection{Live status} + +Live status of entries: +\begin{enumerate} +\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 is dead if (of either a message version data +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 +\end{enumerate} + +When data is at the end of the queue ready to expunge, if: +\begin{enumerate} +\item The key-value entry is not dead, it must be reinserted at the +beginning of the queue. + +\item If the slot sequence number is not dead, then a message sequence +entry must be inserted + +\item If the queue state entry is not dead, it must be reinserted at the +beginning of the queue +\end{enumerate} + + +\paragraph{Reads:} +Client sends a sequence number. Server replies with either: all data +entries or all newer data entries. + +\paragraph{Writes:} +Client sends slot, server verifies that sequence number is valid, +checks entry hash, and replies with an accept message if all checks +pass. On success, client updates its sequence number. + +\paragraph{Local state on each client:} +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 For each slot: + (a) check its HMAC + (b) check that the previous entry HMAC field matches the previous + entry +\item Check that the last message version for our machine matches our +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 +\item That the number of entries received is consistent with the size +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 + (b) a request to the server + +\subsection{Formal Guarantees} + +Rahmadi should clean this section up. + +\begin{defn}[System Execution] +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. +\end{defn} + + +\begin{defn}[Suborder] +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'$. +\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. +\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. +\end{defn} + +\begin{defn}[Error-free execution] +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 +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. +\end{proof} + +\begin{defn}[State of Data Structure] +Define in terms of playing all updates sequentially onto local data +structure. +\end{defn} + +\begin{theorem} +Algorithm gives consistent view of data structure. +\end{theorem} +\begin{proof} +Exercise for Rahmadi. +\end{proof} + +\subsection{Future Work} +\paragraph{Support Messages} + A message is dead once receiving machine sends an entry with a newer + sequence identifier + +\paragraph{Persistent data structures} + Root object w/ fields + Other objects can be reachable from root + Each object has its own entries + Dead objects correspond to dead + +\paragraph{Multiple App Sharing} + +Idea is to separate subspace of entries... Shared with other cloud... +\end{document} diff --git a/doc/makefile b/doc/makefile new file mode 100644 index 0000000..cff4a15 --- /dev/null +++ b/doc/makefile @@ -0,0 +1,8 @@ +LATEX := pdflatex -halt-on-error + +default: + $(LATEX) iotcloud.tex + +clean: + rm -f *.dvi *.log *.aux *.blg *.bbl *~ + rm -f iotcloud.ps iotcloud.pdf -- 2.34.1