Secure multi-party computation (MPC) allows mutually distrusting parties to cooperatively compute, using a cryptographic protocol, a function over their private data. This short paper presents Symphony, an expressive yet concise domain-specific language for expressing MPCs. Symphony starts with the standard, simply-typed λ calculus extended with integers, sums, products, recursive types, and references. It layers on two additional elements: (1) A datatype representing secret shares, which are the basis of multiparty computation, and (2) a simple mechanism called par blocks to express which scopes are to be executed by which parties, and which determine to whom various data values are visible at any given time. The meaning of a Symphony program can be expressed using a single-threaded semantics even though in actuality the program will be run by multiple communicating parties in parallel. Our distributed semantics is expressed naturally as piecewise, single-threaded steps of slices of the program among its parties. We prove that these two semantic interpretations of a program coincide, and we prove a standard type soundness result. To demonstrate Symphony's expressiveness, we have built an interpreter for it (with some extensions) and used it to implement a number of realistic MPC applications, including sorting, statistical and numeric computations, and private information retrieval.

[ .pdf ]

@inproceedings{darais21symphony,
  title = {Symphony: A Concise Language Model for {MPC}},
  booktitle = {Informal Proceedings of the Workshop on Foundations on Computer Secuirty (FCS)},
  author = {Ian Sweet and David Darais and David Heath and Ryan Estes and William Harris and Michael Hicks},
  year = 2021,
  month = jun
}

This file was generated by bibtex2html 1.99.