### changeset 327:255072c0714d

More paper
author Sigurd Meldgaard Wed, 30 Jun 2010 13:23:39 +0200 011fbd39e4f5 c92e686a49a2 paper/pysmcl.tex 1 files changed, 26 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/paper/pysmcl.tex	Mon Jun 28 11:06:14 2010 +0200
+++ b/paper/pysmcl.tex	Wed Jun 30 13:23:39 2010 +0200
@@ -51,20 +51,22 @@
\date{2010}
\begin{document}
\maketitle
-\begin{abstract}We present the implementation of an embedded language for specifying secure multiparty computations.
+\begin{abstract}We present the implementation of an embedded language
+  for specifying secure multiparty computations. We describe how we
+  analyze programs in order to ensure security, and how we desugar
+  certain language constructs in order to  ease programming.
\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}.
+We describe 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
@@ -126,7 +128,6 @@
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.
@@ -467,6 +468,14 @@
time, this will be necessary to show security, but may have to be left
to be done by hand''.

+An important difference from the work on SMCL is the way we handle the
+information that is released from out'' statements. Where in SMCL an
+out(x)'' statement caused any variable \texttt{x} depends on to be
+considered insecure from the view point of the analysis. Our approach
+as described is to require the user to declare exactly what can
+intentionally be leaked (by using result''), and then inferring that
+it is OK to reveal what is revealed.
+
\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
@@ -742,7 +751,10 @@
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.
+will be as secure as the chosen runtime. At the time of writing VIFF
+has runtimes for both actively and passively corrupted players with
+perfect security based on the GMW87-protocol, and a cryptographic
+runtime with self-trust. %TODO cite properly

%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
@@ -915,8 +927,9 @@

\section{Conclusion}
We have described an embedded domain specific language for describing
-secure multiparty computations, and the implementation on top of the
-VIFF runtime.
+secure multiparty computations, and the analysis we do to ensure
+security of the computation, and the implementation on top of the VIFF
+runtime.

\bibliographystyle{plain} \bibliography{refs}