Secure ZK Circuits via Formal Methods Guest Lecturer: Yu Feng (UCSB & Veridise) Zero Knowledge  Proofs Instructors: Dan Boneh, Shafi Goldwasser, Dawn Song, Justin Thaler, Yupeng Zhang EORGETOWN UNIVERSITY AM    TEXAS A&M Motivation Bugs in blockchain software are extremely costly Bugs in any of these layers can be catastrophic when exploited! /// 2
→ Apr 18, 2022 ① 2 min read Flash loan vulnerability in smart contract m
CRYPTO WORLD Solana suffered its second outage in a month, sending price plunging share f Y in W POINT outage in the las DoS vulnerability in consensus protocol experiment isn't saving the country’s finances Jakuh Porzycki / NurPhoto via / Grity Images 4
Zcash team fixes serious vulnerability that allowed counterfeiting Malware and Vulnerabilities • The vulnerability was discovered by a cryptographer from Zcash Company in March 2018. • Attackers could create fake Zcash coins in large numbers by exploiting this vulnerability. Bug in arithmetic circuit implementing zkSNARK! ZKP MOOC 5
6 Section 1 Formal Methods in a Nutshell 7 What is Formal Methods Set of mathematically rigorous techniques for finding bugs and constructing proofs about software ZKP MOOC 8
STATIC Execute the program on interesting inputs & monitor what happens Analyze source code and reason about all executions
ZKP MOOC
10

● Blue irregular shape is the actual states ● Red region corresponds to “bad states” ● Due to undecidability, we can never determine exactly what the blue region is ● Over-approximate blue region with the regular green region above ZKP MOOC 11
False Positives False Negatives ZKP MOOC 12
ZKP MOOC 13
ZKP MOOC 14 Static Analysis via Abstract Interpretation Idea: Emulate all possible program paths if(flag) X = 1; else When in doubt, conservatively assume either path could be taken and merge information for different paths 15 Abstract Interpretation Tools in Web3 • Slither (TrailOfBits) • Sailfish (Bose et al, Oakland’22) • Vanguard (Veridise)
●Program implementation: Source code of the program, or intermediate representation ●The specification: A formal description of the property to be verified ●Human annotations (optional): Loop invariants, Contract invariants
ZKP MOOC
17

Formal specification: Precise mathematical description of intended program behavior, typically in some formal logic ((finish(bid, msg . value = X ∧ msg . sender = L)) ∧ ♦ finish(close, L ≠ winner) If auction closes with me not being the winner, I ZKP MOOC 18 Formal Verification Tools in Web3 • Certora prover (Certora) • K framework (Runtime Verification) Different Flavors of Static Analysis Formal verification checks program against provided specification Abstract Interpretation . Looks for known types of bugs Doesn’t require specifications Formal Verification Can find (prove absence of) any bug Requires specifications 20 Section 2 Formal Methods in ZK: part I 21
Sourče Code: Witness Generation and Constraints 22
|Program: P Set of Constraints: C Input: x Inputs: x, y Output: y Output: true or false For every x, y. P(x) = y if and only if C(x, y) is true Every input-output of P must satisfy G Every (x,y) which satisfy C must be an input-out pair of P 23
(2) Two Requirements: Every input-out pair of P satisfies C For any x, y which satisfy C, P(x) = y Overconstrained Bugs Underconstrained Bugs Exists x , y where P(x) = y but C(x, y) is false Exists x, y where C(x, y) is true but P(x) ≠

24

Could be used to drain all tokens ZK Circuit Workflow Underconstrained bugs: Verifier can accept bad inputs/ outputs Tornado.cash got hacked. By us.
BigMod incorrectly omits range checks on the remainder #10
osure of recent vulnerabilities
We have recently patched two severe bugs in Aztec 2.0. The first was found by an Aztec engineer and the second by community members. 1. Lack of range constraints for the  tree_index  variable 25 ZKP MOOC
Corresponds to signals whose constraints always evaluate to true, accepting everything Unconstrained Signals ZKP MOOC 27
Buggy Implementation template Num2Bits(n) { signal input in; signal output out[n]; var lc1 = 0; var e2 = 1; } lc1 === in; Constraints for n = 3 input in output  out, out, out, outo • (outo − 1) = 0 out1 · (out1 − 1) = 0 outo + 2 * out1 = in Attacker can pass in any value for out, https://github.com/iden3/circomlib/blob/master/circuits/bitify.circom 28 ZKP MOOC
Sub-circuits often assume constraints are placed on inputs and outputs Corresponds to cases where the use of a sub-circuit do not follow Unsafe Component Usage ZKP MOOC
template withdraw(n) { assert(n <= 252); signal input bal; signal input amt; signal output out; lt.out === 0 component n2b1 = Num2Bits(n); // assert (bal < 2^n) n2b1.in <== bal; component n2b2 = Num2Bits(n); // assert (amt < 2^n) n2b2.in <== amt; ^component lt = LessThan(n); // check amt < bal lt.in[0] <== bal; lt.in[1] <== amt; out <== bal – amt; Without the missing constraint, attacker can withdraw more funds than they have ZKP MOOC 30
Not all computation can be directly expressed as a constraint Corresponds to constraints that do not capture a computation’s semantics Constraint/ Computation Discrepancy
Accepts arbitrary out when a and b are 0! ZKP MOOC 32
Goal: Identify discrepancies between computation and constraints o ＜ーー i O === i Output Signal ZKP MOOC 33
Source Code Common Vulnerability Report Used to evaluate 258 circuits from 17 public Circom projects on Github wash ZKP MOOC 34
Identified 32 previously unknown vulnerabilities! Developers have the most difficulty reasoning about a computation’s semantics! ZKP MOOC 35 Section 3 Formal Methods in ZK: part II
Static Analysis of Constraints (SA) Apply predefined rules to quickly detect if circuit is properly constrained input x output y Since y is linear in x, z we immediately infer it is not under constrained SMT Solver Underconstrained can be expressed as SMT query ∃y₁, y₂ ⋅ P [y₁/y] ∧ P [y₂/y] ∧ y₁ ≠ y₂ SAT means the circuit is underconstrained ZKP MOOC 37 If it can prove P is constrained Polynomial Field Equations If it can prove P is unconstrained Otherwise Combine the strengths of Static Analysis and SMT! Fast but imprecise! Precise but slow! Static Analysis and SMT phases interact in a loop ZKP MOOC 38
Takes as input field equations P, and set of signals K proven At the start of the algorithm K = {}. ↑ K' New set K'of signals proven unique. K ⊆ K' If OutputSignals ⊆ K' we return Otherwise we send K' as input to SMT Phase

39

K" computed assuming K. Larger K = faster query. K C K" If OutputSignals ⊂ K'' we return If OutputSignals ∩ Kuncons̸= ∅ we return p X lf K = K" we return ?? Otherwise we send K" to Static Analysis phase and repeat. ZKP MOOC 40
Picus Output ./picus-solve.sh ./benchmarks/motivating/ ladder.r1cs # number of constraints: 9 # parsing alternative r1cs... |# configuring precondition... safe.
42
•  Automated Detection of Underconstrained Circuits for Zero- Knowledge Proofs, PLDI’23 •  Practical Security Analysis of Zero-Knowledge Proof Circuits •  Certifying Zero-Knowledge Circuits with Refinement Types