--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/semantics/semantics.tex	Mon May 18 09:55:37 2009 +0200
@@ -0,0 +1,236 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[utf8]{inputenc}
+% \usepackage[danish]{babel}
+\usepackage[T1]{fontenc}
+\usepackage{graphicx}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{hyperref}
+\usepackage{url}
+\usepackage{pysec}
+
+\title{Semantics of PySMCL}
+\author{Sigurd Meldgaard}
+\date{11. May 2009}
+\begin{document}
+\maketitle
+\section{Language}
+\begin{figure}[htbp]
+  \begin{center}
+%    \begin{boxeddisp}{.95\linewidth}
+  \begin{tabular}{lcll}
+     \VAR{x}&& &identifier\\
+
+     \nt{P} &::=& $\nt{fd}^*$ &\mbox{\rm program}\\
+
+     \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}\\\\
+
+     \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}\\ \\
+
+     \nt{e} &::=& \VAR{x} &\mbox{identifier}\\
+            &$\mid$ & \nt{n} &\mbox{number}\\
+            &$\mid$ & \VAR{f}($\nt{e}$) &\mbox{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}\\
+  \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$. 
+\section{Analysis}
+
+A program can be seen as programming a trusted third party (an ideal
+functionality). This is translated into a program that runs on each
+client and by the means of \emph{secure multiparty computation} (MPC)
+effectuates the same computation as the ideal functionality would have
+done.
+
+We wish to verify that the implementation securely implements the
+functionality in the UC-model. This is guaranteed by the
+implementation of the MPC-protocol, and in principle any computation
+can be done in terms of the basic operations.
+
+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
+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).
+
+\subsection{Propagation of secret values}
+We want to know what variables can contain secret values at which
+program points. We represent the program with a control flow graph.
+
+The set of variables that are considered secret at any given program
+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}
+\end{cases}\\
+&v=S & \env(v) &= \JOIN(v)\\
+\end{align*}
+Where
+\[ \JOIN(v) = \bigcup_{w \in pred(v)}\env(w) \]
+
+An expression is secret in an environment $\Gamma$ if it is a secret
+variable, a call to a secret function or it is an operation on a secret value:
+\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}\\
+\SECRET(f(e), \Gamma)& =s(f)\\
+\end{align*}
+
+\subsection{Errors}
+It is an error to eg. make a \KWD{while} condition be a secret
+value. Or to call a non-secret function with a secret value.
+
+\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\\
+\end{align*}
+A function definition $\KWD{@secret}\ \KWD{def}\ f(x): S$ is rejected if \error(S, \{x\}).
+\subsection{Range analysis}
+Variables hold values that are members of a finite field (typically
+$F_p$ for a large prime $p$).
+
+It is often of concern what the possible values of a secret expression
+is. For example many applications of MPC requires use of integers, but
+the implementation only provides values in a field. For restricted
+cases we can, if we make assumptions on the input, show that the
+computations are equivalent (that no wrap-around occurs)
+
+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.
+
+\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.
+
+When a variable is considered random it means that it is uniformly
+distributed within its interval (from the range analysis) and unknown
+to all players.
+
+Here is an example program generating a random non-zero element of the
+field.
+\begin{align*}
+&\KWD{@secret}\\
+&\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")\\
+\end{align*}
+It is important to track $b$, so that it is not used again (never used
+as parameter to another function, or returned).
+
+Another program computes the multiplicative inverse of a non-zero
+value in the field (assuming inverse$_{\text{public}}$(x) computes the
+inverse of a public value):
+\begin{align*}
+&\KWD{@secret}\\
+&\KWD{def}\ \text{inverse}(x):\\
+&\ \ \ 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")\\
+\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.
+
+Here we use an array of secret values, and assuming they are sorted,
+we can do a binary search, and leave only 
+\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")\\
+\end{align*}
+
+\subsection{Secret \KWD{if}s}
+Any $\KWD{if}$-statement having a secret condition are to be rewritten
+in the following way:
+\begin{verbatim}
+if(c):
+   x := e1
+else:
+   y := e2
+\end{verbatim}
+Becomes:
+\begin{verbatim}
+c1 := c
+invariant("c1 = 0 or c1 = 1")
+x := c1 * e1
+y := (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.
+
+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
+\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\\
+\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