\subsection{Server Algorithm}\r
$s \in SN$ is a sequence number set\\\r
$sv \in SV$ is a slot's value\\\r
-$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\\r
-\r
+$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\ \\\r
\textbf{State} \\\r
\textit{SL = set of live slots on server} \\\r
\textit{max = maximum number of slots (input only for resize message)} \\\r
$kv$ is a key-value entry $\tuple{k,v}$, $kv \in D$ \\\r
$ss$ is a slot sequence entry $\tuple{id,s_{last}}$, \r
id + last s of a machine, $ss \in D$ \\\r
-$qs$ is a queue state entry, $qs \in D$ \\\r
+$qs$ is a queue state entry (contains $max$ size of queue), $qs \in D$ \\\r
$cr$ is a collision resolution entry $\tuple{s_{col},id_{col}}$, \r
s + id of a machine that wins a collision, $cr \in D$ \\\r
$D = \{kv,ss,qs,cr\}$ \\\r
$Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
$sv_s = \tuple{s, E(Dat_s)} = \r
\tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\\r
-\r
\textbf{States} \\\r
+\textit{$hmac_{p_g}$ = the HMAC value of the previous slot \r
+($hmac_{p_g} = \emptyset$ for the first slot)} \\\r
+\textit{$id_{self}$ = machine Id of this client} \\\r
+\textit{$max_g$ = maximum number of slots (initially $max_g > 0$)} \\\r
+\textit{m = number of slots on client (initially $m = 0$ and $m \leq n$)} \\\r
+\textit{$sl_{last}$ = info of last slot in queue = \r
+ $\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\\r
\textit{DT = set of $\tuple{k,v}$ on client} \\\r
\textit{MS = set of $\tuple{id, s_{last}}$ of all clients on client \r
(initially empty)} \\\r
\textit{$MS_g$ = set MS to save all $\tuple{id, s_{last}}$ pairs while\r
traversing DT after a request to server (initially empty)} \\\r
+\textit{SK = Secret Key} \\\r
\textit{$SM$ = set of $\tuple{s, id}$ of all slots in a previous read\r
-(initially empty)} \\\r
-\textit{$max_g$ = maximum number of slots (initially $max_c > 0$)} \\\r
-\textit{m = number of slots on client (initially $m = 0 and m \leq n$)} \\\r
-\textit{$hmac_{p_g}$ = the HMAC value of the previous slot \r
-($hmac_{p_g} = \emptyset$ for the first slot)} \\\r
-\textit{$id_{self}$ = machine Id of this client} \\\r
-\textit{SK = Secret Key} \\ \\\r
+(initially empty)} \\ \\\r
\textbf{Helper Functions} \\\r
$MaxSlot(SL_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}\r
\in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \geq s_s$ \\\r
\in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s = s_s$ \\\r
$SeqN(\tuple{s, sv})=s$ \\\r
$SlotVal(\tuple{s, sv})=sv$ \\\r
+$CreateLastSL(s,sv,id)=\tuple{s,sv,id}=sl_{last}$ \\\r
$Decrypt(SK_s,sv_s)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
$GetSeqN(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=s$ \\\r
$GetMacId(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=id$ \\\r
$GetVal(\tuple{k, v})=v$ \\\r
$GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v} \r
\in DT_s \wedge \forall \tuple{k_s, v_s} \in DT_s, k = k_s$ \\\r
+$MaxLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \r
+\wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \geq s_{s_{last}}$ \\\r
+$MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \r
+\wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \leq s_{s_{last}}$ \\\r
\r
\begin{algorithmic}[1]\r
\Procedure{ReportError}{$msg$}\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{GetColRes}{$Dat_s$}\r
+\Function{GetColRes}{$Dat_s$}\Comment{At most 2 $cr$ entries in a slot}\r
\State $DE_s \gets GetDatEnt(Dat_s)$\r
\State $de_{cr} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
de_s \in D \land de_s = cr$\r
\State $\tuple{s_{ret},id_{ret}} \r
\gets \emptyset$\r
\EndIf\r
-\State \Return{$\tuple{s_{ret},id_{ret}}$}\r
+\State $de_{r_{cr}} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
+ de_s \in D \land de_s = cr \land de_s \neq de_{cr}$\r
+\If{$de_{r_{cr}} \neq \emptyset$}\r
+ \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \gets GetCR(de_{r_{cr}})$\r
+\Else\r
+ \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \r
+ \gets \emptyset$\r
+\EndIf\r
+\State \Return{$\{\tuple{s_{ret},id_{ret}},\tuple{s_{r_{ret}},id_{r_{ret}}}\}$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\EndProcedure\r
\end{algorithmic}\r
\r
+\begin{algorithmic}[1]\r
+\Procedure{CheckCollision}{$MS_s,SM_s,\tuple{s_s,id_s}$}\r
+\If{$\tuple{s_s,id_s} \neq \emptyset$}\r
+ \State $s_s \gets GetS(\tuple{s_s,id_s})$\r
+ \State $id_s \gets GetId(\tuple{s_s,id_s})$\r
+ \State $s_{s_{last}} \gets GetLastSeqN(MS_s,id_s)$\r
+ \If{$s_{s_{last}} < s_s$}\r
+ \State $\Call{CheckColRes}{SM_s,\tuple{s_s,id_s}}$\r
+ \EndIf\r
+\EndIf\r
+\EndProcedure\r
+\end{algorithmic}\r
+\r
\begin{algorithmic}[1]\r
\Procedure{CheckColRes}{$SM_s,\tuple{s_t,id_t}$}\Comment{Check $id_s$ in $SM_s$}\r
\State $s_t \gets GetS(\tuple{s_t,id_t})$\r
\EndProcedure\r
\end{algorithmic}\r
\r
+\begin{algorithmic}[1]\r
+\Function{StoreLastSlot}{$MS_s,sl_l,s_s,sv_s,id_s$}\r
+\State $s_{min} \gets MinLastSeqN(MS_s)$\r
+\If{$s_{min} \neq \emptyset \land s_{min} = s_s$}\Comment{$MS$ initially empty}\r
+ \State $sl_l \gets CreateLastSL(s_s,sv_s,id_s)$\r
+\EndIf\r
+\State \Return{$sl_l$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
\begin{algorithmic}[1]\r
\Function{UpdateDT}{$DT_s,Dat_s$}\r
\State $DE_s \gets GetDatEnt(Dat_s)$\r
\If{$\neg \Call{ValidHmac}{DE_g,SK,hmac_{c_g}}$}\r
\State \Call{ReportError}{'Invalid current HMAC value'}\r
\EndIf\r
- \State $hmac_{p_g} \gets Hmac(Dat_g,SK)$\Comment{Update $hmac_{p_g}$ for next check}\r
+ \State $hmac_{p_g} \gets Hmac(DE_g,SK)$\Comment{Update $hmac_{p_g}$ for next check}\r
\State $qs_g \gets \Call{GetQueSta}{Dat_g}$\Comment{Handle qs}\r
\If{$qs_g \neq \emptyset \land qs_g > max_g$}\r
\State $max_g \gets qs_g$\r
\If{$\tuple{id_d,s_{d_{last}}} \neq \emptyset$}\r
\State $MS_g \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_g}$\r
\EndIf\r
- \State $\tuple{s_e,id_e} \gets \r
+ \State $\{\tuple{s_e,id_e},\tuple{s_f,id_f}\} \gets \r
\Call{GetColRes}{Dat_g}$\Comment{Handle cr}\r
- \If{$\tuple{s_e,id_e} \neq \emptyset$}\r
- \State $s_e \gets GetS(\tuple{s_e,id_e})$\r
- \State $id_e \gets GetId(\tuple{s_e,id_e})$\r
- \State $s_{c_{last}} \gets GetLastSeqN(MS,id_e)$\r
- \If{$s_{c_{last}} < s_e$}\r
- \State $\Call{CheckColRes}{SM,\tuple{s_e,id_e}}$\r
- \EndIf\r
- \EndIf\r
+ \State $\Call{CheckCollision}{MS,SM,\tuple{s_e,id_e}}$\Comment{From normal slot}\r
+ \State $\Call{CheckCollision}{MS,SM,\tuple{s_f,id_f}}$\Comment{From reinsertion}\r
+ \State $sl_{last} \gets \Call{StoreLastSlot}{MS,sl_{last},s_g,sv_g,id_g}$\r
\State $DT \gets \Call{UpdateDT}{DT,Dat_g}$\r
\EndFor\r
\State $SM \gets SM_{curr}$\r
$Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
$sv_s = \tuple{s, E(Dat_s)} = \r
\tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\\r
-\r
\textbf{States} \\\r
\textit{$cp$ = data entry $DE$ maximum size/capacity} \\\r
\textit{$cr_p$ = saved cr entry $\tuple{s,id}$ on client if there is a collision\r
(sent in the following slot)} \\\r
+\textit{$cr_{p_{last}}$ = saved cr entry $\tuple{s,id}$ on client if there is a \r
+collision in reinserting the last slot (sent in the following slot)} \\\r
\textit{$ck_p$ = counter of $kv \in KV$ for putting pairs (initially 0)} \\\r
\textit{$ck_g$ = counter of $kv \in KV$ for getting pairs (initially 0)} \\\r
-\textit{$id_{self}$ = machine Id of this client} \\\r
\textit{$hmac_{c_p}$ = the HMAC value of the current slot} \\\r
\textit{$hmac_{p_p}$ = the HMAC value of the previous slot \r
($hmac_{p_p} = \emptyset$ for the first slot)} \\\r
+\textit{$id_{self}$ = machine Id of this client} \\\r
+\textit{$sl_{last}$ = info of last slot in queue = \r
+ $\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\\r
+\textit{$th_p$ = threshold number of dead slots for a resize to happen} \\\r
+\textit{$m'_p$ = offset added to $max$ for resize} \\\r
\textit{$KV$ = set of $\tuple{ck, \tuple{k,v}}$ of kv entries on client} \\\r
-\textit{$ST$ = set of $DE$ objects on client} \\\r
\textit{$SL_p$ = set of returned slots on client} \\\r
-\textit{SK = Secret Key} \\\r
-\r
+\textit{SK = Secret Key} \\ \\\r
\textbf{Helper Functions} \\\r
$CreateDat(s,id,hmac_p,DE,hmac_c)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
+$CreateCR(s,id)=\tuple{s,id}$ \\\r
+$CreateQS(max')=qs$ \\\r
+$CreateSS(id,s_{last})=\tuple{id,s_{last}}$ \\\r
$Encrypt(Dat_s,SK_s)=sv_s$ \\\r
$GetStatus(\tuple{status,SL})=status$ \\\r
$GetSL(\tuple{status,SL})=SL$ \\\r
+$GetLastS(sl = \tuple{s,sv,id})=s$ \\\r
+$GetSV(sl = \tuple{s,sv,id})=sv$ \\\r
+$GetID(sl = \tuple{s,sv,id})=id$ \\\r
$GetColSeqN(SL_s,s_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}\r
\in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s = s_s$ \\\r
-$CreateCR(s,id)=\tuple{s,id}$ \\\r
$GetKV(KV_s,k_s)= \tuple{ck,\tuple{k, v}}$ \textit{such that} \r
$\tuple{ck,\tuple{k, v}} \in KV_s \wedge\r
\forall \tuple{ck_s,\tuple{k_s, v_s}} \in KV_s, k = k_s$ \\\r
-$MaxLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \r
-\wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \geq s_{s_{last}}$ \\\r
\r
\begin{algorithmic}[1]\r
\Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$}\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{GetDEPairs}{$KV_s$}\r
+\Function{CheckResize}{$MS_s,th_s,max'_t,m'_s$}\r
+\State $s_{last_{min}} \gets MinLastSeqN(MS_s)$\r
+\State $s_{last_{max}} \gets MaxLastSeqN(MS_s)$\r
+\State $n_{live} \gets s_{last_{max}} - s_{last_{min}}$\Comment{Number of live slots}\r
+\State $n_{dead} \gets max'_t - n_{live}$\r
+\If{$n_{dead} \leq th_s$}\r
+ \State $max'_s \gets max'_t + m'_s$\r
+\Else\r
+ \State $max'_s \gets \emptyset$\r
+\EndIf\r
+\State \Return{$max'_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{CheckNeedSS}{$MS_s,max'_t$}\Comment{Check if $ss$ is needed}\r
+\State $s_{last_{min}} \gets MinLastSeqN(MS_s)$\r
+\State $s_{last_{max}} \gets MaxLastSeqN(MS_s)$\r
+\State $n_{live} \gets s_{last_{max}} - s_{last_{min}}$\Comment{Number of live slots}\r
+\State $n_{dead} \gets max'_t - n_{live}$\r
+\If{$n_{dead} = 0$}\r
+ \State $need \gets true$\r
+\Else\r
+ \State $need \gets false$\r
+\EndIf\r
+\State \Return{$need$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{HandleCollision}{$\tuple{stat_s,SL_s}$}\r
+\State $stat_s \gets GetStatus(\tuple{stat_s,SL_s})$\r
+\State $SL_s \gets GetSL(\tuple{stat_s,SL_s})$\r
+\If{$\neg stat_s$}\Comment{Handle collision}\r
+ \State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_s,s_s)$\r
+ \State $s_{col} \gets SeqN(\tuple{s_{col},sv_{col}})$\r
+ \State $sv_{col} \gets SlotVal(\tuple{s_{col},sv_{col}})$\r
+ \State $Dat_{col} \gets Decrypt(SK,sv_{col})$\r
+ \State $id_{col} \gets GetMacId(Dat_{col})$\r
+ \State $\tuple{s_{col},id_{col}} \gets CreateCR(s_{col},id_{col})$\r
+ \State $cr_s \gets \tuple{s_{col},id_{col}}$\r
+\Else\r
+ \State $cr_s \gets \emptyset$\r
+\EndIf\r
+\State $\Call{ProcessSL}{SL_s}$\r
+\State \Return{$cr_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{ReinsertLastSlot}{$need_s,sl_{s_{last}},max'_s$}\r
+\If{$need_s$}\r
+ \State $s_s \gets GetLastS(sl_{s_{last}})$\r
+ \State $sv_s \gets GetSV(sl_{s_{last}})$\r
+ \State $\tuple{stat_s,SL_s} \gets \Call{PutSlot}{s_s,sv_s,max'_s}$\r
+ \State $cr_s \gets \Call{HandleCollision}{\tuple{stat_s,SL_s}}$\r
+\EndIf\r
+\State \Return{$cr_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{GetDEPairs}{$KV_s,max'_s,need_s,sl_s$}\r
\State $DE_{ret} \gets \emptyset$\r
\State $cp_s \gets cp$\r
-\If{$cr_p \neq \emptyset$}\r
+\If{$cr_p \neq \emptyset$}\Comment{Check and insert a $cr$}\r
\State $DE_{ret} \gets DE_{ret} \cup cr_p$\r
\State $cp_s \gets cp_s - 1$\r
\EndIf\r
-\If{$|KV_s| \leq cp$}\Comment{KV set can extend multiple slots based on $cp$}\r
+\If{$cr_{p_{last}} \neq \emptyset$}\Comment{Check and insert a $cr$}\r
+ \State $DE_{ret} \gets DE_{ret} \cup cr_{p_{last}}$\r
+ \State $cp_s \gets cp_s - 1$\r
+\EndIf\r
+\If{$max'_s \neq \emptyset$}\Comment{Check and insert a $qs$}\r
+ \State $qs_s \gets max'_s$\r
+ \State $DE_{ret} \gets DE_{ret} \cup qs_s$\r
+ \State $cp_s \gets cp_s - 1$\r
+\EndIf\r
+\If{$need_s$}\Comment{Check and insert a $ss$}\r
+ \State $id_s \gets GetID(sl_s)$\r
+ \State $s_{s_{last}} \gets GetLastS(sl_s)$\r
+ \State $ss_s \gets CreateSS(id_s,s_{s_{last}})$\r
+ \State $DE_{ret} \gets DE_{ret} \cup ss_s$\r
+ \State $cp_s \gets cp_s - 1$\r
+\EndIf\r
+\If{$|KV_s| \leq cp$}\Comment{$KV$ set can extend multiple slots}\r
\State $DE_{ret} \gets DE_{ret} \cup\r
\{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s\}$\r
\Else\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{PutDataEntries}{$max'_p$}\r
+\Procedure{PutDataEntries}{$th_p,m'_p$}\r
\State $s_p \gets MaxLastSeqN(MS)$\r
-\State $DE_p \gets GetDEPairs(KV)$\r
+\State $max'_p \gets \Call{CheckResize}{MS,th_p,max'_g,m'_p}$\r
+\State $need_p \gets \Call{CheckNeedSS}{MS,max'_g}$\r
+\State $DE_p \gets \Call{GetDEPairs}{KV,max'_p,need_p,sl_{last}}$\r
\State $hmac_{c_p} \gets Hmac(DE_p,SK)$\r
-\State $Dat_p \gets CreateSlot(s_p,id_{self},hmac_{p_p},DE_p,hmac_{c_p})$\r
+\State $Dat_p \gets CreateDat(s_p,id_{self},hmac_{p_p},DE_p,hmac_{c_p})$\r
\State $hmac_{p_p} \gets hmac_{c_p}$\r
\State $sv_p \gets Encrypt(Dat_p,SK)$\r
\State $\tuple{stat_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$\r
-\State $stat_p \gets GetStatus(\tuple{stat_p,SL_p})$\r
-\State $SL_p \gets GetSL(\tuple{stat_p,SL_p})$\r
-\If{$\neg stat_p$}\Comment{Handle collision}\r
- \State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_p,s_p)$\r
- \State $s_{col} \gets SeqN(\tuple{s_{col},sv_{col}})$\r
- \State $sv_{col} \gets SlotVal(\tuple{s_{col},sv_{col}})$\r
- \State $Dat_{col} \gets Decrypt(SK,sv_{col})$\r
- \State $id_{col} \gets GetMacId(Dat_{col})$\r
- \State $\tuple{s_{col},id_{col}} \gets CreateCR(s_{col},id_{col})$\r
- \State $cr_p \gets \tuple{s_{col},id_{col}}$\r
-\Else\r
- \State $cr_p \gets \emptyset$\r
-\EndIf\r
-\State $\Call{ProcessSL}{SL_p}$\r
-\State \Return{$ST$}\r
-\EndFunction\r
+\State $cr_p \gets \Call{HandleCollision}{\tuple{stat_p,SL_p}}$\r
+\State $cr_{p_{last}} \gets \Call{ReinsertLastSlot}{need_p,sl_{last},max'_p}$\r
+\EndProcedure\r
\end{algorithmic}\r
\r
\subsection{Formal Guarantees}\r
projects / iotcloud.git / commitdiff