Foundations of zkSNARKs

This is an overview of foundational papers relevant to zkSNARKs. It’s mostly based on presentations by Jens Groth at the IC3 Bootcamp at Cornell University in July 2018 and at the 2nd ZKProof Standards workshop in Berkeley, CA in April 2019.

Jens talks about three recurring motifs:

1. Language - what statements can we prove
2. Security - what are our assumptions, unconditional soundness vs. unconditional zero knowledge
3. Efficiency - prover, verifier computation, interaction, setup size, succinctness

The following papers in theoretical computer science/cryptography set the boundaries of what we are working with (note that some papers deal with more than one aspect of ZKPs):

Theory

[GMR85] Goldwasser, Micali, Rackoff [The Knowledge Complexity of Interactive Proof Systems]

• The paper which introduced the notion of interactive proofs, which constitute the most basic primitive underlying all modern zero-knowledge proof and argument systems
• GMR also define zero knowledge within the context of IP, along with notions such as completeness and soundness, which are fundamental for the theory of IP
• As a first use case, the others present zero knowledge interactive proofs for quadratic (non)residuosity

Language

[GMW91] Goldreich, Micali, Wigderson [Proofs that Yield Nothing But their Validity or All Languages in NP have Zero-Knowledge Proofs]

• look at graph 3-coloring problem
• prove that NP-complete languages have proof systems

Security

[GMW91] Goldreich, Micali, Wigderson [Proofs that Yield Nothing But their Validity or All Languages in NP have Zero-Knowledge Proofs]

• one-way functions suffice for computational zero-knowledge

[BC86] Brassard, Crépeau [All-or-Nothing Disclosure of Secrets]

• you can get perfect (unconditional) zero-knowledge as opposed to computational zero-knowledge

[BCC88] Brassard, Chaum, Crépeau [Minimum Disclosure Proofs of Knowledge]

• look at zero-knowledge against unbounded adversaries

Efficiency

[BFM88] Blum, de Santis, Micali, Persiano [Non-interactive Zero-knowledge]

• CRS (common reference string) for non-interactive ZKPs

[Kilian92] Kilian [A note on efficient zero-knowledge proofs and arguments]

• how to get succinct interactive proofs

Pairing-based cryptography

Later on we have some ideas from pairing-based cryptography:

[BGN05] Dan Boneh, Eu-Jin Goh, Kobbi Nissim [Evaluating 2-DNF Formulas on Ciphertexts]

• pairing-based double-homomorphic encryption scheme

Non-interactive zero-knowledge

From there, we can ask, how to get perfect non-interactive zero-knowledge?

[GOS06] Jens Groth, Rafail Ostrovsky, Amit Sahai [Perfect Non-Interactive Zero Knowledge for NP]

• efficient, uses circuit-SAT

[GS08] Jens Groth, Amit Sahai [Efficient Non-Interactive Proof Systems for Bilinear Groups]

• efficient, uses a practical language (R1CS)

[Gro10] Jens Groth [Short pairing-based non-interactive zero-knowledge arguments]

• preprocessing zk-SNARKs
• power knowledge of exponent(KoE) assumption
• universal CRS, works for any circuit

Succinctness

And then, how to get succinctness?

[GW11] Gentry, Wichs [Separating Succinct Non-Interactive Arguments From All Falsifiable Assumptions]

• SNARG = Succinct non-interactive argument
• justifies need for KoE assumption

[BCCT12] Bitansky, Canetti, Chiesa, Tromer [From extractable collision resistance to succinct non-Interactive arguments of knowledge, and back again]

• zk-SNARK
• verifier time polynomial in statement size (ease of verification)

[GGPR13] Gennaro, Gentry, Parno, Raykova [Quadratic Span Programs and Succinct NIZKs without PCPs]

• quadratic span programs, quadratic arithmetic programs
• specialized CRS, tailored to specific circuit

This is a graph of various constructions in this video at 34:00

Implementations

And at this point we begin to see implementations:

[PHGR13] Parno, Gentry, Howell, Raykova [Pinocchio: Nearly Verifiable Practical Computation]

Relating back to the three motifs, Jens talks about the following areas for improvement with regard to each of the three motifs:

1. Language: Pairing-friendly languages, interoperability between languages
2. Security: Setup - multi-crs, mpc-generated, updatable; Formal verification
3. Efficiency: Asymmetric pairings, commit-and-prove

Reference Texts:

• Introduction to Modern Cryptography by Katz, Lindell
• Algebra by M. Artin
• Abstract Algebra by Dummit and Foote
• Introduction To Commutative Algebra, by M. Atiyah and I. Macdonald
• Arithmetic of Elliptic Curves by J. Silverman

ZKP Compiler Pipeline Design

Motivation Question

• The motivating question in defensive ZKP compiler pipeline design is:
  • If most general-purpose applications of ZKPs will require general-purpose programmable privacy, what compiler stack can allow developers to safely write programs and also produce efficient outputs?
• This is the motivating question simply because the things that are many are the programs. Eventually, we’ll have a few proof systems and maybe a few different compiler stacks and those might have some bugs and we’ll need to iron out those bugs and formally verify those parts - but the proof systems and compiler stacks will be relatively small in number compared to the actual programs.
  • Consider comparable examples, such as the Ethereum Virtual Machine (EVM) and the Solidity compiler. Early on in the history of the EVM and Solidity, the EVM and the Solidity compiler both had a lot of bugs, and often, bugs in programs were if not equally likely then at least non-trivially likely to be due to a bug in the compiler or in the EVM as opposed to a bug in the program caused by a developer not thinking about their model or writing the Solidity code correctly.
  • But, over time, as the EVM and Solidity “solidified” and became better understood and more formally modeled in different ways, the frequency of those bugs has declined, in the case of the EVM perhaps to zero and in the case of Solidity to a very low number and to mostly minor ones. Now most of the problems, if you go on Rekt, most bugs nowadays are not bugs in the Solidity compiler or bugs in the EVM but rather bugs in code written by developers - sometimes mistakes caused by the model of the program itself being unclear or wrong (with respect to what the developer probably intended), sometimes mistakes in the use of the Solidity language to express that model, but in both cases the result of an incongruity at the developer level. If you’re interested in preventing bugs, you have to focus on this layer because most of the bugs are written by developers.
• This holds doubly so for programs involving zero-knowledge proof systems (ZKPs) and privacy, because most developers aren’t going to be intricately familiar with the implementation details of zero-knowledge proof systems, and if the compilation stack requires that they understand these details in order to write programs safely, their programs are going to have a lot of bugs. It’s really hard to understand cryptography, especially if you don’t have a deep background in it and especially if you’re writing a complex application at the same time.
• Of course, if you have a very safe compiler stack but it’s not fast enough and the performance costs are too high for actual applications, no one will be any safer because no one will use it. So, the question can be rephrased a wee bit:
  • What compiler stacks can provide the most protection to developers, while also being efficient enough that they will actually be used?

General Constraints

• There are some different constraints in circuit / ZKP compiler design than in the design of ordinary compilers.
  • For one, there are some very specific “threshold latency constraints”, where execution times under a few seconds will be fine but execution times over that will render many applications impossible.
  • In most cases, at least if you want privacy, users have to be creating the proofs, and when users are creating the proofs there’s a really big user experience difference between 3 seconds latency and 9 seconds latency, even though this is only a constant factor of 3.
  • With normal compilers, you might be able to tolerate such small factor differences in the interest of making it easier to write programs (see: Javascript) - if you’re running a spreadsheet tax calculation program, for example, a difference of a factor of 3 may not actually matter that much - the person would just do something else while the program is running as long as they aren’t running it too frequently.
  • With normal compilers you also tend to care about user interaction latency, which has deep implications in compiler design. For example, it means that languages with automatic memory management tend to do incremental garbage collection, which limits garbage collector latency, as opposed to simpler garbage collection algorithms which can cause unpredictable latency spikes.
  • This doesn’t apply when writing circuits to be used in ZKP systems, because all of the interactions are non-interactive with respect to one individual program - the compiler should instead optimize for making the total prover execution time as low as possible.
• Another class of parties who could potentially write bugs are the circuit compiler developers - us! - so it behooves the ecosystem to come up with at least some reusable complements of the compiler stack that can be shared by multiple parties and jointly verified. To that end, the subsequent parts of this post craft a high-level taxonomy of current approaches to circuit compilation and describe their trade-offs.
• This taxonomy categorizes compilation approaches in three broad classes, which are defined and analyzed in order:
  1. DSL approach
  2. ISA/VM approach
  3. Direct approach

DSL Approach

• The first approach and the approach that quite logically the ecosystem started with is herein termed the “DSL approach”.
• DSL stands for “domain-specific language”, and the DSL approach is to take something like R1CS or PLONK or AIR and build a language on top of it, crafting abstractions iteratively in order to simplify the job of the programmer.
• DSL instructions in this sort of a system typically act like constraint-writing macros - some variables can be tracked, there’s some sort of simplified compilation going on, but there’s no intermediate instruction set or abstract machine, and instructions in the DSL translate pretty directly to constraints. Examples of this approach include:
  • Zokrates
  • Circom
  • Snarky
  • Leo
  • Juvix Circuits
  • Cairo (although over time it has gotten closer to an ISA/VM approach)
  • probably many others
• While these languages are quite different, written with different syntaxes and targeting different proof systems, they are all following the same kind of general approach of starting with a low-level constraint system and iteratively adding abstractions on top. With the DSL approach, each program is compiled to its own circuit.
• Advantages of the DSL approach:
  • It’s relatively easy to write a DSL because you can iteratively build abstractions on top of constraints - you don’t need to have a whole separately-defined instruction set or architecture
  • Because you have this low-level control, you can use a DSL as an easier way of writing hand-rolled circuit optimisations - it’s easy to reason about performance when the developer has a good understanding of exactly what constraints each instruction is translated into
• Disadvantages of the DSL approach:
  • DSLs aren’t as capable of high-level abstraction, at least not without more complex compiler passes and semantics more removed from the underlying constraint systems
  • If there are a lot of different DSLs for different proof systems, developers are always going to need the semantics of some proof-system-specific language in order to write circuits, and the semantics of these DSLs are quite different than the semantics of the languages most developers already know
  • If developers are writing programs that include some circuit components and some non-circuit components, those are two different semantics and languages, and the conversions in-between are a likely location for the introduction of bugs
  • Most DSLs don’t built in much of the way of a type system for reasoning about the behavior about programs, so developers who wish to verify that their programs satisfy certain correctness criteria will need to use external tools in order to accomplish this

ISA/VM Approach

• The next compilation approach is termed ISA (instruction set architecture) / VM (virtual machine) compilation. This approach is more involved.
  • ISA/VM compilation requires clearly defining an intermediate virtual machine and instruction set architecture which then intermediates in the compilation pipeline between the high-level languages in which developers are writing programs and the low-level zero-knowledge proof systems with which proofs are being made.
  • Although it is possible to write VM instructions directly, in this approach it is generally assumed that developers won’t (and these VMs are not optimized for developer ergonomics).
• This can be done with an existing instruction set.
  • For example, the Risc0 team has done this with the RISC-V microarchitecture - originally designed for CPUs with no thought given to ZKP systems - but Risc0 has written a STARK prover and verifier for RISC5 which is compatible with the existing specification of the RISC-V ISA.
• This can also be done with a custom-built VM and instruction set designed specifically to be efficient for a particular proof system, and potentially for recursive verification in the VM or some other specific application you might want to support efficiently.
  • For example, the Miden VM is designed to be more efficient to prove and verify in a STARK than an architecture such as RISC5 (which was not designed for this) might be, and the Triton VM has been designed specifically to make recursive proof verification in the VM relatively inexpensive.
• All of these approaches use one circuit for all programs, and support many higher-level languages - the higher-level languages just need to compile to the specified instruction set - and all of these examples are von Neumann architecturestyle machines - so there’s a stack, operations on the stack, some form of memory, storage, I/O, and maybe some co-processors or built-in operations.
• Advantages of the ISA/VM approach:
  • Developers can use higher-level languages which they are either already familiar with or are easier to learn than low-level circuit DSLs
  • In the case of using an existing microarchitecture, such as RISC-V, you can reuse tons of existing tooling - anything which compiles to RISC-V, which is anything which compiles to LLVM, which is almost everything you would care about - can be used with the Risc0 circuit, prover, and verifier
  • Even in the case of a new instruction set architecture, such as with Miden VM and Triton VM, compilation techniques to these kinds of stack-based VMs for both imperative and functional languages are pretty well-known already, and compiler authors can reuse a lot of existing work that is not specific to ZKPs or circuits
• Disadvantages of the ISA/VM approach:

Direct Approach

• The third approach, for lack of a better word, is just referred to here as direct. The basic idea here is to somehow directly compile higher-level programs to circuits.
• Advantages of direct compilation:
• Disadvantages of direct compilation:

Takeaways

• So many compiler options! It’s all a little exhausting - and prompts the question: what might be expected to happen, and where, accordingly, can efforts best be spent right now?
• This is also similar to the structure of cryptographic systems today - if you look at how people implement cryptographic protocols, there’s usually hardware support (after standardization) for specific optimized primitives (hash functions, encryption algorithms), which are tied together in protocols themselves written in higher-level languages which are easier to develop in and reason about.
• Finally, a minor exhortation: agreement on and convergence to specific standard primitives and intermediate interfaces can help facilitate deduplication of work across the ecosystem and an easier learning environment for developers.

Programming Languages