Symphony: Expressive Secure Multiparty Computation with Coordination

Ian Sweet, David Darais, David Heath, William Harris, Ryan Estes, Michael Hicks

Research output: Contribution to journalArticlepeer-review

Abstract

Context 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. Inquiry 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? Approach 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 lan-guages, 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. Knowledge 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 MP programs, finding that Symphony can express optimized protocols that other languages cannot, and that in general Symphony programs operate efficiently. Grounding 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. Importance 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.

Original languageEnglish (US)
Article number14
JournalArt, Science, and Engineering of Programming
Volume7
Issue number3
DOIs
StatePublished - 2023
Externally publishedYes

Keywords

  • coordination
  • distributed programming
  • formal metatheory
  • programming language
  • secure multiparty computation

ASJC Scopus subject areas

  • Software
  • Artificial Intelligence
  • Theoretical Computer Science
  • Computational Theory and Mathematics
  • Modeling and Simulation

Fingerprint

Dive into the research topics of 'Symphony: Expressive Secure Multiparty Computation with Coordination'. Together they form a unique fingerprint.

Cite this