# HG changeset patch
# User Sigurd Meldgaard
# Date 1271410721 7200
# Node ID 72bd059a692cbcb80542ccac16a639a4828c237e
# Parent e461d9e51c40b5ec6afd2b9078beaad394b664a5
Lots of corrections and improvements
diff r e461d9e51c40 r 72bd059a692c provsec/paper.tex
 a/provsec/paper.tex Fri Apr 16 11:03:53 2010 +0200
+++ b/provsec/paper.tex Fri Apr 16 11:38:41 2010 +0200
@@ 167,10 +167,6 @@
Properties of variables, such as whether they are secret or not are
inferred from how they are used in the source code as far as possible,
As a part of the evaluation process planned for the last year of the
project, annotations may be introduced to specify the intentions of
the programmer. The set of annotations will be developed as needed, as
a result of the evaluation process.
As mentioned, the syntax is identical to a subset of Python, but with
a special interpretation of various primitives. To maintain PySMCL as
@@ 263,7 +259,7 @@
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
+Notice that, like in VIFF 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
@@ 451,23 +447,25 @@
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 sketchy in
 the prototype, details are to be filled in during the evaluation
 phase.
+ 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}
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
\cite{nipkow02} , to print out proof burdens that can be proved
formally, and then mechanically checked. We are intending on using the
Simpl framework \cite{schirmer06} to model the 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''.
+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
@@ 501,8 +499,9 @@
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 fixpoint analysis will terminate.
+The range analysis is based on values in a finite lattice (by the use
+of a widening function), so we know that a fixpoint analysis will
+terminate.
The current implementation is doing a simplistic analysis on the
controlflow graph, but it is still useful to use in combination with
@@ 510,9 +509,9 @@
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.

+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
@@ 582,7 +581,7 @@
\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,
+\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:
@@ 595,7 +594,7 @@
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
+ 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.
@@ 613,9 +612,9 @@
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
+Now we have computed in variables suffixed with \KWD{\_then} the value
of variables as they would be if \verbcond=1, and in those suffixed
\KWD{_else} what they would be if \verbcond=0.
+\KWD{\_else} what they would be if \verbcond=0.
Finally we emit statements for obliviously combining the values of the
variables of the two branches. These are one assignment for each
@@ 692,24 +691,23 @@
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
+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$
+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 verifyer will print a proof
+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 (this is implemented in
practice by giving them an extra parameter, the \emph{runtime}, without the
runtime program cannot create or operate on secret values, and so cannot do
harm.
+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}
+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
@@ 727,7 +725,8 @@
In VIFF there exists several different runtimes with different
security and performance characteristics with respect to correctness,
passive/active security, termination etc.
+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
@@ 876,7 +875,8 @@
for example in conjunction with the Pydev plugin
(\url{http://pydev.org/}). It interacts with the analysis framework,
highlights errors, and gives information about inferred values, and
describes rewrites. See figure \ref{screenshot}
+describes rewrites. To get an impression of the kind of feedback the
+plugin provides, see the screen shot in figure \ref{screenshot}
\section{The prototype}
We have implemented a prototype of an analysis framework, and runtime