General-purpose probabilistic proof systems operate on programs expressed as systems of arithmetic constraints-an unfriendly representation. There are two broad approaches in the literature to turning friendlier, high-level programs into constraints suitable for proof systems: direct translation and CPU emulation. Direct translators compile a program into highly optimized constraints; unfortunately, this process requires expressing all possible paths through the program, which results in compile times that scale with the program's runtime rather than its size. In addition, the prover must pay the cost of every possible program path, even those untaken by a given input. In contrast, CPU emulators don't compile programs to constraints; instead, they “execute” those programs, expressed as CPU instructions, on a CPU emulator that is itself expressed as constraints. As a result, this approach can't perform powerful, program-specific optimizations, and may require thousands of constraints where direct translation could use a clever handful. Worse, CPU emulators inherit an impractically expensive program state representation from the CPUs they emulate. This paper presents a compiler and proof system, CoBBL, that combines the benefits of CPU emulation and direct translation: it takes advantage of program-specific optimizations, but doesn't pay for an unnecessary state representation or unexecuted computation. CoBBL outperforms CirC, a state-of-the-art direct translator, by 1-30× on compile time and 26–350 ×on prover time, and outperforms Jolt, a state-of-the-art CPU emulator, on prover time by 1.1-1.8× on Jolt-friendly benchmarks, and up to 100× on other benchmarks.

In recent years, online anonymity has become increasingly important but is under threat due to the challenges of moderating anonymous spaces. A promising cryptographic solution, known as anonymous blocklisting, allows users to post anonymously while still enabling moderation. Moderation via anonymous blocklisting roughly works by requiring that when users post a message they attach a cryptographic proof that they did not author any posts on a “blocklist”. Existing anonymous blocklisting schemes are unfortunately still far from achieving practical performance for large block-lists. This is essentially due to all prior works requiring a user to (cryptographically) reprocess blocklist entries many times. Relatedly, prior works have relatively high verification times and proof sizes. In this work, we introduce ALPACA, the first anonymous blocklisting system with the property that a user only needs to do a constant amount of work per blocklist entry. Thus, our scheme has asymptotically optimal performance. Our scheme is also the first to have verification times and proof sizes that are independent of the number of blocklist entries. Our key technique is a new variant of incrementally verifiable computation (IVC), designed to ensure anonymity. Along the way, we introduce new definitions to formally establish security. On a mid-range laptop, ALPACA's proof generation time is always 6.15 seconds and proof size is 25.6KBs. On a server, the verification time is always 400ms.

Parallel mixing is a common technique for efficiently unlinking messages from their senders' identity. It involves multiple servers arranged in a stratified mix-network (mixnet), each shuffling a fraction of the messages in parallel with others and then relaying them to a subsequent server. By the end of the route through the mixnet's servers, after applying each server's local shuffle, all messages are mixed together, hiding the senders' identities. Unfortunately, parallel mixing is bottlenecked by the busiest server in each mixnet stratum and does not offer a way to ensure load balancing across the servers. Thus, Sybil clients can coordinate to route their messages through one victim server in the middle of the mixnet and subsequent strata, stalling message delivery for everyone and keeping their identities hidden since their messages were already shuffled with those from other clients. This paper presents BalancedMixnet, a new protocol for load balancing clients across the servers in a parallel mix network while ensuring sender anonymity. Our protocol relies on anonymous credentials to ensure clients use a route through the mixnet that is selected uniformly at random and, at the same time, let servers verify that the message is from a valid client and prevent replay attacks. The cost of issuing and validating credentials can be easily amortized across multiple messages from the same client. We implement and evaluate BalancedMixnet, illustrating that the cost of integrating it into a parallel mixnet is modest and provides substantial benefits against Sybil attacks.

Modern secure messaging protocols typically aim to provide deniability. Achieving this requires that convincing cryptographic transcripts can be forged without the involvement of genuine users. In this work, we observe that parties may wish to revoke deniability and avow a conversation after it has taken place. We propose a new protocol called Not-on-the-Record-Yet (NOTRY) which enables users to prove a prior conversation transcript is genuine. As a key building block we propose avowable designated verifier proofs which may be of independent interest. Our implementation in- curs roughly 8× communication and computation overhead over the standard Signal protocol during regular operation. We find it is nonetheless deployable in a realistic setting as key exchanges (the source of the overhead) still complete in just over 1ms on a modern computer. The avowal protocol induces only constant computation and communication performance for the communicating parties and scales linearly in the number of messages avowed for the verifier—in the tens of milliseconds per avowal.

This article discusses the relationship between two frameworks: universal composability ( \(\mathsf{UC}\) ) and robust compilation ( RC ). In cryptography, \(\mathsf{UC}\) is a framework for the specification and analysis of cryptographic protocols with a strong compositionality guarantee: \(\mathsf{UC}\) protocols remain secure even when composed with other protocols. In programming language security, RC is a novel framework for determining secure compilation by proving whether compiled programs are as secure as their source-level counterparts no matter what target-level code they interact with. Presently, these disciplines are studied in isolation, though we argue that there is a deep connection between them and exploring this connection will benefit both research fields. This article formally proves the connection between \(\mathsf{UC}\) and RC and then it explores the benefits of this connection (focussing on perfect, rather than computational \(\mathsf{UC}\) ). For this, this article first identifies which conditions must programming languages fulfil in order to possibly attain \(\mathsf{UC}\) -like composition. Then, it proves \(\mathsf{UC}\) of both an existing and a new commitment protocol as a corollary of the related compilers attaining RC . Finally, it mechanises these proofs in DEEPSEC, obtaining symbolic guarantees that the protocol is indeed \(\mathsf{UC}\) . Our connection lays the groundwork towards a better and deeper understanding of both \(\mathsf{UC}\) and RC , and the benefits we showcase from this connection provide evidence of scalable mechanised proofs for \(\mathsf{UC}\) .

Abstract Zero Knowledge Proofs (ZKPs) are cryptographic protocols by which a prover convinces a verifier of the truth of a statement without revealing any other information. Typically, statements are expressed in a high-level language and then compiled to a low-level representation on which the ZKP operates. Thus,a bug in a ZKP compiler can compromise the statement that the ZK proof is supposed to establish.This paper takes a step towards ZKP compiler correctness by partially verifying afield-blastingcompiler pass, a pass that translates Boolean and bit-vector logic into equivalent operations in a finite field. First, we define correctness for field-blasters and ZKP compilers more generally. Next, we describe the specific field-blaster using a set of encoding rules and define verification conditions for individual rules. Finally, we connect the rules and the correctness definition by showing that if our verification conditions hold, the field-blaster is correct. We have implemented our approach in the CirC ZKP compiler and have proved bounded versions of the corresponding verification conditions. We show that our partially verified field-blaster does not hurt the performance of the compiler or its output; we also report on four bugs uncovered during verification.

We introduce the first practical protocols for fully decentralized sealed-bid auctions using timed commitments. Timed commitments ensure that the auction is finalized fairly even if all participants drop out after posting bids or if n bidders collude to try to learn the nth bidder's bid value. Our protocols rely on a novel non-malleable timed commitment scheme which efficiently supports range proofs to establish that bidders have sufficient funds to cover a hidden bid value. This allows us to penalize users who abandon bids for exactly the bid value, while supporting simultaneous bidding in multiple auctions with a shared collateral pool. Our protocols are concretely efficient and we have implemented them in an Ethereum-compatible smart contract which automatically enforces payment and delivery of an auctioned digital asset.

Many applications in finance and healthcare need access to data from multiple organizations. While these organizations can benefit from computing on their joint datasets, they often cannot share data with each other due to regulatory constraints and business competition. One way mutually distrusting parties can collaborate without sharing their data in the clear is to use secure multiparty computation (MPC). However, MPC’s performance presents a serious obstacle for adoption as it is difficult for users who lack expertise in advanced cryptography to optimize. In this paper, we present Silph, a framework that can automatically compile a program written in a high-level language to an optimized, hybrid MPC protocol that mixes multiple MPC primitives securely and efficiently. Compared to prior works, our compilation speed is improved by up to 30000×. On various database analytics and machine learning workloads, the MPC protocols generated by Silph match or outperform prior work by up to 3.6×.

Cryptographic tools like proof systems, multi-party computation, and fully homomorphic encryption are usually applied to computations expressed as systems of arithmetic constraints. In practice, this means that these applications rely on compilers from high-level programming languages (like C) to such constraints. This compilation task is challenging, but not entirely new: the software verification community has a rich literature on compiling programs to logical constraints (like SAT or SMT). In this work, we show that building shared compiler infrastructure for compiling to constraint representations is possible, because these representations share a common abstraction: stateless, non-uniform, non-deterministic computations that we call existentially quantified circuits, or EQCs. Moreover, we show that this shared infrastructure is useful, because it allows compilers for proof systems to benefit from decades of work on constraint compilation techniques for software verification. To make our approach concrete we create CirC, an infrastructure for building compilers to EQCs. CirC makes it easy to compile to new EQCs: we build support for three, R1CS (used for proof systems), SMT (used for verification and bug-finding), and ILP (used for optimization), in $\approx 2000$ LOC. It’s also easy to extend CirC to support new source languages: we build a feature-complete compiler for a cryptographic language in one week and $\approx 900$ LOC, whereas the reference compiler for the same language took years to write, comprises $\approx 24000$ LOC, and produces worse-performing output than our compiler. Finally, CirC enables novel applications that combine multiple EQCs. For example, we build the first pipeline that (1) automatically identifies bugs in programs, then (2) automatically constructs cryptographic proofs of the bugs’ existence.

We introduce compact certificate schemes, which allow any party to take a large number of signatures on a message M, by many signers of different weights, and compress them to a much shorter certificate. This certificate convinces the verifiers that signers with sufficient total weight signed M, even though the verifier will not see—let alone verify—all of the signatures. Thus, for example, a compact certificate can be used to prove that parties who jointly have a sufficient total account balance have attested to a given block in a blockchain.After defining compact certificates, we demonstrate an effi-cient compact certificate scheme. We then show how to implement such a scheme in a decentralized setting over an unreliable network and in the presence of adversarial parties who wish to disrupt certificate creation. Our evaluation shows that compact certificates are 50–280× smaller and 300–4000 cheaper to verify than a natural baseline approach.

Real-world cryptographic code is often written in a subset of C intended to execute in constant-time, thereby avoiding timing side channel vulnerabilities. This C subset eschews structured programming as we know it: if-statements, looping constructs, and procedural abstractions can leak timing information when handling sensitive data. The resulting obfuscation has led to subtle bugs, even in widely-used high-profile libraries like OpenSSL.

We present a zero-knowledge argument for NP with low communication complexity, low concrete cost for both the prover and the verifier, and no trusted setup, based on standard cryptographic assumptions. Communication is proportional to d log G (for d the depth and G the width of the verifying circuit) plus the square root of the witness size. When applied to batched or data-parallel statements, the prover's runtime is linear and the verifier's is sub-linear in the verifying circuit size, both with good constants. In addition, witness-related communication can be reduced, at the cost of increased verifier runtime, by leveraging a new commitment scheme for multilinear polynomials, which may be of independent interest. These properties represent a new point in the tradeoffs among setup, complexity assumptions, proof size, and computational cost. We apply the Fiat-Shamir heuristic to this argument to produce a zero-knowledge succinct non-interactive argument of knowledge (zkSNARK) in the random oracle model, based on the discrete log assumption, which we call Hyrax. We implement Hyrax and evaluate it against five state-of-the-art baseline systems. Our evaluation shows that, even for modest problem sizes, Hyrax gives smaller proofs than all but the most computationally costly baseline, and that its prover and verifier are each faster than three of the five baselines.

Systems for verifiable outsourcing incur costs for a prover, a verifier, and precomputation; outsourcing makes sense when the combination of these costs is cheaper than not outsourcing. Yet, when prior works impose quantitative thresholds to analyze whether outsourcing is justified, they generally ignore prover costs. Verifiable ASICs (VA)---in which the prover is a custom chip---is the other way around: its cost calculations ignore precomputation.

Internet-of-Things devices often collect and transmit sensitive information like camera footage, health monitoring data, or whether someone is home. These devices protect data in transit with end-to-end encryption, typically using TLS connections between devices and associated cloud services. But these TLS connections also prevent device owners from observing what their own devices are saying about them. Unlike in traditional Internet applications, where the end user controls one end of a connection (e.g., their web browser) and can observe its communication, Internet-of-Things vendors typically control the software in both the device and the cloud. As a result, owners have no way to audit the behavior of their own devices, leaving them little choice but to hope that these devices are transmitting only what they should.

JavaScript, like many high-level languages, relies on runtime systemswritten in low-level C and C++. For example, the Node.js runtime systemgives JavaScript code access to the underlying filesystem, networking, and I/O by implementing utility functions in C++. Since C++'s typesystem, memory model, and execution model differ significantly fromJavaScript's, JavaScript code must call these runtime functions viaintermediate binding layer code that translates type, state, and failure between the two languages. Unfortunately, binding code isboth hard to avoid and hard to get right. This paper describes several types of exploitable errors that bindingcode creates, and develops both a suite of easily-to-build static checkersto detect such errors and a backwards-compatible, low-overhead API toprevent them. We show that binding flaws are a serious security problem byusing our checkers to craft 81 proof-of-concept exploits forsecurity flaws in the binding layers of the Node.js and Chrome, runtimesystems that support hundreds of millions of users. As one practical measure of binding bug severity, we were awarded $6,000 in bounties for just two Chrome bug reports.

This paper presents an architecture for a discrete, high-entropy hardware random number generator. Because it is constructed out of simple hardware components, its operation is transparent and auditable. Using avalanche noise, a non-deterministic physical phenomenon, the circuit is inherently probabilistic and resists adversarial control. Furthermore, because it compares the outputs from two matched noise sources, it rejects environmental disturbances like RF energy and power supply ripple. The resulting hardware produces more than 0.98 bits of entropy per sample, is inexpensive, has a small footprint, and can be disabled to conserve power when not in use.

A manufacturer of custom hardware (ASICs) can undermine the intended execution of that hardware, high-assurance execution thus requires controlling the manufacturing chain. However, a trusted platform might be orders of magnitude worse in performance or price than an advanced, untrusted platform. This paper initiates exploration of an alternative: using verifiable computation (VC), an untrusted ASIC computes proofs of correct execution, which are verified by a trusted processor or ASIC. In contrast to the usual VC setup, here the prover and verifier together must impose less overhead than the alternative of executing directly on the trusted platform. We instantiate this approach by designing and implementing physically realizable, area-efficient, high throughput ASICs (for a prover and verifier), in fully synthesizable Verilog. The system, called Zebra, is based on the CMT and Allspice interactive proof protocols, and required new observations about CMT, careful hardware design, and attention to architectural challenges. For a class of real computations, Zebra meets or exceeds the performance of executing directly on the trusted platform.