WYS*: A DSL for Verified Secure Multi-party Computations

TL;DR

Wys* is a novel embedded domain-specific language within F* that allows developers to write, verify, and extract secure multi-party computation protocols with formal correctness and security guarantees.

Contribution

It introduces the first DSL for MPC that integrates formal verification, enabling correctness and security proofs directly within the programming environment.

Findings

Successfully implemented and verified protocols like private set intersection and joint median.

Formalized the semantics and proved correctness/security properties of Wys* programs.

Extracted a verified interpreter from Wys* programs using F*'s extraction capabilities.

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.