ZK Vulnerabilities: Sharp rocks hidden in deep water
In this blog post, we will talk about common vulnerabilities in Circom programs and their root causes. If you are not familiar with either zkSNARKs, R1CS or the Circom programming language, we highly recommend that you first read our previous blog post A Gentle Introduction to ZKPs and Circom before you continue with this one.
Background
As security auditors at Veridise, we’ve looked at a lot of ZK circuits and uncovered potentially disastrous vulnerabilities. (For instance, see our previous blog Circom-Pairing: A Million-Dollar ZK Bug Caught Early.) When reflecting on our time auditing ZK circuits, one of the things we noted was how helpful it was (especially at the beginning) to have the common vulnerability tracker from 0xPARC. When looking at code in a new or unfamiliar framework, especially a new paradigm like ZK, it is easy to get lost, and having a document that details common types of bugs in the framework gives you a concrete list of things to look for. However, we quickly found that many of the bugs we were discovering in these circuits were not covered by the tracker. So, we decided to re-examine the bugs we found, identify the common patterns, and share them to help ZK implementers avoid (and help ZK auditors find 🙂) these sharp rocks hidden in deep water.
Constraint-Computation Discrepancies
Recall from our previous blog post (A Gentle Introduction to ZKPs and Circom) that many ZKP languages, including Circom, compile the program to two different programs: (a) a witness generator function (henceforth referred to as “computation”), and (b) a set of constraints. Intuitively, for the circuit to be correct, the computation P and the constraints C must have the same semantics with respect to each other: Given an input x, it should be the case that P(x) = y (where y is the output signal) if and only if C(x,y) evaluates to true. We refer to this relationship as the “fundamental ZKP invariant”, and, if this invariant does not hold, the program likely contains a bug. We refer to such problems as “constraint-computation discrepancies”.
But how do these constraint-computation discrepancies arise in practice? One might be tempted to think that this should never happen because you can always use the <== operator in Circom. Recall from the previous blog that this operator simultaneously generates constraints and performs assignment for witness generator. So, if you always use <== instead of < — and ===, why would these problems ever arise?
Well, the problem is that many types of computation cannot be directly expressed as a constraint (particularly due to the requirement that constraints must be compilable down to R1CS). As a result, there are many situations where one cannot use the <== operator and must try to express the computation and constraint differently, while still ensuring that our fundamental ZKP invariant is satisfied.
To gain more insight about these vulnerabilities caused by “computation-constraint discrepancies”, let’s consider the Edwards2Montgomery circuit:
template Edwards2Montgomery() {
signal input in[2];
signal output out[2];
out[0] <-- (1 + in[1]) / (1 - in[1]);
out[1] <-- out[0] / in[0];
out[0] * (1-in[1]) === (1 + in[1]);
out[1] * in[0] === out[0];
}
component main = Edwards2Montgomery();This circuit is intended to convert a point on an Edwards curve to one on the corresponding Montgomery curve. Let’s consider the constraints here first: when out[0] = 0, out[1] = 0 and in[1] = -1, those two constraints will be: 0 * 2 === 0 and 0 * in[0] === 0 . Note that both of these equations will be satisfied (and proof verified) regardless of what is provided for in[0]!
To summarize, the semantics of out[1] ← out[0] / in[0] are different from its corresponding constraint out[1] * in[0] === out[0] when out[1] and out[0] are 0. Clearly, this code violates the fundamental ZKP invariant because, in the constraint part, in[1] can have an arbitrary value and still satisfy the constraint! To fix the problem, the developer needs to constrain the divisors to be non-zero.
Missing Input-Output Dependencies
A second bug pattern we came across a fair amount during our audits is due to missing dependencies between the circuit’s inputs and outputs. As an example, consider the following bug we came across during one of our audits:
template ChunkedMul(m, n, base){
signal input in1[m];
signal input in2[n];
signal carry[m+n];
signal output out[m+n];
component lt[m+n];
...
// carry[m+n-1] is constrained by in1 and in2 before.
out[m+n-1] <-- carry[m+n-1];
for(i = 0; i< m+n; i++) {
lt[i] = LessThanPower(base);
lt[i].in <== out[i];
out[i] * lt[i].out === out[i];
}
}
component main = ChunkedMul(3, 3, 51);This code snippet from the ed25519-circom project corresponds to the template of the ChunkedMul circuit, which implements a chunked multiply algorithm to perform multiplication on two values. These values are represented as arrays (of size m and size n) such that every element in the array should be less than 2 ** base. The output signal out is declared as an array of size m+n and should represent the result of the multiplication. However, there is actually a vulnerability here: (Assume we are in the iteration when i = m+n-1, shown in the above code snippet.)
// carry[m+n-1] is constrained by in1 and in2 before.
out[m+n-1] <-- carry[m+n-1];
lt[m+n-1] = LessThanPower(base);
lt[m+n-1].in <== out[m+n-1];
out[m+n-1] * lt[m+n-1].out === out[m+n-1];The intention of the developer here is to assign the value of carry[m+n-1] to out[m+n-1] and constrain out[m+n-1] to be less than 2 ** base.
Let’s check the constraints here:
First, the intermediate signal carry[m+n-1] is constrained by the input signals in1 and in2.
Second, out[m+n-1] and lt[m+n-1] are constrained by each other.
And then…?
It is obvious out[m+n-1] is not constrained by carry[m+n-1] and any other signals which are constrained by any input signals!
Therefore, a malicious user can convince the verifier that signal out[m+n-1] is an arbitrary value less than 2 ** base! According to the project’s documentation, this template implements a crucial operator that is directly applied to the inputs of the overall algorithm. Thus, the vulnerability uncovered by our audit exposes a substantial attack surface for the whole system. To fix this problem, the developer needs to add additional constraints asserting that out[m+n-1] is equal to carry[m+n-1].
Unsafe Component Use
Many ZKP languages support so-called “components”, which are auxiliary circuits used in the top-level circuit definition. Essentially, we can think of “ components” as calling a third party library in a regular programming language. But, just as traditional APIs make certain assumptions about how they should be used (e.g., input should not be zero or “read” should not be called before “open”), components often also make certain assumptions about their usage! For example, a component may assume that users will constrain their input or output signals in certain ways. Thus, if the developer is unaware of such (implicit or explicit) assumptions made by the component, they may end up using it in an unsafe way and introduce subtle bugs into their application. In fact, the bug described in Circom-Pairing: A Million-Dollar ZK Bug Caught Early is exactly such a case: the bug is caused by the output of a component being unconstrained in the top-level circuit!
ZKAP: The tool protects your ZKP Circuit
While some bugs in Circom programs are quite obvious and can be detected using simple syntactic checks, others are much more subtle and require deeply understanding program semantics. To help us (and others) find bugs in Circom programs more reliably, we built a new static analysis tool called ZKAP that can be used to catch a large family of bugs in ZK circuits. If you are interested in learning more, please check out the preprint of one of our recent publications: https://eprint.iacr.org/2023/190.pdf
About Veridise
Veridise is a blockchain security company that provides audits and software analysis tools for all layers of the blockchain ecosystem, including smart contracts, web3 applications, zero-knowledge circuits, and blockchain implementations. Co-founded by a team of formal verification and software security researchers, Veridise provides state-of-the-art tooling for hardening blockchain security. Our clients can work with us in a variety of ways, including hiring us for security audits, using our automated security analysis tools (for testing, static analysis, formal verification), or a combination of these.
If you’re interested in learning more information, please consider following us on social media or visiting our website:
Website | Twitter | Facebook | LinkedIn | Github | Request Audit
