Formal verification of secure multi-party computations

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.