changeset 11:547e0708702b

Updates to semantics document
author Sigurd Meldgaard <stm@daimi.au.dk>
date Wed, 20 May 2009 13:50:01 +0200
parents d85656eb00e1
children ad18c37411d7
files semantics/pysec.sty semantics/semantics.tex
diffstat 2 files changed, 114 insertions(+), 64 deletions(-) [+]
line wrap: on
line diff
--- a/semantics/pysec.sty	Wed May 20 13:49:04 2009 +0200
+++ b/semantics/pysec.sty	Wed May 20 13:50:01 2009 +0200
@@ -31,9 +31,10 @@
 \newcommand\CLInnerVAR[1]{\mathord{\mathit{#1}}}
 \newcommand\CLInnerSTR[1]{{\tt#1}}
 \newcommand\JOIN{{\ensuremath{\text{JOIN}}}}
-\newcommand\env{{\ensuremath{\text{secret}_s}}}
+\newcommand\env{{\ensuremath{\text{secret-vars}}}}
 \newcommand\SECRET{{\ensuremath{\text{secret}_e}}}
 \newcommand\error{{\ensuremath{\text{error}}}}
+\newcommand\retval{{\ensuremath{\text{retval}}}}
 
 \newcommand\CLInnerMacros{\let\KWD\CLInnerKWD\let\OPR\CLInnerOPR
   \let\TYP\CLInnerTYP\let\VAR\CLInnerVAR\let\STR\CLInnerSTR}
--- a/semantics/semantics.tex	Wed May 20 13:49:04 2009 +0200
+++ b/semantics/semantics.tex	Wed May 20 13:50:01 2009 +0200
@@ -14,7 +14,7 @@
 \date{11. May 2009}
 \begin{document}
 \maketitle
-\section{Language}
+\section{The language}
 \begin{figure}[htbp]
   \begin{center}
 %    \begin{boxeddisp}{.95\linewidth}
@@ -23,33 +23,36 @@
 
      \nt{P} &::=& $\nt{fd}^*$ &\mbox{\rm program}\\
 
-     \nt{fd} &::=&  \KWD{def} \VAR{f}($\VAR{x}^*$): \nt{S} &\mbox{\rm Normal function definition (no analysis)}\\ 
+     \nt{fd} &::=&  \KWD{def} \VAR{f}($\VAR{x}^*$): \nt{S} &\mbox{\rm Normal function definition (no analysis)}\\
             &$\mid$&\KWD{@secret\ def} \VAR{f}($\VAR{x}^*$): \nt{S} &\mbox{\rm Definition of secret function}\\\\
-            &$\mid$&\KWD{@ideal\ def} \VAR{f}($\VAR{x}^*$): \nt{S} &\mbox{\rm Definition of ideal function}\\\\
+%            &$\mid$&\KWD{@ideal\ def} \VAR{f}($\VAR{x}^*$): \nt{S} &\mbox{\rm Definition of ideal function}\\\\
 
      \nt{S} &::=& \VAR{x} := \nt{e} &\mbox{\rm assignment}\\
             &$\mid$& \KWD{if} \nt{e}: \nt{S}$_1$ else \nt{S}$_2$ &\mbox{\rm conditional}\\
             &$\mid$& \KWD{while} \nt{e}: \nt{S} &\mbox{\rm while loop}\\
             &$\mid$& \nt{S}$_1; $\nt{S}$_2$ &\mbox{\rm sequence} \\
             &$\mid$& \KWD{return} \nt{e} &\mbox{\rm return}\\
-            &$\mid$& \KWD{invariant}("\nt{e}") &\mbox{\rm $e$ must always hold at this point of execution (to be proven)}\\ \\
-            &$\mid$& \KWD{result}(\nt{e}) &\mbox{\rm $e$ is declared the result of the ideal functionality}\\ \\
+            &$\mid$& \KWD{invariant}("\nt{e}") &\mbox{\rm $e$ must always hold}\\ & & &\text{at this point of execution (to be proven)}\\
+            &$\mid$& \KWD{precondition}("\nt{e}") &\mbox{\rm $e$ must always hold when $f$ is called}\\
+            &$\mid$& \KWD{postcondition}("\nt{e}") &\mbox{\rm $e$ must always hold when $f$ returns}\\
+            &$\mid$& \KWD{result}(\nt{e}) &\mbox{\rm $e$ is declared the intended result of a computation}\\
 
      \nt{e} &::=& \VAR{x} &\mbox{identifier}\\
             &$\mid$ & \nt{n} &\mbox{number}\\
-            &$\mid$ & \VAR{f}($\nt{e}$) &\mbox{function application}\\
+            &$\mid$ & \VAR{f}($\nt{e}^*$) &\mbox{\rm function application}\\
             &$\mid$& $\nt{e}\circ (\nt{e}_2)$ &\mbox{\rm binary operation, $\circ \in \{+,-,*,<,\leq,=\}$}\\
             &$\mid$& \nt{e}$_1$.get(\nt{e}$_2$) &\mbox{\rm retrieve secret value from party \nt{e}$_1$}\\
-            &$\mid$& \KWD{Secret}(\nt{e}) &\mbox{\rm result of \nt{e} becomes secret}\\
             &$\mid$& \KWD{open}(\nt{e}$_1$) &\mbox{\rm result of \nt{e} is revealed}\\
-            &$\mid$& \KWD{random}() &\mbox{\rm random secret number}\\
+            &$\mid$& \KWD{random-element}() &\mbox{\rm a random secret number}\\
+            &$\mid$& \KWD{random-multiplicative}() &\mbox{\rm a random secret number different from zero}\\
+            &$\mid$& \KWD{random-bit}() &\mbox{\rm a random secret bit (0 or 1)}\\
   \end{tabular}\vspace{1cm}
-\KWD{precondition} and \KWD{postcondition} are synonyms of \KWD{invariant}
 %    \end{boxeddisp}
   \end{center}
   \caption{\label{fig:corepysmcl}Abstract syntax for Core PySMCL}
 \end{figure}
-Let $s(f)$ be a predicate telling if $f$ was defined with $@secret def f(): S$. 
+Let $s(f)$ be a predicate telling if $f$ was defined as a secret
+function with $@\KWD{secret}\ \KWD{def}\ f(): S$.
 \section{Analysis}
 
 A program can be seen as programming a trusted third party (an ideal
@@ -66,17 +69,18 @@
 But sometimes things can be done faster by revealing some intermediate
 values, and we want to ensure that these values does not give the
 adversary any information that he could not compute himself. This is
-done in the UC-framework be exhibiting a \emph{simulator} that from
+shown in the UC-framework by exhibiting a \emph{simulator} that from
 the publicly available information computes values that are
 distributed as the revealed values.
 
 In order to automatically confirm this property we make a static
 analysis of the code, and try to see where a simulator can be inferred
-from the context, and for cases where it can not we generate a proof
-burden for the programmer, he has to write a simulator, and show
-correctness of it (and ideally also running-time).
+from the context, and for cases where it can not be inferred
+automatically we generate a proof burden for the programmer, he has to
+write a simulator, and show correctness of it (and ideally also
+show the running-time).
 
-\subsection{Propagation of secret values}
+\subsection{Propagation of known secret variables}
 We want to know what variables can contain secret values at which
 program points. We represent the program with a control flow graph.
 
@@ -84,9 +88,9 @@
 point is given by the union of variables considered secret at any control flow
 predecessor plus the ones that are assigned a secret value in an assignment.
 \begin{align*}
-&v=x:=e&\env(v) &= 
-\begin{cases}\JOIN(v) \cup {x} &\text{if }\SECRET(e, \JOIN(v))\\
-  \JOIN(v) & \text{otherwise}
+&v=x:=e&\env(v) &=
+\begin{cases}\JOIN(v) \cup \{x\} &\text{if }\SECRET(e, \JOIN(v))\\
+  \JOIN(v) - \{ x \}& \text{otherwise}
 \end{cases}\\
 &v=S & \env(v) &= \JOIN(v)\\
 \end{align*}
@@ -98,7 +102,6 @@
 \begin{align*}
 \SECRET(x, \Gamma)& = x \in \Gamma \\
 \SECRET(e_1 \circ e_2 ,\Gamma)& = \SECRET(e_1, \Gamma) \vee \SECRET(e_2, \Gamma) \\
-\SECRET(x, \Gamma)& = x \in \Gamma \\
 \SECRET(\KWD{open}(e), \Gamma)& = \text{False}\\
 \SECRET(\KWD{random}(), \Gamma)& = \text{True}\\
 \SECRET(\KWD{get}(i), \Gamma)& = \text{True}\\
@@ -106,20 +109,17 @@
 \end{align*}
 
 \subsection{Errors}
-It is an error to eg. make a \KWD{while} condition be a secret
+It is an error to e.g. make a \KWD{while} condition be a secret
 value. Or to call a non-secret function with a secret value.
 
+The error-predicate:
 \begin{align*}
-\error(S_1; S_1)& = \error(S_1, \env(S_1)) \vee \error(S_2, \Gamma)\\
-\error(\KWD{while}(c): S, \Gamma)& = \error(S) \vee \SECRET(c, \env(v)) \vee \error_e(c, \env(v)) \\%XXX
-\begin{cases}
- \text{True} &\text{if $f$ is a secret function}\\
- \text{False} &\text{otherwise}
-\end{cases}\\
-\end{align*}
-And function call of a non-secret function with a secret value is an error:
-\begin{align*}
-\error_e(f(x), \Gamma)& = s(f) \wedge x\in \Gamma\\
+&v = S_1; S_2 &\error(v) = & \error(S_1) \vee \error(S_2)\\
+&v = \KWD{while}(c): S &\error(v) =& \error(S, \JOIN(S)) \\
+                        &&&\vee \SECRET(e,\JOIN(v)) \vee \error(e, \JOIN(v))\\
+&v = x := e & \error(v) = & \error_e(e)\\
+&v = e_1\circ e_2 & \error_e(v, \Gamma) = & \error_e(e_1, Gamma) \vee \error_e(e_2, \Gamma)\\
+&v = f(e) & \error_e(v, \Gamma) = & \error(e, Gamma) \vee (\neg s(f) \wedge \SECRET(e, \Gamma))\\
 \end{align*}
 A function definition $\KWD{@secret}\ \KWD{def}\ f(x): S$ is rejected if \error(S, \{x\}).
 \subsection{Range analysis}
@@ -135,17 +135,31 @@
 Often it is also interesting to do computations with single bits,
 therefore the interval [0; 1] is of certain value.
 
-Therefore we make a range analysis on secret variables.
+Therefore we make a range analysis on each variable at every program
+point. The range of an expression is computed as follows:
 
+\begin{align*}
+&range(e_1+e_2)=(range(e_1)_0 + range(e_2)_0; range(e_1)_1 + range(e_2)_1)\\
+&range(e_1-e_2)=(range(e_1)_0 - range(e_2)_1; range(e_1)_1 - range(e_2)_0)\\
+&range(e_1*e_2)=(range(e_1)_0 * range(e_2)_0; range(e_1)_1 * range(e_2)_1)\\
+&range(e_1==e_2)=(0;1)\\
+&range(e_1\leq e_2)=(0;1)\\
+&range(n)=(n;n)\\
+&range(random())=(0;p-1)\\
+&range(random-bit())=(0;1)\\
+\end{align*}
+
+The range becomes $\bot$ when the endpoints of a range exceeds 0 or
+$p$ respectively, telling that we cannot guarantee anything about the
+number anymore.
 \subsection{Randomness}
 A random secret variable has a value that is unknown to every player,
 but is known to be distributed according to some fixed distribution.
 This can be used to ``screen'' other secret values, by adding or
 multiplying them with the random value before opening.  This can be
 useful for a technique called \emph{random self reduction} where an
-operation is done on an opened screened value, and the result is made
-secret, and the original random value is used for un-screening the
-result.
+operation is done on an opened screened value, and the original (still
+hidden) random value is used for un-screening the result.
 
 When a variable is considered random it means that it is uniformly
 distributed within its interval (from the range analysis) and unknown
@@ -158,11 +172,11 @@
 &\KWD{def}\ \text{random-not-zero}():\\
 &\ \ \ a := random()\\
 &\ \ \ b := random()\\
-&\ \ \ if(open(a*b) == 0):\\
-&\ \ \ \ \ \ return \text{random-not-zero}\\
-&\ \ \ \KWD{invariant}("a!=0 and b!=0")\\
-&\ \ \ return a\\
-&\ \ \ \KWD{postcondition}("\text{return-value}!=0")\\
+&\ \ \ \KWD{if}(open(a*b) == 0):\\
+&\ \ \ \ \ \ \KWD{return}\ \text{random-not-zero}()\\
+&\ \ \ \KWD{invariant}("a\neq 0 \wedge b\neq 0")\\
+&\ \ \ \KWD{return}\ a\\
+&\ \ \ \KWD{postcondition}("\retval\neq0")\\
 \end{align*}
 It is important to track $b$, so that it is not used again (never used
 as parameter to another function, or returned).
@@ -173,28 +187,66 @@
 \begin{align*}
 &\KWD{@secret}\\
 &\KWD{def}\ \text{inverse}(x):\\
-&\ \ \ precondition("x!=0")\\
+&\ \ \ \KWD{precondition}("x\neq 0")\\
 &\ \ \ r := \text{random-not-zero}()\\
 &\ \ \ y := \text{open}(r*x)\\
-&\ \ \ return y * \text{inverse}_{\text{public}}(y)\\
-&\ \ \ \KWD{postcondition}("\text{return-value}*\text{return-value}=1")\\
+&\ \ \ \KWD{return}\ y * \text{inverse}_{\text{public}}(y)\\
+&\ \ \ \KWD{postcondition}("x*\retval=1")\\
 \end{align*}
 
 \subsection{Simulation of openings}
-Random values can always be simulated but only under the assumption
-that it is really unknown to everyone, just generate a number with the
-same distribution.
+Random secret values can always be simulated; just generate a number
+with the same distribution.
+
+But only under the assumption that it is really unknown to everyone.
+
+If an intermediate value is opened, and it is not screened by a random
+value, we have to show that the value can be simulated from the final
+result.
 
-Here we use an array of secret values, and assuming they are sorted,
-we can do a binary search, and leave only 
+In this example an equality predicate between two secret values is
+computed. If the values are equal, their difference times a random
+non-zero value will open to zero, otherwise it will open to a random
+value revealing nothing else.
+\begin{align*}
+&\KWD{@secret}\\
+&\KWD{def}\ \text{open-equals}(x, y):\\
+&\ \ \ r := \text{random-not-zero}()\\
+&\ \ \ c := \text{open}((x-y)*r)\\
+&\ \ \ result(c == 0)\\
+&\ \ \ \KWD{return}\ c == 0\\
+&\ \ \ \KWD{postcondition}("\text{if }x=y\text{ then }\retval=1 \text{ else }\retval=0")\\
+\end{align*}
+The proof burden will be that of exhibiting a function that given the
+value of the predicate ``$c == 0$'' returns a value distributed as
+``(x-y)*r''.
+
+
+In the following example use an array of secret values, and assuming
+they are sorted, we can do a binary search, and open the result of
+every comparison. If the index of the result is going to be opened
+anyway (it is the \KWD{result} of the computation), we can simulate
+these opened values from the result. The proof burden generated will
+require the exhibition of a simulator that can compute the result of $open(xs[mid])$
 \begin{align*}
 &\KWD{@secret}\\
 &\KWD{def}\ \text{binary-search}(xs):\\
-&\ \ \ precondition("x!=0")\\
-&\ \ \ r := \text{random-not-zero}()\\
-&\ \ \ y := \text{open}(r*x)\\
-&\ \ \ return y * \text{inverse}_{\text{public}}(y)\\
-&\ \ \ \KWD{postcondition}("\text{return-value}*\text{return-value}=1")\\
+&\ \ \ \KWD{precondition}("\text{sorted}\ xs")\\
+&\ \ \ \KWD{precondition}("0 \geq xs[0]")\\
+&\ \ \ \KWD{precondition}("xs[len(xs)-1] \geq 0")\\
+&\ \ \ low := 0\\
+&\ \ \ high := len(bids)\\
+&\ \ \ \KWD{while}(low < high):\\
+&\ \ \ \ \ \ \KWD{invariant}("xs[high] >= 0 \wedge 0 >= xs[low]")\\
+&\ \ \ \ \ \ mid := (low + high) // 2\\
+&\ \ \ \ \ \ r := open(xs[mid] \geq 0)\\
+&\ \ \ \ \ \ \KWD{if}\ r:\\
+&\ \ \ \ \ \ \ \ \ high := mid\\
+&\ \ \ \ \ \ \KWD{else}:\\
+&\ \ \ \ \ \ \ \ \ low := mid\\
+&\ \ \ \KWD{result}(mid)\\
+&\ \ \ \KWD{return}\ mid\\
+&\ \ \ \KWD{postcondition}("xs[\retval - 1] < 0 \leq xs[\retval]")\\
 \end{align*}
 
 \subsection{Secret \KWD{if}s}
@@ -205,32 +257,29 @@
    x := e1
 else:
    y := e2
+   y := e3
 \end{verbatim}
 Becomes:
 \begin{verbatim}
 c1 := c
 invariant("c1 = 0 or c1 = 1")
-x := c1 * e1
-y := (1 - c1) * e2
+x := c1 * e1 + (1 - c) * e2
+y := y * c1 + (1 - c1) * e2
 \end{verbatim}
 After this analysis both $x$ and $y$ are now secret values, so the
 whole analysis has to be repeated until we reach a fixed point.
 
+The branches must contain only assignments and nested \KWD{if}
+statements if the rewrite is to make sense.
+
 An alternative to this is to allow \KWD{if} only on non-secret values,
-and have a secret function $\KWD{if}_{secret} defined as$ taking two arguments
+and have a secret function $\KWD{if}_{secret}$ defined as taking two arguments
 \begin{align*}
 &\KWD{@secret}\\
 &\KWD{def}\ \text{if}_{secret}(c,t,e):\\
 &\ \ \ \KWD{precondition}("c\in\{0,1\}")\\
-&\ \ \ \KWD{return} c*t + (1-c)*e\\
+&\ \ \ \KWD{return}\ c*t + (1-c)*e\\
 \end{align*}
 
-\section{Example programs}
-\begin{align*}
-&\KWD{@}\\
-&\KWD{def}\ \text{if}_{secret}(c,t,e):\\
-&\ \ \ \KWD{precondition}("c\in\{0,1\}")\\
-&\ \ \ \KWD{return} c*t + (1-c)*e\\
-\end{align*}
 
 \end{document}
\ No newline at end of file