Wys: A DSL for Verified Secure Multi-party Computations. Aseem Rastogi, Nikhil Swamy, and Michael Hicks. In Proceedings of the Symposium on Principles of Security and Trust (POST), April 2019.

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) for writing MPCs. Wys is an embedded DSL hosted in F, a verification-oriented, effectful programming language. Wys source programs are essentially F programs written in a custom MPC effect, meaning that the programmers can use F’s logic to verify the correctness and security properties of their programs. To reason about the distributed runtime 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. 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.

[ .pdf ]

@inproceedings{wysstar18wysstar,
  author = {Aseem Rastogi and Nikhil Swamy and Michael Hicks},
  title = {Wys$^*$: A DSL for Verified Secure Multi-party Computations},
  booktitle = {Proceedings of the Symposium on Principles of Security and Trust (POST)},
  month = apr,
  year = 2019
}

This file was generated by bibtex2html 1.99.