Formal verification of secure multi-party computations


August 28, 2015


Aseem Rastogi


Microsoft Research


In secure multi-party computation (SMC), mutually distrusting parties cooperatively compute functions of their private data; in the process, they only learn certain results as per the protocol (e.g., the final output). Applications of SMC include auction, private set intersection, statistical computation, and online games such as poker. Recently we designed a high-level functional programming language, called Wysteria, for writing SMCs. We hypothesized that Wysteria makes it easy to analyze SMC programs, since the language provides an easy-to-understand single-threaded interpretation that corresponds to the actual multi-threaded semantics.

In our current work, we validate that hypothesis and provide a framework for formally verifying the correctness and security properties of SMCs. Specifically, we embed Wysteria in F* (Nikhil Swamy et. al.) by defining a new monad and specifying the Wysteria type system checks as pre- and post-conditions of the API. The embedding enables programmers to use F*’s expressive logic to verify properties of their programs. We also formalize the Wysteria interpreter in F*, and mechanize the proof of simulation theorem that relates the two semantics of Wysteria. Finally we extract the interpreter F* code to OCaml and provide a verified interpreter for running SMCs.


Aseem Rastogi

Aseem Rastogi is a Ph.D. student at the Computer Science dept. of University of Maryland, College Park, advised by Michael Hicks. His research interests broadly span the areas of programming languages, program verification, and security. In particular, his research focuses on designing programming languages, type systems, and other static analyses, that help programmers write provably secure and better performing software.