Workshop Details

In this talk I will give an overview of a series of works where we have looked at the problem of formally verifying cryptographic software, including implementations of highly efficient low-level primitives, synthesis of provably secure zero-knowledge protocol implementations and various components in secure multiparty computation software stacks. The talk will cover the different formal verification techniques and tools, lessons learned, and ongoing work.

We show how one can use the EasyCrypt proof assistant to mechanize proofs of security of cryptographic protocols within the universally composable (UC) security framework.  This allows, for the first time, the mechanization of the entire sequence of steps needed for proving simulation-based security in a modular way:

(*) specifying the real protocol and desired ideal functionality;

(*) constructing a simulator and demonstrating its validity, possibly via reduction to hard computational problems;

(*) invoking the universal composition operation and demonstrating that it indeed preserves security.

We work with a variant of UC security in which real protocols, ideal functionalities, adversaries, simulators and environments are represented by modules in the EasyCrypt programming language (as opposed to interactive Turing machines). We formalize a UC message routing system based on hierarchical addresses, and employ an interface module that firewalls the environment from a real protocol/ideal functionality and adversary/simulator.

We illustrate our approach on a recently completed case study involving one-time-pad encryption, where the key comes from Diffie-Hellman key-exchange. We conclude by surveying the lessons learned from our case study, and pointing the way toward future work.

Joint work with Ran Canetti and Mayank Varia.

Homomorphic Encryption is an emerging technology that enables computing on data while the data is encrypted. A major challenge with homomorphic encryption is that it takes extensive expert knowledge to design meaningful and useful programs that are constructed from atomic homomorphic encryption operations. 

In this talk I'll present some preliminary work done by Galois and the New Jersey Institute of Technology to address this challenge. We built an environment for developing homomorphic encryption applications in Julia, a high-level language, the same way as "cleartext'' applications are typically written in Julia. We  achieve this by using symbolic execution to automate the construction of an optimized computation circuit where both the circuit size and multiplicative depth are chosen by the compiler.

Current algorithms for secure multi-party computation (MPC) scale poorly with data size, which makes MPC on "big data" prohibitively slow and inhibits its practical use. In this work, we set out to both address this problem and to, at the same time, make MPC more accessible for data analysts who are unfamiliar with current MPC frameworks.

Many analytics queries can maintain MPC's end to-end security guarantee without using cryptographic MPC techniques for all operations. Conclave is a query compiler that accelerates such queries by transforming them into a combination of data-parallel, local cleartext processing and small MPC steps. When parties trust others with specific subsets of the data, Conclave applies new hybrid MPC-cleartext protocols to run additional steps outside of MPC and improve scalability further.

Our Conclave prototype generates code for cleartext processing in Python and Spark, and for secure MPC using the Sharemind and Obliv-C frameworks. Conclave scales to data sets between three and six orders of magnitude larger than state-of-the-art MPC frameworks support on their own. Thanks to its hybrid protocols and additional optimizations, Conclave also substantially outperforms SMCQL, the most similar existing system.

I discuss our previous and ongoing work on using language-based information flow to capture security requirements in a way that permits automatic transformation into distributed programs employing cryptographic protocols. When confidentiality and integrity requirements are expressed as types in the programming language, a compiler can automatically partition and replicate code and data and to insert appropriate cryptographic protocols where needed.

Secure multi-party computation (MPC) is a cryptographic primitive that enables several parties to compute jointly over their collective private data sets. Over the past decade, a number of general and special-purpose MPC software frameworks have been developed. The designs of these frameworks focus on optimizing commonly used primitives or on providing efficient MPC implementations of specific algorithms. However, they have certain limitations that hinder their adoption (and consequently the adoption of MPC) in practical real-world applications: (1) Many of these frameworks are built using legacy software stacks or domain specific languages that make them difficult to use as part of a larger application. (2) Existing frameworks do not provide easy-to-use abstractions for expressing asymmetries in the roles and capabilities of participating parties. (3) Existing frameworks are often tied to the underlying assumptions that are used to optimize their protocols; customizing them to support a similar set of assumptions, or updating them with new primitives, is non-trivial. (4) Deploying and using MPC applications built with these frameworks requires substantial technical, logistical, and maintenance effort and expertise; detection and recovery from failures during deployment must be done manually.

The JavaScript Implementation of Federated Functionalities (JIFF) is an MPC framework built specifically to address the above concerns. JIFF is built using JavaScript to support MPC applications that run on web and mobile platforms. It supports MPC applications in which parties join and leave the computation dynamically and carry out the computation asynchronously, while providing mechanisms for recovery from network and crash failures. JIFF supports and simplifies designing and deploying arbitrarily asymmetric MPC applications, and is highly customizable to accommodate the idiosyncrasies of deployment scenarios: users have the ability to easily specialize or modify any of the underlying primitives, protocols, preprocessing stages, and assumptions. Thanks to these features and flexibilities, MPC applications written with JIFF can be integrated easily as components within server-client(s) web and mobile applications and server(s)-to-server(s) systems. We used JIFF to implement several MPC libraries and applications spanning data-structures (sorting and searching), machine learning (linear regression and principle component analysis), and relational data workflows (i.e., SQL-like queries). Several of these applications use various levels of asymmetry (e.g., the outsourced, parallelized, or hierarchical MPC models). JIFF has been deployed in real-world privacy-preserving studies on income inequality and on diversity in contracting by large businesses, both in Boston.

We present a new 4-party protocol for secure computation that is secure against a single malicious corruption.  Our protocol requires sending just 1.5 ring elements per party, per gate, which in the special case of Boolean circuits, this amounts to sending 1.5 bits per party, per gate.  This is extremely useful in a setting where many users outsource their computation over large volumes of secret-shared data to a small number of servers. Technically, our key technique can be viewed as a variant of the “dual execution” approach, but, because we rely on four parties instead of two, we can avoid any leakage, achieving the standard notion of malicious security.

The notion of covert security for secure two-party computation serves as a compromise between the traditional semi-honest and malicious security definitions. Roughly, covert security ensures that cheating behavior is detected by the honest party with reasonable probability. It provides more realistic guarantees than semi-honest security with significantly less overhead than is required by malicious security.

The rationale for covert security is that it dissuades cheating by parties that care about their reputation and do not want to risk being caught. Further thought, however, shows that a much stronger disincentive is obtained if the honest party can generate a publicly verifiable certificate of misbehavior when cheating is detected. While the corresponding notion of publicly verifiable covert (PVC) security has been explored, existing PVC protocols are complex and less efficient than the best-known covert protocols, and have impractically large certificates.

We propose a novel PVC protocol that significantly improves on prior work. Our protocol uses only \`\`off-the-shelf'' primitives (in particular, it avoids signed oblivious transfer) and, for deterrence factor 1/2, has only 20-40% overhead (depending on the circuit size and network bandwidth) compared to state-of-the-art semi-honest protocols. Our protocol also has, for the first time, constant-size certificates of cheating (e.g., 354 bytes long at the 128-bit security level).

As our protocol offers strong security guarantees with low overhead, we suggest that it is the best choice for many practical applications of secure two-party computation.

This is joint work with Cheng Hong (Alibaba Group), Jonathan Katz (UMD), Wen-jie Lu (University of Tsukuba) and Xiao Wang (MIT and Boston University).

Since the introduction of secure multiparty computation (MPC) in the '80s, it has been a common practice to consider a broadcast channel when designing MPC protocols. Well-known lower bounds show that the number of rounds of deterministic broadcast protocols must be linear in the number of corrupted parties. The seminal works of Ben-Or and Rabin showed how to overcome these limitations via randomization, igniting the study of protocols over point-to-point channels with emph{probabilistic termination} (PT) and expected constant round complexity. However, absent a rigorous simulation-based definition, the suggested protocols are proven secure in a property-based manner, and therefore guarantee limited, if any, composability.

Composing PT protocols affects the round complexity of the resulting protocol in somewhat unexpected ways. For instance, the expected round complexity of the parallel composition of expected-constant-round protocols might be logarithmic in number of instances. Sequential composition of PT protocol also raises subtle issues since the parties fall out-of-sync and cannot start the protocol at the same round.

In this work, we put forth the first simulation-based treatment of MPC with probabilistic termination in the UC framework and prove a universal composition theorem for PT protocols. Our theorem allows one to compile a protocol using deterministic-termination hybrids into a protocol that uses expected-constant-round subprotocols for emulating these hybrids, preserving the expected round complexity of the calling protocol. We showcase our definitions and compiler by providing the first composable protocols (with simulation-based security proofs) over point-to-point channels for the following primitives: (1) expected-constant-round perfect Byzantine agreement, (2) expected-constant-round perfect parallel broadcast, and (3) MPC with round complexity independent of the number of parties.

We proceed to analyze whether the techniques used for parallel composition of broadcast (which is a privacy-free functionality) can be generalized for composing in parallel arbitrary MPC protocols, and provide both feasibility and infeasibility results. We show an efficient protocol-compiler that outputs a protocol that realizes the parallel composition of $m$ protocols, without increasing the expected round complexity; moreover, the compiler requires only black-box access to the underlying emph{protocols}. Using known techniques, a similar result cannot be achieved given only black-box access to the emph{functionalities} realized by the protocols.

This is a joint work with Sandro Coretti, Juan Garay and Vassilis Zikas.

Signal is a famous secure messaging protocol used by billions of people, by virtue of many secure text messaging applications including Signal itself, WhatsApp, Facebook Messenger, Skype, and Google Allo. At its core it uses the concept of "double ratcheting," where every message is encrypted and authenticated using a fresh symmetric key; it has many attractive properties, such as forward security, post-compromise security, and "immediate (no-delay) decryption," which had never been achieved in combination by prior messaging protocols.

While the formal analysis of the Signal protocol, and ratcheting in general, has attracted a lot of recent attention, we argue that none of the existing analyses is fully satisfactory. To address this problem, we give a clean and general definition of secure messaging, which clearly indicates the types of security we expect, including forward security, post-compromise security, and immediate decryption. We are the first to explicitly formalize and model the immediate decryption property, which implies (among other things) that parties seamlessly recover if a given message is permanently lost---a property not achieved by any of the recent "provable alternatives to Signal." We build a modular "generalized Signal protocol" from the following components: (a) continuous key agreement (CKA), a clean primitive we introduce and which can be easily and generically built from public-key encryption (not just Diffie-Hellman as is done in the current Signal protocol) and roughly models "public-key ratchets;" (b) forward-secure authenticated encryption with associated data (FS-AEAD), which roughly captures "symmetric-key ratchets;" and (c) a two-input hash function that is a pseudorandom function (resp. generator with input) in its first (resp. second) input, which we term PRF-PRNG. As a result, in addition to instantiating our framework in a way resulting in the existing, widely-used Diffie-Hellman based Signal protocol, we can easily get post-quantum security and not rely on random oracles in the analysis.

Joint work with Joël Alwen and Sandro Coretti.  The paper will appear at Eurocrypt 2019, and can be found at https://eprint.iacr.org/2018/1037

Oblivious linear-function evaluation (OLE) is a secure two-party protocol allowing a receiver to learn a linear combination of two field elements held by a sender. Vector OLE (VOLE) extends OLE by allowing the receiver to learn a linear combination of two vectors held by the sender. OLE and VOLE serve as useful building blocks in secure computation of arithmetic circuits, analogous to the roles of oblivious transfer (OT) and string OT for Boolean circuits.

We suggest a new approach for fast generation of pseudo-random instances of VOLE via a deterministic local expansion of a pair of short correlated seeds and no interaction. This provides the first example of compressing a non-trivial and cryptographically useful correlation with good concrete efficiency. Our VOLE generators are based on a combination of function secret sharing (FSS) for multi-point functions and linear codes in which decoding is intractable.

We present several applications of VOLE generators, including efficient secure computation protocols with "silent" preprocessing that only requires a low-communication setup phase and no further interaction.

Joint work with Elette Boyle, Geoffroy Couteau, and Niv Gilboa.  

We study the problem of secure two-party computation of arithmetic circuits. This problem is motivated by privacy-preserving numerical computations, such as ones arising in the context of machine learning training and classification. In this work, we design, optimize, and implement an actively secure protocol for secure two-party arithmetic computation. A distinctive feature of our protocol is that it can make a fully modular black-box use of any passively secure implementation of oblivious linear function evaluation (OLE). OLE is a commonly used primitive for secure arithmetic computation, analogously to the role of oblivious transfer in secure Boolean computation.

For typical circuits, our protocol requires roughly 4 invocations of passively secure OLE per multiplication gate. This significantly improves over the recent TinyOLE protocol (Döttling et al., ACM CCS 2017), which requires 22 invocations of actively secure OLE in general, or 44 invocations of a specific code-based passively secure OLE.

Our protocol follows the high-level approach of the IPS compiler (Ishai et al., CRYPTO 2008, TCC 2009), optimizing it in several ways. In particular, we adapt optimization ideas that were used in the context of the practical zero-knowledge argument system Ligero (Ames et al., ACM CCS 2017) to the more general setting of secure computation, and explore the possibility of boosting efficiency by employing a “leaky” passively secure OLE protocol.

We showcase the efficiency of our protocol by applying it to several useful instances of secure arithmetic computation and provide an implementation. Our benchmarks include a general passive-to-active OLE compiler, authenticated generation of “Beaver triples”, and a system for securely outsourcing neural network classification. The latter is the first actively secure implementation of its kind, strengthening the passive security provided by recent related works (Mohassel and Zhang, IEEE S&P 2017; Juvekar et al., USENIX 2018).

This is joint work with Carmit Hazay, Yuval Ishai and Antonio Marcedone.

The obvious step in building a universal framework is the ability to switch between LSSS (linear secret sharing schemes) when there is a high number of rounds due to many non-linear operations to constant round protocols such as Garbled Circuits (GC). Currently, this can be done efficiently when the parties act semi-honestly (ABY) or with three parties and an honest majority (ABY3).

We provide a new construction for multiparty share conversion resistant against a dishonest majority which is competitive with a weaker adversary such as ABY or ABY3. Our construction (denoted Marbled Circuits) uses LSSS and GC in a generic way and allows to connect the best protocol for dishonest majority for arithmetic circuits with the fastest protocol for garbling boolean circuits. To realize this we introduce a new preprocessing form called daBits - random bits authenticated in both worlds (LSSS and GC). These daBits can also be used in various access structures such as MPC with honest majority and active security.

In this talk we investigate the difficulties we encounter when trying to integrate our share conversion method into a fully-fledged system such as SCALE-MAMBA (S&M). Since S&M supports multiple LSSS with various access structures and connects different types of online phases with their specific preprocessing material it seems to be an ideal candidate for Marbled Circuits.

In the end we argue the case that if the research community focuses on fully integrating the preprocessing material for different protocols then it would become more easier to build complex protocols on top of them. Furthermore, these protocols can be later used by people outside our research bubble we often find ourselves in.

Secure multi-party computation (MPC) is a general cryptographic technique that allows distrusting parties to compute a function of their individual inputs, while only revealing the output of the function. Given the importance, it is crucial that the protocols are specified and implemented correctly. In the programming language community, it has become good practice to use computer proof assistants to verify correctness proofs. In the field of cryptography, EasyCrypt is the state of the art proof assistant. It provides an embedded language for probabilistic programming, together with a specialized logic, embedded into an ambient general purpose higher-order logic. It allows us to conveniently express cryptographic properties. EasyCrypt has been used successfully on many applications, including public-key encryption, signatures, differential privacy, and two-party computation with security against semi-honest adversaries. Here we show for the first time that it can also be used to prove security of MPC against a malicious adversary. We formalize additive and replicated secret sharing schemes and apply them to Maurer’s simple MPC protocol for secure addition and multiplication. Our method extends to general polynomial functions. We follow the insights from EasyCrypt that security proofs can often be reduced to proofs about program equivalence, a topic that is well understood in the verification of programming languages. In particular, we show that for a class of MPC protocols in the passive case the non-interference-based (NI) definition is equivalent to a standard simulation-based security definition. For the active case, we provide a new non-interference based alternative to the usual simulation-based cryptographic definition that is tailored specifically to our protocol.

Joint work with Helene Haagh, Aleksandr Karbyshev, Bas Spitters (Aarhus University) and Pierre-Yves Strub (École Polytechnique).

Many implementations of secure computation use fixed-key AES; this results in substantial performance benefits due to hardware support for AES and the ability to avoid recomputing the AES key schedule. Surveying these implementations, however, we find that most utilize AES in a heuristic fashion; in the best case this leaves a gap in the security proof, but in many cases we show it allows for explicit attacks.

Motivated by this unsatisfactory state of affairs, we initiate a comprehensive study of how to use fixed-key block ciphers for secure computation — in particular for OT extension and circuit garbling — efficiently and securely. Our results provide end-to-end security proofs for implementations of secure-computation protocols based on fixed-key block ciphers (modeled as random permutations). Perhaps surprisingly, at the same time our work also results in noticeable performance improvements over the state-of-the-art.

Work by Chun Guo, Jonathan Katz, Xiao Wang, and Yu Yu.

Reporting sexual assault and harassment is an important and difficult problem that has received increased attention especially since late 2017 when accusations against high-profile individuals led to a viral #MeToo movement outspoken about the widespread prevalence of sexual violence.  A centerpiece of the discussion revolved around the means by which to record and process such accusations.  In this paper we focus on methods of reporting sexual assault in a confidential manner that ensures the privacy of both accuser and accused. Only when a set number of accusations are lodged against the same party will the identities of the accusers and accused be revealed to the appropriate parties. We propose the WhoToo protocol, which utilizes various cryptographic techniques to address the

Tor is a widely popular tool for online privacy. Despite its focus on privacy, Tor benefits from some transparency about the operation of its network. Measurements of Tor help direct its developers, inform its users, and guide policymakers. Existing approaches to making these measurements, including Tor’s current techniques, are limited in the types of measurements that can be made.

We present a system that uses secure multiparty computation protocols to give Tor full power to compute any function of its relays’ observations while keeping the observations themselves private. We show how it scales to Tor’s thousands of relays, tolerates network churn, and provides security depending only on Tor’s core trust assumptions.

We demonstrate how to use our system to compute two broadly-applicable statistics: the median of relay inputs and the cardinality of set union across relays. We implement our protocols and experimentally test their performance in networks like Tor using the Shadow simulator. Our experiment show that, when processing the inputs of 7,000 relays, the system can compute from 36 to 151 median computations per day and from 134 to 533 set union cardinalities per day, depending on the trust assumptions of the network. Thus, the system enables large numbers of complex analytics to be securely computed over the Tor network.

Route recommendation services (e.g. Google maps) have become widespread and incorporate numerous factors (e.g. traffic and road closures) to compute optimal routes. Utilizing these services, however, comes at a cost to user's privacy: the service provider learns the source and destination locations of the user for every query that is submitted. Previous protocols for privacy preserving route recommendation algorithms have been constructed using tools such as garbled circuits and private information retrieval (PIR), but have had large overheads in latency and bandwidth.

In this work, we present an MPC protocol and architecture for route recommendation that guarantees: (1) low latency and bandwidth for user queries (2) scalability with respect to the number of users (3) independence from the underlying route recommendation algorithm. We provide a differential privacy-esque extension to our protocol in order to provide meaningful guarantees against inference attacks. Our protocol extends to other applications of key-value PIR protocols.

This work is implemented using JIFF, an easy to use general-purpose framework for implementing MPC protocols in a contemporary web technology stack."