Abstract
In a Secure Multiparty Computation (SMC), mutually distrusting parties
use cryptographic techniques to cooperatively compute over their
private data; in the process each party learns only explicitly
revealed outputs. In this paper, we present WYSTERIA, a high-level
programming language for writing SMCs. As with past languages, like
Fairplay, WYSTERIA compiles secure computations to circuits that are
executed by an underlying engine. Unlike past work, WYSTERIA provides
support for mixed-mode programs, which combine local, private
computations with synchronous SMCs. WYSTERIA complements a standard
feature set with built-in support for secret shares and with wire
bundles, a new abstraction that supports generic n-party
computations. We have formalized WYSTERIA, its refinement type system,
and its operational semantics. We show that WYSTERIA programs have an
easy-to-understand singlethreaded interpretation and prove that this
view corresponds to the actual multi-threaded semantics. We also prove
type soundness, a property we show has security ramifications, namely
that information about one party's data can only be revealed to
another via (agreed upon) secure computations. We have implemented
WYSTERIA, and used it to program a variety of interesting SMC
protocols from the literature, as well as several new ones. We find
that WYSTERIA's performance is competitive with prior approaches while
making programming far easier, and more trustworthy.
Bibtex Entry
@INPROCEEDINGS{rastogi14wysteria,
AUTHOR = {Aseem Rastogi and Matthew A. Hammer and Michael Hicks},
TITLE = {Knowledge Inference for Optimizing Secure Multi-party Computation},
BOOKTITLE = {In Proceedings of the 35th IEEE Symposium on Security and Privacy (Oakland) 2014},
MONTH = MAY,
YEAR = 2014
}
Paper
Implementation