Tips for secure circom

--- title: Tips for secure Circom circuits tags: Templates, Talk description: View the slide with "Slide Mode". --- # 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. ```js signal c <== a*b; ``` Split it into: ```js c <-- a*b; ``` and ```js c === a*b; ``` --- ```js 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 ```js a === qr[0]*b + qr[1] ``` - Does this ensure that `qr[0]` and `qr[1]` are quotient and remainder? --- Removing all computation ```js 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: $$ (p-1) + 1 = 0 \mod p $$ ```js signal a <== x+y+z; ``` For `a=11`: ```json "x": "5", "y": "7", "z": p-1 ``` ```json "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 - [circom_tester](https://github.com/iden3/circom_tester) by iden3: afaik can't test with fake witness. - [circomkit](https://github.com/erhant/circomkit) by [erhant](https://twitter.com/0xerhant): can test with fake witness. - Formal verification tools: CODA, Picus by Veridise. [circom-bigint report](https://f8t2x8b2.rocketcdn.me/wp-content/uploads/2023/02/VAR-circom-bigint.pdf). - [circomspect](https://github.com/trailofbits/circomspect) by ToB: static analyzer. --- ### Resources - ZK bug tracker: https://github.com/0xPARC/zk-bug-tracker - Moonmath manaul: https://github.com/LeastAuthority/moonmath-manual - Elliptic curves basics: https://hackmd.io/@blockdev/BJIW0Rlr3 - Rareskills ZK book: https://www.rareskills.io/zk-book