@inproceedings{rastogi2019wys, author = {Rastogi, Aseem and Swamy, Nikhil and Hicks, Michael}, title = {Wys*: A DSL for Verified Secure Multi-party Computations}, booktitle = {Principles of Security and Trust (POST 2019)}, year = {2019}, month = {April}, abstract = {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.}, url = {http://approjects.co.za/?big=en-us/research/publication/wys-a-dsl-for-verified-secure-multi-party-computations/}, }