Title: WYS*: A DSL for Verified Secure Multi-party Computations,
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 mixed-mode 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 to extract an interpreter that we have proved
matches this semantics, yielding a partially verified implementation. Wys* is
the first DSL to enable formal verification of MPC programs. We have
implemented several MPC protocols in Wys*, including private set intersection,
joint median, and an MPC card dealing application, and have verified their
correctness and security.