Mercurial > pysmcl
changeset 6:516288f9b647
semantics/semantics.tex
author | Sigurd Meldgaard <stm@daimi.au.dk> |
---|---|
date | Mon, 18 May 2009 09:55:37 +0200 |
parents | 3917d9bb1e21 |
children | dc2f4211ed1b |
files | semantics/semantics.tex |
diffstat | 1 files changed, 236 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /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