changeset 258:d0e2cf70ef28

Started a paper for provsec, just a copy of the cace-work made to compile in a std. latex form
author Sigurd Meldgaard <>
date Tue, 16 Feb 2010 11:09:00 +0100
parents 2ec1672bb6be
children 9e3792abc90f
files provsec/paper.tex
diffstat 1 files changed, 682 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/provsec/paper.tex	Tue Feb 16 11:09:00 2010 +0100
@@ -0,0 +1,682 @@
+% \usepackage[danish]{babel}
+\SetWatermarkText{\input "|hg parents --template='{node}'"}
+\newcommand{\nt}[1]{{\it #1}}
+\title{PySCML --- An Embedded Language for Specifying Secure Multiparty Computations}
+Sigurd Meldgaard (AU)\\
+Ivan Damg{\aa}rd (AU)\\
+Thomas Jakobsen (AI)\\
+Janus Dam Nielsen (AI)\\
+Michael Schwartzbach (AU)\\
+This document describes the implementation of PySMCL, a domain specific language for secure
+multiparty computation, embedded in Python. The implementation includes a
+static verifier and a preprocessor for the language, allowing
+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).
+To avoid confusion, we have kept the original title of this deliverable (Compilers/Interpreters)
+although the tool implementing the language is  perhaps better described as a preprocessor. Part of what the preprocessor does is nevertheless similar to a compiler in that it translates PySMCL code into Python code that can be executed by the VIFF 
+framework which serves as a  ``virtual machine'' in the project. It therefore provides exactly the functionality that was intended in the workplan.
+The PySMCL language was already specified in D4.2. However, subsequent work has shown 
+that it was appropriate to revise the syntax in several ways. This document therefore contains a revised specification which replaces the old version, and the intention is for this document to also be a 
+self-contained description of PySMCL.
+This document also serves as documentation showing that the project has successfully passed
+milestone M4.6: Compilers/interpreters, Implementation of appropriate compilers and interpreters completed.
+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.
+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$.
+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 the final secret values to the appropriate players.
+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.
+The goal of PySMCL is to allow programmers who are not experts in Cryptography or MPC to specify a desired computation that is to be executed securely, and to specify what data should become known to certain players at given times. In a nutshell, one can say that a PySMCL program specifies the computation that the above mentioned trusted party would do, had he been available. 
+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 
+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. 
+One then runs the PySMCL preprocessor, which  will perform static
+analysis of these special sections, tracking the flow of secret values, and
+generating warnings for programmers if information is unintentionally revealed.
+If the analysis finds potential security problems, 
+it will give feedback to the programmer, possibly with some
+help towards fixing the problem, and/or help towards proving that the issue in question is actually not a
+security problem.
+If the analysis does not find errors, a translated program is output. This is still a syntactically 
+valid Python program that can be executed using the VIFF framework.
+In order to allow real execution of the program by all players
+concurrently, a configuration file must also be written and supplied
+to the preprocessor. This file specifies where the players will be
+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, and focused around a small While-like language, 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. 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.
+As mentioned, the syntax is identical to a subset of Python, but with a special 
+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{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 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}
+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
+\verb|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.
+The execution of the program is initiated by evaluating the
+\verb|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 (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
+value to a specific player is used, only for that player the function
+returns a value, for other players it will return \verb|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.
+@ideal_functionality(secrets=["a"], range={"a":(0,1)})
+def negate(a):
+    return 1 - a
+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.
+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, a dummy function \KWD{precondition} can be called inside 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 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.
+@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))
+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 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. 
+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.
+\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
+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.
+\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}
+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:
+\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, at least keeping track of which secret values
+  contain Boolean values (such as the variable $bigger$ in the above example).
+The feedback from the verifier to the programmer is used to alert the
+user, if 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
+  The opening is marked as intentional, by using 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.
+  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). 
+  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.
+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{}), to print out
+proof burdens that can be proved formally, and then mechanically
+checked. We are using the Simpl framework
+\url{} 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''.
+\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
+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.
+The range analysis is based on values in a finite lattice, 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 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:
+\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. 
+  Rewrite output statements,
+  so they block the computation until the opened value is ready.
+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
+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.
+For example:
+    if(x == y):
+        a = b
+    else:
+        if(x > y):
+            a = c
+        else:
+            a = d
+Where \verb|x==y|, and \verb|x>y| are found to be secret, is first
+rewritten into:
+if(x == y):
+    a = b
+    a_then0 = c
+    a_else0 = d
+    cond0 = x > y
+    a = a_else0 + (a_then0 - a_else0) * cond0
+And then in a second step to:
+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
+Notice that we need to take special care that the temporary variables
+\verb|a_then0|, \verb|cond0| etc. are not combined in the second step,
+as they will never by used outside the transformed if.
+\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 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
+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 counterintuitive 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.
+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{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, these values can be assumed to be monotonic.
+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 open 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:
+                     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
+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)
+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:
+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
+%% \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{}), that can be used for example in conjunction with the Pydev plugin (\url{}). It interacts with the analysis framework, highlights errors, and gives information about inferred values, and describes rewrites.
+  \centering
+  \includegraphics[width=1.0\textwidth]{screenshot}
+  \caption{A screenshot of the auction program edited with the Eclipse
+    plugin. Two boxes with output from the tool are shown.}
+\section{The prototype}
+A prototype of an analysis framework, and run-time environment for
+PySMCL has been implemented in Python. It builds on top of VIFF. Also
+an Eclipse plug-in communicating with the analysis is made.
+It is publicly available from the Mercurial repository on
+\url{}. It can be obtained by running the
+command \verb|hg clone|. Installation instructions
+is in the \verb|INSTALL| text file.
+%\input references.tex