Dieses Kapitel vertieft sich in den kritischen Bereich des Datenschutzes in verteilten Anwendungen und konzentriert sich auf die Rolle der sicheren Mehrparteienberechnung (MPC) bei der Gewährleistung von Vertraulichkeit und Integrität. Die Autoren präsentieren einen bahnbrechenden Ansatz, der die Satisfiability Modulo Theory (SMT) nutzt, um die Verifikation von Sicherheitseigenschaften in Low-Level-MPC-Protokollen zu automatisieren. Durch die Entwicklung eines dezidierbaren Typensystems behandelt das Kapitel die Grenzen manueller Korrekturmethoden und früherer automatisierter Ansätze, die häufig mit Skalierbarkeit und Flexibilität zu kämpfen haben. Der Text führt Vertraulichkeits- und Integritätssysteme ein, die durch die SMT-Verifizierung verstärkt werden, was die Durchsetzung von Hypereigenschaften wie die schrittweise Freigabe und robuste Deklassifizierung ermöglicht. Anhand detaillierter Beispiele und Bewertungen zeigen die Autoren die praktischen Vorteile ihres Ansatzes auf, darunter deutliche Leistungsverbesserungen und die Fähigkeit, komplexe Protokolle effizient zu verifizieren. Das Kapitel diskutiert auch die Auswirkungen auf Anwendungen in der realen Welt, wie etwa datenschutzerhaltendes maschinelles Lernen und Blockchain-Technologien, was es zu einer unverzichtbaren Lektüre für jeden macht, der an der Verbesserung der Sicherheit verteilter Systeme interessiert ist.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Secure Multi-Party Computation (MPC) is an important enabling technology for data privacy in modern distributed applications. We develop a new type theory to automatically enforce correctness, confidentiality, and integrity properties of protocols written in the Prelude/Overture language framework. Judgements in the type theory are predicated on SMT verifications in a theory of finite fields, which supports precise and efficient analysis. Our approach is automated, compositional, scalable, and generalizes to arbitrary prime fields for data and key sizes.
1 Introduction
Data privacy is a critical concern in distributed applications including privacy-preserving machine learning [15, 16, 18, 20] and blockchains [12, 14, 21, 30]. Secure multiparty computation (MPC) is a key software-based enabling technology for these applications. MPC protocols provide both confidentiality and integrity properties, formulated as real/ideal (aka simulator) security and universal composability (UC) [11], with well-studied manual proof methods [19]. MPC security semantics has also been reformulated as hyperproperties [3, 13, 28] to support automated language-based proof methods. Recent research in the SMT community has developed theories of finite fields [24] with clear relevance to verification of cryptographic schemes that rely on field arithmetic. The goal of this paper is to combine these two approaches in a decidable type system for verifying correctness and security properties of MPC protocols.
Our focus is on low-level MPC protocols. Previous high-level MPC-enabled languages such as Wysteria [25] and Viaduct [3] are designed to provide effective programming of full applications, and incorporate sophisticated compilation techniques such as orchestration [2] to guarantee high-level security properties. But these approaches rely on libraries of low-level MPC protocols, such as binary and arithmetic circuits. These low-level protocols are probabilistic, encapsulate abstractions such as secret sharing and semi-homomorphic encryption, and are complementary to high-level language design.
Anzeige
1.1 Overview and Contributions
Our work is based on the \( Prelude \)/\( Overture \) framework developed in previous work [28]. The prior work developed the language and semantics, plus two mechanisms for verifying security: an automated approach for protocols in \(\mathbb {F}_2\) (the binary field), based on enumerating all possible executions of the protocol, that scales only to very small protocols; and a manual approach based on a program logic. In Section 2 we recall the \( Overture \) language model and key definitions. In Section 3 we recall formulations of program distributions, and key probabilistic hyperproperties of MPC in \( Overture \).
Together, our contributions automate the verification of security properties in \( Prelude \)/\( Overture \). In this work, we build on [28] by developing automatic verification approaches that work for arbitrary finite fields and scale to large protocols. To accomplish this, we develop new type systems for compositional verification, and use SMT to automate the checks that were accomplished by enumeration in prior work. Specifically, we make the following contributions:
i.
In Section 4, an interpretation of protocols in \( Overture \) as SMT constraints (Theorem 4.2) and methodology for verifying correctness properties.
ii.
In Section 5, a confidentiality type system for \( Overture \) protocols with a soundness property guaranteeing that information is released only through explicit declassifications (Theorem 5.1).
iii.
In Section 6, an integrity type system for \( Overture \) protocols with a soundness property guaranteeing robustness in malicious settings (Theorem 6.1).
iv.
In Section 7, a dependent Hoare type system and algorithm for the \( Prelude \) language that is sound for the confidentiality and integrity type systems (Theorem 7.1), with independently verified, compositional \(\varPi \) types for functions.
In all cases, our type systems are boosted by verification mechanisms provided by Satisfiability Modulo Finite Fields [24]. In Section 8 we develop and discuss evaluation and implementation of the the Goldreich-Micali-Wigderson (GMW) protocol. In an extended version of this paper we also discuss the Bendlin-Damgard-Orland-Zakarias (BDOZ) protocol [29].
1.2 Related Work
The goal of the \( Overture / Prelude \) framework is to automate correctness and security verification of low-level protocols. Other prior work has considered automated verification of high-level protocols and manual verification of low-level protocols.
Anzeige
The most closely related work is [28], where foundations for \( Overture / Prelude \) are introduced including a verification algorithm. However, this algorithm only works for \(\mathbb {F}_2\)– e.g., binary circuits– and does not scale due to exponential complexity, necessitating semi-automated proof techniques. In contrast, our type systems scale to arbitrary prime fields and whole program analysis for larger circuits (protocols). So our work is a significant advancement of \( Overture / Prelude \). Our work is also closely related to Satisfiability Modulo Finite Fields [24] but only in the sense that we apply their method as we discuss in Section 4 and subsequently.
Other low-level languages with probabilistic features for privacy preserving protocols have been proposed. The \(\lambda _{\textrm{obliv}}\) language [9] uses a type system to automatically enforce so-called probabilistic trace obliviousness. But similar to previous work on oblivious data structures [31], obliviousness is related to pure noninterference, not the conditional form related to passive MPC security (Definition 3.8). The Haskell-based security type system in [22] enforces a version of noninterference that is sound for passive security, but does not consider malicious security. And properties of real/ideal passive and malicious security for a probabilistic language have been (manually) formulated in EasyCrypt [13].
Several high-level languages have been developed for writing MPC applications. Previous work on analysis for the SecreC language [4, 6] is concerned with properties of complex MPC circuits, in particular a user-friendly specification and automated enforcement of declassification bounds in programs that use MPC in subprograms. The Wys\(^\star \) language [26], based on Wysteria [25], has similar goals and includes a trace-based semantics for reasoning about the interactions of MPC protocols. Their compiler also guarantees that underlying multi-threaded protocols enforce the single-threaded source language semantics. These two lines of work were focused on passive security. The Viaduct language [3] has a well-developed information flow type system that automatically enforces both confidentiality and integrity through hyperproperties such as robust declassification, in addition to rigorous compilation guarantees through orchestration [2]. However, these high level languages lack probabilistic features and other abstractions of low-level protocols, the implementation and security of which are typically assumed as a selection of library components.
Program logics for probabilistic languages and specifically reasoning about properties such as joint probabilistic independence is also important related work. Probabilistic Separation Logic (PSL) [1] develops a logical framework for reasoning about probabilistic independence (aka separation) in programs, and they consider several (hyper)properties, such as perfect secrecy of one-time-pads and indistinguishability in secret sharing, that are critical to MPC. Lilac [17] extends this line of work with formalisms for conditional independence which is also particularly important for MPC [28].
The Cryptol and SAW tools [10] allow programmers to program security protocols that are verified using SMT. However they are used for cryptographic protocols more generally, and are not designed specifically for MPC as our framework is.
2 \( Overture \) Syntax and Operational Semantics
The \( Overture \) language establishes a basic model of synchronous protocols between a federation of clients exchanging values in the binary field. We identify clients by natural numbers and federations- finite sets of clients- are always given statically. Our threat model assumes a partition of the federation into honestH and corruptC subsets. We model probabilistic programming via a random tape semantics. That is, we will assume that programs can make reference to values chosen from a uniform random distributions defined in the initial program memory. Programs aka protocols execute deterministically given the random tape.
2.1 Syntax
Fig. 1.
Syntax of \( Overture \)
The syntax of \( Overture \), defined in Figure 1, includes values v and standard operations of addition, subtraction, and multiplication in a finite field \(\mathbb {F}_p\) where p is some prime. Protocols are given input secret values \(\texttt {s[}w\texttt {]}\) as well as random samples \(\texttt {r[}w\texttt {]}\) on the input tape, implemented using a memory as described below (Section 2.2) where w is a distinguishing identifier string. Protocols are sequences of assignment commands of three different forms:
\(\texttt {m[}w\texttt {]}\texttt {@}\iota _2 := \varepsilon \texttt {@}\iota _1\): This is a message send where expression \(\varepsilon \) is computed by client \(\iota _1\) and sent to client \(\iota _2\) as message \(\texttt {m[}w\texttt {]}\).
\(\texttt {p[}w\texttt {]} := \varepsilon \texttt {@}\iota \): This is a public reveal where expression \(\varepsilon \) is computed by client \(\iota \) and broadcast to the federation, typically to communicate intermediate results for use in final output computations.
\(\texttt {out}\texttt {@}\iota := \varepsilon \texttt {@}\iota \): This is an output where expression \(\varepsilon \) is computed by client \(\iota \) and reported as its output. As a sanity condition we disallow commands \(\texttt {out}\texttt {@}\iota _1 := \varepsilon \texttt {@}\iota _2\) where \(\iota _1\ne \iota _2\).
The distinction between messages and broadcast public reveal is consistent with previous formulations, e.g., [22]. To identify and distinguish between collections of variables in protocols we introduce the following notation.
Definition 2.1
We let x range over variables which are identifiers where client ownership is specified- e.g., \(\texttt {m[} foo \texttt {]}\texttt {@}\iota \) is a message \( foo \) that was sent to \(\iota \). We let X range over sets of variables, and more specifically, S ranges over sets of secret variables \(\texttt {s[}w\texttt {]}\texttt {@}\iota \), R ranges over sets of random variables \(\texttt {r[}w\texttt {]}\texttt {@}\iota \), M ranges over sets of message variables \(\texttt {m[}w\texttt {]}\texttt {@}\iota \), P ranges over sets of public variables \(\texttt {p[}w\texttt {]}\), and O ranges over sets of output variables \(\texttt {out}\texttt {@}\iota \). Given a program \(\pi \), we write \( iovars (\pi )\) to denote the particular set \(S \cup M \cup P \cup O\) of variables in \(\pi \) and \( secrets (\pi )\) to denote S, and we write \( rands (\pi )\) to denote the particular set R of random samplings in \(\pi \). We write \( vars (\pi )\) to denote \( iovars (\pi ) \cup rands (\pi )\). For any set of variables X and clients I, we write \(X_I\) to denote the subset of X owned by any client \(\iota \in I\), in particular we write \(X_H\) and \(X_C\) to denote the subsets belonging to honest and corrupt parties, respectively.
In all cases we disallow overwriting of variables, since assignment is intended to represent distinct message sends. An example of a \( Overture \) protocol, for additive secret sharing, is discussed in Section 4.2.
2.2 Semantics
Fig. 2.
Semantics of \( Overture \) expressions (T) and programs (B).
Memories are fundamental to the semantics of \( Overture \) and provide random tape and secret inputs to protocols, and also record message sends, public broadcast, and client outputs.
Definition 2.2
Memories \(\sigma \) are finite (partial) mappings from variables x to values \(v \in \mathbb {F}_p\). The domain of a memory is written \(\textrm{dom}(\sigma )\) and is the finite set of variables on which the memory is defined. We write \(\sigma \{ x \mapsto v\}\) for \(x\not \in \textrm{dom}(\sigma )\) to denote the memory \(\sigma '\) such that \(\sigma '(x) = v\) and otherwise \(\sigma '(y) = \sigma (y)\) for all \(y \in \textrm{dom}(\sigma )\). We write \(\sigma \subseteq \sigma '\) iff \(\textrm{dom}(\sigma ) \subseteq \textrm{dom}(\sigma ')\) and \(\sigma (x) = \sigma '(x)\) for all \(x \in \textrm{dom}(\sigma )\). Given any \(\sigma \) and \(\sigma '\) with \(\sigma (x) = \sigma '(x)\) for all \(x \in \textrm{dom}(\sigma ) \cap \textrm{dom}(\sigma ')\), we write \(\sigma \uplus \sigma '\) to denote the memory with domain \(X = \textrm{dom}(\sigma ) \cup \textrm{dom}(\sigma ')\) such that:
In our subsequent presentation we will often want to consider arbitrary memories that range over particular variables and to restrict memories to particular subsets of their domain:
Definition 2.3
Given a set of variables X and memory \(\sigma \), we write \(\sigma _X\) to denote the memory with \(\textrm{dom}(\sigma _X) = X\) and \(\sigma _X(x) = \sigma (x)\) for all \(x \in X\). We define \( mems (X)\) as the set of all memories with domain X:
So for example, the set of all random tapes for a protocol \(\pi \) is \( mems ( rands (\pi ))\), and the memory \(\sigma _{ secrets (\pi )}\) is \(\sigma \) restricted to the secrets in \(\pi \).
Given a variable-free expression \(\varepsilon \), we write \(\llbracket \varepsilon \rrbracket \) to denote the standard interpretation of \(\varepsilon \) in the arithmetic field \(\mathbb {F}_{p}\). With the introduction of variables to expressions, we need to interpret variables with respect to a specific memory, and all variables used in an expression must belong to a specified client. Thus, we denote interpretation of expressions \(\varepsilon \) computed on a client \(\iota \) as \(\llbracket \sigma ,\varepsilon \rrbracket _{\iota }\). This interpretation is defined in Figure 2, along with the big-step reduction relation \(\Rightarrow \) to evaluate commands. Reduction is a mapping from configurations\((\sigma ,\pi )\) to final stores where all three command forms- message send, broadcast, and output- are implemented as updates to the memory \(\sigma \).
Oblivious Transfer A passive secure oblivious transfer (OT) protocol based on previous work [1] can be defined in \( Overture \), albeit assuming some shared randomness. Alternatively, a simple passive secure OT can be defined with the addition of public key cryptography as a primitive. But given the diversity of approaches to OT, we instead assume that OT is abstract with respect to its implementation, and any use is of the form \(\texttt {m[}w\texttt {]}\texttt {@}\iota _1 := \texttt {OT(}\varepsilon _1\texttt {@}\iota _1,\varepsilon _2,\varepsilon _3 \texttt {)}\texttt {@}\iota _2\) – given a choice bit\(\varepsilon _1\) provided by a receiver \(\iota _1\), the sender \(\iota _2\) sends either \(\varepsilon _2\) or \(\varepsilon _3\). Critically, \(\iota _2\) learns nothing about \(\varepsilon _1\) and \(\iota _1\) learns nothing about the unselected value. We return to the formal interpretation of OT in Section 4.
2.3 \( Overture \) Adversarial Semantics
Fig. 3.
Adversarial semantics of \( Overture \).
In the malicious model we assume that corrupt clients are in thrall to an adversary \(\mathcal {A}\) that does not necessarily follow the rules of the protocol. We model this by positing a \( rewrite _{\mathcal {A}}\) function which is given a corrupt memory \(\sigma _C\) and expression \(\varepsilon \), and returns a rewritten expression that can be interpreted to yield a corrupt input. We define the evaluation relation that incorporates the adversary in Figure 3.
A key technical distinction of the malicious setting is that it typically incorporates “abort”. Honest parties implement strategies to detect rule-breaking– aka cheating– by using, e.g., message authentication codes with semi-homomorphic properties as in BDOZ/SPDZ [23]. If cheating is detected, the protocol is aborted. To model this, we extend \( Overture \) with an assert command:
As we will discuss, this form of asserting equality between expressions is sufficient to capture MAC checking and support integrity in protocols. The big-step adversarial semantics relation \(\Rightarrow _{\mathcal {A}}\) is then defined in Figure 3 as a mapping from configurations to a store \(\sigma \) or \(\bot \).
Protocol Runs Our semantics require that random tapes contain values for all program values \(\texttt {r[}w\texttt {]}\texttt {@}\iota \) sampled from a uniform distribution over \(\mathbb {F}_p\). Input memories also contain input secret values and possibly other initial view elements as a result of pre-processing, e.g., Beaver triples for efficient multiplication, and/or MACed share distributions as in BDOZ/SPDZ [11, 23]. We define \( runs (\pi )\) as the set of final memories resulting from execution of \(\pi \) given any initial memory, possibly augmented with a preprocessed memory (a memory that satisfies a predicate \( preproc \)), and \( runs _\mathcal {A}(\pi )\) is the analog in the malicious setting. Since we constrain programs to not overwrite any variable, we are assured that final memories contain both a complete record of all initial secrets as well as views resulting from communicated information. This formulation will be fundamental to our consideration of probability distributions and hyperproperties of protocols.
Definition 2.4
Given \(\pi \) with \( secrets (\pi ) = S\) and \( rands (\pi ) = R\) and predicate \( preproc \) on memories, define:
MPC protocols are intended to implement some ideal functionality\(\mathcal {F}\) with per-client outputs. In the \( Overture \) setting, given a protocol \(\pi \) that implements \(\mathcal {F}\), with \( iovars (\pi ) = S \cup M \cup P \cup O\), the domain of \(\mathcal {F}\) is \( mems (S)\) and its range is \( mems (O)\). Security in the MPC setting means that, given \(\sigma \in mems (S)\), a secure protocol \(\pi \) does not reveal any more information about honest secrets \(\sigma _H\) to parties in C beyond what is implicitly declassified by \(\mathcal {F}(\sigma )\). Security comes in passive and malicious flavors, wherein the adversary either follows the rules or not, respectively. Characterization of both real world protocol execution and simulation is defined probabilistically. In this work we will focus on the enforcement of hyperproperties of passive and malicious security developed in related work [28], that were shown to be sound for real/ideal security properties that are traditionally used for MPC. As in that work we use probability mass functions to express joint dependencies between input and output variables, as a metric of information leakage.
3.1 Probability Mass Functions (pmfs)
Pmfs map realizations of variables in a joint distribution to values in [0..1]. For convenience and following [1, 28] we use memories to represent realizations, so for example given a pmf \(\mathcal {P}\) over variables \(\{ \texttt {s[}x\texttt {]}\texttt {@}1, \texttt {m[}y\texttt {]}\texttt {@}2 \}\) we write \(\mathcal {P}(\{ \texttt {s[}x\texttt {]}\texttt {@}1 \mapsto 0, \texttt {m[}y\texttt {]}\texttt {@}2 \mapsto 1 \})\) to denote the (joint) probability that \(\texttt {s[}x\texttt {]}\texttt {@}1 = 0 \wedge \texttt {m[}y\texttt {]}\texttt {@}2 = 1\). Recall from Section 2.2 that \(\uplus \) denotes the combination of memories, so for example \(\{ \texttt {s[}x\texttt {]}\texttt {@}1 \mapsto 0\} \uplus \{\texttt {m[}y\texttt {]}\texttt {@}2 \mapsto 1 \} = \{ \texttt {s[}x\texttt {]}\texttt {@}1 \mapsto 0, \texttt {m[}y\texttt {]}\texttt {@}2 \mapsto 1 \}\).
Definition 3.1
A probability mass function\(\mathcal {P}\) is a function mapping memories in \( mems (X)\) for given variables X to values in \(\mathbb {R}\) such that:
Now, we can define a notion of marginal and conditional distributions as follows, which are standard for discrete probability mass functions.
Definition 3.2
Given \(\mathcal {P}\) with \(\textrm{dom}(\mathcal {P}) = mems (X_2)\), the marginal distribution of variables \(X_1 \subseteq X_2\) in \(\mathcal {P}\) is denoted \({\mathcal {P}}_{X_1}\) and defined as follows:
Given \(\mathcal {P}\), the conditional distribution of \(X_1\) given \(X_2\) where \(X_1 \cup X_2 \subseteq \textrm{dom}(\mathcal {P})\) and \(X_1 \cap X_2 = \varnothing \) is denoted \(\mathcal {P}_{({X_1}|{X_2})}\) and defined as follows:
We also define some convenient syntactic sugarings. The first will allow us to compare marginal distributions under different realization conditions (as in, e.g., Definition 3.8), the others are standard.
Definition 3.4
Given \(\mathcal {P}\), for all \(\sigma _1 \in mems (X_1)\) and \(\sigma _2 \in mems (X_2)\) define:
As in previous work [1, 9, 17, 28], probabilistic independence, aka separation, is an important concept and we adopt the following standard notation to express conditional and unconditional separation:
Definition 3.5
We write \(\mathcal {P}|X_1 \vdash X_2 * X_3\) iff for all \(\sigma \in mems (X_1 \cup X_2)\) and \(\sigma ' \in mems (X_3)\) we have \(\mathcal {P}(\sigma |\sigma ') = \mathcal {P}(\sigma _{X_1}|\sigma ') * \mathcal {P}(\sigma _{X_2}|\sigma ')\). If \(X_1\) is empty we write \(\mathcal {P} \vdash X_2 * X_3\).
3.2 Basic Distribution of a Protocol
We treat all elements of \( runs (\pi )\) as equally likely. This establishes the basic program distribution that can be marginalized and conditioned to quantify input/output information dependencies.
Definition 3.6
The basic distribution of\(\pi \), written \(\textrm{BD}(\pi )\), is defined such that for all \(\sigma \in mems ( vars (\pi ))\):
For any \(\mathcal {A}\) the basic \(\mathcal {A}\)distribution of\(\pi \), written \(\textrm{BD}(\pi ,\mathcal {A})\), is defined such that for all \(\sigma \in mems ( iovars (\pi ) \cup R)\):
Information about honest secrets can be revealed to corrupt clients through messages sent from honest to corrupt clients, and through publicly broadcast information from honest clients. Dually, corrupt clients can impact protocol integrity through the messages sent from corrupt to honest clients, and through publicly broadcast information from corrupt clients. We call the former corrupt views, and the latter honest views. We let V range over sets of views, i.e., subsets of \(M \cup P\).
Definition 3.7
(Corrupt and Honest Views). We let V range over views which are sets of messages and reveals. Given a program \(\pi \) with \( iovars (\pi ) = S \cup M \cup P \cup O\), define \( views (\pi ) \triangleq M \cup P\), and define \(V_{H \rhd C}\) as the messages and reveals in \(V = M \cup P\) sent from honest to corrupt parties, called corrupt views:
3.4 Hyperproperties of Confidentiality and Integrity
In this section we restate hyperproperties developed in previous work [28]. The reader is referred to that paper for a more thorough discussion of their relation to real/ideal security. In this paper, we leverage that relation to establish security properties in our type system.
Confidentiality Since MPC protocols release some information about secrets through outputs of \(\mathcal {F}\), they do not enjoy strict noninterference. Public reveals and protocol outputs are fundamentally forms of declassification. But the following property of probabilistic noninterference conditioned on output is sound for passive security [28].
Definition 3.8
(Noninterference modulo output). We say that a program \(\pi \) with \( iovars (\pi ) = S \cup V \cup O\) satisfies noninterference modulo output iff for all H and C and \(\sigma _1 \in mems (S_C \cup O)\) and \(\sigma _2 \in mems (V_{H \rhd C})\) we have:
This conditional noninterference property implies that corrupt views give the adversary no better chance of guessing honest secrets than just the output and corrupt inputs do.
In practice, MPC protocols typically satisfy a gradual release property [27], where messages exchanged remain probabilistically separable from secrets, with only declassification events (reveals and outputs) releasing information about honest secrets.
Definition 3.9
Given H, C, a protocol \(\pi \) with \( iovars (\pi ) = S \cup M \cup P \cup O\) satisfies gradual release iff \(\textrm{BD}(\pi ) \vdash M_C * S_H\).
IntegrityIntegrity is an important hyperproperty in security models that admit malicious adversaries. Consistent with formulations in deterministic settings, we define protocol integrity as the preservation of high equivalence (of secrets and views). Intuitively, this property says that any adversarial strategy either “mimics” a passive strategy with some choice of inputs or causes an abort.
Definition 3.10
(Integrity). We say that a protocol \(\pi \) with \( iovars (\pi ) = S \cup V \cup O\) has integrity iff for all H, C, and \(\mathcal {A}\), if \(\sigma \in runs _\mathcal {A}(\pi )\) then there exists \(\sigma ' \in mems (S)\) with \(\sigma _{S_H} = \sigma '_{S_H} \) and:
where \(X \triangleq (V_{H \rhd C}\cup O_H) \cap \textrm{dom}(\sigma )\).
Integrity plus noninterference modulo output implies malicious security in the real/ideal model [28], and integrity plus gradual release is a probabilistic form of robust declassification [27].
4 \( Overture \) Constraint Verification
In previous work it was shown that the semantics of \( Overture \) in \(\mathbb {F}_2\) can be implemented with Datalog [28], which is a form of constraint programming. In this paper we extend this idea to arbitrary prime fields by using a more general form of SMT constraint programming, Satisfiability Modulo Finite Fields [24]. As we will show in subsequent sections, this interpretation supports correctness guarantees, and also static type analyses for enforcing confidentiality and integrity properties.
We introduce the following syntax of SMT-style constraints for \( Overture \):
$$ \begin{array}{rcl} \phi :\,\!:= x \mid \phi +\phi \mid \phi -\phi \mid \phi *\phi \qquad E :\,\!:= \phi \equiv \phi \mid E \wedge E \mid \lnot E \end{array} $$
Note that constraint terms \(\phi \) are similar to expressions \(\varepsilon \) except that \(\phi \) can “cross party lines”. This is needed to express correctness properties– for example, in the Goldreich-Micali-Wigderson (GMW) protocol wire values in circuits are represented by reconstructive shares [11]. If by convention shares of values n are represented by \(\texttt {m[}n\texttt {]}\) on clients, then assuming two clients \(\{ 1,2 \}\) the reconstructed value can be expressed as \(\texttt {m[}n\texttt {]}\texttt {@}1 + \texttt {m[}n\texttt {]}\texttt {@}2\). So, while summing values across clients is disallowed in \( Overture \) protocols, we can express properties of shared values via constraints.
This language of constraints has an obvious direct interpretation in Satisfiability Modulo Finite Fields [24]. We can leverage this to implement a critical entailment property, written \( E _1 \models E _2\). Our entailment relation is based on satisfiability in a standard sense, where we represent models as memories \(\sigma \) (mappings from variables to values).
Definition 4.1
We write \(\sigma \models E \) iff \(\sigma \) satisfies, aka is a model of, \( E \). We write \( E _1 \models E _2\) iff \(\sigma \models E_1\) implies \(\sigma \models E_2\) for all \(\sigma \), and note that this relation is a preorder.
Given this Definition, the following Theorem is well-known and a fundamental technique in SMT to implement our (common) notion of entailment.
Theorem 4.1
\( E _1 \models E _2\) iff \( E _1 \wedge \lnot E _2\) is not satisfiable.
4.2 Programs as Constraint Systems
Fig. 4.
Interpretation of \( Overture \) expressions (T) and programs (B) as constraints
A central idea of our approach is that we can interpret any protocol \(\pi \) as a set of equality constraints (denoted \(\lfloor \pi \rfloor \)) and use an SMT solver to verify properties relevant to correctness, confidentiality, and integrity. Further, we can leverage entailment for tractability– we can use annotations to obtain a weakened precondition for relevant properties. That is, given \(\pi \), program annotations or other cues can be used to find a minimal \( E \) with \(\lfloor \pi \rfloor \models E \) for verifying correctness and security.
The mapping \(\lfloor \cdot \rfloor \) from programs \(\pi \) to constraints is defined in Figure 4. The interpretation of OT is omitted from this figure which is general. For \(\mathbb {F}_2\) (where we allow negation \(\lnot \) of expressions) the interpretation is:
In general we will assume that any preprocessing predicate is defined via a constraint \( E _{ pre }\), i.e., \( preproc (\sigma ) \iff \sigma \models E _{ pre }\) for all \(\sigma \). The correctness of the SMT interpretation of programs is characterized as follows.
Theorem 4.2
\(\sigma \) is a model of \( E _{ pre }\wedge \lfloor \pi \rfloor \) iff \(\sigma \in runs (\pi )\).
Example: Correctness of 3-Party Addition Consider the following 3-party additive secret sharing protocol, where each party generates three additive, information theoretically secure secret shares by subtracting random field values used as one-time-pads. Two shares are communicated to the other clients and one remains local. This technique is information-theoretically secure [11] due to the one-time use of random values– that is, \(< 3\) shares reveal nothing about the secret, but the sum of all three is the secret. Each party publicly reveals the sums all their shares and then outputs the sum of the reveals.
It is well-known that adding or subtracting a sample from a uniform distribution in a finite field yields a value in a uniform distribution, meaning that samples can be used as one-time-pads with perfect secrecy [1, 9]. In our type system for confidentiality, we aim to approximate distributions by tracking which program variables an expression may depend on. But we also want to capture this fundamental mechanism of encryption. As we will show, SMT can be used in this and other contexts to support confidentiality properties of protocols.
For example, given some string y and a message send such as:
we would assign the following type to denote that \(\texttt {m[}w\texttt {]}\texttt {@}1\) is dependent on both \(\texttt {s[}w\texttt {]}\texttt {@}2\) and \(\texttt {r[}w\texttt {]}\texttt {@}2\):
we want the type of \(\texttt {m[}w\texttt {]}\texttt {@}1\) to be an “encrypted” type that is by itself independent of \(\texttt {s[}w\texttt {]}\texttt {@}2\). However, we also want to track the joint dependence of \(\texttt {m[}w\texttt {]}\texttt {@}2\) on \(\texttt {r[}w\texttt {]}\texttt {@}2\) and \(\texttt {s[}w\texttt {]}\texttt {@}2\), in case information about \(\texttt {r[}w\texttt {]}\texttt {@}2\) is subsequently leaked. In short, we assign \(\texttt {m[}w\texttt {]}\texttt {@}1\) a “ciphertext type”, aka a ciphertype:
indicating syntactically that \(\texttt {m[}w\texttt {]}\texttt {@}1\) is an encryption of a value dependent on \(\texttt {s[}w\texttt {]}\texttt {@}2\) with \(\texttt {r[}w\texttt {]}\texttt {@}2\).
Of course, there are other methods for encrypting values in MPC protocols– but we can observe that many are algebraically equivalent to this fundamental schema. For example, in Yao’s Garbled Circuits (YGC) in \(\mathbb {F}_{2}\), the “garbler” represents encrypted wire values as a random sample (for 1) or its negation (for 0), and shares its secret input encoding with the “evaluator” by using it as a selection bit. That is, assuming that client 2 is the garbler and client 1 is the evaluator, we can define:
This allows us to assign the same ciphertype to \(\texttt {m[}w\texttt {]}\texttt {@}1\) as above– that is, \(c(\texttt {r[}w\texttt {]}\texttt {@}2,\{ \texttt {s[}w\texttt {]}\texttt {@}2 \})\). Since this is a one-time-pad scheme, it is also important that we ensure that samples are used at most once for encryption. As in previous work [9] we use type linearity to enforce this.
Fig. 5.
Syntax and Derivation Rules for \( Overture \) Confidentiality Types
The syntax of types \(T\) and type environments \(\varGamma \) are presented in Figure 51. We also define type judgements for expressions and programs by direct interpretation as terms \(\phi \) and constraints \( E \) respectively, via the encoding \(\lfloor \cdot \rfloor \). The Encode rule enforces linearity by requiring that variables used for encryption are added to judgements, and guaranteed to not be used elsewhere via a form of union that ensures disjointness of combined sets:
Definition 5.1
\(R_1;R_2 = R_1 \cup R_2\) if \(R_1 \cap R_2 = \varnothing \) and is otherwise undefined.
The DepTy rule handles all cases and just records the dependencies on variables in the term, a conservative approximation of dependencies. The Send rule records the types of messages, reveals, and outputs in environments, and the Seq rule combines the types of sequenced programs. Given this we define validity of program type judgements as follows.
Definition 5.2
Given preprocessing predicate \( E _{ pre }\) and protocol \(\pi \) we say \(R, E \vdash E _{ pre }\wedge \lfloor \pi \rfloor : \varGamma \) is valid iff it is derivable and \( E _{ pre }\wedge \lfloor \pi \rfloor \models E \).
It is important to note that this presentation of derivations is logical, not algorithmic– in particular it is not syntax-directed due to the Encode rule.
5.1 Detecting Leakage Through Dependencies
Given a valid typing, we can leverage structural type information to conservatively approximate the information accessible by the adversary who has control over all corrupt clients in C given a partitioning H, C. In particular, if the adversary has access to an encrypted value and another value that is dependent on its one-time-pad key– i.e., access to values with types of the forms:
then we can conservatively assume that the adversary can decrypt the value of type \(T\) and thus have access to those values.
In Figure 6 we define derivation rules for the “leakage” judgement \(\varGamma ,C \vdash _{ leak } T\) which intuitively says that given a protocol with type environment \(\varGamma \) and corrupt clients C, the adversary may be able to observe dependencies on values of type \(T\) in their adversarial messages. The real aim of this relation is to determine if \(\varGamma ,C \vdash _{ leak } \{ \texttt {s[}w\texttt {]}\texttt {@}\iota \}\) with \(\iota \in H\)– that is, if the adversary may observe dependencies on honest secrets.
Our main type soundness result combines typing and leakage judgements, and guarantees gradual release of protocols– that is, that adversarial messages reflect no dependencies on honest secrets. Proof details are provided in an extended version of this paper [29].
Theorem 5.1
Given \(\pi \) with \( views (\pi ) = M \cup P\), if \(R, E \vdash E _{ pre }\wedge \lfloor \pi \rfloor : \varGamma \) is valid and for all H, C we have \(\varGamma ,M_C \vdash _{ leak } T\) with T closed and \(S_H \cap T = \varnothing \), then \(\pi \) satisfies gradual release.
Fig. 6.
Dependencies in Views: Derivation Rules
It is important to recall from [28] that gradual release does not imply passive security, since it only concerns adversarial messages, but not public reveals of outputs where dependencies on input secrets can occur even in secure protocols. Nevertheless, gradual release is an important confidentiality property for MPC (and other distributed) protocols.
6 Integrity Types
Our integrity type system is essentially a taint analysis, with machinery to allow consideration of any H, C partitioning. We also include rules to consider MAC codes to prevent cheating. We consider a semi-homomorphic encryption scheme that is used in BDOZ and SPDZ [5, 7, 8, 23] and is applicable to various species of circuits. However other MAC schemes could be considered with a modified derivation rule incorporated with our taint analysis framework. BDOZ/SPDZ assumes a pre-processing phase that distributes shares with MAC codes to clients. This integrates well with pre-processed Beaver Triples to implement malicious secure, and relatively efficient, multiplication [11].
In BDOZ, a field value v is secret shared among 2 clients with accompanying MAC values. Each client \(\iota \) gets a pair of values \((v_\iota ,m_\iota )\), where \(v_\iota \) is a share of v reconstructed by addition, i.e., \(v = \llbracket v_1 +v_2 \rrbracket \), and \(m_\iota \) is a MAC of \(v_\iota \). More precisely, \(m_\iota = k + (k_\varDelta * v_\iota )\) where keysk and \(k_\varDelta \) are known only to \(\iota ' \ne \iota \) and \(k_\varDelta \). The local keyk is unique per MAC, while the global key\(k_\varDelta \) is common to all MACs authenticated by \(\iota '\). This is a semi-homomorphic encryption scheme that supports addition of shares and multiplication of shares by a constant– for more details the reader is referred to Orsini [23]. We note that while we restrict values v, m, and k to the same field in this presentation for simplicity, in general m and k can be in extensions of \(\mathbb {F}_p\).
Fig. 7.
Syntax and derivation rule of \( Overture \) integrity types
As in [28], we use \(\langle \texttt {m[}w\texttt {]} \rangle \) to refer to secret-shared values reconstructed with addition, and by convention each share of \(\langle \texttt {m[}w\texttt {]} \rangle \) is represented as \(\texttt {m[}w\texttt {s}\texttt {]}\texttt {@}\iota \), the MAC of which is represented as a \(\texttt {m[}w\texttt {m}\texttt {]}\texttt {@}\iota \) for all \(\iota \), and each client holds a key \(\texttt {m[}w\texttt {k}\texttt {]}\texttt {@}\iota \) for authentication of the other’s share. Each client also holds a global key \(\texttt {m[}\texttt {delta}\texttt {]}\). For any such share identified by string w, the BDOZ MAC scheme is defined by the equality predicate \(\psi _{ BDOZ }(w)\):
The integrity of values during protocol executions depends on the partitioning H, C, since any value received from a member of C is initially considered to be low integrity. But as for confidentiality types, we want our basic type analysis to be generalizable to arbitrary H, C. So integrity type judgements, defined in Figure 7, are of the form \( E \vdash \pi : \varDelta \), where \( E \) plays a similar role as in confidentiality types, as a possibly weakened expression of algebraic properties of \(\pi \), and environments \(\varDelta \) record dependency information that can be specialized to a given H, C. Integrity environments are ordered lists since order of evaluation is important for tracking integrity– validating low integrity information through MAC checking allows subsequent treatment of it as high integrity, but not before. Note that MAC checking is not a form of endorsement as it is usually defined (as a dual of declassification [27]), since a successful check guarantees no deviation from the protocol.
The typing of protocols depends on a type judgement for expressions of the form \(\vdash _{\iota } \varepsilon : V\), which records messages and reveals V used in the construction of \(\varepsilon \). This source is recorded in \(\varDelta \) for message sends– so for example, for some string w letting:
Given pre-processing predicate \( E _{ pre }\) and protocol \(\pi \), we say \( E \vdash \pi : \varDelta \) is valid iff it is derivable and \( E _{ pre }\wedge \lfloor \pi \rfloor \models E\).
In the above example, note that the environment implicitly records that \(\texttt {p[}w\texttt {]}\) depends on data from client 1, which in turn depends on data from client 2. The rule for MAC checking allows an overwrite of the dependency. We implement a malicious-secure arithmetic circuit that applies this rule in extended version of this paper [29].
Fig. 8.
Assigning integrity labels to variables
6.2 Assigning Integrity Labels
In all cases, we want to determine the integrity level of computed values based on assumed partitionings H, C. In the previous example, we want to say that \(\texttt {p[}w\texttt {]}\) has low integrity if either client 1 or 2 is corrupt. To this end we define security labelings\(\mathcal {L}\) which are mappings from variables x to security levels \(\varsigma \). By default, given a partitioning H, C this labeling maps messages to the integrity level of the owner.
Definition 6.2
Given H, C, define \(\mathcal {L}_{H,C}\) such that \(\mathcal {L}_{H,C}(\texttt {m[}w\texttt {]}\texttt {@}\iota ) = \textrm{High}\) if \(\iota \in H\) and \(\textrm{Low}\) otherwise for all \(\texttt {m[}w\texttt {]}\texttt {@}\iota \).
But the values of messages and reveals may be affected by values sent by other parties, which is recorded in the \(\varDelta \) obtained from its typing. To determine whether this impacts integrity for any given H, C, we apply the inductively defined rewrite relation \(\varDelta \underset{H,C}{\leadsto }\ \mathcal {L}\), axiomatized in Figure 8. The composition of typing and this latter rewriting obtains essentially a traditional taint analysis, modulo MAC checking. Our main type soundness result for integrity is then given as follows. Proof details are given in [29].
Theorem 6.1
Given \( E _{ pre }\) and \(\pi \) with \( iovars (\pi ) = S \cup V \cup O\), if \( E \vdash \pi : \varDelta \) is valid and for all H, C with \(\varDelta \underset{H,C}{\leadsto }\ \mathcal {L}\) we have \(\mathcal {L}(x) = \textrm{High}\) for all \(x \in V_{H \rhd C}\cup O_H\), then \(\pi \) has integrity for all H, C.
7 Compositional Type Verification in \( Prelude \)
The \( Prelude \) language [28] includes structured data and function definitions for defining composable protocol elements at a higher level of abstraction than \( Overture \). The \( Prelude \) language is a metalanguage aka metaprogramming language, where an \( Overture \) protocol is the result of computation. In addition to these declarative benefits of \( Prelude \), component definitions support compositional verification of larger protocols. Separate verification of well-designed components results in confidentiality and integrity properties to be recorded in their types, allowing for significant reduction of SMT verification in whole program analysis, as we illustrate with extended examples in Section 8 and in an extended version of this paper [29].
Fig. 9.
\( Prelude \) syntax.
7.1 Syntax and Semantics
The syntax of \( Prelude \) is defined in Figure 9. It includes a syntax of values \(\nu \) that include client ids \(\iota \), identifier strings w, expressions \(\varepsilon \) in field \(\mathbb {F}_p\), record values, and \( Overture \) variables x. \( Prelude \) expression forms allow dynamic construction of these values. \( Prelude \)instruction forms allow dynamic construction of \( Overture \) protocols \(\pi \) that incorporate expression evaluation. The syntax also supports definitions of functions that compute values \(\nu \) and, as a distinct form, functions that compute protocols \(\pi \). Formally, we consider a complete metaprogram to include both a codebase and a “main” program that uses the codebase. We disallow recursion, mainly to guarantee decidability of type dependence (Section 7.2).
Definition 7.1
A codebase\(\mathcal {C}\) is a list of function declarations. We write \( \mathcal {C}(f) = y_1,\ldots ,y_n,\ e\) if \(f(y_1,\ldots ,y_n) \{ e \} \in \mathcal {C}\), and we write \( \mathcal {C}(f) = y_1,\ldots ,y_n,\ \textbf{c}\) if \(f(y_1,\ldots ,y_n) \{ \textbf{c}\} \in \mathcal {C}\).
Fig. 10.
Semantics of \( Prelude \) expressions.
We define a big-step evaluation relation \(\Rightarrow \) in Figures 10 and 11 for expressions and instructions, respectively. In this definition we write \(e[\nu /y]\) and \(\textbf{c}[\nu /y]\) to denote the substitution of \(\nu \) for free occurrences of y in e or \(\textbf{c}\) respectively. The rules are mostly standard. Note that we do not include an evaluation rule for the form \(\texttt {m[}e\texttt {]}\texttt {@}e\ \texttt {as}\ \breve{\phi }\) which is a type annotation that we assume is erased from programs prior to evaluation. We defer discussion of this form, as well as the syntactic category \(\breve{\phi }\), to the next Section.
Fig. 11.
Semantics of \( Prelude \) instructions.
7.2 Dependent Hoare Type Theory
Our first goal in the \( Prelude \) type theory is to define an algorithmic system that is sound for both confidentiality and integrity typings as defined in Sections 5 and 6. Returning to the YGC secret encoding example in Section 5, note that the key equivalence of the \(\texttt {mux}\) expression with a one-time-pad encryption we observe there is not trivial. To ensure that this sort of equivalence can be picked up by the type system, we introduce an \(\texttt {as}\) annotation form that allows the programmer to provide the needed hint.
Consider the following \(\texttt {encode}\) function definition that generalizes this YGC encoding for any identifier y and sender, receiver pair s, r. The second line in the body is a hint that the message \(\texttt {m[}y\texttt {]}\texttt {@}r\) can be considered equivalent to \(\lnot \texttt {s[}y\texttt {]}\texttt {@}s +\texttt {r[}y\texttt {]}\texttt {@}s\):
This hint can be validated using SMT, and then the syntactic structure of \(\lnot \texttt {s[}y\texttt {]}\texttt {@}s +\texttt {r[}y\texttt {]}\texttt {@}s\) allows its immediate interpretation as a one-time-pad encoding.
Our second goal in the \( Prelude \) type system is to minimize the amount of SMT solving needed for type verification. Returning to the \(\texttt {encode}\) example, type checking in our systems only requires the hint to be verified once, with the guarantee that \(\texttt {encode}\) can be applied anywhere without needing to re-verify the hint in application instances. To verify the hint in \(\texttt {encode}\), we can just choose arbitrary “fresh” values \(w,\iota _1,\iota _2\) for y, s, and r, evaluate \(\texttt {encode}(w,\iota _1,\iota _2) \Rightarrow \pi \), and then verify:
Since \(\texttt {encode}\) is closed, validity is guaranteed for any instance of y, s, and r.
We generalize these benefits of compositional verification by allowing pre- and postcondition annotations on \( Prelude \) functions. For example, consider a GMW-style, 2-party “and-gate” function \(\texttt {andgmw}(x,y,z)\). In this protocol, each party \(\iota \in \{1,2\}\) holds an additive secret share \(\texttt {m[}x\texttt {]}\texttt {@}\iota \) of values identified by x and y, and at the end of the protocol each hold a secret share \(\texttt {m[}z\texttt {]}\texttt {@}\iota \), where:
We provide details of \(\texttt {andgmw}\) and other GMW protocol elements in Section 8. Our point now is that, similarly to the \(\texttt {encode}\) example, we can verify this postcondition once as a correctness property for \(\texttt {andgmw}\), and then integrate instances of it into circuit correctness properties with the guarantee that each instance also holds for any \(\texttt {andgmw}\) gate. Since the program logic of \(\texttt {andgmw}\) is non-trivial, and typical circuits can use up to thousands of gates, this has significant practical benefits by greatly reducing SMT overhead in whole-program analysis.
Fig. 12.
Algorithmic type judgements for \( Overture \).
Overtureexpression type algorithm. A core element of \( Prelude \) type checking is type checking of \( Overture \) expressions. The integrity type system presented in Section 6 is already algorithmic and ready to use. But confidentiality typing presented in Section 5 is not syntax-directed due to the Encode rule. But as described above, by introducing hint annotations we can “coerce” any relevant expression form into the simplest equivalent syntactic form for one-time-pad encoding. Thus, in Figure 12 we present the algorithm for confidentiality type judgements, where we eliminate the need for integrated SMT solving by assuming this sort of casting.
The following Lemma establishes correctness of algorithmic confidentiality type checking, and makes explicit that SMT checking is eliminated in the judgement.
Lemma 7.1
If \(\Vdash \lfloor \phi \rfloor : (R,T)\) then \(R, E \vdash \phi : T\) for any \( E \).
Dependent Hoare types for instructions. Hoare-style types for instructions have the following form:
$$ \{ E _1 \}\ \varGamma ,R \cdot \varDelta \ \{ E _2 \} $$
Here, \( E _1\) and \( E _2\) are the pre- and postconditions respectively, \(\varGamma \) is the confidentiality type environment of the protocol resulting from execution of the instruction, which is sound wrt confidentiality typing, R are the one-time-pads consumed in the confidentiality typing, and \(\varDelta \) is the sound integrity type environment.
Fig. 13.
Evaluation of expressions within types and constraints.
To obtain a more complete type system, and to generalize function typings, we also introduce a form of type dependency, specifically dependence on \( Prelude \) expressions. Dependent \(\varPi \) types have the form:
where \(y_1,\ldots ,y_n\) range over values \(\nu \) and each of \(\breve{ E _1}\) etc. may contain expressions with free occurrences of \(y_1,\ldots ,y_n\)– the syntax of these forms is in Figure 13. These \(\varPi \) types are assigned to functions and instantiated at application points.
For example, here is a valid typing of \(\texttt {encode}\). It says that under any precondition, evaluating \(\texttt {encode}\) results in a cipher type for the encoded message \(\texttt {m[}x\texttt {]}\texttt {@}r\), which consumes the one-time-pad \(\texttt {r[}x\texttt {]}\texttt {@}s\), and the integrity of \(\texttt {m[}x\texttt {]}\texttt {@}r\) is determined by the security level of s. The postcondition expresses the key confidentiality property of \(\texttt {m[}x\texttt {]}\texttt {@}r\), but also may be practically useful for correctness properties since it is a simpler expression form than the \(\texttt {mux}\) form:
A key property of this example and our type system generally is that once the \(\varPi \) type is verified, typing any application of it requires verification of the precondition instance, but not the postcondition instance.
7.3 Algorithmic Type Validity in \( Prelude \)
Fig. 14.
\( Prelude \) type derivation rules for instructions.
We equate types up to evaluation of subexpressions as defined in Figure 13. Since expression evaluation is total we can just evaluate types of closed instructions, which are guaranteed to have closed types, to obtain Hoare typings for instructions. In Figure 14 we define the type derivation rules for \( Prelude \). In the Mesg rule we use algorithmic confidentiality and integrity type checking in a straightforward manner. In the Encode rule, we verify the hint given in the type annotation, and then use it for type checking. In the App rule we verify preconditions of the given function type and instantiate the type and postconditions with the given expression arguments. The Sig rule we specify how to verify \(\varPi \) types for functions. Note that the values \(\nu _1,\ldots ,\nu _n\) chosen to instantiate the function parameters are chosen “fresh”, meaning that any strings and client identifiers occurring as substrings in \(\nu _1,\ldots ,\nu _n\) are unique and not used in any program source code. This ensures generality of verification as demonstrated in an extended version of this paper [29].
Fig. 15.
\( Prelude \) type derivation rules for function definitions.
We allow the programmer to specify a type signature \(\textrm{sig}\) that maps functions in \(\mathcal {C}\) to valid dependent Hoare typings. Define:
Definition 7.2
\(\textrm{sig}\) is verified iff \(f : \textrm{sig}(f)\) is valid for all \(f \in \textrm{dom}(\textrm{sig})\).
In practice, to define \(\textrm{sig}\) the programmer only needs to specify pre- and postconditions, as we illustrate in Section 8 and [29], since the rest of the type is reconstructed by type checking.
The following Theorem establishes our main result, that the \( Prelude \) type checking is sound with respect to both confidentiality and integrity typings. Since these typings imply security hyperproperties of confidentiality and integrity, \( Prelude \) type checking implicitly enforces them. Proof details are given [29].
Theorem 7.1
(Soundness of\( Prelude \)type checking). Given preprocessing predicate \( E _{ pre }\), program \(\textbf{c}\), and verified \(\textrm{sig}\), if the judgement:
$$\vdash \textbf{c} : \{ E _{ pre } \}\ \varGamma ,R \cdot \varDelta \ \{ E \} $$
is derivable then \(\textbf{c}\Rightarrow \pi \) and:
1.
\(R, E \vdash E _{ pre }\wedge \lfloor \pi \rfloor : \varGamma \) is valid.
2.
\( E \vdash \pi : \varDelta \) is valid.
8 Examples and Evaluation
In Section 4 we gave the example of 3-party additive sharing for any field \(\mathbb {F}_{p}\). In Sections 6 and 7.2 we discussed the example of YGC input encoding. Now we consider examples that illustrate the versatility of the \(\text {Encode}\) typing rule for confidentiality and the use of postconditions for correctness. In an extended version of this paper we also exemplify the use of both pre- and postconditions for integrity [29].
To evaluate our system especially regarding performance, using the Satisfiability Modulo Fields theory in cvc5 on an Apple M1 processor, we have verified correctness of additive sharing protocols in fields up to size \(\mathbb {F}_{2^{31} - 1}\) (an approximation of 32-bit integers) which takes \(\sim \)7ms to compute for 3 parties and not significantly more than for, e.g., \(\mathbb {F}_{2}\). We have also verified the semi-homomorphic encryption properties leveraged in the BDOZ circuit library functions defined in [29] in fields up to size \(\mathbb {F}_{2^{31} - 1}\) which take \(\sim \)8ms for the property used for the postcondition of the \(\texttt {mult}\) gate. This is categorically better performance than can be achieved using previous brute-force methods in \(\mathbb {F}_{2}\) [28].
Fig. 16.
2-party GMW circuit library.
GMW Input Encoding and And Gate. In the 2-party GMW protocol [11], another garbled binary circuit protocol, values are encrypted in a manner similar to using secret sharing as described in Sections 4.2 and 6. In our definition of GMW we use the convention that shared values \(\langle \texttt {m[}w\texttt {]} \rangle \) are identified by strings w and encoded as shares \(\texttt {m[}w\texttt {]}\texttt {@}1\) and \(\texttt {m[}w\texttt {]}\texttt {@}2\). Ciphertypes reflect the confidentiality of GMW input encodings as defined in the \(\texttt {encodegmw}\) function in Figure 16. No programmer annotation is needed given the syntax of the function body. More interestingly, the \(\texttt {andgmw}\) gate definition shows how a programmer hint can express the relevant confidentiality property of the output share \(\texttt {m[}z\texttt {]}\texttt {@}2\) on client 2, using the \(\texttt {as}\) casting. The non-trivial equivalence can be verified by SMT once during verification, and subsequently confidentiality is expressed in the dependent type of the function (as for \(\texttt {encode}\)).
Note also that the \(\texttt {andgmw}\) function is decorated with a postcondition that expresses the correctness property of the function. Although not strictly necessary for confidentiality, this annotation can at least help eliminate bugs, and also can be used compositionally for whole-program correctness properties. As for confidentiality hints, this postcondition needs to be verified only once at the point of definition and subsequently is guaranteed to hold for any application.
9 Conclusion and Future Work
In this paper we have defined confidentiality and integrity type systems for the \( Prelude / Overture \) language model. These type systems resemble previous security type systems in probabilistic settings, but their accuracy is boosted by the integral use of SMT verification. Our work significantly improves automation, scalability, and flexibility of static analysis in the \( Prelude / Overture \) as compared to prior work.
We see several promising avenues for future work. Concurrency will be important to capture common MPC idioms such as commitment and circuit optimizations and to consider the UC security model [2, 11]. We also hope to improve our type system to enforce the declassification bounds determined by ideal functionalities, beyond gradual release.
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.
