changeset 318:72bd059a692c

Lots of corrections and improvements
author Sigurd Meldgaard <stm@daimi.au.dk>
date Fri, 16 Apr 2010 11:38:41 +0200
parents e461d9e51c40
children 7c546cb11b58
files provsec/paper.tex
diffstat 1 files changed, 40 insertions(+), 40 deletions(-) [+]
line wrap: on
line diff
--- 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 fix-point 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 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
@@ -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 \verb|cond|=1, and in those suffixed
-\KWD{_else} what they would be if \verb|cond|=0.
+\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
@@ -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 plug-in
 (\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
+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