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

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 \):

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

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 :

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

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

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 .

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 \)

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:

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 \)

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 .

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:

Further, we capture the preconditions using the following predicate:

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

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 :

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:

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

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.

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.

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.

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.

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.

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:

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:

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.

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:

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:

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

Our confluence result then says:

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

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.

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