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].Footnote 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 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 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.Footnote 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

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 mode. In it, a computation is carried out using an MPC protocol among multiple principals. Here is the joint median in \(\textsc {Wys}^\star \):

figure e

The four arguments to 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 and are, respectively, and . The construct indicates that thunk should be run in mode among principals in the set . In this mode, the code has access to the secrets of the principals , which it can reveal using the coercion. As we will see later, the type of ensures that parties cannot each others’ inputs outside mode.Footnote 3 Also note that the code freely uses standard F\(^\star \) library functions like and . 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 function Upon reaching the 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 with

Although 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, mode, supports such mixed-mode computations. The construct states that each principal in should locally execute the thunk , simultaneously; any principal not in the set simply skips the computation. Within , while running in mode, principals may engage in secure computations via .

Here is an optimized version of using :

figure al

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

One might wonder whether the 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 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 ). 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 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 (e.g., using an or an ) only ever access data belonging to ?

  2. 2.

    Is it correct? For example, does correctly compute the median of Alice and Bob’s inputs?

  3. 3.

    Is it secure? For example, do the optimizations in , 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 for computations that use MPC combinators and . Using along with the 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 , 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 monad models the ideal behavior of 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 The 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 or in an context. The trace of a computation records the sequence and nesting structure of outputs of the jointly executed expressions—the result of a computation and its trace constitute its observable behavior. The 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 is a pair of a mode tag (either or ) and a set of principals . A is a forest of trace element ( ) trees. The leaves of the trees record messages that are received as the result of executing an thunk. The tree structure represented by the nodes record the set of principals that are able to observe the messages in the trace .

figure by

Every \(\textsc {Wys}^\star \) computation e has a monadic computation type . The type indicates that e is in the monad (so it may perform multi-party computations); is its result type; is a precondition on the mode in which may be executed; and is a postcondition relating the computation’s mode, its result value, and its trace of observable events. When run in a context with mode satisfying the precondition predicate may produce the trace , and if and when it returns, the result is a -typed value validating . 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 and to the actual implementation and focus instead on specifications of \(\textsc {Wys}^\star \) specific combinators. We describe , , and , 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 in \(\textsc {Wys}^\star \)

figure cr

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

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

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

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

figure ee

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

Defining in \(\textsc {Wys}^\star \)

figure es

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

2.4 Correctness and Security Verification

Using the monad and the type, we can write down precise types for our and 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 . We first define a pure specification of median of two tuples:

figure fn

Further, we capture the preconditions using the following predicate:

figure fo

Using these, we prove the following top-level specification for :

figure fq

This signature establishes that when Alice and Bob simultaneously execute (in mode), with secrets and , then, if and when the protocol terminates, (a) if their inputs satisfy the precondition , 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 thunk in , i.e., it is secure.

Correctness and Security of The security proof of 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 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 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 :

figure gd

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

Using this function, we prove correctness of , thus:

figure gh

The delimited release property is then captured by the following lemma:

figure gi

The lemma proves that for two runs of 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 .

In short, because the 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 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 ), into the \(\textsc {Wys}^\star \) AST as a data structure (in ). Except for the \(\textsc {Wys}^\star \) specific nodes ( , , 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.
figure 1

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

Full size image

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 node, where the interpreter’s back-end compiles , on-the-fly, for particular values of the secrets in ’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., , , list combinators such as , , 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 generating and communicating (XOR-based) secret shares [57] for their secret inputs, and then cooperatively evaluating the boolean circuit for 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 abstraction helps here. Recall that for , the types of the inputs are of the form and . 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.
figure 2

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

Full size image

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 creates a map from principals in \(e_1\) (which is a principal set) to the value computed by \(e_2\). projects the value of principal \(e_1\) from the map \(e_2\), and concatenates the two maps. The maps are used if an 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 \)— 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.
figure 3

Runtime configuration syntax

Full size image
Fig. 4.
figure 4

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

Full size image

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 M; X; L; T; e. 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 and . Our technical report [54] shows other \(\textsc {Wys}^\star \) specific constructs.

Rules S-aspar and S-parret (Fig. 4) reduce an 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 and contains all the principals from the set \(s\). It then pushes a 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 , essentially making observations during the reduction of e (i.e., T) visible only to principals in \(s\).

Turning to , the rule S-assec checks the precondition of the API, and the rule S-assecret generates a trace observation , as per the postcondition of the API. As mentioned before, 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 and shown in Sect. 2.

Fig. 5.
figure 5

Distributed semantics, multi-party rules

Full size image
Fig. 6.
figure 6

Distributed semantics, selected local rules (the mode M is always )

Full size image

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 (P; S) 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 (Fig. 6) to model how a single principal behaves while in 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 . (See technical report [54] for more local evaluation rules.) A principal either participates in the 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 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 —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 , 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 function for this purpose:

figure hk

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 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 . The function is analogous to , but in the opposite direction—it strips off the parts of v that are not accessible to p:

figure hm

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

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 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 function as before. Traces are sliced as follows:

figure hn

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 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 such that 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 .

Now suppose that for a \(\textsc {Wys}^\star \) source program, we prove in F\(^\star \) a postcondition that the result is 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, ’s output will also be n, and for all other principals their outputs will be . 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 in F\(^\star \) and prove that it corresponds to the rules; i.e., that for all input configurations C, \((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 that repeatedly invokes on the AST of the source program (produced by the F\(^\star \) extractor run in a custom mode), unless the AST is an node. Functions and are extracted to OCaml by the standard F\(^\star \) extraction process.

Local evaluation is not defined for the 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 expression, it calls into a circuit library we have written that converts the AST of the second argument of 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 function is essentially a big switch-case on the current expression, that calls into the functions from the semantics specification. The 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 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:

figure hu

Type types the shares of values of type . Our implementation currently supports shares of values only; the 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 and are marked , meaning that they can only be used in specifications for reasoning purposes. In the concrete code, shares are created and combined using the and functions. Together, the specifications of these functions enforce that the shares are created and combined by the same set of parties (through ), and that recovers the original value (through ). The \(\textsc {Wys}^\star \) interpreter transparently handles the low-level details of extracting shares from the GMW implementation of Choi et al. ( ), and reconstituting the shares back ( ).

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 ( is the set of three parties in the computation):

figure ik

The specification says that the function takes two arguments: is the list of secret shares of already dealt cards, and is the secret shares of the newly dealt card. The function returns a boolean that is iff the concrete value ( ) of is different from the concrete values of all the elements of the list . Using F\(^\star \), we verify that the implementation of 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 \):

figure it

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 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 . Instead of naive comparisons, Huang et al. [28] observe that once an element of Alice’s set matches an element of Bob’s set , the inner loop can return immediately, skipping the comparisons of with the rest of Bob’s set. Furthermore, 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 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 (omitted for space reasons), and show that the trace of is precisely .

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

To show that does not reveal more than the intersection of the input sets, we prove the following lemma.

figure ji

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.Footnote 4 We can reason about the traces of 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.Footnote 5 This establishes the security of .

Finally, we can connect to by showing that there exists a function , such that for any trace , the trace of , , can be computed by . 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 . As such, the optimizations do not reveal further information.

5 Related Work

Source 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 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 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 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.

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 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.