changeset 283:62fdd50b8b41

provsec: added what is basically an English version of Ivan's comment Now I just need to figure out what that kind of proof looks like.
author Sigurd Meldgaard <stm@daimi.au.dk>
date Thu, 18 Mar 2010 13:46:33 +0100
parents 3e3f0a417637
children f040bee9b392
files provsec/paper.tex
diffstat 1 files changed, 44 insertions(+), 34 deletions(-) [+]
line wrap: on
line diff
--- a/provsec/paper.tex	Wed Mar 17 11:46:14 2010 +0100
+++ b/provsec/paper.tex	Thu Mar 18 13:46:33 2010 +0100
@@ -37,7 +37,7 @@
 \section{Introduction}
 This document describes the implementation of PySMCL, a domain specific language for secure
 multiparty computation, embedded in Python. The implementation includes a
-static verifier and a preprocessor for the language, allowing
+static verifier working with an Eclipse plugin and a preprocessor for the language, allowing
 automatic verification of various security properties for
 programs. This work builds on the existing prototype language
 SMCL,  and works on top of the VIFF framework (see D4.3).
@@ -73,7 +73,7 @@
 target language that 
 PySMCL programs will be translated into.
 
-The goal of PySMCL is to allow programmers who are not experts in Cryptography or MPC to specify a desired computation that is 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 party would do, had he been available. 
+The goal of PySMCL is to allow programmers who are not experts in 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 party would do, had he been available. 
 It is then the responsibility of the underlying runtime (in our case VIFF and Python) to make sure the
 computation is done by executing a suitable MPC protocol among the players, without releasing more information than the trusted party would have done.
 
@@ -86,19 +86,19 @@
 high-level MPC primitives to be expressed directly, without considering low-level
 VIFF or MPC  protocol details. 
 
-Eclipse constantly runs the PySMCL preprocessor, which performs static
-analysis of these special sections, tracking the flow of secret values, and
-generating warnings for programmers if information is unintentionally revealed.
-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.
-If the analysis does not find errors, a translated program is output. This is still a syntactically 
-valid Python program that can be executed using the VIFF framework.
+The Eclipse plugin 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.
 
 In order to allow real execution of the program by all players
 concurrently, a configuration file must also be written and supplied
-to the preprocessor. This file specifies where the players will be
+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.
 
@@ -534,29 +534,39 @@
 
 $\pi_P$ works as follows: The players follow the instructions of $P$. When $P$ contains an \verb|input| statement the designated player sends input to the $F$, when the program contains computation on hidden values, the players ask $F$ to do it, and when $P$ contains \verb|output| statements the players ask $F$ to output the target values.
 
-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.).
+Any if-statement with a secret condition will be rewritten, and looping is not allowed with a secret, so the programs will never branch on secret values and the players will never have to disagree, or be uncertain on what to do next.
+
+Now we define a functionality $F_P$, working just as $F$, but it has a new command $P$ that, when called, makes the functionality run the program $P$ --- taking inputs when $P$ would, outputting \emph{only} what is marked as \verb|result| in $P$. At all times $F_P$ will tell the adversary where in the program execution it is.
+
+We now want to show that $pi_P$ with acces to $F$ is implementing $F_P$.
+
+The main thing we need to show, is that any \verb|open| that $pi_P$ will do, can only release information (do an \verb|open|) when there is a way to simulate this output from the information $F_P$ outputs from the $result$ instructions.
+
+Also we need to show that the only parts of $pi_P$ that can \verb|open| information are the ones that are marked by \verb|@ideal_functionality|.
+
+%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.
+%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.
 
 \section{Example: Binary Search in Auctions}
 A known example of secure multi-party computation used in practice is