- Write detailed documentation and spec before writing the circuits.
- Bugs can be discovered here!
- Will help you while writing and reviewing the circuits.
- Example: Something is intended to be private but it's actually not in circuits.
ZK stack
- Underlying theory (Groth16, Plonk, STARK)
- Implementing theory: Circom / Halo2 / Winterfell - Proving and Verifiction
- Application: Circuits in Circom - Easiest to start with if no cryptography background.
Bugs in ZK applications
- Privacy bugs: expected private property not private.
- Verify incorrect computation, or reject correct computation.
Types of circuits
- Cryptography primitives: ECDSA, Hash
- Libraries: LessThan, IsZero
- User Applications: Tornado Cash, zk rollups
You may have to write libraries yourself to write applications.
Understand Elliptic Curves
- Many cryptographic primitives rely on Elliptic curves.
- Ethereum addresses, ECDSA, BLS signatures, Hashes, …
Split computation and constraints
- Computation and proof generation is in adversarial setting.
- Just focusing on constraints helps internalize this fact.
Split it into:
and
function quotient_and_remainder(a,b) {
return [a/b, a%b];
}
signal input a;
signal input b;
signal qr[2] <-- quotient_and_remainder(a,b);
a === qr[0]*b + qr[1]
Removing all computation
- Does this ensure that
qr[0]
and qr[1]
are quotient and remainder?
Removing all computation
- Does this ensure that
qr[0]
and qr[1]
are quotient and remainder?
- Missing constraint:
qr[1] < b
.
Signal overflow
ZK circuits operate on field elements:
For a=11
:
"x": "5",
"y": "7",
"z": p-1
"x": "5",
"y": "6",
"z": "0"
p=21888242871839275222246405745257275088
548364400416034343698204186575808495617
- EVM uint size: 256 bits
- BN254 prime field, common Circom field: 254 bits
uint
passed as a public input to a verifier may overflow.
- Ensure
uint
fits in the field range (< p
).
Library Integration
- Library assumptions should be documented.
- Libraries built for high-performance circuits do not enforce preconditions on inputs.
- Minimizing constraints is critical for circuits built on top of it.
- Precondition constraint is done outside the library.
LessThan
- You may expect
LessThan(n)
to compare two signals of max n
bits, but it doesn't verify the bit length.
- According to
LessThan(2)
: 1 >= p-2
.
- Fix: Constraint the inputs to specific max bit using
Num2Bits
.
Under-constrained signals
- A broad class of bugs.
- Free input signals.
- Underconstrained signals during library integration.
- Or simply just missing contraining a signal.
Logic Bugs
- The algorithm developed through the circuits. Any footguns or bugs there?
- What if a shielded pool allows depositing arbitrary amount?
- Integration with smart contracts.
Testing
Resources