### changeset 329:c3a826ce9a0c

Some corrections, paper is though now moved to an svn repo
author Sigurd Meldgaard Mon, 05 Jul 2010 12:55:23 +0200 c92e686a49a2 8379a9bac9c0 paper/pysmcl.tex 1 files changed, 49 insertions(+), 64 deletions(-) [+]
line wrap: on
line diff
--- a/paper/pysmcl.tex	Mon Jul 05 12:45:16 2010 +0200
+++ b/paper/pysmcl.tex	Mon Jul 05 12:55:23 2010 +0200
@@ -64,7 +64,7 @@
language for secure multiparty computation, embedded in Python. The
implementation includes a static verifier working with an Eclipse
plug-in and a preprocessor for the language, allowing automatic
-verification of various security properties for programs. This work
+verification of various security properties of programs. This work
builds on the existing prototype language SMCL\cite{damnielsen09}, and
works on top of the VIFF framework\cite{geisler10}.

@@ -75,9 +75,9 @@

\section{Concepts}
Secure multiparty computation (MPC) deals with scenarios where a
-number of players each possesses some private data, and want to compute
-a certain result from these data without revealing anything, except
-for the intended result. There are numerous examples of such
+number of players each possessing some private data, and wanting to
+compute a certain result from these data without revealing anything
+except for the intended result. There are numerous examples of such
scenarios. Examples include elections, auctions, procurements,
benchmarking, etc.  If a completely trusted party was available, the
problem could easily be solved by sending all input to this party and
@@ -85,21 +85,21 @@
assumption.  A secure MPC protocol allows the players to do the
computation securely {\em without}\/ the help of trusted parties. In
other words, a secure protocol creates a situation that is equivalent
-to having a trusted party do the computation, without assuming such a
-party is actually available.
+to having a trusted third party do the computation, without assuming
+such a party is actually available.

-To understand the analysis we plan to do of PySMCL programs, it is
-important to realize that the output of the intended computation of
-course may reveal information on the inputs supplied by the
-parties. But since this was the purpose of doing the computation in
-the first place, this is not a security breach. What we are concerned
-about is whether we reveal {\em more}\/ information than necessary. As
-an example, consider two parties $A,B$ who each have a private natural
-number as input $n_A, n_B$, respectively.  Suppose they want to
-compare $n_A$, $n_B$ securely. This means the output is one bit that
-is 1 if $n_A\geq n_B$ and 0 otherwise. Now, if the result is 1 and
-$n_A=1000$, say, then $A$ knows that $0< n_B\leq 1000$, but $A$ should
-learn nothing further about $n_B$.
+To understand the analysis we do of PySMCL programs, it is important
+to realize that the output of the intended computation of course may
+reveal information on the inputs supplied by the parties. But since
+this was the purpose of doing the computation in the first place, this
+is not a security breach. What we are concerned about is whether we
+reveal {\em more}\/ information than necessary. As an example,
+consider two parties $A,B$ who each have a private natural number as
+input $n_A, n_B$, respectively.  Suppose they want to compare $n_A$,
+$n_B$ securely. This means the output is one bit that is 1 if $n_A\geq +n_B$ and 0 otherwise. Now, if the result is 1 and $n_A=1000$, say,
+then $A$ knows that $0< n_B\leq 1000$, but $A$ should learn nothing
+further about $n_B$.

We model this using the Universal Composability (UC) framework of
Canetti \cite{canetti00}. This means that we specify exactly what
@@ -118,7 +118,7 @@
target language that PySMCL programs will be embedded in.

The goal of PySMCL is to allow programmers who are not experts in
-Cryptography or MPC to specify a desired computation to be executed
+cryptography or MPC to specify a desired computation to be executed
securely, and to specify what data should become known to certain
players at given times. In a nutshell, one can say that a PySMCL
program specifies the computation that the above mentioned trusted
@@ -136,21 +136,23 @@
MPC primitives to be expressed directly, without considering low-level
VIFF or MPC protocol details.

-The Eclipse plug-in will on each file-save run the PySMCL preprocessor,
-which performs static analysis of these special sections, tracking the
-flow of secret values.  If the analysis finds potential security
-problems, it will give feedback to the programmer, possibly with some
-help towards fixing the problem, and/or help towards proving that the
-issue in question is actually not a security problem.  The program can
-be run, upon loading of the program the preprocessing phase is run on
-each secret function. This is now still a syntactically valid Python
-program that can be executed using the VIFF framework.
+The Eclipse plug-in will run the PySMCL preprocessor every time the
+file is saved, which performs static analysis of these special
+sections, tracking the flow of secret values.  If the analysis finds
+potential security problems, it will give feedback to the programmer,
+possibly with some help towards fixing the problem, and/or help
+towards proving that the issue in question is actually not a security
+problem.  The program can be run, upon loading of the program the
+preprocessing phase is run on each secret function. This is now still
+a syntactically valid Python program that can be executed using the
+VIFF framework.

In order to allow real execution of the program by all players
concurrently, a configuration file must also be written and supplied
to the VIFF runtime. This file specifies where the players will be
-located (e.g., their IP-numbers). A wrapper script is included that
+located (e.g., their IP-numbers). A wrapper script is included with
+configuration files.

\section{The language}
The language is syntactically a restrictive subset of Python for which
@@ -189,7 +191,6 @@
\nt{P} &::=& $\overline{\nt{d}}$ &\mbox{\rm program}\\ \\

\nt{d} &::=& \KWD{def} \VAR{f}($\overline{\VAR{x}}$): \nt{S} &\mbox{\rm method definition}\\ \\
-      \\ \\

\nt{S} &::=& pass & \mbox{\rm NOP}\\
&$\mid$ & \VAR{x} = \nt{e} &\mbox{\rm assignment}\\
@@ -245,11 +246,11 @@
detail.

\subsection{Semantics}
-The execution of the program is initiated by evaluating the
-\KWD{main} function. The main function should not return anything,
-but rather print or otherwise communicate the result of the
-computation. The semantics are like those of Python. Local variables
-are introduced by assigning to them first time.
+The execution of the program is initiated by evaluating the \KWD{main}
+function. The main function should not return anything, but rather
+print or otherwise communicate the result of the computation to the
+player. The semantics are like those of Python. Local variables are
+introduced by assigning to them first time.

Secret values can be introduced by \KWD{random}, \KWD{random\_bit} and
\KWD{input}. Random values are unknown to all players.
@@ -376,7 +377,7 @@
\KWD{output(a)} is a possible security breach, leaking the value of
\KWD{a}, and therefore causes the generation of a proof burden from
the analysis that a can be derived from the public values and the
-result. (In this case the burden cannot be proven).
+result. (In this case the burden cannot be fulfilled).

Opening \KWD{max} using the \KWD{result} function is interpreted as
if this is an intended result of the computation, it is therefore
@@ -465,8 +466,8 @@
\cite{schirmer06} to model the imperative programs, and the user has
to prove the existence of a simulating function. Still it is not clear
if this can also include proof that the simulator works in polynomial
-time, this will be necessary to show security, but may have to be left
-to be done by hand''.
+time, this would be necessary to formally show security, but may have
+to be left to be done by hand''.

An important difference from the work on SMCL is the way we handle the
information that is released from out'' statements. Where in SMCL an
@@ -647,7 +648,7 @@
\subsection{Output and Timing of Operations}
We compile PySMCL into VIFF programs. VIFF uses a system of
deferreds'' to give the impression of programming a synchronous
-machine, but doing as much work in parallel as possible (see D4.3 for
+machine, but doing as much work in parallel as possible (see \cite{geisler10} for
details). The result of any computation involving secret shared values
is a deferred, that deferred can be used again in new computations
giving new deferreds.
@@ -756,30 +757,14 @@
perfect security based on the GMW87-protocol, and a cryptographic
runtime with self-trust. %TODO cite properly

-%Givet semantikken af sproget burde det være indlysende hvad
-%protokollen gør: spillerne kører gennem P (i hovedet så et sige), de sender input til F når P indeholder
-%en input kommando, vi beder om de aritmetiske operationer der er i P, og beder F om
-%output når vi kommer til en output komando i P. Mht kontrolflow tror jeg vi skal antage
-%at det der udføreres er programmet som det ser ud efter omskrivning (af if statements f.eks.).
-
-%Dernæst definerer vi en ny funktionalitet F_P som kan alt det F kan,
-% men den har en ny kommando P man kan kalde. Når den udføres, kører
-% funktionaliteten P, den forventer input der hvor P forventer det,
-% *men* den sender kun det output ud der er defineret som result.
-% Derudover holder den undervejs adversary orienteret om hvor den er
-% henne i kontrol flowet.  Dette skal modellere at vi i den virkelige
-% verden ikke kan skjule for fjenden hvor vi er henne i programmet.
-%
-%Ideen skulle så være at vise en sætning der siger at under visse betingelser, så implementerer
-%\pi_P (med adgang til F) funktionaliteten F_P.
-%
-%Betingelserne er vel så at P compiler, at der findes beviser for at alle åbninger der ikke er
-%resultater er OK, og at alle dele af P der gør noget potentielt farligt faktisk er markeret med
-%@ideal_functionality.
-%
-%Bemærkning; hvis vi siger at det F_P gør er at udføre P som det ser ud inden omskrivninger
-%(af if's), så vil beviset automatisk skulle indeholde et bevis for at omskrivningen af if's på
-%hemmelige værdier er OK.
+\begin{figure}[htbp]
+  \centering
+  \includegraphics[width=0.5\linewidth]{uc}
+  \caption{For the computation to be secure, no adversary must be able
+    to distinguish between communicating with the simulator and
+    communicating with the real protocol running on top of the ideal
+    runtime.}
+\end{figure}

\section{Example: Binary Search in Auctions}