Advertisement

\(\textsc {Wys}^\star \): A DSL for Verified Secure Multi-party Computations

  • Aseem RastogiEmail author
  • Nikhil Swamy
  • Michael Hicks
Open Access
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11426)

Abstract

Secure multi-party computation (MPC) enables a set of mutually distrusting parties to cooperatively compute, using a cryptographic protocol, a function over their private data. This paper presents \(\textsc {Wys}^\star \), a new domain-specific language (DSL) for writing mixed-mode MPCs. \(\textsc {Wys}^\star \) is an embedded DSL hosted in F\(^\star \), a verification-oriented, effectful programming language. \(\textsc {Wys}^\star \) source programs are essentially F\(^\star \) programs written in a custom MPC effect, meaning that the programmers can use F\(^\star \)’s logic to verify the correctness and security properties of their programs. To reason about the distributed runtime semantics of these programs, we formalize a deep embedding of \(\textsc {Wys}^\star \), also in F\(^\star \). We mechanize the necessary metatheory to prove that the properties verified for the \(\textsc {Wys}^\star \) source programs carry over to the distributed, multi-party semantics. Finally, we use F\(^\star \)’s extraction to extract an interpreter that we have proved matches this semantics, yielding a partially verified implementation. \(\textsc {Wys}^\star \) is the first DSL to enable formal verification of MPC programs. We have implemented several MPC protocols in \(\textsc {Wys}^\star \), including private set intersection, joint median, and an MPC-based card dealing application, and have verified their correctness and security.

1 Introduction

Secure multi-party computation (MPC) enables two or more parties to compute a function f over their private inputs \(x_i\) so that parties don’t see each others’ inputs, but rather only see the output \(f(x_1,...,x_n)\). Using a trusted third party to compute f would achieve this goal, but in fact we can achieve it using one of a variety of cryptographic protocols carried out only among the participants [12, 26, 58, 65]. One example use of MPC is private set intersection (PSI): the \(x_i\) could be individuals’ personal interests, and the function f computes their intersection, revealing which interests the group has in common, but not any interests that they don’t. MPC has also been used for auctions [18], detecting tax fraud [16], managing supply chains [33], privacy preserving statistical analysis [31], and more recently for machine learning tasks [19, 21, 30, 38, 44].

Typically, cryptographic protocols expect f to be specified as a boolean or arithmetic circuit. Programming directly with circuits and cryptography is painful, so starting with the Fairplay project [40] many researchers have designed higher-level domain-specific languages (DSLs) for programming MPC s [6, 14, 17, 19, 23, 27, 29, 34, 37, 39, 45, 48, 49, 52, 56, 61]. These DSLs compile source code to circuits which are then given to the underlying cryptographic protocol. While doing this undoubtedly makes it easier to program MPC s, these languages still have several drawbacks regarding both security and usability.

This paper presents \(\textsc {Wys}^\star \), a new MPC DSL that addresses several problems in prior DSLs. Unlike most previous MPC DSLs, \(\textsc {Wys}^\star \) is not a standalone language, but is rather an embedded DSL hosted in F\(^\star \) [59], a full-featured, verification-oriented, effectful programming language. \(\textsc {Wys}^\star \) has the following two distinguishing elements:

1. A program logic for MPC (Sects. 2 and 3). In their most general form, MPC applications are mixed-mode: they consist of parties performing (potentially different) local, in-clear computations (e.g. I/O, preprocessing inputs) interleaved with joint, secure computations. \(\textsc {Wys}^\star \) is the first MPC DSL to provide a program logic to formally reason about the correctness and security of such applications, e.g., to prove that the outputs will not reveal too much information about a party’s inputs [41].1

To avoid reasoning about separate programs for each party, \(\textsc {Wys}^\star \) builds on the basic programming model of the Wysteria MPC DSL [52] that allows applications to be written as a single specification. \(\textsc {Wys}^\star \) presents a shallow embedding of the Wysteria programming model in F\(^\star \). When writing \(\textsc {Wys}^\star \) source programs, programmers essentially write F\(^\star \) programs in a new Open image in new window effect, against a library of MPC combinators. The pre- and postcondition specifications on the combinators encode a program logic for MPC. The logic provides observable traces—a novel addition to the Wysteria semantics—which programmers can use to specify security properties such as delimited release [55]. Since \(\textsc {Wys}^\star \) programs are F\(^\star \) programs, F\(^\star \) computes verification conditions (VCs) for them which are discharged using Z3 [2] as usual.

We prove the soundness of the program logic—that the properties proven about the \(\textsc {Wys}^\star \) source programs carry over when these programs are run by multiple parties in a distributed manner—also in F\(^\star \). The proof connects the pre- and postconditions of the \(\textsc {Wys}^\star \) combinators to their distributed semantics in two steps. First, we implement the combinators in F\(^\star \), proving the validity of their pre- and postconditions against their implementation. Next, we reason about this implementation and the distributed runtime semantics through a deep embedding of \(\textsc {Wys}^\star \) in F\(^\star \). Essentially, we deep-embed the \(\textsc {Wys}^\star \) combinator abstract syntax trees (ASTs) as an F\(^\star \) datatype and formalize two operational semantics for them: a conceptual single-threaded semantics that models their F\(^\star \) implementation, and the actual distributed semantics that models the multi-party runs of the programs. We prove, in F\(^\star \), that the single-threaded semantics is sound with respect to the distributed semantics (Sect. 3). While we use F\(^\star \), the program logic is general and it should be possible to embed it in other verification frameworks (e.g., in Coq, in the style of Hoare Type Theory [46]).

2. A full-featured, partially verified implementation (Sect. 3). \(\textsc {Wys}^\star \)’s implementation is, in part, formally verified. The hope is that formal verification will reduce the occurrence of security threatening bugs, as it has in prior work [15, 36, 50, 63, 64].

We define an interpreter in F\(^\star \) that operates over the \(\textsc {Wys}^\star \) ASTs produced by a custom F\(^\star \) extraction for the Open image in new window effect. While the local computations are executed locally by the interpreter, the interpreter compiles secure-computation ASTs to circuits, on the fly, and executes them using the Goldreich, Micali and Wigderson (GMW) multi-party computation protocol [26]. The \(\textsc {Wys}^\star \) AST (and hence the interpreter) does not “bake in” standard F\(^\star \) constructs like numbers and lists. Rather, inherited language features appear abstractly in the AST, and their semantics is handled by a foreign function interface (FFI). This permits \(\textsc {Wys}^\star \) programs to take advantage of existing code and libraries available in F\(^\star \).

To prove the interpreter behaves correctly, we prove, in F\(^\star \), that it correctly implements the formalized distributed semantics. The circuit library and the GMW implementation are not verified—while it is possible to verify the circuit library [4], verifying a GMW implementation is an open research question. But the stage is set for verified versions to be plugged into the \(\textsc {Wys}^\star \) codebase. We characterize the Trusted Computing Base (TCB) of the \(\textsc {Wys}^\star \) toolchain in Sect. 3.5.

Using \(\textsc {Wys}^\star \) we have implemented several programs, including PSI, joint median, and a card dealing application (Sect. 4). For PSI and joint median we implement two versions: a straightforward one and an optimized one that improves performance but increases the number of adversary-observable events. We formally prove that the optimized and unoptimized versions are equivalent, both functionally and w.r.t. privacy of parties’ inputs. Our card dealing application relies on \(\textsc {Wys}^\star \)’s support for secret shares [57]. We formally prove that the card dealing algorithm always deals a fresh card.

In sum, \(\textsc {Wys}^\star \) constitutes the first DSL that supports proving security and correctness properties about MPC programs, which are executed by a partially verified implementation of a full-featured language. No prior DSL provides these benefits (Sect. 5). The \(\textsc {Wys}^\star \) implementation, example programs, and proofs are publicly available on Github at https://github.com/FStarLang/FStar/tree/stratified_last/examples/wysteria.2

2 Verifying and Deploying \(\textsc {Wys}^\star \) Programs

We illustrate the main concepts of \(\textsc {Wys}^\star \) by showing, in several stages, how to program, optimize, and verify the two-party joint median example [32, 53]. In this example, two parties, Alice and Bob, each have a set of n distinct, locally sorted integers, and they want to compute the median of the union of their sets without revealing anything else; our running example fixes \(n = 2\), for simplicity.

2.1 Secure Computations with Open image in new window

In \(\textsc {Wys}^\star \), as in its predecessor Wysteria [52], an MPC is written as a single specification that executes in one of the two computation modes. The primary mode is called Open image in new window mode. In it, a computation is carried out using an MPC protocol among multiple principals. Here is the joint median in \(\textsc {Wys}^\star \):
The four arguments to Open image in new window are, respectively, principal identifiers for Alice and Bob, and Alice and Bob’s secret inputs expressed as tuples. In \(\textsc {Wys}^\star \), values specific to each principal are sealed with the principal’s name (which appears in the sealed container’s type). As such, the types of Open image in new window and Open image in new window are, respectively, Open image in new window and Open image in new window . The Open image in new window construct indicates that thunk Open image in new window should be run in Open image in new window mode among principals in the set Open image in new window . In this mode, the code has access to the secrets of the principals Open image in new window , which it can reveal using the Open image in new window coercion. As we will see later, the type of Open image in new window ensures that parties cannot Open image in new window each others’ inputs outside Open image in new window mode.3 Also note that the code freely uses standard F\(^\star \) library functions like Open image in new window and Open image in new window . The example extends naturally to \(n > 2\) [3].

To run this program, both Alice and Bob would start a \(\textsc {Wys}^\star \) interpreter at their host and direct it to run the Open image in new window function Upon reaching the Open image in new window thunk, the interpreters coordinate with each other to compute the result using the underlying MPC protocol. Section 2.5 provides more details.

2.2 Optimizing Open image in new window with Open image in new window

Although Open image in new window gets the job done, it can be inefficient for large n. However, it turns out if we reveal the result of comparison on line 2 to both the parties, then the computation on line 3 (resp. line 4) can be performed locally by Alice (resp. Bob) without the need of cryptography. Doing so can massively improve performance: previous work [32] has observed a \(30{\times }\) speedup for \(n = 64\).

This optimized variant is a mixed-mode computation, where participants perform some local computations interleaved with small, jointly evaluated secure computations. \(\textsc {Wys}^\star \)’s second computation mode, Open image in new window mode, supports such mixed-mode computations. The construct Open image in new window states that each principal in Open image in new window should locally execute the thunk Open image in new window , simultaneously; any principal not in the set Open image in new window simply skips the computation. Within Open image in new window , while running in Open image in new window mode, principals may engage in secure computations via Open image in new window .

The secure computation on line 2 only computes Open image in new window and returns the result to both the parties. Line 3 is then a Open image in new window mode computation involving only Alice in which she discards one of her inputs based on Open image in new window . Similarly, on line 4, Bob discards one of his inputs. Finally, line 5 compares the remaining inputs using Open image in new window and returns the result as the final median.

One might wonder whether the Open image in new window mode is necessary. Could we program the local parts of a mixed-mode program in normal F\(^\star \), and use a special compiler to convert the Open image in new window mode parts to circuits and pass them to a GMW MPC service? We could, but it would complicate both writing MPC s and formally reasoning that the whole computation is correct and secure. In particular, programmers would need to write one program for each party that performs a different local computation (as in Open image in new window ). The potential interleaving among local computations and their synchronization behavior when securely computing together would be a source of possible error and thus must be considered in any proof. For example, Alice’s code might have a bug in it that prevents it from reaching a synchronization point with Bob, to do a GMW-based MPC. For \(\textsc {Wys}^\star \), the situation is much simpler. Programmers may write and maintain a single program. This program can be formally reasoned about directly using a SIMD-style, “single-threaded” semantics, per the soundness result from Sect. 3.4. This semantics permits reasoning about the coordinated behavior of multiple principals, without worry about the effects of interleavings or wrong synchronizations. Thanks to Open image in new window mode, invariants about coordinated local computations are directly evident since we can soundly assume the lockstep behavior (e.g., loop iterations in the PSI example in Sect. 4).

2.3 Embedding a Type System for \(\textsc {Wys}^\star \) in F\(^\star \)

Designing high-level, multi-party computations is relatively easy using Wysteria’s abstractions. Before trying to run such a computation, we might wonder:
  1. 1.

    Is it realizable? For example, does a computation that is claimed to be executed only by some principals Open image in new window (e.g., using an Open image in new window or an Open image in new window ) only ever access data belonging to Open image in new window ?

     
  2. 2.

    Is it correct? For example, does Open image in new window correctly compute the median of Alice and Bob’s inputs?

     
  3. 3.

    Is it secure? For example, do the optimizations in Open image in new window , which produce more visible outputs, potentially leak more about the inputs?

     

By embedding \(\textsc {Wys}^\star \) in F\(^\star \) and leveraging its extensible, monadic, dependent type-and-effect system, we address each of these three questions. We define a new indexed monad called Open image in new window for computations that use MPC combinators Open image in new window and Open image in new window . Using Open image in new window along with the Open image in new window type, we can ensure that protocols are realizable. Using F\(^\star \)’s capabilities for formal verification, we can reason about a computation’s correctness. By characterizing observable events as part of Open image in new window , we can define trace properties of MPC programs to reason about their security.

To elaborate on the last: we are interested in application-level security properties, assuming that the underlying cryptographic MPC protocol (GMW [26] in our implementation) is secure. In particular, the Open image in new window monad models the ideal behavior of Open image in new window mode—a secure computation reveals only the final output and nothing else. Thus the programmer could reason, for example, that optimized MPC programs reveal no more than their unoptimized versions. To relate the proofs over ideal functionality to the actual implementation, as is standard, we rely on the security of the cryptographic protocol and the composition theorem [20] to postulate that the implementation securely realizes the ideal specification.

The Open image in new window The Open image in new window monad provides several features. First, all DSL code is typed in this monad, encapsulating it from the rest of F\(^\star \). Within the monad, computations and their specifications can make use of two kinds of ghost state: modes and traces. The mode of a computation indicates whether the computation is running in an Open image in new window or in an Open image in new window context. The trace of a computation records the sequence and nesting structure of outputs of the jointly executed Open image in new window expressions—the result of a computation and its trace constitute its observable behavior. The Open image in new window monad is, in essence, the product of a reader monad on modes and a writer monad on traces [43, 62].

Formally, we define the following F\(^\star \) types for modes and traces. A mode Open image in new window is a pair of a mode tag (either Open image in new window or Open image in new window ) and a set of principals Open image in new window . A Open image in new window is a forest of trace element ( Open image in new window ) trees. The leaves of the trees record messages Open image in new window that are received as the result of executing an Open image in new window thunk. The tree structure represented by the Open image in new window nodes record the set of principals that are able to observe the messages in the trace Open image in new window .

Every \(\textsc {Wys}^\star \) computation e has a monadic computation type Open image in new window . The type indicates that e is in the Open image in new window monad (so it may perform multi-party computations); Open image in new window is its result type; Open image in new window is a precondition on the mode in which Open image in new window may be executed; and Open image in new window is a postcondition relating the computation’s mode, its result value, and its trace of observable events. When run in a context with mode Open image in new window satisfying the precondition predicate Open image in new window may produce the trace Open image in new window , and if and when it returns, the result is a Open image in new window -typed value Open image in new window validating Open image in new window . The style of indexing a monad with a computation’s pre- and postcondition is a standard technique [7, 47, 59]—we defer the definition of the monad’s Open image in new window and Open image in new window to the actual implementation and focus instead on specifications of \(\textsc {Wys}^\star \) specific combinators. We describe Open image in new window , Open image in new window , and Open image in new window , and how we give them types in F\(^\star \), leaving the rest to the online technical report [54]. By convention, any free variables in the type signatures are universally prenex quantified.

Defining Open image in new window in \(\textsc {Wys}^\star \)

The type of Open image in new window is dependent on the first parameter, Open image in new window . Its second argument Open image in new window is the thunk to be evaluated in Open image in new window mode. The result’s computation type has the form Open image in new window , for some precondition and postcondition predicates \(\phi \) and \(\psi \), respectively. We use the Open image in new window and Open image in new window keywords for readability—they are not semantically significant.

The precondition of Open image in new window is a predicate on the mode Open image in new window of the computation in whose context Open image in new window is called. For all the Open image in new window to jointly execute Open image in new window , we require all of them to transition to perform the Open image in new window call simultaneously, i.e., the current mode must be Open image in new window . We also require the precondition Open image in new window of Open image in new window to be valid once the mode has transitioned to Open image in new window —line 2 says just this.

The postcondition of Open image in new window is a predicate relating the initial mode Open image in new window , the result Open image in new window , and the trace Open image in new window of the computation. Line 3 states that the trace of a secure computation Open image in new window is just a singleton Open image in new window , reflecting that its execution reveals only result Open image in new window . Additionally, it ensures that the result Open image in new window is related to the mode in which Open image in new window is run ( Open image in new window ) and some trace Open image in new window according to Open image in new window , the postcondition of Open image in new window . The API models the “ideal functionality” of secure computation protocols (such as GMW) where the participants only observe the final result.

Defining Open image in new window in \(\textsc {Wys}^\star \). As discussed earlier, a value Open image in new window of type Open image in new window encapsulates a Open image in new window value that can be accessed by calling Open image in new window . This call should only succeed under certain circumstances. For example, in Open image in new window mode, Bob should not be able to reveal a value of type Open image in new window . The type of Open image in new window makes the access control rules clear:

The Open image in new window function is a Open image in new window function, meaning that it can only be used in specifications for reasoning purposes. On the other hand, Open image in new window can be called in the concrete \(\textsc {Wys}^\star \) programs. Its precondition says that when executing in Open image in new window , all current participants must be listed in the seal, i.e., Open image in new window . However, when executing in Open image in new window , only a subset of current participants is required: Open image in new window . This is because the secure computation is executed jointly by all of Open image in new window , so it can access any of their individual data. The postcondition of Open image in new window relates the result Open image in new window to the argument Open image in new window using the Open image in new window function.

Defining Open image in new window in \(\textsc {Wys}^\star \)

The type of Open image in new window enforces the current mode to be Open image in new window , and Open image in new window to be a subset of current principals. Importantly, the API scopes the trace Open image in new window of Open image in new window to model the fact that any observables of Open image in new window are only visible to the principals in Open image in new window . Note that Open image in new window did not require such scoping, as there Open image in new window and the set of current principals in Open image in new window are the same. The Open image in new window predicate enforces that Open image in new window is a zero-order type (i.e. closures cannot be sealed), and that in case Open image in new window is already a sealed type, its set of principals is a subset of Open image in new window .

2.4 Correctness and Security Verification

Using the Open image in new window monad and the Open image in new window type, we can write down precise types for our Open image in new window and Open image in new window programs, proving various useful properties. We discuss the statements of the main lemmas and the overall proof structure. By programming the protocols as a single specification using the high-level abstractions provided by \(\textsc {Wys}^\star \), our proofs are relatively straightforward—in all the proofs of this section, F\(^\star \) required no additional hints. In particular, we rely heavily on the view that both parties execute (different fragments of) the same code, thus avoiding the unwieldy task of reasoning about low-level message passing.

Correctness and Security of Open image in new window . We first define a pure specification of median of two Open image in new window tuples:
Further, we capture the preconditions using the following predicate:
Using these, we prove the following top-level specification for Open image in new window :

This signature establishes that when Alice and Bob simultaneously execute Open image in new window (in Open image in new window mode), with secrets Open image in new window and Open image in new window , then, if and when the protocol terminates, (a) if their inputs satisfy the precondition Open image in new window , then the result is the joint median of their inputs and (b) the observable trace consists only of the final result, as there is but a single Open image in new window thunk in Open image in new window , i.e., it is secure.

Correctness and Security of Open image in new window The security proof of Open image in new window is particularly interesting, because the program intentionally reveals more than just the final result, i.e., the output of the first comparison. We would like to verify that this additional information does not compromise the privacy of the parties’ inputs. To do this, we take the following approach.

First, we characterize the observable trace of Open image in new window as a pure, specification-only function. Then, using relational reasoning, we prove a noninteference with delimited release property [55] on these traces. Essentially we prove that, for two runs of Open image in new window where Bob’s inputs and the output median are the same, the observable traces are also the same irrespective of Alice’s inputs. Thus, from Alice’s perspective, the observable trace does not reveal more to Bob than what the output already does. We prove this property symmetrically for Bob.

We start by defining a trace function for Open image in new window :

A trace will have four elements: output of the first Open image in new window computation, two empty scoped traces for the two local Open image in new window computations, and the final output.

Using this function, we prove correctness of Open image in new window , thus:
The delimited release property is then captured by the following lemma:

The lemma proves that for two runs of Open image in new window where Bob’s input and the final output remain same, but Alice’s inputs vary arbitrarily, the observable traces are the same. As such, no more information about information leaks about Alice’s inputs via the traces than what is already revealed by the output. We also prove a symmetrical lemma Open image in new window .

In short, because the Open image in new window monad provides programmers with the observable traces in the logic, they can then be used to prove properties, relational or otherwise, in the pure fragment of F\(^\star \) outside the Open image in new window monad. We present more examples and their verification details in Sect. 4.

2.5 Deploying \(\textsc {Wys}^\star \) Programs

Having defined a proved-secure MPC program in \(\textsc {Wys}^\star \), how do we run it? Doing so requires the following steps (Fig. 1). First, we run the F\(^\star \) compiler in a special mode that extracts the \(\textsc {Wys}^\star \) code (say Open image in new window ), into the \(\textsc {Wys}^\star \) AST as a data structure (in Open image in new window ). Except for the \(\textsc {Wys}^\star \) specific nodes ( Open image in new window , Open image in new window , etc.), the rest of the program is extracted into FFI nodes that indicate the use of, or calls into, functionality provided by F\(^\star \) itself.
Fig. 1.

Architecture of an \(\textsc {Wys}^\star \) deployment

The next step is for each party to run the extracted AST using the \(\textsc {Wys}^\star \) interpreter. This interpreter is written in F\(^\star \) and we have proved (see Sect. 3.5) that it implements a deep embedding of the \(\textsc {Wys}^\star \) semantics, also specified in F\(^\star \) (Figs. 5 and 6, Sect. 3). The interpreter is extracted to OCaml by the usual F\(^\star \) extraction. Each party’s interpreter executes the AST locally until it reaches an Open image in new window node, where the interpreter’s back-end compiles Open image in new window , on-the-fly, for particular values of the secrets in Open image in new window ’s environment, to a boolean circuit. First-order, loop-free code can be compiled to a circuit; \(\textsc {Wys}^\star \) provides specialized support for several common combinators (e.g., Open image in new window , Open image in new window , list combinators such as Open image in new window , Open image in new window , Open image in new window etc.).

The circuit is handed to a library by Choi et al. [22] that implements the GMW [26] MPC protocol. Running the GMW protocol involves the parties in Open image in new window generating and communicating (XOR-based) secret shares [57] for their secret inputs, and then cooperatively evaluating the boolean circuit for Open image in new window over them. While our implementation currently uses the GMW protocol, it should be possible to plugin other MPC protocols as well.

One obvious question is how both parties are able to get this process off the ground, given that they don’t know some of the inputs (e.g., other parties’ secrets). The Open image in new window abstraction helps here. Recall that for Open image in new window , the types of the inputs are of the form Open image in new window and Open image in new window . When the program is run on Alice’s host, the former will be a pair of Alice’s values, whereas the latter will be an opaque constant (which we denote as \(\bullet \)). The reverse will be true on Bob’s host. When the circuit is constructed, each principal links their non-opaque inputs to the relevant input wires of the circuit. Similarly, the output map component of each party is derived from their output wires in the circuit, and thus, each party only gets to see their own output.

3 Formalizing and Implementing \(\textsc {Wys}^\star \)

In the previous section, we presented examples of verifying properties about \(\textsc {Wys}^\star \) programs using F\(^\star \)’s logic. However, these programs are not executed using the F\(^\star \) (single-threaded) semantics; they have a distributed semantics involving multiple parties. So, how do the properties that we verify using F\(^\star \) carry over?
Fig. 2.

\(\textsc {Wys}^\star \) syntax

In this section, we present the metatheory that answers this question. First, we formalize the \(\textsc {Wys}^\star \) single-threaded (ST) semantics, that faithfully models the F\(^\star \) semantics of the \(\textsc {Wys}^\star \) API presented in Sect. 2. Next, we formalize the distributed (DS) semantics that multiple parties use to run \(\textsc {Wys}^\star \) programs. Then we prove the former is sound with respect to the latter, so that properties proved of programs under ST apply when run under DS. We have mechanized the proof of this theorem in F\(^\star \).

3.1 Syntax

Figure 2 shows the complete syntax of \(\textsc {Wys}^\star \). Principals and principal sets are first-class values, and are denoted by p and \(s\) respectively. Constants in the language also include () (unit), booleans (\(\top \) and \(\bot \)), and FFI constants \(\mathsf {c}\). Expressions e include the regular forms for functions, applications, let bindings, etc. and the \(\textsc {Wys}^\star \)-specific constructs. Among the ones that we have not seen in Sect. 2, expression Open image in new window creates a map from principals in \(e_1\) (which is a principal set) to the value computed by \(e_2\). Open image in new window projects the value of principal \(e_1\) from the map \(e_2\), and Open image in new window concatenates the two maps. The maps are used if an Open image in new window computation returns different outputs to the parties.

Host language (i.e., F\(^\star \)) constructs are also part of the syntax of \(\textsc {Wys}^\star \), including constants \(\mathsf {c}\) for strings, integers, lists, tuples, etc. Likewise, host language functions/primitives can be called from \(\textsc {Wys}^\star \) Open image in new window is the invocation of a host-language function \(\mathsf {f}\) with arguments \(\bar{e}\). The FFI confers two benefits. First, it simplifies the core language while still allowing full consideration of security relevant properties. Second, it helps the language scale by incorporating many of the standard features, libraries, etc. from the host language.
Fig. 3.

Runtime configuration syntax

Fig. 4.

\(\textsc {Wys}^\star \) ST semantics (selected rules)

3.2 Single-Threaded Semantics

We formalize the semantics in the style of Hieb and Felleisen [24], where the redex is chosen by (standard, not shown) evaluation contexts E, which prescribe left-to-right, call-by-value evaluation order. The ST semantics, a model of the F\(^\star \) semantics and the \(\textsc {Wys}^\star \) API, defines a judgment \(C \rightarrow C'\) that represents a single step of an abstract machine (Fig. 4). Here, C is a configuration MXLTe. This five-tuple consists of a mode M, a stack X, a local environment L, a trace T, and an expression e. The syntax for these elements is given in Fig. 3. The value form \(\mathsf {v}\) represents the host language (FFI) values. The stack and environment are standard; trace T and mode M were discussed in the previous section.

For space reasons, we focus on the two main \(\textsc {Wys}^\star \) constructs Open image in new window and Open image in new window . Our technical report [54] shows other \(\textsc {Wys}^\star \) specific constructs.

Rules S-aspar and S-parret (Fig. 4) reduce an Open image in new window expression once its arguments are fully evaluated—its first argument s is a principal set, while the second argument \((L_1, \lambda x.e)\) is a closure where \(L_1\) captures the free variables of thunk \(\lambda x.e\). S-aspar first checks that the current mode M is Open image in new window and contains all the principals from the set \(s\). It then pushes a Open image in new window frame on the stack, and starts evaluating e under the environment \(L_1[x \mapsto ()]\). The rule S-asparret pops the frame and seals the result, so that it is accessible only to the principals in \(s\). The rule also creates a trace element Open image in new window , essentially making observations during the reduction of e (i.e., T) visible only to principals in \(s\).

Turning to Open image in new window , the rule S-assec checks the precondition of the API, and the rule S-assecret generates a trace observation Open image in new window , as per the postcondition of the API. As mentioned before, Open image in new window semantics models the ideal, trusted third-party semantics of secure computations where the participants only observe the final output. We can confirm that the rules implement the types of Open image in new window and Open image in new window shown in Sect. 2.
Fig. 5.

Distributed semantics, multi-party rules

Fig. 6.

Distributed semantics, selected local rules (the mode M is always Open image in new window )

3.3 Distributed Semantics

In the DS semantics, principals evaluate the same program locally and asynchronously until they reach a secure computation, at which point they synchronize to jointly perform the computation. The semantics consists of two parts: (a) a judgment of the form \(\pi \longrightarrow \pi '\) (Fig. 5), where a protocol \(\pi \) is a tuple (PS) such that P maps each principal to its local configuration and S maps a set of principals to the configuration of an ongoing, secure computation; and (b) a local evaluation judgment Open image in new window (Fig. 6) to model how a single principal behaves while in Open image in new window mode.

Rule P-Par in Fig. 5 models a single party taking a step, per the local evaluation rules. Figure 6 shows these rules for Open image in new window . (See technical report [54] for more local evaluation rules.) A principal either participates in the Open image in new window computation, or skips it. Rules L-aspar1 and L-parret handle the case when \(p \in s\), and so, the principal p participates in the computation. The rules closely mirror the corresponding ST semantics rules in Fig. 4. One difference in the rule L-asparret is that the trace T is not scoped. In the DS semantics, traces only contain Open image in new window elements; i.e., a trace is the (flat) list of secure computation outputs observed by that active principal. If \(p \not \in s\), then the principal skips the computation with the result being a sealed value containing the opaque constant \(\bullet \) (rule L-aspar2). The contents of the sealed value do not matter, since the principal will not be allowed to unseal the value anyway.

As should be the case, there are no local rules for Open image in new window —to perform a secure computation parties need to combine their data and jointly do the computation. Rule P-enter in Fig. 5 handles the case when principals enter a secure computation. It requires that all the principals \(p \in s\) must have the expression form Open image in new window , where \(L_p\) is their local environment associated with the closure. Each party’s local environment contains its secret values (in addition to some public values). Conceptually, a secure computation combines these environments, thereby producing a joint view, and evaluates e under the combination. We define an auxiliary Open image in new window function for this purpose:

The rule P-enter combines the principals’ environments, and creates a new entry in the S map. The principals are now waiting for the secure computation to finish. Rule P-sec models a stepping rule inside the Open image in new window mode.

The rule P-exit applies when a secure computation has completed and returns results to the waiting principals. If the secure computation terminates with value v, each principal p gets the value Open image in new window . The Open image in new window function is analogous to Open image in new window , but in the opposite direction—it strips off the parts of v that are not accessible to p:

In the rule P-exit, the \(\triangleleft \) notation is defined as:

Open image in new window

That is, the returned value is also added to the principal’s trace to note their observation of the value.

3.4 Metatheory

Our goal is to show that the ST semantics faithfully represents the semantics of \(\textsc {Wys}^\star \) programs as they are executed by multiple parties, i.e., according to the DS semantics. We do this by proving simulation of the ST semantics by the DS semantics, and by proving confluence of the DS semantics. Our F\(^\star \) development mechanizes all the metatheory presented in this section.

Simulation. We define a Open image in new window function that returns the corresponding protocol \(\pi _C\) for an ST configuration C. In the P component of \(\pi _C\), each principal \(p \in s\) is mapped to their slice of the protocol. For slicing values, we use the same Open image in new window function as before. Traces are sliced as follows:

The slice of an expression (e.g., the source program) is itself. For all other components of C, slice functions are defined analogously.

We say that C is terminal if it is in Open image in new window mode and is fully reduced to a value (i.e. when \(C = \_; X; \_; \_; e\), e is a value and X is empty). Similarly, a protocol \(\pi = (P, S)\) is terminal if S is empty and all the local configurations in P are terminal. The simulation theorem is then the following:

Theorem 1

(Simulation of ST by DS). Let \(s\) be the set of all principals. If \(C_1 \rightarrow ^{*} C_2\), and \(C_2\) is terminal, then there exists some derivation Open image in new window such that Open image in new window is terminal.

To state confluence, we first define the notion of strong termination.

Definition 1

(Strong termination). If all possible runs of protocol \(\pi \) terminate at \(\pi _t\), we say \(\pi \) strongly terminates in \(\pi _t\), written \(\pi \Downarrow \pi _t\).

Our confluence result then says:

Theorem 2

(Confluence of DS). If \(\pi \longrightarrow ^{*} \pi _t\) and \(\pi _t\) is terminal, then \(\pi \Downarrow \pi _t\).

Combining the two theorems, we get a corollary that establishes the soundness of the ST semantics w.r.t. the DS semantics:

Corollary 1

(Soundness of ST semantics). Let \(s\) be the set of all principals. If \(C_1 \rightarrow ^* C_2\), and \(C_2\) is terminal, then Open image in new window .

Now suppose that for a \(\textsc {Wys}^\star \) source program, we prove in F\(^\star \) a postcondition that the result is Open image in new window Open image in new window n, for some \(n > 0\). By the soundness of the ST semantics, we can conclude that when the program is run in the DS semantics, it may diverge, but if it terminates, Open image in new window ’s output will also be Open image in new window n, and for all other principals their outputs will be Open image in new window Open image in new window . Aside from the correspondence on results, our semantics also covers correspondence on traces. Thus the correctness and security properties that we prove about a \(\textsc {Wys}^\star \) program using F\(^\star \)’s logic, hold for the program that actually runs.

3.5 Implementation

The formal semantics presented in the prior section is mechanized as an inductive type in F\(^\star \). This style is useful for proving properties, but does not directly translate to an implementation. Therefore, we implement an interpretation function Open image in new window in F\(^\star \) and prove that it corresponds to the rules; i.e., that for all input configurations C, Open image in new window \((C) = C'\) implies that \(C \rightarrow C'\) according to the semantics. Then, the core of each principal’s implementation is an F\(^\star \) stub function Open image in new window that repeatedly invokes Open image in new window on the AST of the source program (produced by the F\(^\star \) extractor run in a custom mode), unless the AST is an Open image in new window node. Functions Open image in new window and Open image in new window are extracted to OCaml by the standard F\(^\star \) extraction process.

Local evaluation is not defined for the Open image in new window node, so the stub implements what amounts to P-enter and P-exit from Fig. 5. When the stub notices the program has reached an Open image in new window expression, it calls into a circuit library we have written that converts the AST of the second argument of Open image in new window to a boolean circuit. This circuit and the encoded inputs are communicated to a co-hosted server that implements the GMW MPC protocol [22]. The server evaluates the circuit, coordinating with the GMW servers of the other principals, and sends back the result. The circuit library decodes the result and returns it to the stub. The stub then carries on with the local evaluation. Our FFI interface currently provides a form of monomorphic, first-order interoperability between the (dynamically typed) interpreter and the host language.

Our F\(^\star \) formalization of the \(\textsc {Wys}^\star \) semantics, including the AST specification, is 1900 lines of code. This formalization is used both by the metatheory as well as by the (executable) interpreter. The metatheory that connects the ST and DS semantics (Sect. 3) is 3000 lines. The interpreter and its correctness proof are another 290 lines of F\(^\star \) code. The interpreter Open image in new window function is essentially a big switch-case on the current expression, that calls into the functions from the semantics specification. The Open image in new window stub is another 15 lines. The size of the circuit library, not including the GMW implementation, is 836 lines. The stub, the implementation of GMW, the circuit library, and F\(^\star \) toolchain (including the custom \(\textsc {Wys}^\star \) extraction mode) are part of our Trusted Computing Base (TCB).

4 Applications

In addition to joint median, presented in Sect. 2, we have implemented and proved properties of two other MPC applications, dealing for online card games and private set intersection (PSI).

Card Dealing. We have implemented an MPC-based card dealing application in \(\textsc {Wys}^\star \). Such an application can play the role of the dealer in a game of online poker, thereby eliminating the need to trust the game portal for card dealing. The application relies on \(\textsc {Wys}^\star \)’s support for secret shares [57]. Using secret shares, the participating parties can share a value in a way that none of the parties can observe the actual value individually (each party’s share consists of some random-looking bytes), but they can recover the value by combining their shares in Open image in new window mode.

In the application, the parties maintain a list of secret shares of already dealt cards (the number of already dealt cards is public information). To deal a new card, each party first generates a random number locally. The parties then perform a secure computation to compute the sum of their random numbers modulo 52, let’s call it n. The output of the secure computation is secret shares of n. Before declaring n as the newly dealt card, the parties needs to ensure that the card n has not already been dealt. To do so, they iterate over the list of secret shares of already dealt cards, and for each element of the list, check that it is different from n. The check is performed in a secure computation that simply combines the shares of n, combines the shares of the list element, and checks the equality of the two values. If n is different from all the previously dealt cards, it is declared to be the new card, else the parties repeat the protocol by again generating a fresh random number each.

\(\textsc {Wys}^\star \) provides the following API for secret shares:

Type Open image in new window types the shares of values of type Open image in new window . Our implementation currently supports shares of Open image in new window values only; the Open image in new window predicate enforces this restriction on the source programs. Extending secret shares support to other types (such as pairs) should be straightforward (as in [52]). Functions Open image in new window and Open image in new window are marked Open image in new window , meaning that they can only be used in specifications for reasoning purposes. In the concrete code, shares are created and combined using the Open image in new window and Open image in new window functions. Together, the specifications of these functions enforce that the shares are created and combined by the same set of parties (through Open image in new window ), and that Open image in new window recovers the original value (through Open image in new window ). The \(\textsc {Wys}^\star \) interpreter transparently handles the low-level details of extracting shares from the GMW implementation of Choi et al. ( Open image in new window ), and reconstituting the shares back ( Open image in new window ).

In addition to implementing the card dealing application in \(\textsc {Wys}^\star \), we have formally verified that the returned card is fresh. The signature of the function that checks for freshness of the newly dealt card is as follows ( Open image in new window is the set of three parties in the computation):

The specification says that the function takes two arguments: Open image in new window is the list of secret shares of already dealt cards, and Open image in new window is the secret shares of the newly dealt card. The function returns a boolean Open image in new window that is Open image in new window iff the concrete value ( Open image in new window ) of Open image in new window is different from the concrete values of all the elements of the list Open image in new window . Using F\(^\star \), we verify that the implementation of Open image in new window meets this specification.

PSI. Consider a dating application that enables its users to compute their common interests without revealing all of them. This is an instance of the more general private set intersection (PSI) problem [28].

We implement a straightforward version of PSI in \(\textsc {Wys}^\star \):

where the input sets are expressed as lists with public lengths.

Huang et al. [28] provide an optimized PSI algorithm that performs much better when the density of common elements in the two sets is high. We implement their algorithm in \(\textsc {Wys}^\star \). The optimized version consists of two nested loops – an outer loop for Alice’s set and an inner loop for Bob’s – where an iteration of the inner loop compares the current element of Alice’s set with the current element of Bob’s. The nested loops are written using Open image in new window so that both Alice and Bob execute the loops in lockstep (note that the set sizes are public), while the comparison in the inner loop happens using Open image in new window . Instead of naive Open image in new window comparisons, Huang et al. [28] observe that once an element of Alice’s set Open image in new window matches an element of Bob’s set Open image in new window , the inner loop can return immediately, skipping the comparisons of Open image in new window with the rest of Bob’s set. Furthermore, Open image in new window can be removed from Bob’s set, excluding it from any further comparisons with other elements in Alice’s set. Since there are no repeats in the input sets, all the excluded comparisons are guaranteed to be false. We show the full code and its performance comparison with Open image in new window in the technical report [54].

As with the median example from Sect. 2, the optimized PSI intentionally reveals more for performance gains. As such, we would like to verify that the optimizations do not reveal more about parties’ inputs. We take the following stepwise refinement approach. First, we characterize the trace of the optimized implementation as a pure function Open image in new window (omitted for space reasons), and show that the trace of Open image in new window is precisely Open image in new window .

Then, we define an intermediate PSI implementation that has the same nested loop structure, but performs Open image in new window comparisons without any optimizations. We characterize the trace of this intermediate implementation as the pure function Open image in new window , and show that it precisely captures the trace.

To show that Open image in new window does not reveal more than the intersection of the input sets, we prove the following lemma.

The lemma essentially says that for two runs on same length inputs, if the output is the same, then the resulting traces are permutation of each other.4 We can reason about the traces of Open image in new window up to permutation because Alice has no prior knowledge of the choice of representation of Bob’s set (Bob can shuffle his list), so cannot learn anything from a permutation of the trace.5 This establishes the security of Open image in new window .

Finally, we can connect Open image in new window to Open image in new window by showing that there exists a function Open image in new window , such that for any trace Open image in new window , the trace of Open image in new window , Open image in new window , can be computed by Open image in new window . In other words, the trace produced by the optimized implementation can be computed using a function of information already available to Alice (or Bob) when she (or he) observes a run of the secure, unoptimized version Open image in new window . As such, the optimizations do not reveal further information.

5 Related Work

Source Open image in new window Verification. While the verification of the underlying crypto protocols has received some attention [4, 5], verification of the correctness and security properties of MPC source programs has remained largely unexplored, surprisingly so given that the goal of MPC is to preserve the privacy of secret inputs. The only previous work that we know of is Backes et al. [9] who devise an applied pi-calculus based abstraction for MPC, and use it for formal verification. For an auction protocol that computes the Open image in new window function, their abstraction comprises about 1400 lines of code. \(\textsc {Wys}^\star \), on the other hand, enables direct verification of the higher-level MPC source programs, and not their models, and in addition provides a partially verified toolchain.

Wysteria. \(\textsc {Wys}^\star \)’s computational model is based on the programming abstractions of a previous MPC DSL, Wysteria [52]. \(\textsc {Wys}^\star \)’s realization as an embedded DSL in F\(^\star \) makes important advances. In particular, \(\textsc {Wys}^\star \) (a) enhances the Wysteria semantics to include a notion of observable traces, and provides the novel capability to prove security and correctness properties about mixed-mode MPC source programs, (b) expands the programming constructs available by drawing on features and libraries of F\(^\star \), and (c) adds assurance via a (partially) proved-correct interpreter.

Verified Open image in new window Toolchain. Almeida et al. [4] build a verified toolchain consisting of (a) a verified circuit compiler from (a subset of) C to boolean circuits, and (b) a verified implementation of Yao’s [65] garbled circuits protocol for 2-party MPC. They use CompCert [36] for the former, and EasyCrypt [11] for the latter. These are significant advances, but there are several distinctions from our work. The MPC programs in their toolchain are not mixed-mode, and thus it cannot express examples like Open image in new window and the optimized PSI. Their framework does not enable formal verification of source programs like \(\textsc {Wys}^\star \) does. It may be possible to use other frameworks for verifying C programs (e.g. Frama-C [1]), but it is inconvenient as one has to work in the subset of C that falls in the intersection of these tools. \(\textsc {Wys}^\star \) is also more general as it supports general n-party MPC; e.g., the card dealing application in Sect. 4 has 3 parties. Nevertheless, \(\textsc {Wys}^\star \) may use their verified Yao implementation for the special case of 2 parties.

Open image in new window DSLs and DSL Extensions. In addition to Wysteria several other MPC DSLs have been proposed in the literature [14, 17, 27, 29, 34, 37, 39, 48, 49, 52, 56, 61]. Most of these languages have standalone implementations, and the (usability/scalability) drawbacks that come with them. Like \(\textsc {Wys}^\star \), a few are implemented as language extensions. Launchbury et al. [35] describe a Haskell-embedded DSL for writing low-level “share protocols” on a multi-server “SMC machine”. OblivC [66] is an extension to C for two-party MPC that annotates variables and conditionals with an Open image in new window qualifier to identify private inputs; these programs are compiled by source-to-source translation. The former is essentially a shallow embedding, and the latter is compiler-based; \(\textsc {Wys}^\star \) is unique in that it combines a shallow embedding to support source program verification and a deep embedding to support a non-standard target semantics. Recent work [19, 21] compiles to cryptographic protocols that include both arithmetic and boolean circuits; the compiler decides which fragments of the program fall into which category. It would be interesting work to integrate such a backend in \(\textsc {Wys}^\star \).

Mechanized Metatheory. Our verification results are different from a typical verification result that might either mechanize metatheory for an idealized language [8], or might prove an interpreter or compiler correct w.r.t. a formal semantics [36]—we do both. We mechanize the metatheory of \(\textsc {Wys}^\star \) establishing the soundness of the conceptual ST semantics w.r.t. the actual DS semantics, and mechanize the proof that the interpreter implements the correct DS semantics.

General DSL Implementation Strategies. DSLs (for MPC or other purposes) are implemented in various ways, such as by developing a standalone compiler/interpreter, or by shallow or deep embedding in a host language. Our approach bears relation to the approach taken in LINQ [42], which embeds a query language in normal C# programs, and implements these programs by extracting the query syntax tree and passing it to a provider to implement for a particular backend. Other researchers have embedded DSLs in verification-oriented host languages (e.g., Bedrock [13] in Coq [60]) to permit formal proofs of DSL programs. Low\(^\star \) [51] is a shallow embedding of a small, sequential, well-behaved subset of C in F\(^\star \) that extracts to C using a F\(^\star \)-to-C compiler. Low\(^\star \) has been used to verify and implement several cryptographic constructions. Fromherz et al. [25] present a deep embedding of a subset of x64 assembly in F\(^\star \) that allows efficient verification of assembly and its interoperation with C code generated from Low\(^\star \). They design (and verify) a custom VC generator for the deeply embedded DSL, that allows for the proofs of assembly crypto routines to scale.

6 Conclusions

This paper has presented \(\textsc {Wys}^\star \), the first DSL to enable formal verification of efficient source MPC programs as written in a full-featured host programming language, F\(^\star \). The paper presented examples such as joint median, card dealing, and PSI, and showed how the DSL enables their correctness and security proofs. \(\textsc {Wys}^\star \) implementation, examples, and proofs are publicly available on Github.

Footnotes

  1. 1.

    Our attacker model is the “honest-but-curious” model where the attackers are the participants themselves, who play their roles in the protocol faithfully, but are motivated to infer as much as they can about the other participants’ secrets by observing the protocol. Section 2.3 makes the security model of \(\textsc {Wys}^\star \) more precise.

  2. 2.

    This development was done on an older F\(^\star \) version, but the core ideas of what we present here apply to the present version as well.

  3. 3.

    The runtime representation of Open image in new window at Open image in new window ’s host is an opaque constant \(\bullet \) (Sect. 2.5).

  4. 4.

    Holding Bob’s (resp. Alice’s) inputs fixed and varying Alice’s (resp. Bob’s) inputs, as done for Open image in new window in Sect. 2.4, is covered by this more general property.

  5. 5.

    We could formalize this observation using a probabilistic, relational variant of F\(^\star \)  [10].

Notes

Acknowledgments

We would like to thank the anonymous reviewers, Catalin Hriţcu, and Matthew Hammer for helpful comments on drafts of this paper. This research was funded in part by the U.S. National Science Foundation under grants CNS-1563722, CNS-1314857, and CNS-1111599.

References

  1. 1.
  2. 2.
    Z3 theorem prover. z3.codeplex.com
  3. 3.
    Aggarwal, G., Mishra, N., Pinkas, B.: Secure computation of the \(k^{th}\)-ranked element. In: Cachin, C., Camenisch, J.L. (eds.) EUROCRYPT 2004. LNCS, vol. 3027, pp. 40–55. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24676-3_3CrossRefGoogle Scholar
  4. 4.
    Almeida, J.B., et al.: A fast and verified software stack for secure function evaluation. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017 (2017)Google Scholar
  5. 5.
    Almeida, J.B., et al.: Verified implementations for secure and verifiable computation (2014)Google Scholar
  6. 6.
    Araki, T., et al.: Generalizing the SPDZ compiler for other protocols. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018 (2018)Google Scholar
  7. 7.
    Atkey, R.: Parameterised notions of computation. J. Funct. Program. 19, 335–376 (2009).  https://doi.org/10.1017/S095679680900728X. http://journals.cambridge.org/article_S095679680900728X
  8. 8.
    Aydemir, B.E., et al.: Mechanized metatheory for the masses: the PoplMark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50–65. Springer, Heidelberg (2005).  https://doi.org/10.1007/11541868_4CrossRefGoogle Scholar
  9. 9.
    Backes, M., Maffei, M., Mohammadi, E.: Computationally sound abstraction and verification of secure multi-party computations. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010) (2010)Google Scholar
  10. 10.
    Barthe, G., Fournet, C., Grégoire, B., Strub, P., Swamy, N., Béguelin, S.Z.: Probabilistic relational verification for cryptographic implementations. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20–21 January 2014, pp. 193–206 (2014).  https://doi.org/10.1145/2535838.2535847
  11. 11.
    Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71–90. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22792-9_5CrossRefGoogle Scholar
  12. 12.
    Beaver, D., Micali, S., Rogaway, P.: The round complexity of secure protocols. In: STOC (1990)Google Scholar
  13. 13.
    Bedrock, a coq library for verified low-level programming. http://plv.csail.mit.edu/bedrock/
  14. 14.
    Ben-David, A., Nisan, N., Pinkas, B.: FairplayMP: a system for secure multi-party computation. In: CCS (2008)Google Scholar
  15. 15.
    Bhargavan, K., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.Y.: Implementing TLS with verified cryptographic security. In: IEEE Symposium on Security & Privacy, Oakland, pp. 445–462 (2013). http://www.ieee-security.org/TC/SP2013/papers/4977a445.pdf
  16. 16.
    Bogdanov, D., Jõemets, M., Siim, S., Vaht, M.: How the Estonian Tax and Customs Board Evaluated a tax fraud detection system based on secure multi-party computation. In: Böhme, R., Okamoto, T. (eds.) FC 2015. LNCS, vol. 8975, pp. 227–234. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-47854-7_14CrossRefGoogle Scholar
  17. 17.
    Bogdanov, D., Laur, S., Willemson, J.: Sharemind: a framework for fast privacy-preserving computations. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 192–206. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-88313-5_13CrossRefGoogle Scholar
  18. 18.
    Bogetoft, P., et al.: Secure multiparty computation goes live. In: Dingledine, R., Golle, P. (eds.) FC 2009. LNCS, vol. 5628, pp. 325–343. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-03549-4_20CrossRefGoogle Scholar
  19. 19.
    Büscher, N., Demmler, D., Katzenbeisser, S., Kretzmer, D., Schneider, T.: HyCC: compilation of hybrid protocols for practical secure computation. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018 (2018)Google Scholar
  20. 20.
    Canetti, R.: Security and composition of multiparty cryptographic protocols. J. Cryptol. 13(1), 143–202 (2000).  https://doi.org/10.1007/s001459910006MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Chandran, N., Gupta, D., Rastogi, A., Sharma, R., Tripathi, S.: EzPC: programmable, efficient, and scalable secure two-party computation for machine learning. Cryptology ePrint Archive, Report 2017/1109 (2017). https://eprint.iacr.org/2017/1109
  22. 22.
    Choi, S.G., Hwang, K.W., Katz, J., Malkin, T., Rubenstein, D.: Secure multi-party computation of Boolean circuits with applications to privacy in on-line marketplaces (2011). http://eprint.iacr.org/
  23. 23.
    Crockett, E., Peikert, C., Sharp, C.: Alchemy: a language and compiler for homomorphic encryption made easy. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018 (2018)Google Scholar
  24. 24.
    Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theoret. Comput. Sci. 103(2), 235–271 (1992)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Fromherz, A., Giannarakis, N., Hawblitzel, C., Parno, B., Rastogi, A., Swamy, N.: A verified, efficient embedding of a verifiable assembly language. In: 46th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2019 (2019)Google Scholar
  26. 26.
    Goldreich, O., Micali, S., Wigderson, A.: How to play ANY mental game. In: STOC (1987)Google Scholar
  27. 27.
    Holzer, A., Franz, M., Katzenbeisser, S., Veith, H.: Secure two-party computations in ANSI C. In: CCS (2012)Google Scholar
  28. 28.
    Huang, Y., Evans, D., Katz, J.: Private set intersection: are garbled circuits better than custom protocols? In: NDSS (2012)Google Scholar
  29. 29.
    Huang, Y., Evans, D., Katz, J., Malka, L.: Faster secure two-party computation using garbled circuits. In: USENIX (2011)Google Scholar
  30. 30.
    Juvekar, C., Vaikuntanathan, V., Chandrakasani, A.: GAZELLE: a low latency framework for secure neural network inference. In: USENIX Security 2018 (2018)Google Scholar
  31. 31.
    Kamm, L.: Privacy-preserving statistical analysis using secure multi-party computation. Ph.D. thesis, University of Tartu (2015)Google Scholar
  32. 32.
    Kerschbaum, F.: Automatically optimizing secure computation. In: CCS (2011)Google Scholar
  33. 33.
    Kerschbaum, F., et al.: Secure collaborative supply-chain management. Computer 44(9), 38–43 (2011)CrossRefGoogle Scholar
  34. 34.
    Laud, P., Randmets, J.: A domain-specific language for low-level secure multiparty computation protocols. In: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, CCS 2015 (2015)Google Scholar
  35. 35.
    Launchbury, J., Diatchki, I.S., DuBuisson, T., Adams-Moran, A.: Efficient lookup-table protocol in secure multiparty computation. In: ICFP (2012)Google Scholar
  36. 36.
    Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRefGoogle Scholar
  37. 37.
    Liu, C., Huang, Y., Shi, E., Katz, J., Hicks, M.: Automating efficient RAM-model secure computation. In: IEEE Symposium on Security and Privacy, Oakland (2014)Google Scholar
  38. 38.
    Liu, J., Juuti, M., Lu, Y., Asokan, N.: Oblivious neural network predictions via MiniONN transformations. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017 (2017)Google Scholar
  39. 39.
    Malka, L.: VMCrypt: modular software architecture for scalable secure computation. In: CCS (2011)Google Scholar
  40. 40.
    Malkhi, D., Nisan, N., Pinkas, B., Sella, Y.: Fairplay: a secure two-party computation system. In: USENIX Security (2004)Google Scholar
  41. 41.
    Mardziel, P., Hicks, M., Katz, J., Hammer, M., Rastogi, A., Srivatsa, M.: Knowledge inference for optimizing and enforcing secure computations. In: Proceedings of the Annual Meeting of the US/UK International Technology Alliance (2013)Google Scholar
  42. 42.
    Meijer, E., Beckman, B., Bierman, G.: LINQ: reconciling object, relations and xml in the .net framework. In: Proceedings of the 2006 ACM SIGMOD International Conference on Management of Data, SIGMOD 2006, p. 706. ACM, New York (2006).  https://doi.org/10.1145/1142473.1142552
  43. 43.
    Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991).  https://doi.org/10.1016/0890-5401(91)90052-4MathSciNetCrossRefzbMATHGoogle Scholar
  44. 44.
    Mohassel, P., Zhang, Y.: SecureML: a system for scalable privacy-preserving machine learning. In: IEEE S&P (2017)Google Scholar
  45. 45.
    Mood, B., Gupta, D., Carter, H., Butler, K.R.B., Traynor, P.: Frigate: a validated, extensible, and efficient compiler and interpreter for secure computation. In: IEEE EuroS&P (2016)Google Scholar
  46. 46.
    Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP (2008)Google Scholar
  47. 47.
    Nanevski, A., Morrisett, J.G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Program. 18(5–6), 865–911 (2008). http://ynot.cs.harvard.edu/papers/jfpsep07.pdfMathSciNetCrossRefGoogle Scholar
  48. 48.
    Nielsen, J.D.: Languages for secure multiparty computation and towards strongly typed macros. Ph.D. thesis (2009)Google Scholar
  49. 49.
    Nielsen, J.D., Schwartzbach, M.I.: A domain-specific programming language for secure multiparty computation. In: PLAS (2007)Google Scholar
  50. 50.
    PolarSSL verification kit (2015). http://trust-in-soft.com/polarssl-verification-kit/
  51. 51.
    Protzenko, J., et al.: Verified low-level programming embedded in F* (ICFP) (2017)Google Scholar
  52. 52.
    Rastogi, A., Hammer, M.A., Hicks, M.: Wysteria: a programming language for generic, mixed-mode multiparty computations. In: Proceedings of the 2014 IEEE Symposium on Security and Privacy (2014)Google Scholar
  53. 53.
    Rastogi, A., Mardziel, P., Hammer, M., Hicks, M.: Knowledge inference for optimizing secure multi-party computation. In: PLAS (2013)Google Scholar
  54. 54.
    Rastogi, A., Swamy, N., Hicks, M.: WYS*: a DSL for verified secure multi-party computations (2019). https://arxiv.org/abs/1711.06467
  55. 55.
    Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 174–191. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-37621-7_9CrossRefGoogle Scholar
  56. 56.
    Schropfer, A., Kerschbaum, F., Muller, G.: L1 - an intermediate language for mixed-protocol secure computation. In: COMPSAC (2011)Google Scholar
  57. 57.
    Shamir, A.: How to share a secret. Commun. ACM 22(11), 612–613 (1979)MathSciNetCrossRefGoogle Scholar
  58. 58.
    Shamir, A., Rivest, R.L., Adleman, L.M.: Mental poker. In: Klarner, D.A. (ed.) The Mathematical Gardner, pp. 37–43. Springer, Boston (1981).  https://doi.org/10.1007/978-1-4684-6686-7_5CrossRefGoogle Scholar
  59. 59.
    Swamy, N., et al.: Dependent types and multi-monadic effects in F*. In: POPL (2016)Google Scholar
  60. 60.
    The Coq Development Team: The Coq proof assistant. http://coq.inria.fr
  61. 61.
    VIFF, the virtual ideal functionality framework. http://viff.dk/
  62. 62.
    Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 24–52. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-59451-5_2. http://dl.acm.org/citation.cfm?id=647698.734146CrossRefGoogle Scholar
  63. 63.
    Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010 (2010)Google Scholar
  64. 64.
    Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: Proceedings of ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation (2011)Google Scholar
  65. 65.
    Yao, A.C.C.: How to generate and exchange secrets. In: FOCS (1986)Google Scholar
  66. 66.
    Zahur, S., Evans, D.: Obliv-C: a language for extensible data-oblivious computation. Unpublished (2015). http://oblivc.org/downloads/oblivc.pdf

Copyright information

© The Author(s) 2019

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  1. 1.Microsoft ResearchBangaloreIndia
  2. 2.Microsoft ResearchRedmondUSA
  3. 3.University of MarylandCollege ParkUSA

Personalised recommendations