Secure multi-party computation (MPC) enables a set of mutually distrusting parties to cooperatively compute, using a cryptographic protocol, a function over their private data. This paper presents Wys^*, a new domain-specific language (DSL) implementation for writing MPCs. Wys^* is a Verified, Domain-Specific Integrated Language Extension (VDSILE), a new kind of embedded DSL hosted in F^*, a full-featured, verification-oriented programming language. Wys^* source programs are essentially F^* programs written against an MPC library, meaning that the programmers can use F^*'s logic to verify the correctness and security properties of their programs. To reason about the distributed semantics of these programs, we formalize a deep embedding of Wys^*, also in F^*. We mechanize the necessary metatheory to prove that the properties verified for the Wys^* source programs carry over to the distributed, multi-party semantics. Finally, we use F^*'s extraction mechanism to extract an interpreter that we have proved matches this semantics, yielding a verified implementation. Indeed, Wys^* is the first DSL to enable formal verification of source MPC programs, and also the first MPC DSL to provide a verified implementation. With Wys^* we have implemented several MPC protocols, including private set intersection, joint median, and an MPC-based card dealing application, and have verified their security and correctness.

[ arXiv | http ]

@techreport{rastogi16wysstar,
  author = {Aseem Rastogi and Nikhil Swamy and Michael Hicks},
  title = {Wys$^*$: A Verified Language Extension for Secure Multi-Party Computations},
  institution = {CoRR},
  number = {abs/1711.06467},
  year = {2017},
  archiveprefix = {arXiv},
  eprint = {1711.06467},
  month = nov
}

This file was generated by bibtex2html 1.99.