Secure Multiparty Computation (MPC) refers to a family of cryptographic techniques where mutually untrusting parties may compute functions of their private inputs while revealing only the function output.

It can be hard to program MPCs correctly and efficiently using existing languages and frameworks, especially when they require coordinating disparate computational roles. How can we make this easier?

We present Symphony, a new functional programming language for MPCs among two or more parties. Symphony starts from the single-instruction, multiple-data (SIMD) semantics of prior MPC languages, in which each party carries out symmetric responsibilities, and generalizes it using constructs that can coordinate many parties. Symphony introduces first-class shares and first-class party sets to provide unmatched language-level expressive power with high efficiency.

Developing a core formal language called λ-Symphony, we prove that the intuitive, generalized SIMD view of a program coincides with its actual distributed semantics. Thus the programmer can reason about her programs by reading them from top to bottom, even though in reality the program runs in a coordinated fashion, distributed across many machines. We implemented a prototype interpreter for Symphony leveraging multiple cryptographic backends. With it we wrote a variety of MPC programs, finding that Symphony can express optimized protocols that other languages cannot, and that in general Symphony programs operate efficiently.

In addition to developing the formal proofs, the prototype implementation, and the MPC program case studies, we measured the performance of Symphony’s implementation on several benchmark programs and found it had comparable performance Obliv-C, a state-of-the-art two-party MPC framework for C, when running the same programs. We also measured Symphony’s performance on an optimized secure shuffle protocol based on a coordination pattern that no prior language can express, and found it has far superior performance to the standard alternative.

Programming MPCs is in increasing demand, with a proliferation of languages and frameworks. This work lowers the bar for programmers wanting to write efficient, coordinated MPCs that they can reason about and understand. The work applies to developers and cryptographers wanting to design new applications and protocols, which they are able to do at the language level, above the cryptographic details. The λ-Symphony formalization of Symphony, and the proofs about it, are also surprisingly simple, and can be a basis for follow-on formalization work in MPC and distributed programming. All code and artifacts are available, open-source.