changeset 284:f040bee9b392

Cut line-size, added dictionary words
author Sigurd Meldgaard <stm@daimi.au.dk>
date Mon, 12 Apr 2010 12:07:11 +0200
parents 62fdd50b8b41
children 78cd2b45c220
files provsec/paper.tex
diffstat 1 files changed, 291 insertions(+), 205 deletions(-) [+]
line wrap: on
line diff
--- a/provsec/paper.tex	Thu Mar 18 13:46:33 2010 +0100
+++ b/provsec/paper.tex	Mon Apr 12 12:07:11 2010 +0200
@@ -35,31 +35,46 @@
 \end{abstract}
 % keywords: multiparty secure embedded language
 \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 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).
+This document describes the implementation of PySMCL, a domain
+specific language for secure multiparty computation, embedded in
+Python. The implementation includes a 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).
 
-First we informally describe the different components of PySMCL,
-and give an example of how it works. Then follows a more detailed description
-of the tool and its implementation.
+First we informally describe the different components of PySMCL, and
+give an example of how it works. Then follows a more detailed
+description of the tool and its implementation.
 
 \section{Concepts}
-Secure multi-party computation (MPC) deals with scenarios where a number of players
-each possess some private data, and we want 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, Procurement, Benchmarking, etc.
-See CACE deliverable D4.1 for details on such applications.
-If a completely trusted party was available, the problem could easily be solved by sending all 
-input to this party and let him compute the result. This is, however, usually an unrealistic 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.
+Secure multi-party computation (MPC) deals with scenarios where a
+number of players each possess some private data, and we want 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, Procurement,
+Benchmarking, etc.  See CACE deliverable D4.1 for details on such
+applications.  If a completely trusted party was available, the
+problem could easily be solved by sending all input to this party and
+let him compute the result. This is, however, usually an unrealistic
+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 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 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$.
 
 A secure MPC protocol is often implemented by having
 players exchange values that are encrypted or by other means hidden,
@@ -68,33 +83,39 @@
 
 VIFF is a framework implementing the primitives for doing MPC
 implemented in Python. For more details about VIFF and MPC in general,
-see CACE deliverables D4.3 and D4.1, respectively.
-From our point of view, Python together with the VIFF framework is the 
-target language that 
-PySMCL programs will be translated into.
+see CACE deliverables D4.3 and D4.1, respectively.  From our point of
+view, Python together with the VIFF framework is the 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 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.
+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.
 
 \section{Usage scenario}
 %TODO: rewrite for eclipse interaction.
-The programmer will first write his program in PySMCL using the Eclipse plugin,
-specifying a desired computation as described above.
-PySMCL is designed to offer high level constructs
-specialized for the MPC domain. Special sections of a PySMCL program will allow
-high-level MPC primitives to be expressed directly, without considering low-level
-VIFF or MPC  protocol details. 
+The programmer will first write his program in PySMCL using the
+Eclipse plugin, specifying a desired computation as described above.
+PySMCL is designed to offer high level constructs specialized for the
+MPC domain. Special sections of a PySMCL program will allow high-level
+MPC primitives to be expressed directly, without considering low-level
+VIFF or MPC protocol details.
 
-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.
+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
@@ -103,26 +124,36 @@
 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 certain security properties 
-can statically be verified. The syntactic subset we consider is defined below.
+The language is syntactically a restrictive subset of Python for which
+certain security properties can statically be verified. The syntactic
+subset we consider is defined below.
 
-In order to keep the prototype implementation simple, we leave out quite a lot of syntactic constructs from Python, including generators, with-constructs, elif, augmented assignments (assignments of the form \verb|x+=1|), delete statements, global statements, try/except and import statements. And focus on a small While-like language. Some of these are easily rewritten into PySMCL (for example \verb|elif| can be written into a nested if) while others complicate the data flow, and are left out for that reason.
+In order to keep the prototype implementation simple, we leave out
+quite a lot of syntactic constructs from Python, including generators,
+with-constructs, elif, augmented assignments (assignments of the form
+\verb|x+=1|), delete statements, global statements, try/except and
+import statements. And focus on a small While-like language. Some of
+these are easily rewritten into PySMCL (for example \verb|elif| can be
+written into a nested if) while others complicate the data flow, and
+are left out for that reason.
 
-Properties of variables, such as whether they are secret or not are inferred from how they are
-used in the source code as far as possible, 
-As a part of the evaluation process planned for the last year of the project, 
-annotations may be introduced
-to specify the intentions of the programmer. The set of annotations will be developed as needed, as a result of the evaluation process.
+Properties of variables, such as whether they are secret or not are
+inferred from how they are used in the source code as far as possible,
+As a part of the evaluation process planned for the last year of the
+project, annotations may be introduced to specify the intentions of
+the programmer. The set of annotations will be developed as needed, as
+a result of the evaluation process.
 
-As mentioned, the syntax is identical to a subset of Python, but with a special 
-interpretation
-of various primitives. To maintain PySMCL as a syntactic subset, 
-annotations are
-specified in the form of dummy function calls.
+As mentioned, the syntax is identical to a subset of Python, but with
+a special interpretation of various primitives. To maintain PySMCL as
+a syntactic subset, annotations are specified in the form of dummy
+function calls.
 
-The commands for doing the secret computations are designed in the same way as
-those in VIFF,  but with a unified interface to the different variants of the runtime. These variants implement different MPC protocols, so the unified interface means the
-programmer does not need to know any details on the protocols that are implemented.
+The commands for doing the secret computations are designed in the
+same way as those in VIFF, but with a unified interface to the
+different variants of the runtime. These variants implement different
+MPC protocols, so the unified interface means the programmer does not
+need to know any details on the protocols that are implemented.
 
 \begin{figure}[htbp]
   \begin{center}
@@ -184,8 +215,9 @@
 while-language augmented with domain-specific operations operating on
 secret values.
 
-In the figure, the intuition/semantics is briefly hinted at in the comments.
-Below, we (informally) describe the semantics in more detail.
+In the figure, the intuition/semantics is briefly hinted at in the
+comments.  Below, we (informally) describe the semantics in more
+detail.
 
 \subsection{Semantics}
 The execution of the program is initiated by evaluating the
@@ -197,19 +229,18 @@
 Secret values can be introduced by \KWD{random}, \KWD{random\_bit} and
 \KWD{input}. Random values are unknown to all players.
 
-Secret values can be operated on with basic integer arithmetic operations
-(division is not included, since VIFF does not yet support this), and 
-comparison predicates. VIFF actually works on a finite subset of the integers
-which means that overflow can occur. A range analysis is done to help prevent
-this (see below for details).
+Secret values can be operated on with basic integer arithmetic
+operations (division is not included, since VIFF does not yet support
+this), and comparison predicates. VIFF actually works on a finite
+subset of the integers which means that overflow can occur. A range
+analysis is done to help prevent this (see below for details).
 
-Notice that, like
-in VIFF (see D4.3 for details) the binary operators on secret values works on deferreds,
-that are waiting for a value (because it will only be defined once
-certain values are received over the
-network). We can still operate on these values, and get new deferreds,
-that wait for the previous results to become ready, before obtaining
-their own value.
+Notice that, like in VIFF (see D4.3 for details) the binary operators
+on secret values works on deferreds, that are waiting for a value
+(because it will only be defined once certain values are received over
+the network). We can still operate on these values, and get new
+deferreds, that wait for the previous results to become ready, before
+obtaining their own value.
 
 A secret value can be revealed by the \KWD{output} function, that
 returns the hidden value of its argument. If the variant opening a
@@ -227,40 +258,43 @@
     return 1 - a
 \end{verbatim}
 
-Here the decorator called is \verb|ideal_functionality|, a higher order
-function receiving the function \verb|negate| and returning another
-function that is then also named \verb|negate|. While deciding what
-output function to return, it may of course the values of its own arguments (here 
-the values of \verb|secret| and \verb|range|).
+Here the decorator called is \verb|ideal_functionality|, a higher
+order function receiving the function \verb|negate| and returning
+another function that is then also named \verb|negate|. While deciding
+what output function to return, it may of course the values of its own
+arguments (here the values of \verb|secret| and \verb|range|).
 
-We use the \verb|inspect| module from Python, so the decorator can get access to the
-source code and thereby the parse tree of the decorated function, and make
-analyses and changes before rewriting it.
+We use the \verb|inspect| module from Python, so the decorator can get
+access to the source code and thereby the parse tree of the decorated
+function, and make analyses and changes before rewriting it.
 
 This is similar to the way macros work in Lisp, although somewhat more
 brittle. But enables us to implement the functionality of PySMCL fully
 in Python, and letting PySMCL programs be valid Python programs.
 
-This means that using PySMCL functionality will not require any extra compilation
-step, as the analysis and preprocessing is done dynamically as the
-file is loaded by the Python interpreter.
+This means that using PySMCL functionality will not require any extra
+compilation step, as the analysis and preprocessing is done
+dynamically as the file is loaded by the Python interpreter.
 
-The decorator we use is called \KWD{@ideal\_functionality}. It
-takes two named arguments, \KWD{secrets} and \KWD{range}, where
+The decorator we use is called \KWD{@ideal\_functionality}. It takes
+two named arguments, \KWD{secrets} and \KWD{range}, where
 \KWD{secrets} is used to point out which of the inputs to the analyzed
 function are to be considered secret and \KWD{range} describes ranges
 in which the inputs are assumed to be.
 
-In addition, you can call a dummy function \KWD{precondition} inside the PySMCL
-code, typically in the beginning of a function to be analyzed. Such a call does not affect the actual computation, but is to be used by the programmer
-to specify assumptions that can be made on the data computed on, via a text-string given as input
-to \KWD{precondition}.
+In addition, you can call a dummy function \KWD{precondition} inside
+the PySMCL code, typically in the beginning of a function to be
+analyzed. Such a call does not affect the actual computation, but is
+to be used by the programmer to specify assumptions that can be made
+on the data computed on, via a text-string given as input to
+\KWD{precondition}.
 
 \section{Example}
 
-In this section we give a toy example demonstrating some of the ideas in PySMCL,
-and informally describe how the preprocessor will handle the code. In the following sections,
-we give a more complete description of the way the verification and preprocessing works.
+In this section we give a toy example demonstrating some of the ideas
+in PySMCL, and informally describe how the preprocessor will handle
+the code. In the following sections, we give a more complete
+description of the way the verification and preprocessing works.
 
 \begin{verbatim}
 @ideal_functionality(secrets=["a", "b"],
@@ -283,48 +317,55 @@
 The function \verb|f| above is marked as an ideal functionality, and
 therefore subject to preprocessing and verification.
 
-The variables \verb|a| and \verb|b| are marked as secret by
-the \verb|secrets| argument to \verb|ideal_functionality|.
+The variables \verb|a| and \verb|b| are marked as secret by the
+\verb|secrets| argument to \verb|ideal_functionality|.
 
-%The variable \verb|c| is marked secret because it is the result of a call to
-%\verb|Secret|. Of course the value 42 is public, since it occurs in the source code,
-%but the meaning in this case is that the plain value 42 is converted to whatever representation
-%the run-time systems internally uses for secret values. 
+% The variable \verb|c| is marked secret because it is the result of a
+% call to \verb|Secret|. Of course the value 42 is public, since it
+% occurs in the source code, but the meaning in this case is that the
+% plain value 42 is converted to whatever representation the run-time
+% systems internally uses for secret values.
 
 Any calls to external Python functions not passing secret values are
-allowed, moreover calls to other verified functions with secret
-values in the right places are also allowed.
+allowed, moreover calls to other verified functions with secret values
+in the right places are also allowed.
 
-\verb|bigger| is a secret value since it is derived from secret values. It can be
-inferred to contain a Boolean value because it is the result of a
-comparison.
+\verb|bigger| is a secret value since it is derived from secret
+values. It can be inferred to contain a Boolean value because it is
+the result of a comparison.
 
-The if-statement on a Boolean value will be rewritten into something equivalent to:
+The if-statement on a Boolean value will be rewritten into something
+equivalent to:
 
 \verb|max=b + (a - b) * bigger|
 
 This rewrite will mean that any side effect executed in one of the
-branches (by e.g.\ calling a function) will get executed no matter what
-the condition evaluates to. This is necessary since otherwise partial information
-on the secret values could be inferred from the observed flow of the program.
-
-The second conditional is not rewritten because \verb|c| is not secret.
+branches (by e.g.\ calling a function) will get executed no matter
+what the condition evaluates to. This is necessary since otherwise
+partial information on the secret values could be inferred from the
+observed flow of the program.
 
-\verb|open_a| is a possible security breach, leaking the value of \verb|a|, and
-therefore generating an error message from the analysis.
+The second conditional is not rewritten because \verb|c| is not
+secret.
 
-Opening \verb|max| using the \verb|result| function is interpreted as if this is an 
-intended result of the computation, it is therefore allowed to open it.
+\verb|open_a| is a possible security breach, leaking the value of
+\verb|a|, and therefore generating an error message from the analysis.
+
+Opening \verb|max| using the \verb|result| function is interpreted as
+if this is an intended result of the computation, it is therefore
+allowed to open it.
 
 
 \section{The verifier}
 \label{sec:verifier}
-In this section we describe more precisely what the verifier does.
-We first recall that anything that the programmer explicitly specifies as the intended result of the 
-computation is considered public, anything else is by default secret.
+In this section we describe more precisely what the verifier does.  We
+first recall that anything that the programmer explicitly specifies as
+the intended result of the computation is considered public, anything
+else is by default secret.
 
-The goal of the analysis is now to ensure that no secret values are unintentionally leaked. 
-However, it is of course considered secure to reveal information that follows from the intended results.
+The goal of the analysis is now to ensure that no secret values are
+unintentionally leaked.  However, it is of course considered secure to
+reveal information that follows from the intended results.
 
 The verifier performs a static conservative approximating analysis
 making a distinction between, and following the data flow through the
@@ -333,9 +374,11 @@
 \begin{itemize}
 \item Secret/public values.
   %\item Input/output values.
-  %\item Unknown random values (for hiding secret values, such as the variable $b$ in the above example).
+  %\item Unknown random values (for hiding secret values, such as the
+  %  variable $b$ in the above example).
 \item Range analysis, at least keeping track of which secret values
-  contain Boolean values (such as the variable $bigger$ in the above example).
+  contain Boolean values (such as the variable $bigger$ in the above
+  example).
 \end{itemize}
 
 The feedback from the verifier to the programmer is used to alert the
@@ -346,36 +389,47 @@
 possibilities:
 
 \begin{itemize}
-\item
-  The opening is marked as intentional, by making use of the construct \verb|result(output(e))|. This should be done
-  when the opened value is a part of the result that the programmer intends the
+\item The opening is marked as intentional, by making use of the
+  construct \verb|result(output(e))|. This should be done when the
+  opened value is a part of the result that the programmer intends the
   program to compute. Such openings are always considered OK.
-  %\item
-  %The opening is done using the \verb|output| function, and the analysis can determine that
-  %the opening is harmless, for instance if the information flow analysis shows that due to
-  %masking with random numbers, the opened value contains no sensitive information.
-  %In this case the verifier will do nothing further. The analysis of random values is not implemented yet, as it is still unclear how the general rules should look.
+  % \item
+  %   The opening is done using the \verb|output| function, and the
+  %   analysis can determine that
+  %   the opening is harmless, for instance if the information flow
+  %   analysis shows that due to
+  %   masking with random numbers, the opened value contains no
+  %   sensitive information.
+  %   In this case the verifier will do nothing further. The analysis
+  %   of random values is not implemented yet, as it is still unclear
+  %   how the general rules should look.
 \item
   The opening is done using the \verb|output| function.
   % but the analysis cannot determine whether
   %the opening is harmless.
-  The analysis interprets this to mean that
-  the programmer claims the opening is harmless. In technical terms,
-  this means the programmer claims that the opened value can be simulated with an indistinguishable
-  distribution, based only on the intended results of the program.
-  More concretely,
-  this can be the case, for instance, if the opened value directly follows
-  from the intended results (but the programmer gets an efficiency improvement from 
-  revealing the value at an earlier stage). 
+  The analysis interprets this to mean that the programmer claims the
+  opening is harmless. In technical terms, this means the programmer
+  claims that the opened value can be simulated with an
+  indistinguishable distribution, based only on the intended results
+  of the program.  More concretely, this can be the case, for
+  instance, if the opened value directly follows from the intended
+  results (but the programmer gets an efficiency improvement from
+  revealing the value at an earlier stage).
 
-  In such a case, the analysis will generate a warning, informing the programmer about the proof burden that has to be carried in order for the opening to be proved secure, and providing as much help as possible towards giving such a proof. This help can include an overview of the intended results and a summary of the information flow analysis. This part of the implementation is still sketchy in the prototype,
-  details are to be filled in during the evaluation phase.
+  In such a case, the analysis will generate a warning, informing the
+  programmer about the proof burden that has to be carried in order
+  for the opening to be proved secure, and providing as much help as
+  possible towards giving such a proof. This help can include an
+  overview of the intended results and a summary of the information
+  flow analysis. This part of the implementation is still sketchy in
+  the prototype, details are to be filled in during the evaluation
+  phase.
 \end{itemize} 
 
-We note that future work may allow us to do even more than what was anticipated
-in the work plan, namely prove openings to be secure
-via an external proof engine. Ultimately we hope that this can allow
-for (semi)automatic proof that the entire program is secure. Work has
+We note that future work may allow us to do even more than what was
+anticipated in the work plan, namely prove openings to be secure via
+an external proof engine. Ultimately we hope that this can allow for
+(semi)automatic proof that the entire program is secure. Work has
 started to incorporate the verifier with the proof assistant Isabelle
 (\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/}), to print out
 proof burdens that can be proved formally, and then mechanically
@@ -383,8 +437,9 @@
 \url{http://afp.sourceforge.net/entries/Simpl.shtml} to model
 imperative programs, and the user has to proof 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''.
+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''.
 
 \subsection{Functions returning secret values}
 In some applications, the input to a computation is not generated
@@ -400,20 +455,21 @@
 that would be marked this way. But no analysis is done on the function
 itself.
 
-Whatever is returned by this function is considered as secret by the program verifier,
-and is assumed to be internally represented in whatever form the underlying protocol uses for secret data.
+Whatever is returned by this function is considered as secret by the
+program verifier, and is assumed to be internally represented in
+whatever form the underlying protocol uses for secret data.
 
 \subsection{Range analysis}
 
 In order to let PySMCL be easy to program for non-experts, we try to
 let the arithmetic operations look like they are done on integers,
-even though they work on finite domains (typically finite
-fields), i.e.,  operations are actually done modulo some (large) number $q$.
-Therefore we do a range analysis on all values, to see if we
-can guarantee the values to act like integers (not wrapping around).
-The analysis outputs a range for each variable in which the values
-of that variable are guaranteed to lie, assuming that the assertions
-on the input data hold true.
+even though they work on finite domains (typically finite fields),
+i.e., operations are actually done modulo some (large) number $q$.
+Therefore we do a range analysis on all values, to see if we can
+guarantee the values to act like integers (not wrapping around).  The
+analysis outputs a range for each variable in which the values of that
+variable are guaranteed to lie, assuming that the assertions on the
+input data hold true.
 
 The range analysis is based on values in a finite lattice, so we know
 that a fix-point analysis will terminate.
@@ -421,18 +477,19 @@
 The current implementation is doing a simplistic analysis on the
 control-flow graph, but it is still useful to use in combination with
 the rewriting of ifs, where we can guarantee that the condition
-evaluates to a Boolean value. It is also useful for ensuring functions are called
-with the correct ranges.
+evaluates to a Boolean value. It is also useful for ensuring functions
+are called with the correct ranges.
 
 For an array, the analysis describes all values in the array with the
 same range.
 
 
 \section{The preprocessor}
-During translation, the preprocessor transforms the PySCML into plain Python-VIFF\@.
-Apart from straightforward syntactic changes, it will:
+During translation, the preprocessor transforms the PySCML into plain
+Python-VIFF\@.  Apart from straightforward syntactic changes, it will:
 \begin{itemize}
-\item translate primitive operations into appropriate function calls in the VIFF framework.
+\item translate primitive operations into appropriate function calls
+  in the VIFF framework.
 \item Desugar 
   ``if-branching'' on a Boolean secret value into a program that
   calculates both branches secretly. 
@@ -453,7 +510,8 @@
 This is done recursively, with the innermost statements first, to
 allow for nested \verb|if|-statements.
 
-As this rewrite often will make more variables depend on secret values we repeat this operation until a fixpoint is reached.
+As this rewrite often will make more variables depend on secret values
+we repeat this operation until a fixpoint is reached.
 
 For example:
 
@@ -504,45 +562,66 @@
 giving new deferreds.
 
 When revealing a secret value in VIFF, we get back a deferred, but
-often we want to output the value, and write an if statement immediately after
-using the opened value to brach on. This cannot be done in plain VIFF
-because we do not know if the value to be opened is ready when we do the
-branching.
-Therefore a common idiom when writing VIFF code is to put the code 
-doing the branch in a callback-function, and attaching that to the deferred.
-This way, the code will not be called before the value is ready.
+often we want to output the value, and write an if statement
+immediately after using the opened value to brach on. This cannot be
+done in plain VIFF because we do not know if the value to be opened is
+ready when we do the branching.  Therefore a common idiom when writing
+VIFF code is to put the code doing the branch in a callback-function,
+and attaching that to the deferred.  This way, the code will not be
+called before the value is ready.
+
+However, this way of structuring the code is quite counter-intuitive
+to a programmer with no experience with deferred values.
 
-However, this way of structuring the code
-is quite counter-intuitive to  a programmer with no experience
-with deferred values. 
+Therefore, in PySMCL, we rewrite the program, so a call to
+\verb|output| will release the control until the value is ready. This
+way, the program can be written and will compute as a straight line
+program.
 
-Therefore,
-in PySMCL, we rewrite the program, so a call to \verb|output| will release
-the control until the value is ready. This way, the program can be
-written and will compute as a straight line program.
-
-The price we pay for this is loss of efficiency in some cases. For example if 
-several values have to
-be output before execution can continue, then it pays off to collect
-them and wait for all of them at the same time. 
-How to approximate this (which cannot be done in the current version) is left for future work.
+The price we pay for this is loss of efficiency in some cases. For
+example if several values have to be output before execution can
+continue, then it pays off to collect them and wait for all of them at
+the same time.  How to approximate this (which cannot be done in the
+current version) is left for future work.
 \section{Security in the UC model}
 
-One way to think of the runtime is as an ideal functionality $F$ that can recieve inputs from the players, evaluate arithmetic circuits on its internal memory and output results. All of this when asked to do it by honest players.
-
-Running a pySMCL program $P$ corresponds to executing the protocol $\pi_P$ in a hybrid model where $F$ is available.
+One way to think of the runtime is as an ideal functionality $F$ that
+can recieve inputs from the players, evaluate arithmetic circuits on
+its internal memory and output results. All of this when asked to do
+it by honest players.
 
-$\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.
+Running a pySMCL program $P$ corresponds to executing the protocol
+$\pi_P$ in a hybrid model where $F$ is available.
 
-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.
+$\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.
 
-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.
+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.
 
-We now want to show that $pi_P$ with acces to $F$ is implementing $F_P$.
+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.
 
-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.
+We now want to show that $pi_P$ with acces to $F$ is implementing
+$F_P$.
 
-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|.
+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
@@ -550,12 +629,13 @@
 %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.
+%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.
@@ -626,9 +706,9 @@
     print "Market clearing price: " + str(a)
 \end{verbatim}
 
-As mentioned, the preconditions are assertions the programmer makes on the input,
-these are not checked, but can be
-used for proving security. The verifier will output to the user a proof burden like:
+As mentioned, the preconditions are assertions the programmer makes on
+the input, these are not checked, but can be used for proving
+security. The verifier will output to the user a proof burden like:
 
 \begin{verbatim}
 For the function: search
@@ -684,7 +764,12 @@
 %% \end{verbatim}
 
 \section{Editor integration}
-Together with the PySMCL prototype has been developed a simple plug-in for the Eclipse platform (\url{http://eclipse.org/}), that can be used for example in conjunction with the Pydev plugin (\url{http://pydev.org/}). It interacts with the analysis framework, highlights errors, and gives information about inferred values, and describes rewrites.
+Together with the PySMCL prototype has been developed a simple plug-in
+for the Eclipse platform (\url{http://eclipse.org/}), that can be used
+for example in conjunction with the Pydev plugin
+(\url{http://pydev.org/}). It interacts with the analysis framework,
+highlights errors, and gives information about inferred values, and
+describes rewrites.
 
 \begin{figure}
   \centering
@@ -696,13 +781,14 @@
 
 
 \section{The prototype}
-We have implemented a prototype of an analysis framework, and run-time environment for
-PySMCL in Python. It builds on top of VIFF. Also
-an Eclipse plug-in communicating with the analysis framework has been made.
+We have implemented a prototype of an analysis framework, and run-time
+environment for PySMCL in Python. It builds on top of VIFF. Also an
+Eclipse plug-in communicating with the analysis framework has been
+made.
 
 It is publicly available from the Mercurial repository on
 \url{http://hg.viff.dk/pysmcl/}. It can be obtained by running the
-command 
+command
 
 \verb|hg clone http://hg.viff.dk/pysmcl/|.
 
@@ -720,6 +806,6 @@
 \end{document}
 
 
-% Local Words (en_US): deferreds
-% Local Words: VIFF
+% Local Words (en_US): preprocessing multi preprocessor deferreds
+% Local Words: MPC CACE PySMCL SMCL VIFF