Try   HackMD

Tips for safe circom circuits


Write documentation and comments

  • 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.
signal c <== a*b;

Split it into:

c <-- a*b;

and

c === a*b;

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

a === qr[0]*b + qr[1]
  • Does this ensure that qr[0] and qr[1] are quotient and remainder?

Removing all computation

a === qr[0]*b + qr[1]
  • 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:

(p1)+1=0modp

signal a <== x+y+z;

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