Wysteria: A Programming Language for Generic, Mixed-mode Multiparty Computation

People

Wysteria is being designed and developed in Programming Languages group at University of Maryland, College Park (PLUM).

• Aseem Rastogi (Graduate Student, www.cs.umd.edu/~aseem)

• Matthew Hammer (Postdoctoral Researcher, http://www.cs.umd.edu/~hammer/)

• Michael Hicks (Faculty, www.cs.umd.edu/~mwh)

Papers, Talks, and Code

Paper (IEEE Security and Privacy (Oakland) 2014)

Technical Report (Contains complete formal definitions and proofs)

Conference talk

Talk (Crypto reading group)

Talk (Guest lecture in CMSC631)

Code

What is Secure Multiparty Computation?

Secure Multiparty Computation (SMC) enables mutually distrusting parties to cooperatively compute over their private data, while only revealing the final output to each party. As a classical example, two millionaires can use SMC to find out who is richer, without revealing their wealth to each other. In essence, an SMC is analogous to two parties sending their inputs to a trusted third party, who performs the computation and returns the result, but in fact requires no trusted third party. Some practical uses of SMC include auctions (a real example: Secure Multiparty Computation Goes Live), online games (e.g. card games), targeted advertising, etc.

General-purpose SMCs are typically implemented using cryptographic protocols that involve converting the function to be computed into a boolean or arithmetic circuit such that the parties cooperate to obliviously execute the circuit.

What is Wysteria?

Wysteria is a high-level functional programming language for writing mixed-mode secure computations. Such computations interleave local, private computations with secure multiparty computations. Wysteria aims to make such computations easy to write, understand, and reuse. As such it provides several novel features such as support for a generic number of parties, high-level support for secure state, support for sub-computations that involve only a subset of parties, and more. Wysteria has two formal semantics: the first models mixed-mode computations as being run synchronously by all parties, as if within a single thread, while the second more faithfully models local computations as happening independently; we prove that semantics always produce the same result, so the simpler, single-threaded view is sufficient. Wysteria also has a type system that we have proved is sound.

Wysteria is implemented as an interpreter that runs at each party. As it runs, it dynamically compiles the secure computation fragments in a program into boolean circuits, and runs them using an implementation of the GMW protocol. Using Wysteria, we have implemented several examples from existing SMC literature (median, private set intersection, auction, nearest neighbor, etc.), and several new ones (two-round bidding using secure state, secure card dealing, etc.).

The implementation can be downloaded from here: https://bitbucket.org/aseemr/wysteria.

Examples

Let's take a simple example to introduce Wysteria. (The following discussion mirrors that in section 2 of our paper.) Say Alice and Bob want to compare their wealth. Wysteria function for this looks like (Please note that code listings here are just for illustration purposes, and may not work verbatim. For working examples, see the src/examples/ directory in the source code.):

#!ocaml
(*
 * define a function richer (read \w as lambda-w, i.e. introduction of a lambda binding)
 * in Wysteria, principal names start from ! (just a parsing convenience)
 * type of w is W {!Alice, !Bob} nat (explained below)
 *)
let richer = \w:W {!Alice, !Bob} nat .
             let b @ sec({!Alice, !Bob}) =
                 if w[!Alice] > w[!Bob] then
                     true
                 else
                     false
             in
             b

Let's look at Wysteria concepts one-by-one. First, the annotation @ sec({!Alice, !Bob}) says that the code that follows in the let-in scope needs to be run securely, i.e. at run time this computation would be compile to boolean circuits and run using SMC.

Wysteria has a novel feature called Wire Bundles (represented by type W). Wire bundles can be coarsely thought of as maps from parties to values. Wire bundles are dependently typed. A wire bundle type W {!Alice, !Bob} nat denotes a wire bundle that holds a nat each for Alice and Bob.

The function body then projects Alice's and Bob's values from w, and compares them.

The function richer can be called as follows:

#!ocaml

(*
 * say x is Alice's variable, and y is Bob's
 * wire is a keyword in Wysteria, that creates a wire bundle
 * ++ concatenates two wire bundles
 *)
let w = (wire !Alice:x) ++ (wire !Bob:y)
richer w

The code first creates a wire bundle for Alice, then a wire bundle for Bob, concatenates them, and then calls the richer function. It should be noted that wire bundles just provide an abstraction. In the implementation, Alice and Bob only see their own components of the wire bundle. However, the abstraction ensures that the programs can be written as a single specification, rather than a separate program for each party.

In Wysteria principals are first class values, so the function richer, instead of returning a boolean, can also return the principal who is richer.

#!ocaml

(*
 * principals as values
 *)
let richer = \w:W {!Alice, !Bob} nat .
             let b @ sec({!Alice, !Bob}) =
                 if w[!Alice] > w[!Bob] then
                     !Alice
                 else
                     !Bob
             in
             b

Wysteria supports writing the function richer for an arbitrary number of parties. Let's develop this version of richer in steps (let's say this time we want to return the highest salary, we have also implemented the version that returns the principal even in this general setting and it's available in the examples/ directory in the implementation):

#!ocaml

(*
 * x is a variable of type ps (principals)
 * w is dependently typed (i.e. its a wire bundle with principals as x)
 *)
let richer = \x:ps . \w:W x nat .
             ...

Recall that principals are first class values in Wysteria, so richer function takes an argument x that denotes a principal set (type ps). The argument w is dependently typed on x.

The function body now has to iterate over the values of all the principals. Wysteria provides a wire combinator wfold that can be used in secure blocks to do so. (wfold is very similar to List fold operator).

#!ocaml

let richer = \x:ps . \w:W x nat .
             let b @ sec(x) =

                 (*
                  * the x here says that its an iteration over principal set x
                  * wfold takes as argument a wire bundle (w)
                  * an initial accumulator (0)
                  * and a function that takes the value of current accumulator, a principal, and its
                    component in the wire bundle, and returns the new value of the accumulator
                  *) 
                 wfold x (w, 0,
                          \accum:nat . \p:ps . \n:nat .
                          if accum > n then
                              accum
                          else
                              n
                         )
             in
             b

This version of richer can be called as follows:

#!ocaml

let all = { !Alice, !Bob } in
(* as before, let's say x is Alice's value, and y is Bob's *)
let w = (wire !Alice:x) ++ (wire !Bob:y) in

richer all w

The advantage of writing richer as a generic code is that the same function can be used even when computing the richest among three parties (or any number of parties for that matter). E.g.

#!ocaml

let all = { !Alice, !Bob, !Charlie } in
(* z is Charlie's input *)
let w = (wire !Alice:x) ++ (wire !Bob:y) ++ (wire !Charlie:z) in

richer all w

For more examples, please see the examples/ directory of the implementation. For more details on Wysteria, please refer to the paper, technical report, and talk slides.