Secure multi-party computation (MPC) allows mutually distrusting
parties to cooperatively compute, using a cryptographic protocol, a
function over their private data.
This 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 ]

@misc{darais20symphony, title = {Symphony: A Concise Language Model for {MPC}}, author = {David Darais and David Heath and Ryan Estes and William Harris and Michael Hicks}, year = 2020, month = jul }

*This file was generated by
bibtex2html 1.99.*