Circom-Pairing: A Million-Dollar ZK Bug Caught Early
This blog post is also available in the following languages: 简体中文.
In this blog post, we will dissect a critical security issue discovered by Veridise in the circom-pairing library. The circom-pairing library is a circom implementation of elliptic curve pairings for the widely-adopted BLS12–381 curve. This library enables Zero-Knowledge (ZK) systems to verify signatures over the BLS12–381 curve. The Veridise team identified several issues in circom-pairing in the context of a security audit ordered by Succinct Labs, whose innovative bridge design relies heavily on verifying BLS12–381 signatures. The most critical bug discovered by our team could allow attackers to forge signatures.
Are you interested in more details? Buckle up and keep reading! But first, some background on circom-pairing and its design.
The Circom-Pairing Library
Programs in languages like Circom encode computation as a set of constraints. Given these constraints, the compiler generates two artifacts. The first one, called the prover, generates proofs for input-output pairs that satisfy the constraints of the program. In the context of circom-pairing, for instance, we can prove the validity of a BLS12–381 signature for a given public key. The second artifact, called the verifier, can verify the validity of a proof without running the actual computation. Because proof generation time depends on the number of constraints, ZK systems aim to reduce the constraints the verifier needs to check. Given all this, you might think implementing cryptographic pairing algorithms in Circom is a daunting endeavor. Well, you are 100% correct.
Not enough bits. The first challenge in implementing pairings over BLS12–381 stems from the “381” part of the curve’s name, which represents the number of bits needed to describe pair of integers (x,y) that lie on the curve. However, the current ecosystem for verifying circom proofs supports only 254-bit integers. To bypass this limitation, the authors of circom-pairing had to create a library for integers of arbitrary bit length (big integers for short). Each library function operates over a big integer that consists of k registers containing an n-bit integer. For instance, consider the following code excerpt from a function that compares two big integers.
/*
Inputs:
- BigInts a, b
Output:
- out = (a < b) ? 1 : 0
*/
template BigLessThan(n, k){
signal input a[k];
signal input b[k];
signal output out;
...
}As the comment of BigLessThan indicates, the output signal out will be set to 1 if the integer represented by a is less than the integer represented by b. Otherwise, out will be set to 0. Additionally, template BigLessThan ensures that integers a and b are properly formatted, i.e., each of their k registers contain an n-bit integer.
Constraints everywhere. Another challenge in implementing circom-pairing is that verifying BLS12–381 requires checking several million constraints. Optimizing such a complex ZK system posed a tremendous challenge to the circom-pairing developers. A crucial design decision in circom-pairing that drastically reduced the number of generated constraints was to omit data validation in several core templates of the library. For instance, several core circuits in circom-pairing assume their inputs are properly formatted big integers that fall in a certain range. Hence, users of such circuits must also use the BigLessThan template to perform appropriate data validation for the core circuits. As we shall see next, this decision can, unfortunately, backfire.
Did You Check Your Signals? Check Again!
Let’s discuss some bugs. The critical bug discovered by our team originates in a circuit called CoreVerifyPubkeyG1, which, as the name suggests, has the crucial task of verifying a signature for a public key. Before performing the signature verification, CoreVerifyPubkeyG1 must ensure that all of its inputs conform to the assumptions made by the core circom-pairing templates (recall the optimization?). The most important of these assumptions are that all curve coordinates belong to the finite field defined by the curve's prime number q, i.e., the interval [0, q-1), and are properly formatted big integers. These checks happen in the following code snippet, which uses ten instances of our old friend BigLessThan.
// Inputs:
// - pubkey as element of E(Fq)
// - hash represents two field elements in Fp2, in practice hash = hash_to_field(msg,2).
// - signature, as element of E2(Fq2)
// Assume signature is not point at infinity
template CoreVerifyPubkeyG1(n, k){
...
var q[50] = get_BLS12_381_prime(n, k);
component lt[10];
// check all len k input arrays are correctly formatted bigints < q (BigLessThan calls Num2Bits)
for(var i=0; i<10; i++){
lt[i] = BigLessThan(n, k);
for(var idx=0; idx<k; idx++)
lt[i].b[idx] <== q[idx];
}
for(var idx=0; idx<k; idx++){
lt[0].a[idx] <== pubkey[0][idx];
lt[1].a[idx] <== pubkey[1][idx];
... // Initializing parameters for rest of the inputs
}
...
}It looks like everything is in place, right? Well, it isn’t! One crucial thing missing is constraining the output signals of every component in array lt. Recall that the output signal of BigLessThan is set to one if the integer represented by array a is smaller than the one represented by b and zero otherwise. Since the version of CoreVerifyPubkeyG1 above does not check the output signal of any BigLessThan component in lt, it can accept inputs that are larger than q, the curve's prime, or are not properly formatted. Omitting this crucial data validation step at the outermost circuit that implements signature validation exposes a substantial attack surface.
The Fix
Let’s now see how we can fix this issue. Luckily, subtle issues usually have easy fixes. In this case, all we need to do is constraint every output signal of components in lt to be equal to one. Our team came up with the following fix for this issue, which is already merged in the circom-pairing library.
template CoreVerifyPubkeyG1(n, k){
...
var q[50] = get_BLS12_381_prime(n, k);
component lt[10];
... // Loops same as before
var r = 0;
for(var i=0; i<10; i++){
r += lt[i].out;
}
r === 10;
...
}Lessons Learned
As the DeFi history already taught us, even innocuous mistakes can have significant security implications. This history is already repeating itself in the ZK domain, albeit in a more intricate way. Developers not only need to ensure their circuits compute the correct result but they also need to ensure the resulting verifier does not accept more input-output pairs than anticipated. Therefore, traditional end-to-end testing techniques fall short in this domain due to the non-traditional system architecture of ZK systems. To that end, it is important to build new analysis and verification tools that help developers reason about such edge cases. Here at Veridise, our team of program analysis and security experts is constantly building analysis tools that help us uncover such bugs. Stay tuned for future blog posts on ZK-related tooling that we are building that help us find critical issues.
Acknowledgments
We would like to thank Jonathan Wang, Vincent Huang, and Yi Sun, authors of circom-pairing, as well as Uma Roy and John Guibas from Succinct Labs for being excellent collaborators throughout the audit and providing insightful feedback on this blog post.
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
