$$\textsc {Wys}^\star $$ : A DSL for Verified Secure Multi-party Computations
Aseem Rastogi, Nikhil Swamy, Michael Hicks · Lecture notes in computer science · 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 $$\textsc {Wys}^\star $$ , a new domain-specific language (DSL) for writing mixed-mode MPCs. $$\textsc {Wys}^\star $$ is an embedded DSL hosted in F $$^\star $$ , a verification-oriented, effectful programming language. $$\textsc {Wys}^\star $$ source programs are essentially F $$^\star $$ programs written in a custom MPC effect, meaning that the programmers can use F $$^\star $$ ’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 $$\textsc {Wys}^\star $$ , also in F $$^\star $$ . We mechanize the necessary metatheory to prove that the properties verified for the $$\textsc {Wys}^\star $$ source programs carry over to the distributed, multi-party semantics. Finally, we use F $$^\star $$ ’s extraction to extract an interpreter that we have proved matches this semantics, yielding a partially verified implementation. $$\textsc {Wys}^\star $$ is the first DSL to enable formal verification of MPC programs. We have implemented several MPC protocols in $$\textsc {Wys}^\star $$ , including private set intersection, joint median, and an MPC-based card dealing application, and have verified their correctness and security.