TL;DR
Assertions do not add any constraints
Recently we stumbled upon Circom’s assert() statements that were used to enforce some constraints in a project implementing a UTXO-based optimistic privacy-preserving L2. Sadly, it is not a magic tool that allows programmers to go over the complexity of expressing some non-trivial constraints.
Background
Zero-knowledge proofs and ZK circuits
Short version: zero-knowledge proofs allow one to prove that a statement is true without revealing anything else about it apart from the fact that it is true.
ZK circuits, used in zk-SNARKs and zk-STARKs, encode the constraints that define some relations one wants to prove and hold between the inputs and the output of a circuit. Not all relations can be proven by zk-SNARKs, the proof system used by the project we were looking at, they must have a quadratic arithmetic program (QAP) representation, more on QAPs in this article by Vitalik.
What is Circom ?
Circom is a circuit compiler offering a domain-specific language (DSL) that abstracts away the complexity of building the polynomials required to build the zero-knowledge proof. It is currently one of the most widely used DSL for ZK circuits.
Circom lets the programmer define so-called templates which are building blocks for the circuits. The programmer defines input and output signals to the circuit and writes the constraints in the template, e.g. constraining the circuit input x to be equal to zero is expressed with x === 0. In Circom a constraint is expressed with a === b, and a constraint with assignation with a <== b.
Circom assertions are mermaids
Writing constraints that can be proven (QAP) can be tricky, especially when one wants to prove that “something is not”. Let’s take the example of an array where we do not want any duplicates, in our optimistic L2 it is needed to prevent double-spending within the same transaction. The idea is:
The solution that was implemented for the constraint was assert(array[j] == 0 || array[i] != array[j]), which seems correct at first glance. But if we look closer at what the attractive assert() statement does, it turns into a monster. According to Circom’s documentation, the assertions only play a role during circuit compilation and witness generation.
Assertions do not add any constraints in the circuit, they only act as input sanitization. Let’s take the example of circuits A and B, the two circuits are the same and take the signal x as input, the only difference is that the circom code of A contains assert(x != 0). One could generate a proof from B and provide x = 0, this proof will be valid when verified by the verifier built from A.
In our optimistic L2, the consequence is that double spending becomes possible within a transaction and the system does not allow challenging a transaction with itself.
How can we turn an assert into a constraint?
A proper constraint must be added. One possible solution here is to use templates from circomlib:
Conclusion
While it’s easy to mistakenly assume certain behaviors in new fields like zero-knowledge circuits, this issue highlights the importance of understanding the foundational concepts.
Drawing upon lessons from the early days of smart contracts, we must strive not to replicate past errors and take security seriously from the start.
The circom documentation may communicate this crucial caveat more clearly. Extensive testing may have allowed to catch this unexpected behavior.
ChainSecurity Zero-Knowledge circuits audits
ChainSecurity is among the oldest and most trusted smart contract audit companies. Our team conducts smart contract audits since 2017 and we are trusted by many long-term partners such as blue-chip DeFi protocols, promising Web3 projects, and the central banking sector.
Are you interested in an audit of your circuits and in improving the security of your ZK project? We’d love to hear from you at contact@ChainSecurity.com.
Topics Covered in this article
Circom, Circom assert, zero-knowledge circuits security, zk circuits audit, cybersecurity, blockchain security, vulnerability mitigation