### changeset 326:011fbd39e4f5

Renamed article
author Sigurd Meldgaard Mon, 28 Jun 2010 11:06:14 +0200 cd2e7b42b05b 255072c0714d paper/pysmcl.tex paper/refs.bib paper/screenshot.png provsec/paper.tex provsec/refs.bib provsec/screenshot.png pysmcl/test/unit/test_flow.py 7 files changed, 997 insertions(+), 991 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/pysmcl.tex	Mon Jun 28 11:06:14 2010 +0200
@@ -0,0 +1,938 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[utf8]{inputenc}
+% \usepackage[danish]{babel}
+\usepackage[T1]{fontenc}
+\usepackage{graphicx}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{hyperref}
+\usepackage{url}
+\usepackage{fullpage}
+%\usepackage[firstpage]{draftwatermark}
+%\SetWatermarkText{\input "|hg parents --template='{node}'"}
+
+\newcommand{\s}{\sigma}
+\newcommand{\NP}{\mathcal{NP}}
+\newcommand{\A}{\mathcal{A}}
+\newcommand{\from}{\leftarrow}
+\newcommand\CLMathsurround{\mathsurround=0.166666em}
+\newcommand\SmallCLMathsurround{\mathsurround=0.083333em}
+\newcommand{\VAR}[1]{{\ensuremath{\mathit{#1}\SmallCLMathsurround}}}
+\newcommand{\nt}[1]{{\it #1}}
+\newcommand\KWD[1]{{\ensuremath{\mathtt{#1}\CLMathsurround}}}
+
+\newenvironment{changemargin}[2]{%
+\begin{list}{}{%
+\setlength{\topsep}{0pt}%
+\setlength{\leftmargin}{#1}%
+\setlength{\rightmargin}{#2}%
+\setlength{\listparindent}{\parindent}%
+\setlength{\itemindent}{\parindent}%
+\setlength{\parsep}{\parskip}%
+}%
+\item[]}{\end{list}}
+
+\newenvironment{Keywords}{%
+\begin{changemargin}{1cm}{1cm}
+\noindent{\bf Keywords:}
+}
+{\end{changemargin} }
+
+
+\title{PySMCL --- An Embedded Language for Specifying Secure Multiparty Computations}
+\author{
+Ivan Damg{\aa}rd (AU)\\
+Thomas Jakobsen (AI)\\
+Sigurd Meldgaard (AU)\\
+Janus Dam Nielsen (AI)\\
+Michael Schwartzbach (AU)\\
+}
+%\author{Anonymized}
+\date{2010}
+\begin{document}
+\maketitle
+\begin{abstract}We present the implementation of an embedded language for specifying secure multiparty computations.
+\begin{Keywords}Secure multiparty computation, Embedded language, Python, Universal Composability
+\end{Keywords}
+
+\end{abstract}
+\section{Introduction}
+This document describes the design and implementation of PySMCL, a
+domain specific 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 builds on the existing prototype language
+SMCL\cite{damnielsen09}, and works on top of the VIFF
+framework\cite{geisler10}.
+
+First we informally describe the concept of multiparty computation,
+and go through 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 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
+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
+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$.
+
+We model this using the Universal Composability (UC) framework of
+Canetti \cite{canetti00}. This means that we specify exactly what
+knowledge we allow to be public (the ideal world), and then verify that
+only information that can be derived directly from this is ever
+made available to an adversary in the real world protocol.
+
+A secure MPC protocol is often implemented by having players exchange
+values that are encrypted or by other means hidden, performing the
+computations on the hidden values, and opening or decrypting
+(outputting) the final secret values to the appropriate players.
+
+VIFF is a framework implementing the primitives for doing MPC, it is
+itself implemented in Python and described in \cite{geisler10}. From
+our point of view, Python together with the VIFF framework is the
+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
+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}
+The programmer will first write his program in PySMCL using the
+Eclipse plug-in, 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 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.
+
+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.
+
+\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.
+
+In order to keep the prototype implementation simple, we leave out
+quite a lot of syntactic constructs from Python, including generators,
+with-constructs, \KWD{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 \KWD{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 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.
+
+\begin{figure}[htbp]
+  \begin{center}
+    %    \begin{boxeddisp}{.95\linewidth}
+    \begin{tabular}{lcll}
+      \VAR{x}& & &identifier\\
+
+      \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}\\
+      &$\mid$& $x$[$e_1$] = $e_2$ &\mbox{\rm array 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{break}\\
+      %%             &$\mid$& \KWD{continue}\\
+
+      \nt{e} &::=& \VAR{x} &\mbox{variable reference}\\
+      &$\mid$& $x$[$e$] &\mbox{\rm array indexing}\\
+      &$\mid$& \nt{f}(\nt{e}) &\mbox{\rm function application}\\
+      &$\mid$ & \nt{n} &\mbox{number}\\
+      &$\mid$ & $e_1\oplus e_2$ &\mbox{binary operator, $\oplus \in \{+,-,*\}$}\\
+      &$\mid$ & $e_1\sim e_2$ &\mbox{comparison, $\sim \in \{==,<,>,<=,>=\}$}\\
+      &$\mid$& \KWD{input}($e_1, e_2, e_3, e_4$) &\rm retrieve secret value identified by $e_1$ from \\
+      & & & party \nt{e}$_2$ in the range from $e_3$ to $e_4$\\
+      %            &$\mid$& \KWD{Secret}(\nt{e}) &\mbox{\rm result of \nt{e} becomes secret}\\
+      &$\mid$& \KWD{output}(\nt{e}) &\mbox{\rm value of \nt{e}$_2$ becomes public for everyone}\\
+      &$\mid$& \KWD{output}(\nt{e}$_1$,\nt{e}$_2$) &\mbox{\rm value of \nt{e}$_2$ becomes public for identity \nt{e}$_1$}\\
+      &$\mid$& \KWD{result}(\nt{e}$_1$,\nt{e}$_2$) &\mbox{\rm value of \nt{e}$_2$ is marked} \\
+        & & & \mbox{ as the result of the computation}\\
+      &$\mid$& \KWD{random}() &\mbox{\rm random secret number}\\
+      &$\mid$& \KWD{random\_bit}() &\mbox{\rm random secret value in \{0,1\}}\\
+      &$\mid$& \KWD{player}() &\mbox{\rm the id of the current player}\\
+      &$\mid$& \KWD{players}() &\mbox{\rm a list with the ids of all players}\\
+      &$\mid$& \KWD{num\_players}() &\mbox{\rm the number of players}\\
+
+    \end{tabular}
+    %    \end{boxeddisp}
+  \end{center}
+  \caption{\label{fig:corepysmcl}Abstract syntax for PySMCL}
+\end{figure}
+
+The abstract syntax of the calculus is a syntactical subset of
+Python. We use some notational shorthands like $\overline{\nt{e}}$
+which means a possibly comma separated list of expressions:
+$\nt{e}_1,\ldots,\nt{e}_n$. It will be clear from the context if
+commas should be present or not. It is presented in
+figure~\ref{fig:corepysmcl}. A core PySMCL program consists of a
+sequence of function declarations. A certain function called
+\KWD{main} is used as the entry point of the computation.
+
+The set of statements and expressions is similar to a standard
+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.
+
+\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.
+
+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).
+
+Notice that, like in VIFF the binary operators
+on secret values work 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 outputting a
+value to a specific player is used, only for that player the function
+returns a value, for other players it will return \KWD{None}.
+
+\section{Implementation strategy}
+We embed PySMCL in Python by using decorators''.  These are higher
+order functions that take a  function as input and return a
+wrapped or otherwise modified version of the function.
+
+\begin{verbatim}
+@ideal_functionality(secrets=["a"], range={"a":(0,1)})
+def negate(a):
+    return 1 - a
+\end{verbatim}
+
+Here the decorator called is \KWD{ideal\_functionality}, a higher
+order function receiving the function \KWD{negate} and returning
+another function that is then also named \KWD{negate}. While deciding
+what output function to return, it may of course choose the values of
+its own arguments (here the values of \KWD{secret} and \KWD{range}).
+
+We use the \KWD{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.
+
+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}.
+
+\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 work.
+
+\begin{verbatim}
+@ideal_functionality(secrets=["a", "b"],
+                     range={"a": (0,10), "b": (-5, 5)})
+def f(a, b, c):
+    print('Computation started')
+    bigger = a > b
+    if bigger:
+        max = a
+    else:
+        max = b
+    if c:
+        max = max + 2
+    open_a = output(a)
+    rand = random()
+    open_b = output(rand + b)
+    return result(output(max))
+\end{verbatim}
+
+The function \KWD{f} above is marked as an ideal functionality, and
+therefore subject to preprocessing and verification.
+
+By using the \KWD{secrets} argument to \KWD{ideal\_functionality}, the
+variables \KWD{a} and \KWD{b} are marked as secret
+
+% 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.
+
+\KWD{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:
+
+\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 \KWD{c} is not
+secret.
+
+\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).
+
+Opening \KWD{max} using the \KWD{result} function is interpreted as
+if this is an intended result of the computation, it is therefore
+allowed to output 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.
+
+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
+control flow graph of:
+
+\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 Range analysis, keeping track of the intervals which we can
+  guarantee variables to be in. This is especially convenient for
+  Boolean values (such as the variable \KWD{bigger} in the above example).
+\end{itemize}
+
+The feedback from the verifier to the programmer is used to alert the
+user that secret information is passed on to a non-verified function,
+is used for control flow or for array indexing. Alerts may also occur at
+places where information is revealed, since this is where security
+problems could occur. When information is revealed, there are two
+possibilities:
+
+\begin{itemize}
+\item The output 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 \KWD{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. This means the programmer
+  claims that the outputted 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 outputted 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 \KWD{output} 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 somewhat sketchy, as
+  generating full formal proof burdens requires a formalization of the
+  entire Python language, and making the proofs might be more work,
+  and require much more expertise than what can be required from our
+  intended user base.
+\end{itemize}
+
+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 \cite{nipkow02} , to print
+out proof burdens that can be proved formally, and then mechanically
+checked. We are intending on using the \KWD{Simpl} framework
+\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''.
+
+\subsection{Functions returning secret values}
+In some applications, the input to a computation is not generated
+on-line, but is collected, say from a set of clients and stored in a
+database in encrypted form until the computation is to be done. This
+is the case, for instance, for some types of auctions. In such an
+application, we would retrieve the input from the database, convert it
+to the representation used in the protocol and then proceed as usual.
+
+To accommodate for this, PySMCL allows to mark a function as one that
+returns secret output.  A function doing the database retrieval and
+format conversion as described above would be a typical of a function
+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. This can
+be seen as a loophole in the system allowing for the creating of new
+primitives.
+
+\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.
+
+The range analysis is based on values in a finite lattice (by the use
+of a widening function), so we know that a fix-point analysis will
+terminate.
+
+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.
+
+For arrays, the analysis describes all values in the array with a
+common range, and thus takes a conservative estimate that all the
+values must fit in.
+
+\section{The preprocessor}
+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 Desugar
+  if-branching'' on a Boolean secret value into a program that
+  calculates both branches secretly.
+\item
+  Rewrite \KWD{output} calls,
+  so they block the computation until the opened value is ready.
+\end{itemize}
+We now give more details on these rewritings:
+
+\subsection{Rewriting of ifs}
+As the executed code path must not depend on the contents of secret
+variables, we cannot do general branching on a secret condition.
+
+But under restricted conditions, we can rewrite it into a straight-line
+program computing both branches and combining the results of each
+branch.
+
+This is done recursively, with the innermost statements first, to
+allow nested \KWD{if}-state\-ments.
+
+As this rewrite often will make even more variables depend on secret values
+we afterwards repeat the analysis and possibly this operation until a
+fixpoint is reached.
+
+For example:
+
+\begin{verbatim}
+    if(x == y):
+        a = b
+    else:
+        if(x > y):
+            a = c
+        else:
+            a = d
+\end{verbatim}
+
+Where \verb|x==y|, and \verb|x>y| are found to be secret, is first
+rewritten into:
+
+\begin{verbatim}
+if(x == y):
+    a = b
+else:
+    a_then0 = c
+    a_else0 = d
+    cond0 = x > y
+    a = a_else0 + (a_then0 - a_else0) * cond0
+\end{verbatim}
+
+And then in a second step to:
+
+\begin{verbatim}
+a_then1 = b
+a_then0 = c
+a_else0 = d
+cond0 = x > y
+a_else1 = a_else0 + (a_then0 - a_else0) * cond0
+cond1 = x == y
+a = a_else1 + (a_then1 - a_else1) * cond1
+\end{verbatim}
+
+Notice that we need to take special care that the temporary variables
+\KWD{a\_then0}, \KWD{cond0} etc.\ are \emph{not}\/ combined in the second step,
+as they will never by used outside the transformed if.
+
+Here follows a description of the algorithm used for the rewrite:
+
+If the condition of an if statement is secret, we go through the statements of each branch in turn and do as follows:
+\begin{enumerate}
+\item If the statement is an assignment, we look up if we have assigned to that specific variable before during the current branch:
+  \begin{enumerate}
+  \item If the assignment was not synthesized during a recursive
+    invocation of the procedure we do not need it outside this branch,
+    and nothing needs to be changes, so we leave it in place.
+  \item Otherwise, if we have not assigned to this variable before; we
+    suffix the assigned variable name with a fresh \KWD{\_thenx} (or
+    \KWD{\_elsex}) and remember this renaming.
+  \item If we have assigned to this variable before in the same branch
+    we reuse the same name as last time.
+  \item All variables on the right-hand side that have been renamed in
+    previous assignments, are updated to their new name.
+  \end{enumerate}
+\item If the statement is an if-statement we rename variables in its
+  condition, and apply the algorithm recursively, so it becomes a list
+  of straight-line assignments, we then continue the rewriting through
+  these. But we only compute branch-specific values for those that are
+  not synthesized.
+\item If the statement is a \KWD{pass} we leave it.
+\item Other statements trigger an error.
+\end{enumerate}
+The updated statements first from the \emph{then}\/ and then from the
+\emph{else}\/ branch are emitted in place of the if statement.
+
+Now we have computed in variables suffixed with \KWD{\_then} the value
+of variables as they would be if \verb|cond|=1, and in those suffixed
+\KWD{\_else} what they would be if \verb|cond|=0.
+
+Finally we emit statements for obliviously combining the values of the
+variables of the two branches. These are one assignment for each
+variable that is assigned to, in at least one of the branches. If it
+occurs only in one branch we use the original name for the variable
+for that branch. Then we combine them as follows:
+
+\verb|a = a_else + (a_then - a_else) * cond|
+
+Because the range-analysis guarantees us that \KWD{cond} is in $\{0,1\}$ this will give the right value of a.
+
+One subtlety is that function calls are made no matter what the
+condition was, this might give counter-intuitive results, because
+side-effects will happen no matter what branch was chosen --- we leave
+this up to the programmer, as we do not have the infrastructure for
+forbidding side-effects, but function-calls are nice to be able to
+make in the branches.
+
+
+%TODO: Maybe it is better to emit an error, and suggest the function call is moved before the assignment?
+\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
+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.
+
+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 outputted value to branch 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.
+
+Therefore, in PySMCL, we rewrite the program, so a call to
+\KWD{output} will block 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.
+\section{Security in the UC model}
+
+One way to think of the runtime is as an ideal functionality $F$ that
+can receive 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.
+
+$\pi_P$ works as follows: The players follow the instructions of
+$P$. When $P$ contains an \KWD{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
+\KWD{output} statements the players ask $F$ to output the target
+values.
+
+Any if-statement with a secret condition will be rewritten, and
+looping is not allowed with a secret condition, 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. The correctness of the
+protocol thus relies on the correctness of the if-rewriting, so the
+computation of $F_P$ is equivalent to that of $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 \KWD{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 access to $F$ is implementing
+$F_P$.
+
+The main property we need to show, is that any \KWD{output} that $\pi_P$
+will do, can only release information (do an \KWD{output}) when there is
+a way to simulate this output from the information $F_P$ outputs from
+the $result$ instructions, as of now the verifier will print a proof
+burden for each \KWD{output} not directly within an \KWD{result} to show
+the consequences of the program.
+
+A function marked \KWD{ideal\_functionality} should not be called from
+functions that are not themselves marked (in practice they can be
+called, but they are given an extra parameter, the \emph{runtime},
+without the runtime program cannot create or operate on secret values,
+and so cannot do harm, only cause the program to fail).
+
+Also we need to show that the only parts of $\pi_P$ that can \KWD{output}
+information are the ones that are marked by
+\KWD{@ideal\_functionality}: Secret information can only be created by
+those functions, and they can only be called from other such
+functions, and they cannot pass the information to non-analyzed
+functions (unless the user specifically asks for an
+exception). Therefore secret information can only be revealed by an
+analyzed function doing an \KWD{output}, and there will be created a
+proof burden to show the relationship between the \KWD{outputted}'ed value and
+the \KWD{result}.
+
+The security of the implemented protocol is now inherited from the
+primitives of the runtime. Because they are proven to be UC-secure and
+disclose no information at all, any composition of them will have the same
+property.
+
+
+Whenever $\pi_P$ outputs information, this information is coming from
+an \KWD{output} statement (because $\pi_P$ is composed of UC-secure
+primitives releasing no information at all).
+
+A simulator for $\pi_P$ with access to $F_P$ works as follows: it runs
+$F_P$, that will output only the information marked as \KWD{result} in
+the program $P$. The simulator records this, and to simulate the
+transcript of $\pi_P$ it uses the algorithm (that was proved to exist
+by the user as a fulfillment of the proof burden) for deriving a value
+indistinguishable from the \KWD{output} from the \KWD{result}.
+
+In VIFF there exists several different runtimes with different
+security and performance characteristics with respect to correctness,
+passive/active security, termination etc. The implemented protocol
+will be as secure as the chosen runtime.
+
+%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.
+
+
+\section{Example: Binary Search in Auctions}
+A known example of secure multi-party computation used in practice is
+for determining the so called market clearing price from the bids of
+a set of buyers and sellers. The bids say, for every potential price,
+how much each party wants to buy
+or sell at a that price.
+In the example, we assume only one seller and one buyer for simplicity.
+In any case, the required computation is, for each possible price,
+to add all bids from buyers
+and subtract all bids from sellers at that price.
+As a result we have, for each price, a number saying how much total demand
+exceeds supply at that price.
+The market clearing price is by definition the price where this difference
+is (as close as possible to) zero.
+
+Because supply can be assumed to increase with increasing price, and demand will decrease,
+we can assume the difference to be monotone, and hence we can find the
+market clearing price
+by doing a binary search. This requires us to output the result of
+the intermediate comparisons, as arrays cannot be indexed by secret
+values. This is however fine, because the result of the computation is
+the intersection point, and a dishonest party getting access to the
+intersection point could easily compute the results of the comparisons
+him- or herself.
+
+A PySMCL program doing such a computation could look as follows:
+\begin{verbatim}
+@ideal_functionality(secrets=['bids'],
+                     range={'bids': (-100, 100)})
+def search(bids):
+    precondition("a >= b <=> bids[a] >= bids[b]")
+    precondition("0 >= bids[0]")
+    precondition("bids[len(bids)-1] >= 0")
+    low = 0
+    high = len(bids)
+    while(low < high):
+        print low, high
+        mid = (low + high) // 2
+        r = output(bids[mid] >= 0)
+        print mid
+        if r:
+            high = mid
+        else:
+            low = mid+1
+    result(mid)
+    return mid
+
+@ideal_functionality()
+def main():
+    bids = [0] * 100
+    for i in range(100):
+        bids1 = input("Buy at price: " + str(i), 1, 0, 100)
+        bids2 = input("Sell at price: " + str(i), 2, 0, 100)
+        bids[i] = bids1 - bids2
+    a = search(bids)
+    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:
+
+\begin{verbatim}
+For the function: search
+  You can assume: a >= b <=> bids[a] >= bids[b]
+  You can assume: 0 >= bids[0]
+  You can assume: bids[len(bids)-1] >= 0
+ Show that you can compute:
+  The value of bids[mid] >= 0 in line 15
+ From:
+  The value of mid in line 21
+For the function: main
+ Nothing has to be proved
+\end{verbatim}
+
+%% \section{The cake example}
+%% Following is a more meaningful example.  Imagine a group of cryptographers
+%% having weekly meetings. At every meeting one of the participants
+%% is supposed to bring a cake.
+
+%% Some people may feel more willing'' to bring a cake a certain day,
+%% and thus we will choose who brings the cake at random among those persons.
+%% But if nobody feels more willing'', then a random person is chosen among
+%% everybody. Of course, the willingness of an individual is strictly
+%% confidential, and no-one should be able to influence the randomness of the choice.
+
+%% Note that the purpose of such a computation could also be more serious, such as selecting
+%% a volunteer among a set of participants for doing a certain task that must be done, but where
+%% we do not want to expose in public people's willingness to volunteer.
+
+%% Below follows  a PySMCL program for this task.
+%% %The identifier \emph{ConfigFile} is assumed to point to a configuration file that contains the actual identities (e.g., IP-numbers)
+%% %of the players in the group called {\emph participants}.
+
+%% \begin{verbatim}
+%% @secure_function
+%% def who_brings_cake():
+%%     participants = Group(ConfigFile)
+%%     willing = []
+%%     for participant in participants:
+%%         willing.append(participant.get("willing"))
+%%     how_many_willing = sum(willing)
+%%     if how_many_willing == 0:
+%%         cake_bringer = choose_random(participants)
+%%     else:
+%%         cake_bringer_nr = rand() % how_many_willing
+%%         count = 0
+%%         for (i, w) in enumerate(willing):
+%%             if w:
+%%                 count += 1
+%%                 if cake_bringer_nr == count:
+%%                     cake_bringer = i
+%%     return openresult(cake_bringer)
+%% \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 plug-in
+(\url{http://pydev.org/}). It interacts with the analysis framework,
+highlights errors, and gives information about inferred values, and
+describes rewrites. To get an impression of the kind of feedback the
+plug-in provides, see the screen shot in figure \ref{screenshot}
+
+\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.
+
+It is publicly available from the Mercurial repository on
+\url{http://hg.viff.dk/pysmcl/}. It can be obtained by running the
+command
+
+\verb|hg clone http://hg.viff.dk/pysmcl/|.
+
+Installation instructions
+is in the \verb|INSTALL| text file.
+
+%\input{core}
+
+%\input references.tex
+
+\section{Conclusion}
+We have described an embedded domain specific language for describing
+secure multiparty computations, and the implementation on top of the
+VIFF runtime.
+
+
+\bibliographystyle{plain} \bibliography{refs}
+
+\begin{figure}
+  \centering
+  \includegraphics[width=1.0\textwidth]{screenshot}
+  \caption{A screen shot of the auction program edited with the Eclipse
+    plug-in. Two boxes with output from the tool are shown.}
+  \label{screenshot}
+\end{figure}
+
+\end{document}
+
+
+% Local Words (en_US): preprocessing multi preprocessor deferreds
+% Local Words (en_US): Composability analyses runtimes
+% Local Words: MPC CACE PySMCL SMCL VIFF
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/refs.bib	Mon Jun 28 11:06:14 2010 +0200
@@ -0,0 +1,52 @@
+@misc{canetti00,
+    author = {Ran Canetti},
+    title = {Universally Composable Security: A New Paradigm for Cryptographic Protocols},
+    howpublished = {Cryptology ePrint Archive, Report 2000/067},
+    year = {2000},
+    note = {\url{http://eprint.iacr.org/2000/067}},
+}
+
+@PhdThesis{geisler10,
+  author =       {Martin Geisler},
+  title =        {Cryptographic Protocols: Theory and Implementation},
+  school =       {Aarhus University},
+  year =         {2010},
+  OPTkey =       {},
+  OPTtype =      {},
+  OPTaddress =   {},
+  OPTmonth =     {February},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+@PhdThesis{damnielsen09,
+  author =       {Janus Dam Nielsen},
+  title =        {Languages for Secure Multiparty Computation and Towards Strongly Typed Macros},
+  school =       {Aarhus University},
+  year =         {2009},
+  OPTkey =       {},
+  OPTtype =      {},
+  OPTaddress =   {},
+  OPTmonth =     {},
+  OPTnote =      {},
+  OPTannote =    {}
+}
+
+
+@Book{nipkow02,
+  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
+  publisher	= {Springer},
+  series	= {LNCS},
+  volume	= 2283,
+  year		= 2002
+}
+
+@PhdThesis{schirmer06,
+  author = 	 {Norbert Schirmer},
+  title = 	 {Verification of Sequential Imperative Programs in {I}sabelle/{HOL}},
+  school = 	 {Technische Universit\"at M\"unchen},
+  year = 	 {2006},
+}
+
+
Binary file paper/screenshot.png has changed
--- a/provsec/paper.tex	Mon Jun 14 11:51:17 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,938 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage[utf8]{inputenc}
-% \usepackage[danish]{babel}
-\usepackage[T1]{fontenc}
-\usepackage{graphicx}
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage{hyperref}
-\usepackage{url}
-\usepackage{fullpage}
-%\usepackage[firstpage]{draftwatermark}
-%\SetWatermarkText{\input "|hg parents --template='{node}'"}
-
-\newcommand{\s}{\sigma}
-\newcommand{\NP}{\mathcal{NP}}
-\newcommand{\A}{\mathcal{A}}
-\newcommand{\from}{\leftarrow}
-\newcommand\CLMathsurround{\mathsurround=0.166666em}
-\newcommand\SmallCLMathsurround{\mathsurround=0.083333em}
-\newcommand{\VAR}[1]{{\ensuremath{\mathit{#1}\SmallCLMathsurround}}}
-\newcommand{\nt}[1]{{\it #1}}
-\newcommand\KWD[1]{{\ensuremath{\mathtt{#1}\CLMathsurround}}}
-
-\newenvironment{changemargin}[2]{%
-\begin{list}{}{%
-\setlength{\topsep}{0pt}%
-\setlength{\leftmargin}{#1}%
-\setlength{\rightmargin}{#2}%
-\setlength{\listparindent}{\parindent}%
-\setlength{\itemindent}{\parindent}%
-\setlength{\parsep}{\parskip}%
-}%
-\item[]}{\end{list}}
-
-\newenvironment{Keywords}{%
-\begin{changemargin}{1cm}{1cm}
-\noindent{\bf Keywords:}
-}
-{\end{changemargin} }
-
-
-\title{PySMCL --- An Embedded Language for Specifying Secure Multiparty Computations}
-\author{
-Ivan Damg{\aa}rd (AU)\\
-Thomas Jakobsen (AI)\\
-Sigurd Meldgaard (AU)\\
-Janus Dam Nielsen (AI)\\
-Michael Schwartzbach (AU)\\
-}
-%\author{Anonymized}
-\date{2010}
-\begin{document}
-\maketitle
-\begin{abstract}We present the implementation of an embedded language for specifying secure multiparty computations.
-\begin{Keywords}Secure multiparty computation, Embedded language, Python, Universal Composability
-\end{Keywords}
-
-\end{abstract}
-\section{Introduction}
-This document describes the design and implementation of PySMCL, a
-domain specific 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 builds on the existing prototype language
-SMCL\cite{damnielsen09}, and works on top of the VIFF
-framework\cite{geisler10}.
-
-First we informally describe the concept of multiparty computation,
-and go through 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 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
-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
-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$.
-
-We model this using the Universal Composability (UC) framework of
-Canetti \cite{canetti00}. This means that we specify exactly what
-knowledge we allow to be public (the ideal world), and then verify that
-only information that can be derived directly from this is ever
-made available to an adversary in the real world protocol.
-
-A secure MPC protocol is often implemented by having players exchange
-values that are encrypted or by other means hidden, performing the
-computations on the hidden values, and opening or decrypting
-(outputting) the final secret values to the appropriate players.
-
-VIFF is a framework implementing the primitives for doing MPC, it is
-itself implemented in Python and described in \cite{geisler10}. From
-our point of view, Python together with the VIFF framework is the
-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
-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}
-The programmer will first write his program in PySMCL using the
-Eclipse plug-in, 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 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.
-
-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.
-
-\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.
-
-In order to keep the prototype implementation simple, we leave out
-quite a lot of syntactic constructs from Python, including generators,
-with-constructs, \KWD{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 \KWD{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 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.
-
-\begin{figure}[htbp]
-  \begin{center}
-    %    \begin{boxeddisp}{.95\linewidth}
-    \begin{tabular}{lcll}
-      \VAR{x}& & &identifier\\
-
-      \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}\\
-      &$\mid$& $x$[$e_1$] = $e_2$ &\mbox{\rm array 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{break}\\
-      %%             &$\mid$& \KWD{continue}\\
-
-      \nt{e} &::=& \VAR{x} &\mbox{variable reference}\\
-      &$\mid$& $x$[$e$] &\mbox{\rm array indexing}\\
-      &$\mid$& \nt{f}(\nt{e}) &\mbox{\rm function application}\\
-      &$\mid$ & \nt{n} &\mbox{number}\\
-      &$\mid$ & $e_1\oplus e_2$ &\mbox{binary operator, $\oplus \in \{+,-,*\}$}\\
-      &$\mid$ & $e_1\sim e_2$ &\mbox{comparison, $\sim \in \{==,<,>,<=,>=\}$}\\
-      &$\mid$& \KWD{input}($e_1, e_2, e_3, e_4$) &\rm retrieve secret value identified by $e_1$ from \\
-      & & & party \nt{e}$_2$ in the range from $e_3$ to $e_4$\\
-      %            &$\mid$& \KWD{Secret}(\nt{e}) &\mbox{\rm result of \nt{e} becomes secret}\\
-      &$\mid$& \KWD{output}(\nt{e}) &\mbox{\rm value of \nt{e}$_2$ becomes public for everyone}\\
-      &$\mid$& \KWD{output}(\nt{e}$_1$,\nt{e}$_2$) &\mbox{\rm value of \nt{e}$_2$ becomes public for identity \nt{e}$_1$}\\
-      &$\mid$& \KWD{result}(\nt{e}$_1$,\nt{e}$_2$) &\mbox{\rm value of \nt{e}$_2$ is marked} \\
-        & & & \mbox{ as the result of the computation}\\
-      &$\mid$& \KWD{random}() &\mbox{\rm random secret number}\\
-      &$\mid$& \KWD{random\_bit}() &\mbox{\rm random secret value in \{0,1\}}\\
-      &$\mid$& \KWD{player}() &\mbox{\rm the id of the current player}\\
-      &$\mid$& \KWD{players}() &\mbox{\rm a list with the ids of all players}\\
-      &$\mid$& \KWD{num\_players}() &\mbox{\rm the number of players}\\
-
-    \end{tabular}
-    %    \end{boxeddisp}
-  \end{center}
-  \caption{\label{fig:corepysmcl}Abstract syntax for PySMCL}
-\end{figure}
-
-The abstract syntax of the calculus is a syntactical subset of
-Python. We use some notational shorthands like $\overline{\nt{e}}$
-which means a possibly comma separated list of expressions:
-$\nt{e}_1,\ldots,\nt{e}_n$. It will be clear from the context if
-commas should be present or not. It is presented in
-figure~\ref{fig:corepysmcl}. A core PySMCL program consists of a
-sequence of function declarations. A certain function called
-\KWD{main} is used as the entry point of the computation.
-
-The set of statements and expressions is similar to a standard
-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.
-
-\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.
-
-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).
-
-Notice that, like in VIFF the binary operators
-on secret values work 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 outputting a
-value to a specific player is used, only for that player the function
-returns a value, for other players it will return \KWD{None}.
-
-\section{Implementation strategy}
-We embed PySMCL in Python by using decorators''.  These are higher
-order functions that take a  function as input and return a
-wrapped or otherwise modified version of the function.
-
-\begin{verbatim}
-@ideal_functionality(secrets=["a"], range={"a":(0,1)})
-def negate(a):
-    return 1 - a
-\end{verbatim}
-
-Here the decorator called is \KWD{ideal\_functionality}, a higher
-order function receiving the function \KWD{negate} and returning
-another function that is then also named \KWD{negate}. While deciding
-what output function to return, it may of course choose the values of
-its own arguments (here the values of \KWD{secret} and \KWD{range}).
-
-We use the \KWD{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.
-
-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}.
-
-\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 work.
-
-\begin{verbatim}
-@ideal_functionality(secrets=["a", "b"],
-                     range={"a": (0,10), "b": (-5, 5)})
-def f(a, b, c):
-    print('Computation started')
-    bigger = a > b
-    if bigger:
-        max = a
-    else:
-        max = b
-    if c:
-        max = max + 2
-    open_a = output(a)
-    rand = random()
-    open_b = output(rand + b)
-    return result(output(max))
-\end{verbatim}
-
-The function \KWD{f} above is marked as an ideal functionality, and
-therefore subject to preprocessing and verification.
-
-By using the \KWD{secrets} argument to \KWD{ideal\_functionality}, the
-variables \KWD{a} and \KWD{b} are marked as secret
-
-% 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.
-
-\KWD{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:
-
-\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 \KWD{c} is not
-secret.
-
-\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).
-
-Opening \KWD{max} using the \KWD{result} function is interpreted as
-if this is an intended result of the computation, it is therefore
-allowed to output 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.
-
-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
-control flow graph of:
-
-\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 Range analysis, keeping track of the intervals which we can
-  guarantee variables to be in. This is especially convenient for
-  Boolean values (such as the variable \KWD{bigger} in the above example).
-\end{itemize}
-
-The feedback from the verifier to the programmer is used to alert the
-user that secret information is passed on to a non-verified function,
-is used for control flow or for array indexing. Alerts may also occur at
-places where information is revealed, since this is where security
-problems could occur. When information is revealed, there are two
-possibilities:
-
-\begin{itemize}
-\item The output 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 \KWD{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. This means the programmer
-  claims that the outputted 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 outputted 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 \KWD{output} 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 somewhat sketchy, as
-  generating full formal proof burdens requires a formalization of the
-  entire Python language, and making the proofs might be more work,
-  and require much more expertise than what can be required from our
-  intended user base.
-\end{itemize}
-
-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 \cite{nipkow02} , to print
-out proof burdens that can be proved formally, and then mechanically
-checked. We are intending on using the \KWD{Simpl} framework
-\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''.
-
-\subsection{Functions returning secret values}
-In some applications, the input to a computation is not generated
-on-line, but is collected, say from a set of clients and stored in a
-database in encrypted form until the computation is to be done. This
-is the case, for instance, for some types of auctions. In such an
-application, we would retrieve the input from the database, convert it
-to the representation used in the protocol and then proceed as usual.
-
-To accommodate for this, PySMCL allows to mark a function as one that
-returns secret output.  A function doing the database retrieval and
-format conversion as described above would be a typical of a function
-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. This can
-be seen as a loophole in the system allowing for the creating of new
-primitives.
-
-\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.
-
-The range analysis is based on values in a finite lattice (by the use
-of a widening function), so we know that a fix-point analysis will
-terminate.
-
-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.
-
-For arrays, the analysis describes all values in the array with a
-common range, and thus takes a conservative estimate that all the
-values must fit in.
-
-\section{The preprocessor}
-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 Desugar
-  if-branching'' on a Boolean secret value into a program that
-  calculates both branches secretly.
-\item
-  Rewrite \KWD{output} calls,
-  so they block the computation until the opened value is ready.
-\end{itemize}
-We now give more details on these rewritings:
-
-\subsection{Rewriting of ifs}
-As the executed code path must not depend on the contents of secret
-variables, we cannot do general branching on a secret condition.
-
-But under restricted conditions, we can rewrite it into a straight-line
-program computing both branches and combining the results of each
-branch.
-
-This is done recursively, with the innermost statements first, to
-allow nested \KWD{if}-state\-ments.
-
-As this rewrite often will make even more variables depend on secret values
-we afterwards repeat the analysis and possibly this operation until a
-fixpoint is reached.
-
-For example:
-
-\begin{verbatim}
-    if(x == y):
-        a = b
-    else:
-        if(x > y):
-            a = c
-        else:
-            a = d
-\end{verbatim}
-
-Where \verb|x==y|, and \verb|x>y| are found to be secret, is first
-rewritten into:
-
-\begin{verbatim}
-if(x == y):
-    a = b
-else:
-    a_then0 = c
-    a_else0 = d
-    cond0 = x > y
-    a = a_else0 + (a_then0 - a_else0) * cond0
-\end{verbatim}
-
-And then in a second step to:
-
-\begin{verbatim}
-a_then1 = b
-a_then0 = c
-a_else0 = d
-cond0 = x > y
-a_else1 = a_else0 + (a_then0 - a_else0) * cond0
-cond1 = x == y
-a = a_else1 + (a_then1 - a_else1) * cond1
-\end{verbatim}
-
-Notice that we need to take special care that the temporary variables
-\KWD{a\_then0}, \KWD{cond0} etc.\ are \emph{not}\/ combined in the second step,
-as they will never by used outside the transformed if.
-
-Here follows a description of the algorithm used for the rewrite:
-
-If the condition of an if statement is secret, we go through the statements of each branch in turn and do as follows:
-\begin{enumerate}
-\item If the statement is an assignment, we look up if we have assigned to that specific variable before during the current branch:
-  \begin{enumerate}
-  \item If the assignment was not synthesized during a recursive
-    invocation of the procedure we do not need it outside this branch,
-    and nothing needs to be changes, so we leave it in place.
-  \item Otherwise, if we have not assigned to this variable before; we
-    suffix the assigned variable name with a fresh \KWD{\_thenx} (or
-    \KWD{\_elsex}) and remember this renaming.
-  \item If we have assigned to this variable before in the same branch
-    we reuse the same name as last time.
-  \item All variables on the right-hand side that have been renamed in
-    previous assignments, are updated to their new name.
-  \end{enumerate}
-\item If the statement is an if-statement we rename variables in its
-  condition, and apply the algorithm recursively, so it becomes a list
-  of straight-line assignments, we then continue the rewriting through
-  these. But we only compute branch-specific values for those that are
-  not synthesized.
-\item If the statement is a \KWD{pass} we leave it.
-\item Other statements trigger an error.
-\end{enumerate}
-The updated statements first from the \emph{then}\/ and then from the
-\emph{else}\/ branch are emitted in place of the if statement.
-
-Now we have computed in variables suffixed with \KWD{\_then} the value
-of variables as they would be if \verb|cond|=1, and in those suffixed
-\KWD{\_else} what they would be if \verb|cond|=0.
-
-Finally we emit statements for obliviously combining the values of the
-variables of the two branches. These are one assignment for each
-variable that is assigned to, in at least one of the branches. If it
-occurs only in one branch we use the original name for the variable
-for that branch. Then we combine them as follows:
-
-\verb|a = a_else + (a_then - a_else) * cond|
-
-Because the range-analysis guarantees us that \KWD{cond} is in $\{0,1\}$ this will give the right value of a.
-
-One subtlety is that function calls are made no matter what the
-condition was, this might give counter-intuitive results, because
-side-effects will happen no matter what branch was chosen --- we leave
-this up to the programmer, as we do not have the infrastructure for
-forbidding side-effects, but function-calls are nice to be able to
-make in the branches.
-
-
-%TODO: Maybe it is better to emit an error, and suggest the function call is moved before the assignment?
-\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
-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.
-
-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 outputted value to branch 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.
-
-Therefore, in PySMCL, we rewrite the program, so a call to
-\KWD{output} will block 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.
-\section{Security in the UC model}
-
-One way to think of the runtime is as an ideal functionality $F$ that
-can receive 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.
-
-$\pi_P$ works as follows: The players follow the instructions of
-$P$. When $P$ contains an \KWD{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
-\KWD{output} statements the players ask $F$ to output the target
-values.
-
-Any if-statement with a secret condition will be rewritten, and
-looping is not allowed with a secret condition, 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. The correctness of the
-protocol thus relies on the correctness of the if-rewriting, so the
-computation of $F_P$ is equivalent to that of $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 \KWD{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 access to $F$ is implementing
-$F_P$.
-
-The main property we need to show, is that any \KWD{output} that $\pi_P$
-will do, can only release information (do an \KWD{output}) when there is
-a way to simulate this output from the information $F_P$ outputs from
-the $result$ instructions, as of now the verifier will print a proof
-burden for each \KWD{output} not directly within an \KWD{result} to show
-the consequences of the program.
-
-A function marked \KWD{ideal\_functionality} should not be called from
-functions that are not themselves marked (in practice they can be
-called, but they are given an extra parameter, the \emph{runtime},
-without the runtime program cannot create or operate on secret values,
-and so cannot do harm, only cause the program to fail).
-
-Also we need to show that the only parts of $\pi_P$ that can \KWD{output}
-information are the ones that are marked by
-\KWD{@ideal\_functionality}: Secret information can only be created by
-those functions, and they can only be called from other such
-functions, and they cannot pass the information to non-analyzed
-functions (unless the user specifically asks for an
-exception). Therefore secret information can only be revealed by an
-analyzed function doing an \KWD{output}, and there will be created a
-proof burden to show the relationship between the \KWD{outputted}'ed value and
-the \KWD{result}.
-
-The security of the implemented protocol is now inherited from the
-primitives of the runtime. Because they are proven to be UC-secure and
-disclose no information at all, any composition of them will have the same
-property.
-
-
-Whenever $\pi_P$ outputs information, this information is coming from
-an \KWD{output} statement (because $\pi_P$ is composed of UC-secure
-primitives releasing no information at all).
-
-A simulator for $\pi_P$ with access to $F_P$ works as follows: it runs
-$F_P$, that will output only the information marked as \KWD{result} in
-the program $P$. The simulator records this, and to simulate the
-transcript of $\pi_P$ it uses the algorithm (that was proved to exist
-by the user as a fulfillment of the proof burden) for deriving a value
-indistinguishable from the \KWD{output} from the \KWD{result}.
-
-In VIFF there exists several different runtimes with different
-security and performance characteristics with respect to correctness,
-passive/active security, termination etc. The implemented protocol
-will be as secure as the chosen runtime.
-
-%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.
-
-
-\section{Example: Binary Search in Auctions}
-A known example of secure multi-party computation used in practice is
-for determining the so called market clearing price from the bids of
-a set of buyers and sellers. The bids say, for every potential price,
-how much each party wants to buy
-or sell at a that price.
-In the example, we assume only one seller and one buyer for simplicity.
-In any case, the required computation is, for each possible price,
-to add all bids from buyers
-and subtract all bids from sellers at that price.
-As a result we have, for each price, a number saying how much total demand
-exceeds supply at that price.
-The market clearing price is by definition the price where this difference
-is (as close as possible to) zero.
-
-Because supply can be assumed to increase with increasing price, and demand will decrease,
-we can assume the difference to be monotone, and hence we can find the
-market clearing price
-by doing a binary search. This requires us to output the result of
-the intermediate comparisons, as arrays cannot be indexed by secret
-values. This is however fine, because the result of the computation is
-the intersection point, and a dishonest party getting access to the
-intersection point could easily compute the results of the comparisons
-him- or herself.
-
-A PySMCL program doing such a computation could look as follows:
-\begin{verbatim}
-@ideal_functionality(secrets=['bids'],
-                     range={'bids': (-100, 100)})
-def search(bids):
-    precondition("a >= b <=> bids[a] >= bids[b]")
-    precondition("0 >= bids[0]")
-    precondition("bids[len(bids)-1] >= 0")
-    low = 0
-    high = len(bids)
-    while(low < high):
-        print low, high
-        mid = (low + high) // 2
-        r = output(bids[mid] >= 0)
-        print mid
-        if r:
-            high = mid
-        else:
-            low = mid+1
-    result(mid)
-    return mid
-
-@ideal_functionality()
-def main():
-    bids = [0] * 100
-    for i in range(100):
-        bids1 = input("Buy at price: " + str(i), 1, 0, 100)
-        bids2 = input("Sell at price: " + str(i), 2, 0, 100)
-        bids[i] = bids1 - bids2
-    a = search(bids)
-    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:
-
-\begin{verbatim}
-For the function: search
-  You can assume: a >= b <=> bids[a] >= bids[b]
-  You can assume: 0 >= bids[0]
-  You can assume: bids[len(bids)-1] >= 0
- Show that you can compute:
-  The value of bids[mid] >= 0 in line 15
- From:
-  The value of mid in line 21
-For the function: main
- Nothing has to be proved
-\end{verbatim}
-
-%% \section{The cake example}
-%% Following is a more meaningful example.  Imagine a group of cryptographers
-%% having weekly meetings. At every meeting one of the participants
-%% is supposed to bring a cake.
-
-%% Some people may feel more willing'' to bring a cake a certain day,
-%% and thus we will choose who brings the cake at random among those persons.
-%% But if nobody feels more willing'', then a random person is chosen among
-%% everybody. Of course, the willingness of an individual is strictly
-%% confidential, and no-one should be able to influence the randomness of the choice.
-
-%% Note that the purpose of such a computation could also be more serious, such as selecting
-%% a volunteer among a set of participants for doing a certain task that must be done, but where
-%% we do not want to expose in public people's willingness to volunteer.
-
-%% Below follows  a PySMCL program for this task.
-%% %The identifier \emph{ConfigFile} is assumed to point to a configuration file that contains the actual identities (e.g., IP-numbers)
-%% %of the players in the group called {\emph participants}.
-
-%% \begin{verbatim}
-%% @secure_function
-%% def who_brings_cake():
-%%     participants = Group(ConfigFile)
-%%     willing = []
-%%     for participant in participants:
-%%         willing.append(participant.get("willing"))
-%%     how_many_willing = sum(willing)
-%%     if how_many_willing == 0:
-%%         cake_bringer = choose_random(participants)
-%%     else:
-%%         cake_bringer_nr = rand() % how_many_willing
-%%         count = 0
-%%         for (i, w) in enumerate(willing):
-%%             if w:
-%%                 count += 1
-%%                 if cake_bringer_nr == count:
-%%                     cake_bringer = i
-%%     return openresult(cake_bringer)
-%% \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 plug-in
-(\url{http://pydev.org/}). It interacts with the analysis framework,
-highlights errors, and gives information about inferred values, and
-describes rewrites. To get an impression of the kind of feedback the
-plug-in provides, see the screen shot in figure \ref{screenshot}
-
-\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.
-
-It is publicly available from the Mercurial repository on
-\url{http://hg.viff.dk/pysmcl/}. It can be obtained by running the
-command
-
-\verb|hg clone http://hg.viff.dk/pysmcl/|.
-
-Installation instructions
-is in the \verb|INSTALL| text file.
-
-%\input{core}
-
-%\input references.tex
-
-\section{Conclusion}
-We have described an embedded domain specific language for describing
-secure multiparty computations, and the implementation on top of the
-VIFF runtime.
-
-
-\bibliographystyle{plain} \bibliography{refs}
-
-\begin{figure}
-  \centering
-  \includegraphics[width=1.0\textwidth]{screenshot}
-  \caption{A screen shot of the auction program edited with the Eclipse
-    plug-in. Two boxes with output from the tool are shown.}
-  \label{screenshot}
-\end{figure}
-
-\end{document}
-
-
-% Local Words (en_US): preprocessing multi preprocessor deferreds
-% Local Words (en_US): Composability analyses runtimes
-% Local Words: MPC CACE PySMCL SMCL VIFF
-
--- a/provsec/refs.bib	Mon Jun 14 11:51:17 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-@misc{canetti00,
-    author = {Ran Canetti},
-    title = {Universally Composable Security: A New Paradigm for Cryptographic Protocols},
-    howpublished = {Cryptology ePrint Archive, Report 2000/067},
-    year = {2000},
-    note = {\url{http://eprint.iacr.org/2000/067}},
-}
-
-@PhdThesis{geisler10,
-  author =       {Martin Geisler},
-  title =        {Cryptographic Protocols: Theory and Implementation},
-  school =       {Aarhus University},
-  year =         {2010},
-  OPTkey =       {},
-  OPTtype =      {},
-  OPTaddress =   {},
-  OPTmonth =     {February},
-  OPTnote =      {},
-  OPTannote =    {}
-}
-
-@PhdThesis{damnielsen09,
-  author =       {Janus Dam Nielsen},
-  title =        {Languages for Secure Multiparty Computation and Towards Strongly Typed Macros},
-  school =       {Aarhus University},
-  year =         {2009},
-  OPTkey =       {},
-  OPTtype =      {},
-  OPTaddress =   {},
-  OPTmonth =     {},
-  OPTnote =      {},
-  OPTannote =    {}
-}
-
-
-@Book{nipkow02,
-  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
-  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
-  publisher	= {Springer},
-  series	= {LNCS},
-  volume	= 2283,
-  year		= 2002
-}
-
-@PhdThesis{schirmer06,
-  author = 	 {Norbert Schirmer},
-  title = 	 {Verification of Sequential Imperative Programs in {I}sabelle/{HOL}},
-  school = 	 {Technische Universit\"at M\"unchen},
-  year = 	 {2006},
-}
-
-
Binary file provsec/screenshot.png has changed
--- a/pysmcl/test/unit/test_flow.py	Mon Jun 14 11:51:17 2010 +0200
+++ b/pysmcl/test/unit/test_flow.py	Mon Jun 28 11:06:14 2010 +0200
@@ -10,6 +10,12 @@

class FlowToDotTest(unittest.TestCase):

+    def assertEquals(self, a, b, msg = None):
+        if not a==b:
+            write_delta(a, b)
+            raise self.failureException, \
+                (msg or '%s != %s' % (b, b))
+
def test_if(self):
p = 7
prog = parse(
@@ -39,7 +45,7 @@
4->5;
}
"""
-        self.assertEquals(result, expected_result)
+        self.assertEquals(result, expected_result, "%s %s" % (result, expected_result))

def test_while(self):
p = 7