Mercurial > pysmcl
changeset 329:c3a826ce9a0c
Some corrections, paper is though now moved to an svn repo
author | Sigurd Meldgaard <stm@daimi.au.dk> |
---|---|
date | Mon, 05 Jul 2010 12:55:23 +0200 |
parents | c92e686a49a2 |
children | 8379a9bac9c0 |
files | paper/pysmcl.tex |
diffstat | 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 -eases setting up the run-time and loading the configuration files. +located (e.g., their IP-numbers). A wrapper script is included with +PySMCL that eases setting up the run-time and loading the +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}