From: Ali Younis Date: Thu, 13 Oct 2016 22:44:11 +0000 (-0700) Subject: Formal Edits X-Git-Url: http://plrg.eecs.uci.edu/git/?p=iotcloud.git;a=commitdiff_plain;h=2c6c9bff73c4f348b1a9912ead35161d9b811906 Formal Edits --- diff --git a/version2/doc/iotcloud_formal/iotcloud.tex b/version2/doc/iotcloud_formal/iotcloud.tex index 6615895..b13d030 100644 --- a/version2/doc/iotcloud_formal/iotcloud.tex +++ b/version2/doc/iotcloud_formal/iotcloud.tex @@ -5,14 +5,18 @@ \usepackage{amsmath} \usepackage{graphicx} \usepackage{mathrsfs} +\usepackage{amssymb} \usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx \usepackage[all]{xy} +\usepackage{varwidth} + \newtheorem{theorem}{Theorem} \newtheorem{prop}{Proposition} \newtheorem{lem}{Lemma} \newtheorem{defn}{Definition} \newcommand{\note}[1]{{\color{red} \bf [[#1]]}} \newcommand{\push}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax} +\newcommand*\xor{\mathbin{\oplus}} \begin{document} @@ -52,6 +56,9 @@ $n = 0$ \subsection{\textbf{Put Slot}} Put slot is an operation that inserts data into a new slot at the server.\\ +%Put Function +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} \textbf{Put Function:} \begin{algorithmic}[1] \Function{PutSlotServer}{$sv_p$} @@ -60,21 +67,30 @@ Put slot is an operation that inserts data into a new slot at the server.\\ \State $SL \gets SL \cup \{\tuple{s_p,sv_p}\}$ \EndFunction \end{algorithmic} - +\end{varwidth}% +} \subsection{\textbf{Get Slot}} Get slot is an operation that returns all server slots that are greater than some server sequence number.\\ +% Get Function +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} \textbf{Get Function:} \begin{algorithmic}[1] \Function{GetSlotServer}{$s_g$} \State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$} \EndFunction \end{algorithmic} +\end{varwidth}% +} \subsection{\textbf{Delete Slot}} Delete slot is an operation that deletes all live slots that have server sequence numbers that are equal to or less than some server sequence number.\\ +%Delete Function +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} \textbf{Delete Function:} \begin{algorithmic}[1] \Function{DeleteSlotServer}{$s_d$} @@ -82,6 +98,8 @@ Delete slot is an operation that deletes all live slots that have server sequenc \State $SL \gets SL - SD$ \EndFunction \end{algorithmic} +\end{varwidth}% +} @@ -100,22 +118,210 @@ The data structure exposes the following functions: \end{itemize} \subsection{\textbf{Client Notation Conventions}} + +$K$ is the set of all keys.\\ +$MID$ is the set of the machine IDs of the devices that are in the system. +$K_{mid}$ is a set of all keys that have device mid as the arbitrator\\ +$ssn_s$ is the server sequence number of a record $s$\\ $mid_s \in MID$ is the machine ID for the device that created $record_s$.\\ $hmac_s$ is the HMAC of $record_s$\\ $c_{mid}$ is the latest read clock for a device with machine ID $mid$\\ $vc_s = \{c_{mid} | mid \in MID\}$\\ - - -$payload_s = \{x_1, x_2,..., x_k | \forall k, x_k \in \{$transaction, commit, abort, resize, new-key, sequence, delete$\}\}$\\ -$record_s = \tuple{mid_s, vc_s, hmac_s, payload_s}$ \\ +$rid_s = \tuple{mid_s, c_{mid_s}}$ +$k$ is a key entry\\ +$v$ is a value entry\\ +$kv_n$ is a key-value entry $\tuple{k_n,v_n} , k \in K$\\ + +$tid_s = \tuple{mid_s,c_{mid_s}}$\\ +$guard_s = \tuple{\{kv_1, kv_2, ... ,kv_n | \exists mid \in MID, \forall n, kv_n[k] \in K_{mid}\},$ boolean condition using $ \{kv_1, kv_2, ... ,kv_n\}} $\\ +$transaction_s = \{mid_s,vc_{s_t} ,\{kv_1, kv_2,...kv_n | \exists mid \in MID, mid = guard_s[mid], \forall n, kv_n[k] \in K_{mid}\},guard_s\}$\\ +$commit_s = \tuple{tid_s,vc_s}$\\ +$abort_s = \tuple{tid_s,mid_s,vc_s}$\\ +$sequence_s = \tuple{rid_s, ssn_s}$\\ +$delete_s = \tuple{ssn_d}$\\ +$resize_s = \tuple{x | x \in \mathbb{N}}$\\ +$newkey_s = \tuple{k_s, vc_s, ssn_s$ or $-1, mid_s}$\\ + +$payload_s = \{x_1, x_2,..., x_k | \forall k, x_k \in \{$transaction, commit, abort, resize, newkey, sequence, delete$\}\}$\\ +$rd_s = \tuple{mid_s, vc_s, hmac_s, payload_s}$ \\ +$record_s = \tuple{ssn_s,rd_s}$\\ \subsection{\textbf{Client State}} \textit{s = largest server sequence number pulled from the server by a device} \\ - +\textit{R = set of records pulled from the server so far with their server sequence numbers} \\ +\textit{RL = set of records that contain live data} \\ \subsection{Helper Functions} The following helper functions are needed:\\ +%Get Payload Items from Record with SSN +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} +\textbf{Get Payload Items from Record with SSN}: +\begin{algorithmic}[1] +\Function{GetPayloadItemsWithSSN}{$record_s$} + \State $PISSN \gets \emptyset$ \Comment{Set of Payload Items with ssn} + \State $\tuple{ssn_s, rd_s} \gets record_s$ + \State $\tuple{mid_s, vc_s, hmac_s, payload_s} \gets rd_s$\\ + + \ForAll{$payloadItems$ in $payload_s$} + \State $PISSN \gets PISSN \cup \tuple{payloadItem, ssn_s}$ + \EndFor\\ + + \State \Return {$PISSN$} +\EndFunction +\end{algorithmic} +\end{varwidth}% +} + +%Get rid For Record +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} +\textbf{Get rid For Record}: +\begin{algorithmic}[1] +\Function{GetRid}{$record_s$} + \State $\tuple{ssn_s, \tuple{mid_s, \{c_{mid_1}, c_{mid_2}, ... , c_{mid_k}\}, hmac_s, payload_s}} \gets record_s$ + \State \Return {$\tuple{mid_s, c_{mid_s}}$} +\EndFunction +\end{algorithmic} +\end{varwidth}% +} + + +\textbf{Get Transaction Arbitrator}:\\ +\textbf{Transaction Live}:\\ +\textbf{Commit Live}:\\ + +%Sequence Live +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} +\textbf{Sequence Live}: +\begin{algorithmic}[1] +\Function{SequenceLive}{$sequence_s, ssn_{s1}$} + \State $API \gets \emptyset$ \Comment{Set of all Payload Items} + \State $AS \gets \emptyset$ \Comment{Set of all Payload Items that are sequences} + \State $StillHasRecord \gets False$ + \State $\tuple{rid_s, ssn_{s2}} \gets sequence_s$\\ + + \ForAll{$record$ in $R$} + \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} + \If{$rid_s = $\Call{GetRid}{$record$}} + \State $StillHasRecord \gets True$ + \EndIf + \EndFor\\ + + \If{$\lnot StillHasRecord$} \Comment{The Record does not exists anymore} + \State \Return{False} + \EndIf\\ + + \ForAll{$\tuple{ssn, payload}$ in $API$} + \If{$payload$ is a $sequence$} + \State $AS \gets AS \cup \{\tuple{ssn, payload}\}$ \Comment{Extract all sequence payloads} + \EndIf + \EndFor\\ + + \ForAll{$\tuple{ssn_1', \tuple{rid', ssn_2'}}$ in $AS$} + \If{$(rid'=rid_s) \land (ssn_1' > ssn_{s_1})$} + \State \Return{False} + \EndIf + \EndFor \\ + \State \Return{True} +\EndFunction +\end{algorithmic} +\end{varwidth}% +} + +% Delete Live +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} +\textbf{Delete Live}: +\begin{algorithmic}[1] +\Function{DeleteLive}{$delete_s, ssn_s$} + \State $API \gets \emptyset$ \Comment{Set of all Payload Items} + \State $AD \gets \emptyset$ \Comment{Set of all Payload Items that are deletes} + \State $\tuple{ssn_d} \gets delete_s$\\ + + \ForAll{record in R} + \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} + \EndFor\\ + + \ForAll{$\tuple{ssn, payload}$ in $API$} + \If{$payload$ is a $delete$} + \State $AD \gets AD \cup \{\tuple{ssn, payload}\}$ \Comment{Extract all delete payloads} + \EndIf + \EndFor\\ + + \ForAll{delete in AD} + \State $\tuple{{ssn_s}', \tuple{{ssn_d}'}} \gets delete$ + \If{${ssn_d}' > ssn_d$} \Comment{More recently deleted record} + \State \Return{False} + \ElsIf{$({ssn_d}'= ssn_d) \land ({ssn_s}' > ssn_s)$} \Comment{More recent delete of same record} + \State \Return{False} + \EndIf + \EndFor \\ + \State \Return{True} +\EndFunction +\end{algorithmic} +\end{varwidth}% +} + +%Abort Live +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} +\textbf{Abort Live}: +\begin{algorithmic}[1] +\Function{AbortLive}{$abort_s$} + \State $\tuple{tid_s,mid_s,vc_s} \gets abort_s$\\ + \ForAll{record in R} + \State $\tuple{ssn_s',\tuple{mid_s', vc_s', hmac_s', payload_s'}} \gets record$ + \If{$(mid_s'=mid_s) \land (vc_s' > vc_s)$} + \State \Return{True} + \EndIf + \EndFor\\ + \State \Return{False} +\EndFunction +\end{algorithmic} +\end{varwidth}% +} + +%Resize Live +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} +\textbf{Resize Live}: +\begin{algorithmic}[1] +\Function{ResizeLive}{$resize_s, ssn_s$} + \State $API \gets \emptyset$ \Comment{Set of all Payload Items} + \State $AR \gets \emptyset$ \Comment{Set of all Payload Items that are resize} + \State $\tuple{size} \gets resize_s$\\ + + \ForAll{record in R} + \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} + \EndFor\\ + + \ForAll{$\tuple{ssn, payload}$ in $API$} + \If{$payload$ is a $resize$} + \State $AR \gets AR \cup \{\tuple{ssn, payload}\}$ \Comment{Extract all resize payloads} + \EndIf + \EndFor\\ + + \ForAll{$\tuple{ssn', \tuple{size'}}$ in $AR$} + \If{$size' > size$} + \State \Return{False} + \ElsIf{$(size'=size) \land (ssn' > ssn_s)$} + \State \Return{False} + \EndIf + \EndFor \\ + \State \Return{True} +\EndFunction +\end{algorithmic} +\end{varwidth}% +} + + + +\textbf{Evaluate Guard Condition:}\\ + + \textbf{Get Latest Data Structure From Server:}\\ \textbf{Delete Records:}\\ \textbf{Check Data Structure for Malicious Activity:}