### changeset 262:f2610aa01a3d

Removed a lot of overfull hboxes
author Sigurd Meldgaard Tue, 23 Feb 2010 14:30:56 +0100 4df07f0066bf 7b9a5eaf2e88 provsec/paper.tex 1 files changed, 21 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/provsec/paper.tex	Mon Feb 22 15:52:14 2010 +0100
+++ b/provsec/paper.tex	Tue Feb 23 14:30:56 2010 +0100
@@ -105,7 +105,7 @@
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.
+In order to keep the prototype implementation simple, we leave out quite a lot of syntactic constructs from Python, including generators, with-constructs, elif, augmented assignments (assignments of the form \verb|x+=1|), delete statements, global statements, try/except and import statements. And focus on a small While-like language. Some of these are easily rewritten into PySMCL (for example \verb|elif| can be written into a nested if) while others complicate the data flow, and are left out for that reason.

Properties of variables, such as whether they are secret or not are inferred from how they are
used in the source code as far as possible,
@@ -156,7 +156,8 @@
%            &$\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{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}\\
@@ -249,7 +250,7 @@
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
+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}.
@@ -261,7 +262,8 @@
we give a more complete description of the way the verification and preprocessing works.

\begin{verbatim}
-@ideal_functionality(secrets=["a", "b"], range={"a": (0,10), "b": (-5, 5)})
+@ideal_functionality(secrets=["a", "b"],
+                     range={"a": (0,10), "b": (-5, 5)})
def f(a, b, c):
print('Computation started')
bigger = a > b
@@ -281,7 +283,7 @@
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 \verb|secrets| argument to \verb|ideal_functionality|.

%The variable \verb|c| is marked secret because it is the result of a call to
%\verb|Secret|. Of course the value 42 is public, since it occurs in the source code,
@@ -344,7 +346,7 @@

\begin{itemize}
\item
-  The opening is marked as intentional, by using the construct \verb|result(output(e))|. This should be done
+  The opening is marked as intentional, by making use of the construct \verb|result(output(e))|. This should be done
when the opened value is a part of the result that the programmer intends the
program to compute. Such openings are always considered OK.
%\item
@@ -510,8 +512,10 @@
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,
+is quite counter-intuitive to  a programmer with no experience
+with deferred values.
+
+Therefore,
in PySMCL, we rewrite the program, so a call to \verb|output| will release
the control until the value is ready. This way, the program can be
written and will compute as a straight line program.
@@ -651,13 +655,17 @@

\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.
+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
+command
+
+\verb|hg clone http://hg.viff.dk/pysmcl/|.
+
+Installation instructions
is in the \verb|INSTALL| text file.

%\input{core}
@@ -671,5 +679,6 @@
\end{document}

+% Local Words (en_US): deferreds
% Local Words: VIFF