# SoK: What don’t we know? Understanding Security Vulnerabilities in SNARKs

Stefanos Chaliasos
Imperial College London  Jens Ernstberger
Technical University of Munich  David Theodore
Ethereum Foundation  David Wong
zkSecurity  Mohammad Jahanara
Scroll Foundation  Benjamin Livshits
Imperial College London & Matter Labs

###### Abstract

Zero-knowledge proofs (ZKPs) have evolved from being a theoretical concept
providing privacy and verifiability to having practical, real-world
implementations, with SNARKs (Succinct Non-Interactive Argument of Knowledge)
emerging as one of the most significant innovations. Prior work has mainly
focused on designing more efficient SNARK systems and providing security
proofs for them. Many think of SNARKs as “just math,” implying that what is
proven to be correct and secure _is_ correct in practice. In contrast, this
paper focuses on assessing end-to-end security properties of real-life SNARK
_implementations_. We start by building foundations with a system model and by
establishing threat models and defining adversarial roles for systems that use
SNARKs. Our study encompasses an extensive analysis of 141 actual
vulnerabilities in SNARK implementations, providing a detailed taxonomy to aid
developers and security researchers in understanding the security threats in
systems employing SNARKs. Finally, we evaluate existing defense mechanisms and
offer recommendations for enhancing the security of SNARK-based systems,
paving the way for more robust and reliable implementations in the future.

##  1 Introduction

Zero-Knowledge Proofs (ZKPs) have undergone a remarkable evolution from their
conceptual origins in the realm of complexity theory and cryptography [50, 51]
to their current role as fundamental components that enable a wide array of
practical applications [35]. Originally conceptualized as an interactive
protocol where an untrusted prover could convince a verifier of the
correctness of a computation without revealing any other information (zero-
knowledge) [50], ZKPs have, over the past decade, transitioned from theory to
practical widely used implementation [93, 16, 76, 14, 69, 84, 89, 30].

On the forefront of the practical application of general-purpose ZKPs are
Succinct Non-interactive Argument of Knowledge (SNARKs) [47, 82, 52, 43, 25].
SNARKs are non-interactive protocols that allow the prover to generate a
succinct proof. The proof is efficiently checked by the verifier, while
maintaining three crucial properties: completeness, soundness, and zero-
knowledge. What makes SNARKs particularly appealing is their general-purpose
nature, allowing any computational statement represented as a _circuit_ to be
proven and efficiently verified. Typically, SNARKs are used to prove that for
a given function $f$ and a public input $x$, the prover knows a (private)
witness $w$, such as $f(x,w)=y$. This capability allows SNARKs to be used in
various applications, including ensuring data storage integrity [89],
enhancing privacy in digital asset transfers [69, 93] and program execution
[16, 14], as well as scaling blockchain infrastructure [86, 85, 62, 96]. Their
versatility also extends to non-blockchain uses, such as in secure
communication protocols [92, 107, 64] and in efforts to combat disinformation
[57, 31, 59]. Unfortunately, developing and deploying systems that use SNARKs
safely is a challenging task.

In this paper, we undertake a comprehensive analysis of publicly disclosed
vulnerabilities in SNARK systems. Despite the existence of multiple security
reports affecting such systems, the information tends to be scattered.
Additionally, the complexity of SNARK-based systems and the unique programming
model required for writing ZK circuits make it difficult to obtain a
comprehensive understanding of the prevailing vulnerabilities and overall
security properties of these systems. Traditional taxonomies for software
vulnerabilities do not apply in the case of SNARKs; hence, we provide the
seminal work that addresses this gap by providing a holistic taxonomy that
highlights pitfalls in developing and using SNARKs. Specifically, we analyzed
$141$ vulnerability reports spanning nearly $6$ years, from 2018 until 2024.
Our study spans the entire SNARK stack, encompassing the theoretical
foundations, frameworks used for writing and compiling circuits, circuit
programs, and system deployments. We systematically categorize and investigate
a wide array of vulnerabilities, uncovering multiple insights about the extent
and causes of existing vulnerabilities, and potential mitigations.

Contributions.

  * •

SNARKs system and threat models: We provide the first framework for reasoning
about systems built using SNARKs, analyzing interactions between different
components, defining adversaries and their knowledge, and discussing potential
implementation-level vulnerabilities and their impact.

  * •

Study of vulnerabilities: We present the first systematic study of known
vulnerabilities in systems using SNARKs. We gathered $141$ vulnerabilities
from $107$ audit reports, $16$ vulnerability disclosures, as well as a number
of bug trackers of popular SNARK projects. When it comes to SNARKs, this is
the first study of this scale in the literature. Further, because of the
breadth of our coverage, we believe our findings to be representative of the
entire SNARK space.

  * •

Vulnerabilities taxonomy: We introduce a taxonomy for classifying
vulnerabilities in SNARKs, highlighting unique vulnerabilities and common
pitfalls in the SNARK stack that help researchers and practitioners better
understand important threats in the SNARK ecosystem.

  * •

Analyzing defenses: We analyze the main defense techniques proposed by the
research and practitioner communities and highlight some notable gaps.

Key Findings. We find that developers seem to struggle in correctly
implementing arithmetic circuits that are free of vulnerabilities, especially
due to most tools exposing a low-level programming interface that can easily
lead to misuse without extensive domain knowledge in cryptography. In detail,
we find the following flaws to be most pressing: _(i)_ Implementation bugs
across SNARK systems’ layers, including classic vulnerabilities like input
validation errors and over/underflows. These can undermine SNARKs’ core
properties: completeness, soundness, and zero-knowledge. _(ii)_ The unique
programming model for SNARK circuits poses challenges, often leading to under-
constrained circuits. This category emerges from overlooking constraints or
misinterpreting logic into circuits. The low-level nature of SNARK Domain
Specific Languages (DSLs), such as Circom, exacerbates vulnerabilities due to
a lack of common high-level programming features such as basic types. _(iii)_
Design and implementation errors in proof systems are critical yet often
overlooked vulnerabilities. These errors may originate from the frameworks
implementing the proof systems, like an implementation error in Gnark’s Plonk
verifier, or from the theoretical foundations themselves. An example is the
“Frozen Heart” vulnerability, attributed to incomplete descriptions in the
original proof system papers, leading to significant implementation errors
[75].

It is important to highlight that ZK systems are _not_ “just math” — they are
complex, “compositional” systems where cross-layer interactions can introduce
complex vulnerabilities. This paper attempts to cover the entire gamut of
erroneous possibilities in the ZKP space.

##  2 Background on SNARKs

A ZKP enables an entity to prove that a statement is true, without disclosing
anything besides the veracity of the statement. A ZKP is termed a ZK-SNARK if
the proof size and verification time are sublinear in the statement to be
proven, the communication between prover and verifier is non-interactive, and
security holds against a computationally bounded prover. Common ZK-SNARKs are
targeting the problem of circuit satisfiability, where the statement is
represented as an arithmetic circuit. Hence, general-purpose SNARKs prove a
fixed NP relation $\mathfrak{R}$, and allow the prover to convince a verifier
that for the public input $x$ they know a witness $w$ such that
$(x,w)\in\mathfrak{R}$. _Pre-processing SNARKs_ [25], which are the focus of
this work, additionally introduce a _setup_ phase that encodes the relation
being proven into a succinct representation.

In summary, a SNARK is composed of three algorithms:

$\textit{Setup}(pp)\rightarrow(pk,vk)$. Given public parameters $pp$ as input,
output proving and verification keys $pk$ and $vk$.

$\textit{Prove}(pk,x,w)\rightarrow\pi$. Given the proving key $pk$, the public
input $x$, and the witness $w$, output a proof $\pi$.

$\textit{Verify}(vk,x,\pi)\rightarrow\\{0,1\\}$. Given the verification key
$vk$, the public input $x$, and the proof $\pi$, output $1$ if the proof is
valid and $0$ otherwise.

A ZK-SNARK satisfies the following security properties:

Knowledge Soundness.  A dishonest prover cannot convince the verifier of an
invalid statement, except with negligible probability.

Perfect Completeness.  An honest prover can always convince the verifier of
the veracity of a valid statement.

Zero Knowledge.  The proof $\pi$ reveals nothing about the witness $w$, beyond
its existence.

For an in-depth introduction of ZKPs and SNARKs from a theoretical
perspective, we refer the reader to [99].

##  3 System and Threat Models for SNARKs

We introduce a four-layer system model, showing how SNARKs are implemented in
practice. Based on our system model, we provide a holistic threat model
defining SNARK vulnerabilities, adversaries, and their potential impact.

Figure 1: System model of an application based on SNARKs. Note that witness
generation can sometimes be produced by the compiler, while at other times it
may be integrated into the backend.

###  3.1 System Model

Figure 1 depicts the system architecture of an application based on SNARKs for
circuit satisfiability, i.e., argument systems that let the prover show that
given a public input $x$, it knows a witness $w$ such that the circuit
satisfies $\mathcal{C}(x,w)=y$. In our system model, we refer to four distinct
layers. First, the developer specifies the circuit in the Circuit Layer,
according to the specification of the statement to be proven. The Frontend
Layer enables the compilation of the circuit to a SNARK-friendly
representation. The Backend Layer consumes this representation, and provides
the concrete implementation of the proof system. The Integration Layer is the
application logic that interacts with the proof system. We proceed to
introduce the key components in each layer.

_(i)_ Circuit Layer.  SNARKs targeting circuit satisfiability require the
computational statement to be represented as an arithmetic circuit. Most
SNARKs work over elements in a finite field $\mathbb{F}_{p}$, and hence each
wire in the arithmetic circuit is represented as an element in
$\mathbb{F}_{p}$. Note, that there are also SNARKs employing Ring arithmetic
[45], with the purpose of achieving more efficient operations over
$\mathbb{Z}_{2^{64}}$ to match native execution on standard CPUs. When
developing a ZK system, there are several considerations at different levels
of the stack that must be taken into account by developers: _(i)_ determining
what inputs and outputs of the computation are exposed publicly, _(ii)_
encoding the application logic as an arithmetic circuit in $\mathbb{F}_{p}$,
and _(iii)_ specifying how applications should compose with the circuit (e.g.
by ensuring that public inputs are well-formed before verifying a proof).
Specifying circuits correctly is unintuitive, as arithmetic circuits do not
natively support non-arithmetic operations. Moreover, developers face
challenges in translating conventional programming logic into circuit formats
while simultaneously addressing the dual requirements of value assignment for
witnesses and applying constraints to check the validity of solutions. The
prover is responsible for assigning these values (i.e., witness assignments in
the circuit), but the verifier has to check that these assignments adhere to
the constraints (i.e., constraints in the circuit). Crucially, developers must
remember that a malicious prover might manipulate witness values, bypassing
circuit logic. Therefore, it is vital to rigorously constrain the witness
within the circuit to only validate legitimate solutions. If the constraints
are not sound, then there is the risk of exploitation (see Section 5). For
example, expressing $X\neq 0$ is trivial in a “normal” programming language,
whereas encoding it in a custom circuit is non-trivial. By Fermat’s Little
Theorem, one can check $X^{p-1}=1$, but this would cost $O(logp)$ constraints
[77]. An alternative is to have the prover provide a hint $H=X^{-1}$, the
multiplicative inverse of $X$, to check $X\cdot H=1$. Since all nonzero
elements in $\mathbb{F}_{p}$ have a multiplicative inverse, this constrains
$X$ to be nonzero by deduction [60]. We provide a concrete example of a
circuit leveraging a hint in gnark for efficiently computing the square root
in Figure 2. In practice, developer tools employ differing approaches to ease
circuit specification in high-level programming interfaces:

type Circuit struct {
X frontend.Variable `gnark:",private"`
C frontend.Variable `gnark:",public"`
Y frontend.Variable `gnark:",public"`
}
func (circuit *Circuit) Define(api frontend.API) error {
outputs := api.Compiler().NewHint(hint.SqrtHint, 1, circuit.X)
squareRoot := outputs[0]
api.AssertIsEqual(api.Mul(squareRoot, squareRoot), circuit.X)
result := api.Mul(squareRoot, circuit.Const)
api.AssertIsEqual(circuit.Y, result)
return nil
}

Figure 2:  Example circuit written in the eDSL gnark [15]. Lines highlighted
in gray add constraints in the circuit.

Circuit Domain Specific Languages.  Domain Specific Languages (DSLs) are
specialized programming languages designed to address specific problem
domains. In the case of SNARKs, they offer a tailored syntax to efficiently
express constraints in an arithmetic circuit [82, 32, 27, 77, 10, 1]. Learning
a DSL might be challenging, especially for developers not familiar with
SNARKs.

Circuit Embedded Domain Specific Languages.  An Embedded Domain Specific
Language (eDSL) is a type of domain-specific language that is embedded within
a host general-purpose programming language. For developing SNARKs, several
eDSLs have emerged in recent years, embedded as libraries in Golang [15], Rust
[106, 36, 3, 88, 109], TypeScript [73], C++ [94] and Java [60]. eDSLs can
seamlessly interact with other code written in the host language, allowing
easy integration with existing libraries. At the same time, they require
developers to actively distinguish between in-circuit and out-of-circuit
operations, which requires domain expertise to ensure correct implementation.

ZK Virtual Machines.  Circuit DSLs and eDSLs allow developers to specify
circuits in a manner similar to application-specific integrated circuits
(ASIC). Zero-Knowledge Virtual Machines (ZK-VMs) follow a different
programming model, where the arithmetic circuit represents the loop of
fetching instructions from memory and successively executing them (similar to
the fetch-decode-execute cycle as observed in a general-purpose CPU). Common
ZK-VMs target existing Instruction Set Architectures [96, 86, 62, 17, 4]. For
example, ZK-EVMs target the primitive instructions (i.e., “opcodes”) of the
Ethereum Virtual Machine [96, 86, 62], and RISC Zero [17] and Jolt [4] operate
on the RISC-V instruction set. Similarly, there are ZK-VMs for custom ISAs
that are optimized for proving in a SNARK [85, 49]. Some ZK-VMs, such as the
Cairo ZK-VM [49], provide a DSL to specify programs for the ZK-VM. ZK-VMs can
be beneficial as they operate on existing instruction sets and can leverage
existing tooling. Writing circuits directly, while more error-prone, can be
more efficient due to access to low-level optimizations.

_(ii)_ Frontend Layer:  The frontend of a SNARK for circuit-satisfiability
compiles the high-level program written by the developer to a representation
(i.e., arithmetization) which is amenable for the proof system in a backend.
Frontends are agnostic to proof systems, as in they can provide a compilation
of high-level programs to differing arithmetizations. At runtime, the frontend
assigns all intermediate wires in the circuit in order to generate the public
and private parts of the witness. We introduce the components in detail as
follows:

Arithmetization.  An arithmetization is a representation of the constraint
system in a mathematical form, typically a set of algebraic equations, that
can be efficiently processed by the argument system, i.e., the backend of a
SNARK. Common arithmetizations include rank-1 constraint systems (R1CS) [47],
variations of Plonkish arithmetization [43], Arithmetic Intermediate
Representations (AIR) [12] and Customizable Constraint Systems (CCS) [97].
Different arithmetizations result in a different cost profile for the
respective proof system that relies on them, and notably, they introduce
different limitations with respect to how the circuit is defined. For example,
R1CS does not support constraints that have a polynomial degree larger than
two, and AIR requires circuits to be uniform. Notably, Setty et al. provided
CCS, a constraint system that generalizes Plonkish, AIR, and R1CS
arithmetizations [97].

Circuit Compiler.  The circuit compiler in a SNARK implementation compiles the
circuit specified in a high-level DSL or eDSL to the respective
arithmetization. Note, that not all compilers target the compilation of high-
level languages to specific arithmetizations. For example, high-level programs
can first be compiled to VampIR [2] and ACIR [72], which are intermediate
representations that allow compilation to, e.g., R1CS or some form of Plonkish
arithmetization and aim to ease the support of multiple backends. Similarly,
zkLLVM provides a compiler from the LLVM IR to different arithmetizations,
allowing users to prove the execution of, e.g., native Rust, Golang, or C++
[40].

Witness Generation.  The main task of the witness generator is to calculate
the intermediate wires for a given circuit $\mathcal{C}$, given the assignment
of public and private inputs. Note that the concept of a separate witness
generator is not necessarily implemented by every frontend. Often, the circuit
code can be executed to either produce constraints at compile time (e.g., the
line highlighted in grey in Figure 2) or to produce witness values at
runtime/proving (e.g., the hint in Figure 2). When an auxiliary “witness
generator” exists, instructions are generated on how to fill a symbolic
witness table and the witness generator is a binary generated at compile time.

_(iii)_ Backend Layer.  Given the arithmetic circuit and witness, the backend
specifies the algorithmic implementation of proof systems (e.g., Groth16 [52],
Plonk [43], Stark [12], Marlin [25]). At a high level, the backend algorithms
follow the API as in Section 2.

Setup.  In pre-processing SNARKs, the setup algorithm generates the prover and
verifier keys ($pk$ and $vk$) by encoding the circuit relation, with the
primary goal of succinct verification and optimized proving. However,
different SNARKs have vastly differing properties with regard to trust
assumptions, which in turn also impact their performance. Some SNARKs require
a trusted setup, i.e., a randomized setup phase that introduces a trapdoor
either per circuit (i.e., non-universal) [52] or in a universal setup phase
[43]. The randomized part of the setup involves public parameters and random
input to generate a common reference string (CRS) [71], which can be used to
derive $pk$ and $vk$ in the deterministic part of the setup for a concrete
circuit instantiation. The trapdoor needs to be discarded after the setup
proccess is done, as anyone who has knowledge of the trapdoor can forge
proofs. SNARKs that do not employ a trapdoor in the setup phase are commonly
coined transparent [106, 12]. Note, that this introduces a trade-off in
verifier efficiency — transparent SNARKs only have poly-logarithmic-time
verification as compared to constant-time for SNARKs with trusted setup [99].

Prover & Verifier.  The prover consumes the values generated by the frontend,
where the circuit is represented in a specific arithmetization. At a high
level, the prover of a pre-processing SNARK (aside from Groth16 [52]) utilizes
a polynomial commitment to commit to the satisfying witness, and successively
engages with the verifier in an interactive protocol to evaluate the
correctness of assignments with regard to the circuit relation. This “recipe”
leads to a SNARK if the verifier is public-coin [83], and the prover can hash
the transcript of the interactive proof to render the protocol non-interactive
(a process commonly denoted as applying the “Fiat-Shamir heuristic”).
Different proof systems choose different combinations of polynomial
commitments and interactive proofs, resulting in differing properties for the
respective target applications. The most popular approaches include Plonk
[43], which employs a constant-round polynomial interactive oracle proof (IOP)
with the KZG commitment [58]. Halo2 [106] uses the Plonk IOP with the
Bulletproofs polynomial commitment[18]. Another class of protocol combines a
polynomial commitment base on Merkle hashes with a low-degree test, resulting
in a protocol that does not demand for a trusted setup or operations in
elliptic curve groups [11], at the cost of non-constant verification and a
larger proof size [34]. Plonky2 [88] uses the FRI-based polynomial commitment
scheme and combines it with the Plonk IOP. Groth16 [52], the SNARK with the
shortest proof size, is based on probabilistically checkable proofs (PCP) [47]
and pairings over elliptic curves for proof verification. For an in-depth
taxonomy, we refer readers to [99]. Some applications leverage one of the
above SNARKs without the zero-knowledge property, solely relying on non-
interactivity and succinctness (e.g zk-EVMs [96, 86]). In most SNARKs, zero-
knowledge can be obtained cheaply with minor modifications.

_(iv)_ Integration Layer.  In our system model, we collectively term any
application-specific implementation that doesn’t directly relate to the
circuit layer, frontend layer, or backend layer, the integration layer. This
includes source code interacting with any of the other layers, application
logic that may impact the overall security of employing SNARKs, as well as
composition and aggregation of proofs.

Code Interacting with SNARK Components. A SNARK application requires code that
interacts with the functions exposed by the prior layers. Typically,
developers use Solidity, JavaScript, or any other language to perform API
calls to the frontend or backend. For performance reasons, many applications
reduce circuits to their minimal size to fulfill a specific functionality,
outsourcing operations, like range-checks for certain input values, to native
application code.

Complementary ZKP Logic. An application might employ complementary logic
beyond the SNARK itself to ensure its security properties. For example,
nullifiers are commonly used as private values that “nullify” a specific
object upon its use to ensure that specific operations are only executed once.
Consider the use of nullifiers in Tornado Cash [84]. A user deposits a token
in a smart contract and associates a secret nullifier with it. When a user
wants to withdraw, the contract checks that the nullifier has not been used
before to prevent double-spending. The user additionally generates a SNARK
proof, which proves that the nullifier is associated with a deposit, without
revealing the exact deposit to achieve anonymity.

Proof Delegation, Aggregation, Recursion & Composition.  In some applications,
proofs can be too computationally expensive to be generated on end-user
devices. To achieve proof generation on computationally restricted devices,
one may delegate the proof generation to an untrusted party [67]. Similarly,
one may require a fast prover (linear in the size of the statement) and a fast
verifier (constant in the size of the circuit). In this case, common projects
employ a recursive composition of proofs, i.e., they first leverage a SNARK
with a fast prover and successively prove the verification in a SNARK with a
fast verifier. For example, Polygon ZK-EVM [86] composes a FRI-based SNARK
with a Groth16 to obtain the succinct proof size and verification for cheap
verification of proofs in a smart contract, whilst benefiting from the faster
prover time and decreased size of the reference string required for Groth16.
Note that in this case, the trust assumption reduces to the weakest component,
i.e., Groth16 still requires a trusted setup. There are several other works
that employ a similar strategy to obtain efficient SNARK constructions through
aggregation or recursive composition [61, 44, 103, 91, 104, 33].

###  3.2 Threat Model Taxonomy

We consider any usage of a SNARK that violates the intended behavior of one of
the previously discussed layers as a SNARK vulnerability. In this section, we
first define the scope of vulnerabilities at each layer, outline the roles an
adversary can take that may lead to a specific adversarial impact throughout
our system model.

Scope of Vulnerabilities.  In the _(i)_ circuit layer, vulnerabilities may
result from coding mistakes on the implementation of circuits that can lead to
having inconsistent or weak constraints that break the soundness and/or
completeness of the system. A primary reason for this is mistranslation due to
developers not being used to writing in a differing programming model that
introduces surprising pitfalls. In the circuit layer, we exclude logic bugs
that are not necessarily associated with writing SNARK circuits, and focus on
issues that arise from the use of SNARK software specifically. In the _(ii)_
frontend layer, vulnerabilities may primarily arise due to bugs in compiling
from high-level source code to a specific arithmetization. In the _(iii)_
backend layer, vulnerabilities may occur in the prover, where adversarial
provers attempt proof forgery. For SNARKs requiring a trusted setup,
applications might use an MPC-ceremony for generating the reference string
trustlessly. Vulnerabilities in the MPC-ceremony are considered out of scope,
as they do not directly pertain to SNARKs. Vulnerabilities in the _(iv)_
integration layer resemble any issue in the software components that interact
with a SNARK. For example, circuits can have implicit constraints that ought
to be checked in the integration layer. We exclude traditional
vulnerabilities, such as reentrancy for smart contracts, as they are not
unique to systems using SNARKs.

Adversarial Role |  Public Input |  Private Input |  Circuit |  Public Witness |  Private Witness |  Arithmetization |  CRS |  Prover Key |  Verifier Key |  Proof
---|---|---|---|---|---|---|---|---|---|---
$R_{1}$ \- Network Adversary | ✩ | ✘ | ✔ | ✔ | ✘ | ✩ | ✔ | ✩ | ✩ | ✔
$R_{2}$ \- Adversarial User | ✔ | ✔ | ✔ | ✔ | ✔ | ✩ | ✔ | ✩ | ✩ | ✩
$R_{3}$ \- Adversarial Prover | ✔ | ✩ | ✔ | ✔ | ✩ | ✔ | ✔ | ✔ | ✩ | ✔

Table 1:  Categorization of adversarial roles by the knowledge they can obtain
and utilize. A network adversary can observe existing proofs and reuse them
with different inputs to exploit malleability vulnerabilities. The user can
delegate proof generation to a proving service, while the prover can generate
and has complete control over proof generation. Typically, soundness
vulnerabilities due to circuit bugs can exploited only by the prover.
Adversary has “✔” knowledge, “✘” no knowledge, “✩” maybe knowledge.

_(i)_ Adversarial Roles: Throughout this work, we assume that adversaries are
rational agents aiming to attack systems utilizing SNARKs. We outline the
knowledge an adversary can obtain given its role in our system model in Table
1:

R1 - Network Adversary.  A network adversary can observe the public values
transmitted between participants in the SNARK application. Hence, it can
obtain knowledge about the public witness $x$, the public common reference
string, and the proof $\pi$ sent from the prover to the verifier. A network
adversary may attempt to exploit weak simulation extractability of certain
proof systems that can render a proof malleable [48].

R2 - Adversarial User.  In some SNARK applications, users are not involved in
proof generation or proof verification at all. For example, ZK-EVMs provide a
service that leverages SNARKs primarily to minimize transaction costs. In this
case, an adversarial user has oracle access to the prover, i.e., it can submit
an arbitrary number of public inputs (or private inputs, in case of privacy-
preserving delegated proof generation [26]), with the aim of successfully
performing Denial-of-Service (DoS) attacks. Further, an adversarial user may
exploit circuit issues, where the circuit is defined by the prover (i.e., the
service provider) to whom the user delegates the proof.

R3 - Adversarial Prover.  An adversarial prover has knowledge of all input
values, including the verifier key, and may attempt to break the underlying
cryptographic primitives or exploit misconfigurations in the setup phase. The
adversarial prover can easily exploit soundness vulnerabilities in the
verifier, such as under-constrained bugs discussed in Section 5. To mitigate
this risk, systems, including ZK-rollups, may temporarily adopt permissioned
provers, where only authorized entities can generate and submit proofs to the
verifier (typically a smart contract acting as the verifier). This approach
reduces the risk of adversaries exploiting soundness vulnerabilities, although
it does not eliminate the possibility of the permissioned prover exploiting
such vulnerabilities.

_(ii)_ Vulnerability Impact: We categorize the impact of a vulnerability into
the following categories:

I1 - Breaking Soundness.  The vulnerability allows a prover to convince a
verifier of a false statement; that is, it allows the creation of a proof for
an incorrect statement that is nonetheless accepted as valid.

I2 - Breaking Completeness.  The vulnerability allows a prover to submit
proofs of a true statement that leads to an invalid verification by a
verifier. Further, it can be the case that valid proofs are rejected by an
honest verifier.

I3 - Breaking Zero-Knowledge. The vulnerability allows an adversary to break
the zero-knowledge property, i.e., it allows information leakage about the
private witnesses. If an adversary exploits such a vulnerability, they could
gain access to sensitive data, such as secret keys or private inputs, leading
to privacy violations and potentially further exploits based on the
information gained.

Layer | Security | Vulnerability | Bug |  Total [t]
---|---|---|---|---
audits | disclosures | Tracker
Integration | 8 | 1 | 4 |  13 [t]
Circuit | 86 | 10 | 3 | 99
Frontend | 0 | 0 | 6 | 6
Backend | 7 | 5 | 11 | 23
Total | 101 | 16 | 24 | 141 [t]
Table 2: Origins of vulnerability reports. Impact | Soundness | Completeness | Zero Knowledge
---|---|---|---
Integration | 11 | 2 | 0
Circuit | 94 | 5 | 0
Frontend | 2 | 4 | 0
Backend | 17 | 3 | 3
Total | 124 | 14 | 3
Table 3: Impact of SNARK vulnerabilities.

##  4 Methodology

Exploring the security vulnerabilities across the entire SNARK stack presents
a complex challenge for several reasons. Firstly, the unique programming model
required for developing SNARK circuits means that a significant number of
potential security issues are difficult to identify and understand. Secondly,
the tools used for SNARK development are themselves non-standardized and
heterogeneous, each offering different interfaces. The relative novelty of
SNARK technology contributes to a lack of comprehensive documentation and
standards, further complicating the analysis of these tools. Moreover,
instances of vulnerabilities being actively exploited are rare. There are no
incidents of blackhat attacks publicly disclosed related to SNARKs.
Furthermore, in applications that leverage the zero-knowledge property of
SNARKs, it can be especially challenging to determine if an attack has
occurred due to the privacy-preserving nature of these systems. To cope with
these challenges, we apply the following methodology.

Analyzed SNARK Implementations. Our examination focuses on widely deployed
SNARK systems, including ZK-rollups for blockchain scalability (e.g., zkSync
Era [62], Polygon ZK-EVM [86] Scroll [96]),111Notably, ZK-rollups have more
than 1B USD in accumulated value locked in them according to L2BEAT
https://l2beat.com/scaling/summary privacy-centric blockchains (e.g., Zcash
[93], Aztec [6], Aleo [39]), and decentralized privacy applications (e.g.,
Tornado Cash [84]). We also assess key circuit libraries and SNARK frameworks
(e.g., Circom and halo2) [34]. Our analysis further extends to inspecting the
underlying proof systems for known bugs. This comprehensive approach ensures
that we cover a broad spectrum of real-world SNARK applications and the
various layers of technology they rely on.

Data Sources. In our comprehensive study of security vulnerabilities related
to SNARK systems, we have utilized an extensive range of data sources to
ensure a thorough analysis. Our primary source includes critical and high-
impact vulnerabilities identified in $107$ security audit reports of systems
employing SNARKs. Among these, $75$ reports specifically highlighted
vulnerabilities directly related to SNARKs, while the remaining reports
detailed other types of vulnerabilities, such as common smart contract
deficits. Additionally, we have incorporated vulnerabilities from public bug
bounty programs and vulnerability disclosures. These sources provide real-
world examples of how vulnerabilities have impacted operational systems as
well as the measures taken to address them. Furthermore, we delved into bug
trackers of popular GitHub projects related to SNARKs. Our focus here has been
specifically on security-related bugs, filtering out non-security-related
issues. Table 2 in our paper depicts these varied data sources, collectively
forming the foundation of our study of SNARK security.

Classification. We classify vulnerabilities by determining the layer that they
occur in with respect to our system model (cf. Section 3.1). Successively, we
asses the vulnerability type (e.g., over-constrained), identify its root
cause, and assess whether it impacts soundness, completeness, or zero-
knowledge when exploited (cf. Table 3). We provide a full classification of
all vulnerabilities as an open-source dataset as a reference for
practitioners.222https://docs.google.com/spreadsheets/d/1E97ulMufitGSKo_Dy09KYGv-
aBcLPXtlN5QUpwyv66A

Scope. The systems we analyzed might also be susceptible to vulnerabilities
unrelated to SNARKs, such as reentrancy issues in Solidity smart contracts
within the integration layer [5], type checker bugs in the frontend layer’s
compilers [21], or traditional supply chain attacks [63] that can affect the
circuit layer. However, We deliberately targeted SNARK-specific
vulnerabilities to guide future research on enhancing SNARKs security. We
deliberately focused on SNARK-specific vulnerabilities to identify future
research directions for improving SNARKs security. Yet, addressing general
security challenges and following established best practices remain essential
for overall system integrity.

Threats to validity. Our investigation into vulnerabilities within SNARK
systems faces several challenges that could affect the validity of our
findings. Firstly, the absence of proof-of-concept exploits for many bugs
raises questions about their actual exploitability. We try to mitigate this by
excluding non-security vulnerabilities from our dataset. Secondly, while our
classification of vulnerabilities was rigorously reviewed by multiple
researchers and iteratively refined, the possibility of misclassification
cannot be entirely ruled out. Our reliance on publicly available reports means
our analysis may be skewed towards more commonly detected vulnerabilities,
potentially overlooking others that are less apparent but equally prevalent.

##  5 Circuit Issues

Root Cause | UC | OC | CE | Total
---|---|---|---|---
Assigned but Unconstrained | 14 | 0 | 0 | 14
Missing Input Constraints | 25 | 0 | 0 | 25
Unsafe Reuse of Circuit | 9 | 0 | 0 | 9
Wrong translation of logic into constraints | 32 | 0 | 2 | 34
Incorrect Custom Gates | 1 | 0 | 0 | 1
Out-of-Circuit Computation Not Being Constrained | 1 | 0 | 0 | 1
Arithmetic Field Errors | 8 | 0 | 0 | 8
Bad Circuit/Protocol Design | 4 | 0 | 0 | 4
Other Programming Errors | 1 | 1 | 1 | 3
Total | 95 | 1 | 3 | 99

Table 4: Circuit vulnerabilities. UC: Under-Constrained, OC: Over-Constrained,
CI, Computational/Hints Error.

Vulnerabilities at the circuit layer represent the most prevalent threat to
systems using SNARKs (c.f. Table 2). The primary challenge for developers lies
in adapting to a different level of abstraction, coupled with the need to
optimize circuits for efficiency, as they significantly influence the cost of
using a SNARK. This section initially highlights the three primary
vulnerabilities encountered in the circuit layer, followed by outlining the
root causes that lead to these vulnerabilities (see Table 4). In total, $95$
circuit vulnerabilities led to soundness issues and $4$ led to completeness
issues (c.f. Table 3). We present detailed examples of vulnerabilities and
their root causes in Appendix B.1.

###  5.1 Vulnerabilities

V1. Under-Constrained: The most frequent vulnerability in ZK circuits arises
from insufficient constraints. This deficiency causes the verifier to
mistakenly accept invalid proofs, thus undermining the system’s soundness or
completeness.

V2. Over-Constrained: Although less common than under-constrained issues,
circuits can be over-constrained, leading to the rejection of valid witnesses
by honest provers or benign proofs from honest verifiers. This issue stems
from extra constraints in the circuit, where legitimate solutions cannot be
proven or verified, leading to DoS issues. Nevertheless, over-constrained bugs
should not be confused with redundant constraints that add no additional value
but do not lead to any issues other than introducing computational
inefficiencies.

V3. Computational/Hints Error: Occurs when the computational part of a circuit
is erroneous, often leading to completeness issues where for correct inputs,
the witness generation either fails or produces wrong results. Note that
completeness issues can often be transient, meaning that you can fix the
underlying issue without having to update the circuit and recompute the prover
and/or the verifier keys. Computational issues may also result in soundness
issues if the constraints are applied using the same erroneous logic.

###  5.2 Root Causes

R1. Assigned but not Constrained: A frequent issue in ZK circuit design lies
in distinguishing between assignments and constraints. While constraints are
mathematical equations that must be satisfied for any given witness for the
proof to be valid, assignments allocate values to variables during the witness
generation process. The problem arises when variables are assigned values
based on correct computations but lack corresponding constraints. This
oversight can lead the verifier to erroneously accept any value for these
variables.

R2. Missing Input Constraints: Developers sometimes neglect to apply
constraints on input variables in reusable circuits. This omission occurs
either (i) unintentionally or (ii) because they anticipate these constraints
will be enforced at a different interface level (i.e., caller circuit or
integration layer), thus omitting the constraints for optimization reasons.
However, the absence of clear documentation or fully constrained inputs in
these circuits can lead to severe vulnerabilities. Note that this issue is
particularly common in low-level circuit DSLs, such as Circom, which lack
user-defined types.

R3. Unsafe Reuse of Circuit: In ZK circuit design, particularly when using
DSLs like Circom, the practice of reusing circuits (such as templates in
Circom or gadgets in halo2) can introduce vulnerabilities if not handled
correctly. This primarily occurs in two scenarios: _(i)_ Implicit Constraints
in Sub-Circuits, occurred when circuits are reused without appropriately
constraining their inputs or outputs based on the assumption that the user
will apply these constraints on call-site. _(ii)_ Insecure Circuits
Instantiation when circuits are meant to be used for specific setups (e.g.,
specific curves). An example is the Sign template from circomlib, which was
designed solely for the BN254 curve
field.333https://github.com/iden3/circomlib/blob/master/circuits/sign.circom#L23

R4. Wrong translation of logic into constraints: Translating computations for
ZK circuits presents a unique set of challenges, primarily due to the distinct
programming model of ZK circuits compared to traditional CPU-targeted code. A
significant issue arises when translating logic that involves types and
operations available in conventional programming languages but are either
absent or must be re-implemented in ZK frameworks (e.g., fixed-point
arithmetic). This often leads to the need for creative but error-prone
solutions, such as using multiplexers for conditional logic. Developers might
inadvertently omit essential constraints or simplify the logic to reduce the
number of constraints, potentially missing critical corner cases. This can
leave variables under-constrained, allowing them to accept multiple or any
values under certain conditions, thus deviating from the developer’s intent
and introducing vulnerabilities.

R5. Incorrect Custom Gates: In implementations following the TurboPLONK model,
such as Halo2, circuit constraints are defined by using custom gates applied
to specific rows and cells of a table that constitute the Plonkish
representation of the circuit. However, this approach can lead to bugs when
custom gates are incorrectly handled. Errors may arise from inaccurately
determining the appropriate offsets, resulting in misalignment with the
intended behavior of the circuit.

R6. Out-of-Circuit Computation Not Being Constrained: Out-of-circuit
computation refers to computations within the code that do not directly impact
the witness generation yet play a crucial role in the overall functionality.
In DSLs like Circom, certain functions operate outside the circuit logic.
Similarly, in eDSLs, standard code (e.g., vanilla Rust) is used for various
computations that do not affect witness generation. For instance, computations
like division, are typically performed out-of-circuit to optimize circuit
efficiency. This method involves executing the computation externally and then
witnessing the result back into the circuit where it is constrained to ensure
correctness. Issues arise when these out-of-circuit computations lead to
missing assignments or when constraints necessary for the circuit’s integrity
are overlooked. A specific manifestation of this issue is the boomerang issue,
where a variable, initially constrained within the circuit, is temporarily
moved out-of-circuit and then reintegrated without the necessary reapplication
of constraints.

R7. Arithmetic Field Error: Working with field arithmetic in ZK circuits can
be challenging, especially as developers might overlook the nuances of
computations within a finite field. The most common issues in this context are
arithmetic overflows and underflows. We categorize the primary types of
overflows and underflows in ZK circuits as follows: (i) Native Field
Arithmetic Over/Underflow, occurs when circuit computations exceed the finite
field’s limits, causing values to loop back within the field’s range due to
modulo arithmetic. (ii) Overflows in Transformed Formats, risks of overflows
arise when numbers are transformed into bit representations for specific
operations (e.g., range checks) or for emulating non-native arithmetics like
fixed-point arithmetics. This is particularly problematic when multiple bit
representations remain within the field’s overflow limits, leading to under-
constrained vulnerabilities.

R8. Bad Circuit/Protocol Design: Circuit design issues in SNARKs often stem
from fundamental flaws in how circuits are conceptualized, potentially leading
to unintended behaviors or the violation of protocol properties. A common
manifestation of this problem is the incorrect categorization of variables –
such as designating a variable as private when it should be public. These
issues can significantly impact the functionality and security of the
protocol.

R9. Other Programming Errors: This category encompasses a range of common
programming errors that do not fit neatly into other specific vulnerability
categories but still have significant implications for the integrity of SNARK
systems. These errors include, but are not limited to, API misuse, incorrect
indexing in arrays, and logical errors within the computational parts (i.e.,
witness generation) of the circuit that are not directly related to constraint
application.

Countermeasures. To address circuit layer vulnerabilities in SNARK systems,
especially the common issue of under-constrained vulnerabilities, several
straightforward yet effective strategies are recommended. Firstly, adding
missing constraints, particularly range checks, is crucial to ensure the
integrity and robustness of the circuits. In-depth documentation of circuit
design and SNARK system specifications can significantly aid in preventing
misunderstandings and oversights during development and auditing.
Additionally, adopting DSLs, whenever possible, that support modern
programming features, such as abstractions and basic types, enhances the
development process by providing clearer guidelines and reducing the
likelihood of errors. Lastly, the use of specialized security tools designed
for ZK circuits, as detailed in Section 8, can detect some vulnerabilities
during the developing phase, further securing SNARK systems against
vulnerabilities.

##  6 Integration Layer Issues

Root Cause | PDE | PCE | PUD | ZKPCLE |  Total
---|---|---|---|---|---
Integration Design Error | 1 | 2 | 0 | 0 |  3 [t]
Missing Validation Input | 0 | 0 | 9 | 1 | 10
Total | 1 | 2 | 9 | 1 |  13

Table 5: Integration vulnerabilities. PDE: Proof Delegation Error, PCE: Proof
Composition Error, PUD: Passing Unchecked Data, ZKPCLE: ZKP Complementary
Logic Error

Besides circuit-related problems, numerous vulnerabilities in systems
employing SNARKs originate from the integration layer. These vulnerabilities
often stem from improper interactions between the application/system and the
prover or verifier, or from design flaws within this layer that compromise the
inherent properties of SNARKs. Table 5 categorizes all analyzed bugs into
distinct categories and root causes. For examples of integration-specific
vulnerabilities, refer to Appendix B.2.

###  6.1 Vulnerabilities

V4. Passing Unchecked Data: This vulnerability manifests when implicit
constraints on the public inputs expected by the circuit are not enforced by
the application’s verifier. It can result in both soundness and completeness
issues. While unchecked data can be input in the circuit directly or
indirectly (by hashing it), the failure to enforce these implicit constraints
at the integration layer can compromise the integrity of the entire system.

V5. Proof Delegation Error: In scenarios where proof generation is delegated
to an untrusted prover, there’s a risk of malicious activities. For example, a
bad design could lead to the leaking of personal or secret data. This issue
underlines the need for secure and trusted channels in proof delegation and
decentralized proving services [46].

V6. Proof Composition Error: This issue arises when the logic is distributed
across multiple proofs, but the intended behavior is not adequately enforced
by the verifier who is expected to glue parts of certain proofs with parts of
others. The lack of coherence and coordination between different proofs can
lead to undefined behaviors in the application.

V7. ZKP Complementary Logic Error: This category encompasses vulnerabilities
in the integration layer arising from the flawed implementation of logic that
operates in conjunction with ZKPs. An illustrative example of such a flaw is
the poor management of protocol-specific mechanisms like nullifiers. Consider
a privacy-preserving application like Tornado Cash (TC), where users aim to
dissociate deposits from withdrawals. TC employs ZKPs alongside a nullifier
scheme; each deposit involves generating a nullifier and a secret, which, when
hashed, are appended in a Merkle tree in TC.444For more information on how TC
works we refer the reader to the official documentation
https://docs.tornadoeth.cash/generals/how-does-tornado-cash-work Upon
withdrawal, the user submits the nullifier and employs a SNARK to prove
knowledge of the corresponding secret without revealing it, thus unlinking the
withdrawal from the deposit. However, a critical check within the integration
layer is required to ensure the unique use of each nullifier. Without this
check, the system is vulnerable to exploitation, allowing a user to repeatedly
withdraw funds, thus draining TC. This class of bugs, crucially, is not due to
a flaw in the circuit’s design or implementation but stems from an oversight
in auxiliary mechanisms that are integral to the secure and correct
application of ZKPs.

###  6.2 Root Causes

R10. Missing Validation Input: This root cause involves inadequate validation
checks on data before its input into the circuit or before computations that
affect data used later by the circuit. It arises when the integration layer
does not properly validate input data or when the circuit itself lacks
necessary checks. This oversight can lead to the acceptance of inappropriate
data, potentially getting an application stuck, or worse, compromising the
circuit’s computations.

R11. Integration Design Error: Design flaws in the integration code that lead
to undesired behavior or break protocol properties, such as not checking for
duplicate nullifiers, are critical. Furthermore, designing privacy-enhanced
applications poses a significant challenge. It is not straightforward to
create ZK applications with privacy as a core property, and developers may
inadvertently leak information without realizing it. This issue isn’t about
the proof system or constraints; it is about the inherent difficulty in
designing an application that doesn’t subtly leak data. This underscores the
complexity and importance of carefully considering privacy aspects in the
design phase of ZK applications. Fixes often require a high-level redesign
rather than a simple programming correction.

##  7 Frontend/Backend Issues

Layer | Vulnerability | # Bugs
---|---|---
Frontend | Incorrect Constraint Compilation | 3
Witness Generation Error | 3
Total | 6
Backend | Setup Error | 1
Prover Error | 6
Unsafe Verifier | 16
Total | 23
Table 6: Summary of frontend and backend bugs.

The compilation of ZK circuits (frontend), along with proving a witness and
verifying it (backend), rely on the correctness of the underlying software
that implements the compilation process as well as the algorithms that
underpin the proof system. Table 6 provides an overview of vulnerabilities
that can occur within these components. Vulnerabilities in either the frontend
or backend layers pose a significant risk, even if the circuits have been
formally verified or if the proof system is theoretically secure; any defects
in these layers could render the entire system insecure for end-users.

###  7.1 Frontend Vulnerabilities

V8. Incorrect Constraint Compilation: This type of vulnerability emerges from
deficiencies in the compilation phase, specifically in the enforcement of
constraints defined in the ZK circuit. Specifically, such issues may stem from
the arithmetization process or overly aggressive optimization routines that
unintentionally excise vital constraints. Any missteps in these processes can
result in an inaccurate or incomplete translation of the original constraints
at the circuit layer. Consequently, this could permit a verifier to
erroneously accept an invalid proof or, conversely, to reject a legitimate
one. At its core, this vulnerability mirrors a classical compiler bug, wherein
the compiler erroneously interprets high-level DSL code.

V9. Witness Generation Error: This issue arises during the witness generation
phase, where errors in the compilation can produce invalid witnesses or cause
crashes, potentially leading to a denial of service. Typically, such errors
occur due to misinterpretation of the circuit code, or due to the generation
of bogus witness generators in target languages.

###  7.2 Backend Vulnerabilities

V10. Setup Error: This vulnerability arises during the setup phase, where the
generation of public parameters occurs. Incorrect or easily compromised
parameters can significantly undermine the system’s integrity.

V11. Prover Error: Issues within the prover of the proof system fall into this
category. These vulnerabilities can lead to the prover mistakenly rejecting
valid witnesses, accepting invalid ones, or breaking the zero-knowledge
property.

V12. Unsafe Verifier: This category includes vulnerabilities resulting from
inadequate checks on the verifier’s inputs, missing checks during
verification, or bogus mathematical operations, risking the proof system’s
integrity. Vulnerabilities can emerge regardless of whether the verifier is
manually implemented or generated by a framework.

###  7.3 Root Causes

Frontend and backend vulnerabilities can stem from a variety of root causes,
ranging from basic programming errors to configuration issues or deviations
from the specifications of proof systems. These can be as simple as missing
validation checks for proofs or as complex as informational leaks that expose
sensitive data. Additionally, the use of poor-quality or predictable
randomness sources can compromise crucial ZKP properties. Adherence to proof
system specifications is critical in preventing vulnerabilities. A common
issue is the incorrect implementation of the Fiat-Shamir transformation, where
a critical component is omitted during the hashing process of the transcript.

| Vulnerability | Defenses [t]
---|---|---
|  |  Circomspect [100] |  ZKAP [102] |  Korrekt [98] |  Coda [66] |  Ecne [101] |  Picus [80] |  Aleo [28, 29] |  OWBB23 [79] |  SnarkProbe [37] |  CIVER [56] |  Trad Sec*
Circuit | Under-Constrained | ● | ● | ● | ● | ● | ● | ● | ○ | ● | ● |  ○[t]
Over-Constrained | ○ | ○ | ● | ● | ○ | ○ | ● | ○ | ● | ○ | ○
Computational Error | ○ | ○ | ○ | ● | ○ | ○ | ● | ○ | ○ | ○ | ●
Frontend | Incorrect Constraint Compilation | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ● | ○ | ○ | ○
| Witness Generation Error | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ●
Backend | Setup Error | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ● | ○ | ○
Prover Error | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ●
Unsafe Verifier | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ○ | ○ |  ●

Table 7: An overview of papers and tools offering defense mechanisms for
addressing vulnerabilities in SNARK-based systems. While numerous techniques
are concentrated on circuit-layer security, they often face challenges in
scalability or possess limited functionality tied to specific DSLs. The last
column represents traditional security tools (e.g., AFL and property-based
testing) employed by auditors in audit reports. Note that these tools
typically have limited capabilities for detecting SNARK-related bugs. We
excluded the integration layer from the table as no defense detects bugs in
that layer.

##  8 Defenses For SNARKs

This section presents an overview of defense mechanisms aimed at mitigating
the SNARK vulnerabilities detailed in the previous sections. Table 7 compiles,
to our best knowledge, all publications and tools associated with SNARK
security. A filled bullet in the table indicates that the referenced technique
provides at least one defensive measure against the issues indicated by the
corresponding row’s header. Notably, in addition to SNARK-specific strategies,
conventional security tools (e.g., fuzzing) have been utilized in audits,
although they typically fall short in preventing most vulnerabilities due to
the oracle problem [8]. For example, fuzzing might be useful in detecting
completeness bugs, but it often falls short of finding soundness issues. In
the following, we delve into the current defensive measures for each layer,
suggest future steps for preventing SNARK vulnerabilities, and review the
tools employed in the audits we examined.

Circuit Layer Defenses. The circuit layer emerges as the most prominent layer
for SNARK vulnerabilities, leading to the development of various techniques
like static analysis and symbolic execution, particularly targeting under-
constrained bugs. Tools such as Circomspect [100] and ZKAP [102] employ static
analysis using predefined rules to identify under-constrained issues in Circom
circuits. Similarly, Korrect [98] utilizes static analysis and SMT solvers to
spot common pitfalls in Halo2 circuits. SNARKProbe [37] leverages fuzzing and
SMT solvers to test circuits written using R1CS-based libraries. Picus [80],
on the other hand, adopts a more advanced symbolic execution approach to
verify that Circom circuits are not under-constrained. CIVER [56] uses a
modular technique based on the application of transformation and deduction
rules to verify properties of Circom circuits using pre- and post-conditions.
In a different approach, DSLs like Coda [67] and Leo [29, 28] support formal
verification of circuits, aiding developers in creating more secure circuits.

Despite these initial strides in tool development for ZK circuits, significant
limitations remain. Tools relying on SMT solvers, like Picus and Korrect, face
challenges due to limited support and efficiency in handling finite field
arithmetic, leading to performance bottlenecks [54, 78]. Static analysis tools
are often restricted in the range of vulnerabilities they can detect and tend
to be specific to certain languages. CirC [77] compiler represents a step
towards language-agnostic tooling, allowing various DSLs to compile into an
Intermediate Representation, which can then be analyzed for potential
vulnerabilities. Another promising direction is the creation of more secure
DSLs, like Aleo [27], noname [109], and Noir [72], or eDSLs such as o1js [73]
and arkworks R1CS [3], which incorporate strong typing and improved
abstractions to prevent common issues.

Additionally, differential testing [68] against a reference implementation
could be a viable method to identify computational issues. We anticipate that
proper compilation of DSL to an IR could enable more general static analysis
to uncover SNARK vulnerabilities in a DSL-agnostic way. Furthermore, applying
hardening techniques to automatically patch circuits with missing range checks
could enhance security. Complementary to existing approaches, compositional
verification techniques could be applied to verify ZK circuits. Lastly,
advanced fuzzing techniques that generate slightly incorrect witnesses might
prove effective in detecting under-constrained vulnerabilities, while
providing counterexamples. Finally, there is a growing demand for more
advanced testing frameworks in the field. Such frameworks would greatly assist
developers in creating their own unit and integration tests, which could be
instrumental in identifying and rectifying many easily detectable
vulnerabilities prior to deployment.

Integration Layer Defenses. Table 7 highlights a notable gap: there are
currently no specific defenses developed for vulnerabilities in the
integration layer of SNARK systems. However, traditional security methods like
property-based fuzzing or formal verification could be applicable if there’s a
comprehensive specification detailing the expected system behavior and its
interactions with SNARK components. A promising direction for future
development is the creation of security frameworks designed to rigorously test
the integration between client-side code (such as Solidity and JavaScript) and
circuit code. We suggest exploring multi-layer testing and verification
techniques targeting both these components simultaneously. An example could be
a combined testing of Circom and Solidity applications. Additionally, having a
detailed specification of the entire system, including how different
components interact, can significantly enhance the effectiveness of manual
code inspection.

Frontend/Backend Layers Defenses. The infrastructure layer, comprising the
frontend and backend of SNARK systems, has largely been overlooked by security
researchers. Ozdemir et al. [79] acknowledged that a flaw in a ZKP compiler
could undermine the integrity of a ZKP, and took initial steps to mitigate
such risks by partially verifying a key compiler pass in the CirC compiler
[77]. SNARKProve [37] implements a fuzzing framework that can be configured
with custom files (i.e., ideal files) to test specific cryptographic
properties of the backends and frontends. In its initial version, it has been
successful in detecting issues in the Setup phase of the backend. Moreover,
practitioners have employed fuzzing tools like AFL to identify bugs in these
layers. However, these tools are somewhat limited in scope, typically only
capable of detecting crashes, potentially missing more subtle but critical
vulnerabilities such as miscompilations.

As the field progresses with more complex optimizations in the compilation
stage being enabled and the introduction of more advanced proof systems, it is
likely that more vulnerabilities will emerge at the infrastructure layer of
SNARKs. Consequently, there is a pressing need for the development of more
sophisticated testing methodologies for the infrastructure layer. Overcoming
the oracle problem and generating effective test cases are key challenges in
this area. Insights from the extensive body of work on testing conventional
compilers [105, 24, 65, 22] could be valuable in devising strategies for more
effectively testing SNARK compilers.

Tools Applied on Audits. Our analysis of the $75$ audit reports we reviewed
revealed that SNARK-related tools were utilized in only $5$ instances.
Specifically, Picus was employed in $4$ audits, while ZKAP, Ecne, and
Circomspect were each used once. Interestingly, one audit incorporated
differential testing against a reference implementation to identify
computational issues in the circuits. Moreover, traditional security tools
like AFL, Semgrep, and property testing were used in $10$ audits, primarily
for detecting bugs at the circuit and infrastructure levels. This highlights a
significant need for enhanced tooling for both the frontend and backend layers
of SNARK systems.

Multi-Provers as a Defense Mechanism. SNARK proofs are often used in safety-
critical contexts, yet, with the current state of technology, guaranteeing
that a complex SNARK system is bug-free and safe remains an elusive goal. The
multi-prover design enhances safety by introducing redundancy at the proof
system level. A multi-prover system utilizes multiple proof systems besides
the primary SNARK, such as alternative SNARK proofs or TEE-based proofs, and
primary proofs are accepted only if the secondary ones agree with it. This
design trades off liveness with more safety, as a dispute will potentially
bring the system to a halt. Such systems require a dispute resolution
mechanism to handle potential disagreements. In practice, some ZK-Rollup
projects [96], arguably one of the most complex categories of SNARK systems
today, are already experimenting with multi-
provers.555https://scroll.io/blog/scaling-security

##  9 Issues in Proof Systems

While the focus of earlier sections was on implementation and design
vulnerabilities across the four layers introduced in Section 3.1,
vulnerabilities can also exist within the theoretical foundations of SNARKs’
proof systems. This includes the formal descriptions and security proofs of
protocols. Such vulnerabilities are less common but carry significant
implications, potentially affecting all implementations of a given proof
system. For example, the “Frozen Heart” vulnerability within the Plonk proof
system (c.f. Appendix A.2) led to standard implementations of Plonk being
compromised. The discovery of such flaws could severely impact the SNARK
ecosystem, especially protocols that depend on these systems. Vulnerabilities
in the proof system generally stem from two main sources: errors in the
original proof system description, including missing or incorrect security
proofs or incomplete descriptions that could lead developers to introduce
significant vulnerabilities during implementation. We provide a detailed
account of known vulnerabilities in Appendix A.

The primary method for evaluating proof systems currently is peer review,
where researchers assess security proofs, supplemented by occasional manual
audits. Beyond cryptanalysis, employing tools like EasyCrypt [9] and other
computer-aided cryptographic proof software [7] offers a promising avenue for
formalizing and verifying the security properties of zero-knowledge protocols,
as exemplified by Firsov et al.’s work [38]. It is crucial for every proof
system to be accompanied by exhaustive security proofs and to undergo rigorous
review before production use to prevent potential bugs.

##  10 Discussion

In the following, we extract insights on the current state of SNARK security,
highlight key findings, discuss their implications and make recommendations
for future research.

1) Insight – Under-constrained bugs pose a significant threat to SNARK
deployments. Under-constrained bugs emerge as the most prevalent vulnerability
class within ZK circuits. Unlike typical vulnerabilities, their root causes
span from straightforward programming errors to challenges inherent in SNARK
DSLs, including the complexity of translating logic to constraints
efficiently. As developers navigate these peculiarities, ensuring circuits are
thoroughly constrained remains crucial for maintaining system integrity and
security.

2) Insight – Soundness bugs affecting SNARK verifiers lead on average to high
severity bugs. Particularly when soundness bugs are exploitable, typically due
to under-constrained circuits, they can lead to significant security breaches.
Their potential to compromise system security has led to suboptimal
strategies, such as employing multi-provers and permissioned provers,
alongside significant bug bounties, sometimes reaching up to $500k for a
single vulnerability. These measures underscore the critical nature of
soundness in maintaining the trustworthiness of SNARK-based systems.

3) Insight – Low-level circuit DSLs are easy-to-misuse leading to many
vulnerabilities. Crafting efficient ZK circuits often necessitates using low-
level ZK DSLs such as Circom and Gnark, reminiscent of early assembly and C
programming, where common high-level programming features such as abstractions
and basic types are absent. This complexity not only steepens the learning
curve for developers but also increases the likelihood of introducing
vulnerabilities into the circuits. The prevalent use of tools such tools
highlights a regression to an era with bugs due to the absence of modern
programming safeguards, underscoring an urgent need for more user-friendly
DSLs that offer better abstractions and safety features, thereby mitigating
the main shortcomings and reducing the vulnerability surface of SNARK
applications.

4) Challenge – The added complexity of SNARKs present challenges for
developers and auditors. The inherent complexity of SNARKs introduces
significant challenges for both developers and auditors, compounded by the
abstraction levels of ZK circuits and the low-level intricacies of most DSLs.
Developers often find themselves navigating the task of integrating critical
cryptographic operations—such as digital signatures, commitment schemes, and
Merkle trees—within the ZK circuits. This combination of complex cryptographic
code with the unique paradigm of SNARKs places a considerable burden on
ensuring accuracy and security, particularly when such code underpins the most
vital or privacy-sensitive parts of an application. Hence, not only must
developers acquire the technical depth of cryptographic programming within
these new frameworks, but auditors must also adapt their methodologies to
effectively scrutinize these sophisticated systems.

5) Insight – Compiler and proof system implementation bugs can undermine major
protocols. Infrastructure bugs in compilers and proof system implementations
can critically undermine the security of major SNARKs. Even when circuits are
verified and audited, vulnerabilities in the underlying infrastructure or
proof systems can jeopardize the entire application, emphasizing the
importance of holistic testing approaches for the infrastructure layer of the
SNARKs.

6) Challenge – Preliminary security tools show promising results but also
limitations. Recent developments in tools for securing ZK circuits show
promise but face scalability issues and are often limited to specific DSLs or
types of vulnerabilities. The complexity of SNARK systems makes manual code
inspection necessary, pointing to a significant need for better security tools
and educational resources. This combination of advanced tooling and increased
knowledge is crucial for improving the security of the SNARK ecosystem.

7) Insight – Insecure Proof System Instantiation. The selection of
cryptographic curves and fields for SNARK instantiation is a critical decision
that can significantly impact system security. Insecure choices can expose the
system to potential brute force attacks similarly to other cryptographic
protocols, underscoring the necessity of careful selection to ensure the
overall security and integrity of SNARK applications.

8) Challenge – SNARK undetectable exploits. In privacy-preserving blockchains,
such as ZCash, coins enter a privacy pool (a.k.a. shielded value pool) where
they can be transferred without revealing the amount or recipient address. The
transaction validation mechanism relies on SNARKs and a soundness bug can
enable the adversary to print infinite coins inside the privacy pool. Note
that such attacks can remain undetected as long as, at any point, the amount
of coins that exited the pool is smaller or equal to coins that have entered
the pool previously. A partial defense against these attacks is turnstile
enforcement, adding a consensus check to reject blocks violating pool balance,
ensuring exits don’t exceed entries. This highlights the need for privacy-
focused SNARK systems with exploit detection and prevention mechanisms.

##  11 Related Work

SNARK Vulnerabilities. This paper introduces a four-layer system model,
defines threat models along with a detailed taxonomy of vulnerabilities and
root causes across each layer in SNARK systems. Prior works have identified
specific vulnerabilities within SNARKs; for example, Wen et al. [102]
highlighted common vulnerabilities in Circom circuits, while others [98, 101,
80, 37, 56] have focused mainly on under-constrained vulnerabilities and
proposed countermeasures. Ozdemir et al. [79] shed light on potential issues
during the SNARK compilation phase. For security tools related to SNARK
vulnerabilities, Table 7 offers a comprehensive overview. Additionally, the
community maintains a bug tracker dedicated to ZKP-related
vulnerabilities.666https://github.com/0xPARC/zk-bug-tracker Our research
complements these efforts by systematizing knowledge from the examination of
$141$ vulnerabilities and enriching the understanding of SNARK security.

Security of Integrity-Preserving Technologies. Integrity-preserving
computation encompasses a variety of technologies, each presenting unique
security challenges. Similar to our work, Cerdeira et al. [19] examined $124$
CVEs within TEE-based systems and proposed a vulnerability taxonomy for
TrustZone-assisted TEE Systems. Blockchain smart contracts represent another
avenue for integrity-preserving computation; Praitheeshan et al. [87]
identified common software and Ethereum smart contract vulnerabilities,
focusing on issues prevalent at the smart contract layer. Homoliak et al. [55]
introduced a multi-layered security model, systematically addressing
vulnerabilities, threats, and countermeasures for blockchains. Atzei et al.
[5] explored Ethereum’s security vulnerabilities, offering a classification of
common programming pitfalls. Zhou et al. [108] developed a five-layer model
and a comprehensive taxonomy of threat models to analyze and compare incidents
in DeFi. Further, Chaliasos et al. [20] used the dataset from [108] to
evaluate state-of-the-practice smart contract security tools against real-
world vulnerabilities. In a similar way, future work could leverage our
findings to assess the efficacy of emerging security tools for SNARKs against
the vulnerabilities detailed in our dataset.

##  12 Conclusions

In this work, we present comprehensive system and threat models for SNARK
systems’ security, a detailed study, and a taxonomy of $141$ vulnerabilities,
demonstrating that security breaches can affect every layer of systems
employing SNARKs, jeopardizing completeness, soundness, and zero-knowledge
properties. Our work reveals the intricate and unique security challenges
inherent to SNARKs, indicating that defense mechanisms focusing on SNARK
security have significant limitations. By highlighting key insights and
potential advancements in security practices, we underscore the urgency for
continued research and enhanced defenses within the SNARK ecosystem. As SNARKs
become increasingly pivotal in cryptographic applications, our study
emphasizes the necessity for progressive and fortified security measures to
ensure the robustness of these systems.

## Acknowledgments

We thank Shankara Pailoor, Alex Ozdemir, Jean-Philippe Aumasson, and Justin
Traglia for their insightful feedback. We thank the Ethereum Foundation and
0xPARC for supporting this work.

## References

  * [1] Nada Amin, John Burnham, François Garillot, Rosario Gennaro, Daniel Rogozin, Cameron Wong, et al.  Lurk: Lambda, the ultimate recursive knowledge.  Cryptology ePrint Archive, 2023.
  * [2] Anoma.  Vamp-ir: A proof-system-agnostic language for writing arithmetic circuits, 2023.
  * [3] arkworks contributors.  arkworks zksnark ecosystem, 2022.
  * [4] Arasu Arun, Srinath Setty, and Justin Thaler.  Jolt: Snarks for virtual machines via lookups.  Cryptology ePrint Archive, 2023.
  * [5] Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli.  A survey of attacks on ethereum smart contracts (sok).  In Principles of Security and Trust: 6th International Conference, POST 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings 6, pages 164–186. Springer, 2017.
  * [6] Aztec.  Aztec network, 2023.  https://docs.aztec.network/.
  * [7] Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno.  Sok: Computer-aided cryptography.  In 2021 IEEE symposium on security and privacy (SP), pages 777–795. IEEE, 2021.
  * [8] Earl T Barr, Mark Harman, Phil McMinn, Muzammil Shahbaz, and Shin Yoo.  The oracle problem in software testing: A survey.  IEEE transactions on software engineering, 41(5):507–525, 2014\.
  * [9] Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, and Pierre-Yves Strub.  Easycrypt: A tutorial.  International School on Foundations of Security Analysis and Design, pages 146–166, 2012.
  * [10] Marta Bellés-Muñoz, Miguel Isabel, Jose Luis Muñoz-Tapia, Albert Rubio, and Jordi Baylina.  Circom: A circuit description language for building zero-knowledge applications.  IEEE Transactions on Dependable and Secure Computing, 2022.
  * [11] Eli Ben-Sasson, Iddo Bentov, Yinon Horesh, and Michael Riabzev.  Fast reed-solomon interactive oracle proofs of proximity.  In 45th international colloquium on automata, languages, and programming (icalp 2018). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018\.
  * [12] Eli Ben-Sasson, Iddo Bentov, Yinon Horesh, and Michael Riabzev.  Scalable zero knowledge with no trusted setup.  In Advances in Cryptology–CRYPTO 2019: 39th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 18–22, 2019, Proceedings, Part III 39, pages 701–732. Springer, 2019.
  * [13] Eli Ben-Sasson, Alessandro Chiesa, Eran Tromer, and Madars Virza.  Succinct $\\{$Non-Interactive$\\}$ zero knowledge for a von neumann architecture.  In 23rd USENIX Security Symposium (USENIX Security 14), pages 781–796, 2014.
  * [14] Joseph Bonneau, Izaak Meckler, Vanishree Rao, and Evan Shapiro.  Mina: Decentralized cryptocurrency at scale.  New York Univ. O (1) Labs, New York, NY, USA, Whitepaper, pages 1–47, 2020.
  * [15] Gautam Botrel, Thomas Piellard, Youssef El Housni, Ivo Kubjas, and Arya Tabaie.  Consensys/gnark: v0.8.0, 2023.
  * [16] Sean Bowe, Alessandro Chiesa, Matthew Green, Ian Miers, Pratyush Mishra, and Howard Wu.  Zexe: Enabling decentralized private computation.  In 2020 IEEE Symposium on Security and Privacy (SP), pages 947–964. IEEE, 2020.
  * [17] Jeremy Bruestle, Paul Gafni, and the RISC Zero Team.  Risc zero zkvm: Scalable, transparent arguments of risc-v integrity.  https://dev.risczero.com/proof-system-in-detail.pdf, 2023.
  * [18] Benedikt Bünz, Jonathan Bootle, Dan Boneh, Andrew Poelstra, Pieter Wuille, and Greg Maxwell.  Bulletproofs: Short proofs for confidential transactions and more.  In 2018 IEEE symposium on security and privacy (SP), pages 315–334. IEEE, 2018.
  * [19] David Cerdeira, Nuno Santos, Pedro Fonseca, and Sandro Pinto.  Sok: Understanding the prevailing security vulnerabilities in trustzone-assisted tee systems.  In 2020 IEEE Symposium on Security and Privacy (SP), pages 1416–1432. IEEE, 2020.
  * [20] Stefanos Chaliasos, Marcos Antonios Charalambous, Liyi Zhou, Rafaila Galanopoulou, Arthur Gervais, Dimitris Mitropoulos, and Benjamin Livshits.  Smart contract and defi security tools: Do they meet the needs of practitioners?  In 2024 IEEE/ACM 46th International Conference on Software Engineering (ICSE), pages 705–717. IEEE Computer Society, 2023.
  * [21] Stefanos Chaliasos, Thodoris Sotiropoulos, Georgios-Petros Drosos, Charalambos Mitropoulos, Dimitris Mitropoulos, and Diomidis Spinellis.  Well-typed programs can go wrong: A study of typing-related bugs in jvm compilers.  Proceedings of the ACM on Programming Languages, 5(OOPSLA):1–30, 2021.
  * [22] Stefanos Chaliasos, Thodoris Sotiropoulos, Diomidis Spinellis, Arthur Gervais, Benjamin Livshits, and Dimitris Mitropoulos.  Finding typing compiler bugs.  In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 183–198, 2022.
  * [23] Kyle Charbonnet.  Completeness bug on semaphore protocol.  https://github.com/semaphore-protocol/semaphore/issues/90, 2022\.  Accessed: date-of-access.
  * [24] Yang Chen, Alex Groce, Chaoqiang Zhang, Weng-Keen Wong, Xiaoli Fern, Eric Eide, and John Regehr.  Taming compiler fuzzers.  In Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation, pages 197–208, 2013.
  * [25] Alessandro Chiesa, Yuncong Hu, Mary Maller, Pratyush Mishra, Noah Vesely, and Nicholas Ward.  Marlin: Preprocessing zksnarks with universal and updatable srs.  In Advances in Cryptology–EUROCRYPT 2020: 39th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Zagreb, Croatia, May 10–14, 2020, Proceedings, Part I 39, pages 738–768. Springer, 2020.
  * [26] Alessandro Chiesa, Ryan Lehmkuhl, Pratyush Mishra, and Yinuo Zhang.  Eos: Efficient private delegation of zksnark provers.  In USENIX Security Symposium. USENIX Association, 2023.
  * [27] Collin Chin, Howard Wu, Raymond Chu, Alessandro Coglio, Eric McCarthy, and Eric Smith.  Leo: A programming language for formally verified, zero-knowledge applications.  Cryptology ePrint Archive, 2021.
  * [28] Alessandro Coglio, Eric McCarthy, Eric Smith, Collin Chin, Pranav Gaddamadugu, and Michel Dellepere.  Compositional formal verification of zero-knowledge circuits.  Cryptology ePrint Archive, 2023.
  * [29] Alessandro Coglio, Eric McCarthy, and Eric W Smith.  Formal verification of zero-knowledge circuits.  arXiv preprint arXiv:2311.08858, 2023.
  * [30] World Wide Web Consortium et al.  Verifiable credentials data model 1.0: expressing verifiable information on the web.  https://www. w3. org/TR/vc-data-model/?# core-data-model, 2019\.
  * [31] Trisha Datta and Dan Boneh.  Using zk proofs to fight disinformation, 2022.  Accessed: 2023-11-10.
  * [32] Jacob Eberhardt and Stefan Tai.  Zokrates-scalable privacy-preserving off-chain computations.  In 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData), pages 1084–1091. IEEE, 2018.
  * [33] Youssef El Housni and Aurore Guillevic.  Families of snark-friendly 2-chains of elliptic curves.  In Annual International Conference on the Theory and Applications of Cryptographic Techniques, pages 367–396. Springer, 2022.
  * [34] Jens Ernstberger, Stefanos Chaliasos, George Kadianakis, Sebastian Steinhorst, Philipp Jovanovic, Arthur Gervais, Benjamin Livshits, and Michele Orrù.  zk-bench: A toolset for comparative evaluation and performance benchmarking of snarks.  Cryptology ePrint Archive, 2023.
  * [35] Jens Ernstberger, Stefanos Chaliasos, Liyi Zhou, Philipp Jovanovic, and Arthur Gervais.  Do you need a zero knowledge proof?  Cryptology ePrint Archive, Paper 2024/050, 2024.  https://eprint.iacr.org/2024/050.
  * [36] Privacy & Scaling Explorations.  halo2 community edition, 2023.
  * [37] Yongming Fan, Yuquan Xu, and Christina Garman.  Snarkprobe: An automated security analysis framework for zksnark implementations.  International Conference on Applied Cryptography and Network Security, 2024.
  * [38] Denis Firsov and Dominique Unruh.  Zero-knowledge in easycrypt.  In 2023 IEEE 36th Computer Security Foundations Symposium (CSF), pages 1–16. IEEE, 2023.
  * [39] Aleo Network Foundation.  Aleo, 2023.
  * [40] Nil Foundation.  zkllvm.  https://github.com/NilFoundation/zkLLVM, 2023.
  * [41] Ariel Gabizon.  On the security of the bctv pinocchio zk-snark variant.  Cryptology ePrint Archive, Paper 2019/119, 2019.  https://eprint.iacr.org/2019/119.
  * [42] Ariel Gabizon and Zachary J Williamson.  plookup: A simplified polynomial protocol for lookup tables.  Cryptology ePrint Archive, 2020.
  * [43] Ariel Gabizon, Zachary J Williamson, and Oana Ciobotaru.  Plonk: Permutations over lagrange-bases for oecumenical noninteractive arguments of knowledge.  Cryptology ePrint Archive, 2019.
  * [44] Nicolas Gailly, Mary Maller, and Anca Nitulescu.  Snarkpack: Practical snark aggregation.  In International Conference on Financial Cryptography and Data Security, pages 203–229. Springer, 2022.
  * [45] Chaya Ganesh, Anca Nitulescu, and Eduardo Soria-Vazquez.  Rinocchio: Snarks for ring arithmetic.  Journal of Cryptology, 36(4):41, 2023.
  * [46] Sanjam Garg, Aarushi Goel, Abhishek Jain, Guru-Vamsi Policharla, and Sruthi Sekar.  zksaas: Zero-knowledge snarks as a service.  Cryptology ePrint Archive, 2023.
  * [47] Rosario Gennaro, Craig Gentry, Bryan Parno, and Mariana Raykova.  Quadratic span programs and succinct nizks without pcps.  In Advances in Cryptology–EUROCRYPT 2013: 32nd Annual International Conference on the Theory and Applications of Cryptographic Techniques, Athens, Greece, May 26-30, 2013. Proceedings 32, pages 626–645. Springer, 2013.
  * [48] Geometry.  Groth16 malleability.  https://geometry.xyz/notebook/groth16-malleability, 2023.
  * [49] Lior Goldberg, Shahar Papini, and Michael Riabzev.  Cairo–a turing-complete stark-friendly cpu architecture.  Cryptology ePrint Archive, 2021.
  * [50] Shafi Goldwasser, Silvio Micali, and Charles Rackoff.  The knowledge complexity of interactive proof-systems.  In Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing, STOC ’85, pages 291–304. Association for Computing Machinery, 1985\.
  * [51] SHAFI GOLDWASSER, SILVIO MICALI, and CHARLES RACKOFF.  The knowledge complexity of interactive proof systems.  SIAM J. COMPUT, 18(1):186–208, 1989.
  * [52] Jens Groth.  On the size of pairing-based non-interactive arguments.  In Advances in Cryptology–EUROCRYPT 2016: 35th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Vienna, Austria, May 8-12, 2016, Proceedings, Part II 35, pages 305–326. Springer, 2016.
  * [53] Kobi Gurkan.  Tornado cash vulnerability.  https://tornado-cash.medium.com/tornado-cash-got-hacked-by-us-b1e012a3c9a8, 2019\.  Accessed: date-of-access.
  * [54] Thomas Hader, Daniela Kaufmann, and Laura Kovács.  Smt solving over finite field arithmetic.  arXiv preprint arXiv:2305.00028, 2023.
  * [55] Ivan Homoliak, Sarad Venugopalan, Daniël Reijsbergen, Qingze Hum, Richard Schumi, and Pawel Szalachowski.  The security reference architecture for blockchains: Toward a standardized model for studying vulnerabilities, threats, and defenses.  IEEE Communications Surveys & Tutorials, 23(1):341–390, 2020.
  * [56] Miguel Isabel, Clara Rodríguez-Núñez, and Albert Rubio.  Scalable verification of zero-knowledge protocols.  In 2024 IEEE Symposium on Security and Privacy (SP), pages 133–133. IEEE Computer Society, 2024.
  * [57] Daniel Kang, Tatsunori Hashimoto, Ion Stoica, and Yi Sun.  Zk-img: Attested images via zero-knowledge proofs to fight disinformation, 2022.
  * [58] Aniket Kate, Gregory M Zaverucha, and Ian Goldberg.  Constant-size commitments to polynomials and their applications.  In Advances in Cryptology-ASIACRYPT 2010: 16th International Conference on the Theory and Application of Cryptology and Information Security, Singapore, December 5-9, 2010. Proceedings 16, pages 177–194. Springer, 2010.
  * [59] Hankyung Ko, Ingeun Lee, Seunghwa Lee, Jihye Kim, and Hyunok Oh.  Efficient verifiable image redacting based on zk-snarks.  In Proceedings of the 2021 ACM Asia Conference on Computer and Communications Security, ASIA CCS ’21, page 213–226, New York, NY, USA, 2021\. Association for Computing Machinery.
  * [60] Ahmed Kosba, Charalampos Papamanthou, and Elaine Shi.  xjsnark: A framework for efficient verifiable computation.  In 2018 IEEE Symposium on Security and Privacy (SP), pages 944–961. IEEE, 2018.
  * [61] Abhiram Kothapalli, Srinath Setty, and Ioanna Tzialla.  Nova: Recursive zero-knowledge arguments from folding schemes.  In Annual International Cryptology Conference, pages 359–388. Springer, 2022.
  * [62] Matter Labs.  zksync era, 2023.  https://era.zksync.io/.
  * [63] Piergiorgio Ladisa, Henrik Plate, Matias Martinez, and Olivier Barais.  Sok: Taxonomy of attacks on open-source software supply chains.  In 2023 IEEE Symposium on Security and Privacy (SP), pages 1509–1526. IEEE, 2023.
  * [64] Jan Lauinger, Jens Ernstberger, Andreas Finkenzeller, and Sebastian Steinhorst.  Janus: Fast privacy-preserving data provenance for tls 1.3.  Cryptology ePrint Archive, 2023.
  * [65] Vu Le, Mehrdad Afshari, and Zhendong Su.  Compiler validation via equivalence modulo inputs.  ACM Sigplan Notices, 49(6):216–226, 2014.
  * [66] Junrui Liu, Ian Kretz, Hanzhi Liu, Bryan Tan, Jonathan Wang, Yi Sun, Luke Pearson, Anders Miltner, Işıl Dillig, and Yu Feng.  Certifying zero-knowledge circuits with refinement types.  arXiv preprint arXiv:2304.07648, 2023.
  * [67] Tianyi Liu, Tiancheng Xie, Jiaheng Zhang, Dawn Song, and Yupeng Zhang.  Pianist: Scalable zkrollups via fully distributed zero-knowledge proofs.  Cryptology ePrint Archive, 2023.
  * [68] William M McKeeman.  Differential testing for software.  Digital Technical Journal, 10(1):100–107, 1998.
  * [69] Ian Miers, Christina Garman, Matthew Green, and Aviel D Rubin.  Zerocoin: Anonymous distributed e-cash from bitcoin.  In 2013 IEEE Symposium on Security and Privacy, pages 397–411. IEEE, 2013.
  * [70] Wilson Nguyen, Dan Boneh, and Srinath Setty.  Revisiting the nova proof system on a cycle of curves.  Cryptology ePrint Archive, Paper 2023/969, 2023.  https://eprint.iacr.org/2023/969.
  * [71] Valeria Nikolaenko, Sam Ragsdale, Joseph Bonneau, and Dan Boneh.  Powers-of-tau to the people: Decentralizing setup ceremonies.  Cryptology ePrint Archive, 2022.
  * [72] noir contributors.  noir zksnark language, 2022.
  * [73] o1 labs.  Typescript framework for zk-snarks and zkapps.  https://github.com/o1-labs/o1js, 2021.
  * [74] Trail of Bits.  CVE-2019-7167.  Available from MITRE, CVE-ID CVE-2019-7167., 2019.
  * [75] Trail of Bits.  CVE-2022-29566.  Available from MITRE, CVE-ID CVE-2022-29566., 2019.
  * [76] Alex Ozdemir and Dan Boneh.  Experimenting with collaborative $\\{$zk-SNARKs$\\}$:$\\{$Zero-Knowledge$\\}$ proofs for distributed secrets.  In 31st USENIX Security Symposium (USENIX Security 22), pages 4291–4308, 2022.
  * [77] Alex Ozdemir, Fraser Brown, and Riad S Wahby.  Circ: Compiler infrastructure for proof systems, software verification, and more.  In 2022 IEEE Symposium on Security and Privacy (SP), pages 2248–2266. IEEE, 2022.
  * [78] Alex Ozdemir, Gereon Kremer, Cesare Tinelli, and Clark Barrett.  Satisfiability modulo finite fields.  Cryptology ePrint Archive, 2023.
  * [79] Alex Ozdemir, Riad S Wahby, Fraser Brown, and Clark Barrett.  Bounded verification for finite-field-blasting (in a compiler for zero knowledge proofs).  Cryptology ePrint Archive, 2023.
  * [80] Shankara Pailoor, Yanju Chen, Franklyn Wang, Clara Rodríguez, Jacob Van Geffen, Jason Morton, Michael Chu, Brian Gu, Yu Feng, and Işıl Dillig.  Automated detection of under-constrained circuits in zero-knowledge proofs.  Proceedings of the ACM on Programming Languages, 7(PLDI):1510–1532, 2023.
  * [81] Bryan Parno.  A note on the unsoundness of vntinyram’s snark.  Cryptology ePrint Archive, Paper 2015/437, 2015.  https://eprint.iacr.org/2015/437.
  * [82] Bryan Parno, Jon Howell, Craig Gentry, and Mariana Raykova.  Pinocchio: Nearly practical verifiable computation.  Communications of the ACM, 59(2):103–112, 2016.
  * [83] Rafael Pass, Wei-Lung Dustin Tseng, and Douglas Wikström.  On the composition of public-coin zero-knowledge protocols.  SIAM Journal on Computing, 40(6):1529–1553, 2011.
  * [84] Alexey Pertsev, Roman Semenov, and Roman Storm.  Tornado cash privacy solution version 1.4.  Tornado cash privacy solution version, 1, 2019.
  * [85] Polygon.  Miden vm.  https://polygon.technology/polygon-miden, 2023.
  * [86] Polygon.  Polygon zkevm, 2023.  https://polygon.technology/polygon-zkevm.
  * [87] Purathani Praitheeshan, Lei Pan, Jiangshan Yu, Joseph Liu, and Robin Doss.  Security analysis methods on ethereum smart contract vulnerabilities: a survey.  arXiv preprint arXiv:1908.08605, 2019.
  * [88] Mir Protocol.  Plonky2, 2023.
  * [89] Protocol Labs.  Filecoin: A decentralized storage network.  https://filecoin.io/filecoin.pdf, 2023.
  * [90] Nguyen Thoi Minh Quan.  Using zero to attack zero-knowledge proof (zkp) plonk c++.  https://github.com/cryptosubtlety/00, 2021.
  * [91] Deevashwer Rathee, Guru Vamsi Policharla, Tiancheng Xie, Ryan Cottone, and Dawn Song.  Zebra: Anonymous credentials with practical on-chain verification and applications to kyc in defi.  Cryptology ePrint Archive, 2022.
  * [92] Reclaim.  Reclaim protocol.  https://www.reclaimprotocol.org/, 2023.
  * [93] Eli Ben Sasson, Alessandro Chiesa, Christina Garman, Matthew Green, Ian Miers, Eran Tromer, and Madars Virza.  Zerocash: Decentralized anonymous payments from bitcoin.  In 2014 IEEE symposium on security and privacy, pages 459–474. IEEE, 2014.
  * [94] scipt lab.  libsnark, 2020.
  * [95] Scroll.  Scroll fix for missing input constraint in ltchip.  https://github.com/scroll-tech/zkevm-circuits/commit/d0e7a07e8af25220623564ef1c3ed101ce63220e, 2023\.
  * [96] Scroll.  Scroll zkevm, 2023.  https://scroll.io/.
  * [97] Srinath Setty, Justin Thaler, and Riad Wahby.  Customizable constraint systems for succinct arguments.  Cryptology ePrint Archive, 2023.
  * [98] Fatemeh Heidari Soureshjani, Mathias Hall-Andersen, MohammadMahdi Jahanara, Jeffrey Kam, Jan Gorzny, and Mohsen Ahmadvand.  Automated analysis of halo2 circuits.  Cryptology ePrint Archive, 2023.
  * [99] Justin Thaler et al.  Proofs, arguments, and zero-knowledge.  Foundations and Trends® in Privacy and Security, 4(2–4):117–660, 2022.
  * [100] Trail of Bits.  circomspect: A static analyzer for circom 2 circuits.  https://github.com/trailofbits/circomspect, 2023.  Accessed: 2024-01-31.
  * [101] Franklyn Wang.  Ecne.  https://github.com/franklynwang/EcneProject, 2022.
  * [102] Hongbo Wen, Jon Stephens, Yanju Chen, Kostas Ferles, Shankara Pailoor, Kyle Charbonnet, Isil Dillig, and Yu Feng.  Practical security analysis of zero-knowledge proof circuits.  Cryptology ePrint Archive, 2023.
  * [103] Tiancheng Xie, Jiaheng Zhang, Zerui Cheng, Fan Zhang, Yupeng Zhang, Yongzheng Jia, Dan Boneh, and Dawn Song.  zkbridge: Trustless cross-chain bridges made practical.  In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, pages 3003–3017, 2022.
  * [104] Tiancheng Xie, Yupeng Zhang, and Dawn Song.  Orion: Zero knowledge proof with linear prover time.  In Annual International Cryptology Conference, pages 299–328. Springer, 2022.
  * [105] Xuejun Yang, Yang Chen, Eric Eide, and John Regehr.  Finding and understanding bugs in c compilers.  In Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation, pages 283–294, 2011.
  * [106] ZCash.  halo2, 2023.
  * [107] Fan Zhang, Deepak Maram, Harjasleen Malvai, Steven Goldfeder, and Ari Juels.  Deco: Liberating web data using decentralized oracles for tls.  In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, pages 1919–1938, 2020.
  * [108] Liyi Zhou, Xihan Xiong, Jens Ernstberger, Stefanos Chaliasos, Zhipeng Wang, Ye Wang, Kaihua Qin, Roger Wattenhofer, Dawn Song, and Arthur Gervais.  Sok: Decentralized finance (defi) attacks.  In 2023 IEEE Symposium on Security and Privacy (SP), pages 2444–2461. IEEE, 2023.
  * [109] zksecurity.  Noname: a programming language to write zkapps.  https://github.com/zksecurity/noname, 2023.

##  Appendix A Proof System Vulnerabilities

###  A.1 Counterfeiting – Setup Issue

Ben-Sasson et al. [13] presented a variant of Pinocchio [82] with a shorter
verification time and almost similar proving time. Given the similarity
between the two works, the authors do not provide concrete proof of security,
but rather, they reference Pinocchio’s security proof [82]. Despite the
popularity and adoption of this work by major projects such as ZCash, the lack
of security proof turned out to be a fatal choice, as critical soundness
issues were discovered [81, 41].

The trusted setup procedure described in [13] produces extra elements that are
not used neither by the verifier or an honest prover, however they can be used
to break the soundness of the proof system. These “bypass" parameters could be
recovered from the transcript of the trusted setup ceremony. In particular,
the issue enables a malicious prover, to create a proof of knowledge for any
public input given a valid proof for some public input. In the case of ZCash,
this enabled an attacker to produce accepting yet invalid proofs of knowledge
of membership witnesses for coins in the privacy pool, which is enough to
create counterfeit new coins [74].

###  A.2 Frozen Heart – Insecure Fiat Shamir Transformation

Fiat-Shamir (FS) transformation is a ubiquitous tool to compile public-coin
interactive protocols into non-interactive ones, and many SNARKs constructions
rely on it. The idea is simple: in the interactive protocol, replace any
instance of random challenge from the verifier (a.k.a. public-coin flip) with
the cryptographically secure hash of the whole transcript of the protocol up
until that point; this way, the prover does not need to interact with the
verifier anymore. The transformation hinges on the output of the hash function
being pseudo-random.

Note that if at any point a malicious prover does not like the challenge
produced by Fiat-Shamir, his only option is to change his previous messages,
but given that the hash function is cryptographically secure, he is unable to
efficiently find a suitable change. However, invoking Fiat-Shamir with only a
partial transcript of the protocol can create serious soundness issues,
referred to as Frozen Heart attacks [75]. Intuitively, this enables a
malicious prover to execute the steps of the interactive version of the proof
system in an incorrect order, likely breaking the assumptions in the security
proof. In particular, the issue enables a malicious prover, to create an
invalid proof of knowledge for some public input given a valid proof for
another public input.

###  A.3 Soundness and Malleability in Nova IVC

Incrementally Verifiable Computation (IVC) is a cryptographic primitive that
allows efficiently generating proofs for ongoing computation and produces
succinctly verifiable proofs for any prefix of the computation. Nova [61] is a
proof system that utilizes folding to realize IVC. Folding is a procedure to
aggregate two NP statements into a new one in a way that proves the new
statement is enough to prove the two original ones.

In Nova IVC at each new round the statement regarding the prefix of
computation so far is folded with the statement regarding the final step, this
folding has to be done in circuit which could involve non-native arithmetic
operations that are relatively costly. One approach to deal with non-native
arithmetic operations is to use cycles of elliptic curves, switching the
circuit and curve at each step, so that almost all of the in-circuit
arithmetic operations are native. The original implementation of Nova indeed
used a 2-cycle of curves. This variation of the proof system was not fully
specified nor proved to be secure in the original paper. Nguyen et al. [70]
showed that the implementation misses a critical check to verify the
consistency of the inputs to the two circuits, breaking the soundness
completely. Notably, [70] proposes a fix for this issue and provides proof of
security.

Moreover, [70] shows that for non-deterministic computation steps, that is,
computations that rely on auxiliary inputs (witness), Nova IVC proofs are
malleable. That is, an attacker can create invalid proofs of knowledge for
some public input given a valid proof for any public input. The idea is that
if the attacker can extract the witness for the prefix without the final step,
then he can change the auxiliary input for the final step and derive a new
proof that attests to the knowledge of auxiliary inputs in the whole chain of
computation.

##  Appendix B ZK Vulnerabilities Examples

Ref | Year |  Description | Layer | Impact
---|---|---|---|---
[74] | 2019 |  The trusted setup in Zcash’s Pinocchio-based implementation produced additional parameters that compromised the ’toxic waste’ secrecy. This vulnerability enabled malicious provers to create false proofs, leading to the unauthorized creation of Zcash tokens, effectively resulting in token counterfeiting. | Proof System | Breaking Soundness [t]
[53] | 2019 |  A vulnerability in circomlib’s implementation of the MiMC hash function, used in Tornado’s merkle tree of deposits, permitted the verification of incorrect hashes. This flaw could lead to unauthorized withdrawals of 0.1 ETH from Tornado.cash without legitimate deposits. The core issue was a computation in the hash function being performed without the necessary constraint in place, enabling this exploit. | Circuit | Breaking Soundness
[90] | 2021 |  The Aztec Plonk verifier had a flaw where setting two key elements to 0 caused it to mistakenly accept a proof, as it misinterpreted these zeros as the ‘point at infinity’ in elliptic curve cryptography. This vulnerability enables attackers to forge proofs by exploiting the verifier’s handling of these specific zero values. | Backend | Breaking Soundness
[23] | 2022 |  In Solidity, the uint256 type’s capacity to exceed the snark scalar field order poses an overflow risk. To counter this, the Semaphore verifier smart contract fails if a public input, like a group ID, exceeds this order. If a group’s ID is set too high, it causes the verifier to revert, making the group non-functional. Hence, the Semaphore smart contract had to perform a check before passing data to the circuits. | Integration | Breaking Completeness
Table 8: Representative vulnerabilities, exploits, and whitehat attacks for
SNARKs, showing the diversity of affected components and their security
impact.

In Table 8, we present four examples of vulnerabilities relevant to our study
on the security of SNARK systems. These examples demonstrate the range and
complexity of possible security issues that could compromise the
trustworthiness of systems based on SNARKs. To enhance our analysis and offer
deeper understanding into these vulnerabilities, we further explore additional
examples, including code snippets, focusing specifically on the circuit and
integration layers.

###  B.1 Circuit Layer Vulnerability Examples

####  B.1.1 Underconstrained – Assigned but Unconstrained

DSL: Circom
Project: Circomlib
Source: https://tornado-cash.medium.com/tornado-cash-got-hacked-by-
us-b1e012a3c9a8
Fix: https://github.com/iden3/circomlib/pull/22/files

Circom background. Circom enables low-level expression of computations akin to
writing arithmetic circuits, while specifying quadratic, linear, or constant
equations for constraining inputs and outputs. When compiling a Circom
program, two essential artifacts are produced: a witness generation program
and an encoding of the program in Rank-1 Constraint System (R1CS). Circom
operates on “signals,” which are finite field elements (or arrays) variables
defined with the signal keyword. These signals can be designated as inputs or
outputs, while those without such annotations are treated as intermediate
signals. The witness generator, created by the Circom compiler, calculates the
values for all intermediate and output signals based on the input. Circom
includes specific operators for computation (witness calculation) and
constraint generation (R1CS creation). The operators <\-- and \--> are
employed for signal assignment, directing witness generation, whereas === is
used for generating constraints; for instance, x === y - 1 instructs the
Circom compiler to produce a circuit accepting only when x equals y - 1. To
streamline the process where witness generation and constraint logic overlap,
Circom introduces <== and ==> operators for simultaneous signal assignment and
constraint, effectively merging these two aspects.

A common error in DSLs like Circom, which provide distinct APIs for witness
generation and constraints, is assigning a value to a witness without
subsequently constraining it. This oversight introduced a vulnerability within
Circomlib’s MiMC hash template, leading to a critical vulnerability in Tornado
Cash [53], potentially allowing all tokens from its pools to be drained.
Figure 3 illustrates this flaw. The Circom template implements the MiMC-2n/n
hash using a sponge construction. In line $10$, outs[0] is assigned a value
without being constrained. Consequently, a malicious prover could replace the
value of this signal with any arbitrary value, and the verifier would still
accept a proof for it. The correction is demonstrated in line $11$, where the
operator = is replaced with <== for both assignment and constraint. Such
subtle bug could lead to significant consequences, as demonstrated by the
Tornado Cash incident.

⬇

1template MiMCSponge(nInputs, nRounds, nOutputs) {

2 signal input ins[nInputs];

3 signal input k;

4 signal output outs[nOutputs];

5 // S = R||C

6 component S[nInputs + nOutputs - 1];

7 for (var i = 0; i < nInputs; i++) {

8 ...

9 }

10 - outs[0] <\-- S[nInputs - 1].xL_out;

11 + outs[0] <== S[nInputs - 1].xL_out;

12 for (var i = 0; i < nOutputs - 1; i++) {

13 ...

14 }

15}

Figure 3: Circom Circuit example: Underconstrained – Assigned but
Unconstrained

####  B.1.2 Underconstrained – Missing Input Constraint

DSL: Halo2
Project: Scroll zkEVM
Source:
https://github.com/Zellic/publications/blob/master/Scroll%20zkEVM%20-%20Part%201%20-%20Audit%20Report.pdf
Fix: https://github.com/scroll-tech/zkevm-
circuits/commit/d0e7a07e8af25220623564ef1c3ed101ce63220e

Halo2 background. Halo2 utilizes PLONKish arithmetization, a derivative of the
arithmetization introduced by PLONK [43]. The PLONKish arithmetization in
Halo2 is coined “UltraPLONK” and introduces custom gates as well as lookup
tables, based on plookup [42]. In PLONKish circuits, computations are
represented as tables filled with values from a finite field, where each
entry, known as a cell, contributes to the circuit’s overall functionality.
These circuits consist of gates, which impose constraints on specific groups
of cells, thereby dictating the circuit’s logic. The table columns in Halo2
circuits are categorized into three main types: instance, advice, and fixed.
Instance columns hold public inputs, advice columns contain the private
witness (comprising private inputs and intermediate values utilized in circuit
computations), and fixed columns are for constant values defining the circuit.
The circuit’s behavior is handled by gate constraints (polynomial constraints
in the circuit), copy constraints (ensuring certain cells across the table
have matching values), and lookup table constraints, all of which must be
satisfied for the circuit to be valid. Halo2, as a framework based on Plonk,
uses selectors, which are binary variables that activate or deactivate gate
constraints on a per-row basis. Halo2 circuits typically include two functions
called configure and assign (or synthesize) for setting up custom gates (i.e.,
constraints definition) and populating the table with values (i.e., witness
generation), respectively. Overall, Halo2 provides high composability,
enabling the efficient construction and verification of complex cryptographic
proofs.

A prevalent issue across various DSLs and eDSLs for SNARKs is the failure to
properly constrain certain inputs within a circuit. An illustrative case of
this vulnerability is observed in the configure function of LtChip within the
Scroll zkEVM, a component designed to evaluate and enforce a “less than”
operation between two field elements (lhs and rhs). In Figure 4, diff
represents the byte-wise difference between lhs and rhs. However, the initial
implementation of this function neglected to ensure that the diff values fell
within the valid byte range, mistakenly leaving this responsibility to
circuits incorporating the chip. This oversight led to significant
vulnerabilities elsewhere in Scroll’s codebase, where developers assumed diff
was already constrained within the appropriate range. The resolution involved
integrating a range check within the LtChip to explicitly constrain diff to
the byte range, rectifying the assumption of implicit constraint enforcement
[95]. Such oversight is not unique to Halo2 and can also occur in other DSLs
like Circom, particularly when crucial input or output constraints are absent.

⬇

1pub fn configure(

2 meta: &mut ConstraintSystem<F>,

3 q_enable: ..., lhs: ...

4 rhs: ..., u8_table: TableColumn,

5) -> LtConfig<F, N_BYTES> {

6 let lt = meta.advice_column();

7 let diff = [(); N_BYTES].map(|_| meta.advice_column());

8 let range = pow_of_two(N_BYTES * 8);

9 meta.create_gate("lt gate", |meta| {

10 let q_enable = q_enable(meta);

11 let q_enable = q_enable.clone()(meta);

12 let lt = meta.query_advice(lt, Rotation::cur());

13 // get diff_bytes

14 let diff_bytes = ...

15 // Check the correctness of diff_bytes

16 let check_a = ...

17 let check_b = bool_check(lt);

18 [chec.into_iter()

19 .map(move |poly| q_enable.clone() * poly)

20 });

21 + for cell_column in diff {

22 + meta.lookup("range check for u8", |meta| {

23 + ...

24 + });

25 + }

26 LtConfig {lt, diff, u8_table, range}

27}

Figure 4: Halo2 Circuit example: Underconstrained – Missing Input Constraint

####  B.1.3 Underconstrained – Unsafe Reuse of Circuit

DSL: Circom
Project: circom-pairing
Source: https://medium.com/veridise/circom-pairing-a-million-dollar-zk-
bug-%caught-early-c5624b278f25
Fix: https://github.com/yi-sun/circom-
pairing/pull/21/commits/c686f0011f8d18e0c11bd87e0a109e9478eb9e61

⬇

1template CoreVerifyPubkeyG1(n, k){

2 signal input pubkey[2][k];

3 signal input signature[2][2][k];

4 signal input hash[2][2][k];

5

6 var q[50] = get_BLS12_381_prime(n, k);

7 component lt[10];

8 for(var i=0; i<10; i++){

9 lt[i] = BigLessThan(n, k);

10 for(var idx=0; idx<k; idx++)

11 lt[i].b[idx] <== q[idx];

12 }

13 for(var idx=0; idx<k; idx++){

14 // Assign and constraint lt[idx].a

15 ...

16 }

17 + var r = 0;

18 + for(var i=0; i<10; i++){

19 + r += lt[i].out;

20 + }

21 + r === 10;

22 ...

23}

Figure 5: Circom Circuit example: Underconstrained – Unsafe Reuse of Circuit

A common root cause of vulnerabilities in circuits is the unsafe reuse of
other (safe) circuits. In Figure 5, the vulnerability is related to the unsafe
reuse of a sub-circuit within the circom-pairing library in the
CoreVerifyPubkeyG1 template. This template plays a pivotal role in verifying
signatures for public keys, relying on the assumption that all inputs,
specifically curve coordinates, fall within the finite field defined by the
curve’s prime number $q$, thus within the interval from $0$ to $q$ and are
properly formatted big integers. The validation for this assumption is
attempted through ten instances of the BigLessThan component, which sets its
output signal out to $1$ if integer a is less than b, and to $0$ otherwise,
also ensuring a and b’s proper format. However, a critical oversight was the
failure to constrain the output signals of each BigLessThan component in the
lt array. Consequently, the CoreVerifyPubkeyG1 template could accept inputs
exceeding $q$ or improperly formatted, significantly enlarging the attack
surface. The rectification for this flaw involves enforcing every lt
component’s output signal to equal one. This scenario underscores the inherent
risk in implicitly assuming sub-circuit constraints without explicit
enforcement, a common pitfall across DSLs for SNARKs. Addressing such
vulnerabilities necessitates meticulous constraint application, even when
optimizing, to safeguard circuit integrity. The example provided serves as a
cautionary tale, emphasizing the importance of comprehensive constraint
verification in circuit design. Note that this problem is not unique to
SNARKs, and it is important to clarify that the BigLessThan circuit itself is
not faulty in this context. These errors often stem from the intricacies and
challenges associated with the low-level programming model of many SNARK DSLs.
For instance, a language that warns users about unused return values could
help prevent such oversights. Similarly, another prevalent issue within the
same root cause of vulnerabilities occurs when circuits explicitly outline
certain assumptions – for instance, specifying that an input should fall
within a particular range – yet these constraints are not enforced by the
calling function.

####  B.1.4 Underconstrained – Out-of-Circuit Computation not Being
Constrained

DSL: Arkworks
Project: Penumbra
Source: https://penumbra.zone/pdfs/zksecurity_penumbra_2023.pdf
Fix: https://github.com/penumbra-
zone/penumbra/commit/e019839939968012ed2d24cf65bdd86d239b50e9

⬇

1pub fn derive(nk: &NullifierKeyVar, ak: &AuthorizationKeyVar) -> Result<Self,
SynthesisError> {

2 let cs = nk.inner.cs();

3 let ivk_domain_sep = FqVar::new_constant(cs.clone(), *IVK_DOMAIN_SEP)?;

4 let ivk_mod_q = poseidon377::r1cs::hash_2(

5 cs.clone(),

6 cs,

7 &ivk_domain_sep,

8 (nk.inner.clone(), ak.inner.compress_to_field()?),

9 )?;

10 let inner_ivk_mod_q: Fq = ivk_mod_q.value().unwrap_or_default();

11 let ivk_mod_r = Fr::from_le_bytes_mod_order(&inner_ivk_mod_q.to_bytes());

12 let ivk = NonNativeFieldVar::<Fr, Fq>::new_variable(

13 cs,

14 || Ok(ivk_mod_r),

15 AllocationMode::Witness,

16 )?;

17 Ok(IncomingViewingKeyVar { inner: ivk })

18}

Figure 6: Arkworks Circuit example: Underconstrained – Out-of-Circuit
Computation not Being Constrained

Penumbra uses nullifiers in shielded transactions to ensure notes can be spent
without revealing their spend status. A nullifier is deterministically derived
using a nullifier key (nk) and a note commitment. To spend a note, users must
prove ownership of an incoming viewing key (ivk), which is derived from nk.
The ivk derivation involves converting a value from the circuit field
($F_{q}$) to a non-native field ($F_{r}$), as ivk is used for scalar
multiplication (see Figure 6). The vulnerability arises during this field
conversion, where the ivk_mod_q value is taken out of the circuit, converted
to ivk_mod_r, and then reinserted as a witness value under ivk, removing any
constraint linking ivk back to ivk_mod_q. This lapse allows a malicious prover
to manipulate ivk or ivk_mod_q, enabling the creation of incorrect nullifiers
and potential double-spending.

###  B.2 Integration Layer Vulnerability Examples

####  B.2.1 Passing Unchecked Data – Missing Validation Input

⬇

1function collectAirdrop(bytes calldata proof, bytes32 nullifierHash) public {

2 + require(uint256(nullifierHash) < SNARK_FIELD ,"...");

3 require(!nullifierSpent[nullifierHash], "...");

4

5 uint[] memory pubSignals = new uint[](3);

6 pubSignals[0] = uint256(root);

7 pubSignals[1] = uint256(nullifierHash);

8 pubSignals[2] = uint256(uint160(msg.sender));

9 require(verifier.verifyProof(proof, pubSignals), "...");

10 nullifierSpent[nullifierHash] = true;

11 airdropToken.transfer(msg.sender, amountPerRedemption);

12}

Figure 7: Integration example: Passing Unchecked Data – Missing Validation
Input

Language Solidity
Project: zkdrops
Source: https://github.com/a16z/zkdrops/pull/2
Fix: https://github.com/a16z/zkdrops/pull/2/files

Zkdrops is a tool designed for distributing tokens, commonly known as
airdrops, in a privacy-preserving way. Users initially submit a commitment
message publicly and later claim their tokens through a ZKP, verifying their
inclusion in a Merkle tree without revealing their identity. This process
blends their claim with others, maintaining anonymity. To prevent double-
spending, zkdrops employ nullifiers; users must submit a unique nullifier with
their proof to collect tokens. However, a flaw was identified in the system’s
implementation, showcased in the provided Solidity code (c.f. Figure 7). The
issue lies in the failure to validate that the nullifier falls within the
SNARK field’s bounds. This enables the creation of nullifiers that, while
valid uint256 have the same result modulo the field, are treated as distinct
by the spent nullifier dictionary, thereby permitting double-spending. The fix
of this issue involves incorporating a validation step (shown in line 3 of
Figure 7) to ensure nullifier values are properly constrained. This type of
vulnerability is common at the integration layer, underscoring the importance
for developers to rigorously apply and check all assumptions made at the
circuit level within the integration layer to prevent crucial vulnerabilities.

####  B.2.2 Proof Delegation Error – Integration Design Error

⬇

1pub struct Execution<N: Network> {

2 transitions: IndexMap<N::TransitionID, Transition<N>>,

3 global_state_root: N::StateRoot,

4 proof: Option<Proof<N>>,

5}

Figure 8: Integration example: Proof Delegation Error – Integration Design
Error

Language Rust
Project: AleoVM
Source: https://www.zksecurity.xyz/blog/2023-aleo-synthesizer.pdf

To facilitate a function call on the Aleo network, a user decomposes the call
into a sequence of transitions (see Figure 8). Each transition correlates with
a nested function call, implying that if the initial function call, referred
to as main, generates $n$ nested calls, there would be $n+1$ transitions, with
the last transition reflecting the completion of the main function call.
Transitions are linked to specific synthesized circuits, and each circuit is
paired with a proof, though all proofs are ultimately merged into a single
comprehensive proof. The process for each transition circuit begins with the
verification of a signed request, confirming the user’s intention. This
mechanism enables a user to delegate the execution of a particular function to
a third-party prover without granting them the authority to execute additional
functions. Since each transition possesses an individual request, detached
from the overall execution context, a third-party prover can sequentially
exclude callers by omitting subsequent requests during execution. This
scenario permits a third-party prover to truncate the full execution desired
by the user, only processing a limited number of nested calls and possibly
hindering the execution of encompassing logic. For instance, in a situation
where function fn1 invokes fn2, the third-party prover might only acknowledge
the request to execute fn2. Although this vulnerability is not explicitly tied
to ZKPs, it highlights challenges within the broader infrastructure necessary
for implementing and utilizing ZKPs effectively. The issue arises from users
needing to entrust execution to potentially untrusted provers, which, due to
flawed design, allows these provers to alter the intended execution path.
Addressing this requires a redesign incorporating a counter in each transition
circuit as a publicly verifiable input. This counter, incremented with each
transition proof verification, must be included in each request’s signature,
ensuring the integrity and intended sequence of execution.