From July 28 to November 15, 2022, through a joint effort among 0xPRAC Community, Ethereum Foundation, and Veridise, we reviewed the security of the circom-bigint curcuit implementation and its dependent library circomlib. The review covered all circuits implemented using circom in the circom-bigint ’s repository (https://github.com/0xbok/circom-bigint/tree/audit) ∗ and its dependant library (https://github.com/iden3/circomlib) †. We conducted this assessment over 24 person-weeks, with 4 engineers working on commit 7505e5c of the client’s repository (cff5ab6 of its dependant repository). The auditing strategy involved both manual and tool-assisted analysis of the source code performed by engineers from 0xPARC Community, EF, and Veridise. The tools that were used in the audit include a combination of static analysis and interactive theorem prover using Coq. The outcome of the auditing includes 1) this auditing report, and 2) 20K+ lines of machine-checkable proof in Coq.

Summary of issues detected. The audit uncovered 14 issues in circomlib , including 9 issue of critical severity. The critical severity issues (V-BIGINT-COD-001, V-CIRCOMLIB-PIC-001 ∼ V-CIRCOMLIB-PIC-008) correspond to underconstrained issues in circuits, which allow attackers to construct spurious proofs that violate the intended functional behavior yet bypass the validation checks, thus compromising potential functionality of the system that incorporates the target circuits. The rest of the issues include 5 low-severity issues (V-BIGINT-VUL-001 ∼ V-BIGINT-VUL-003, V-CIRCOMLIB-PIC-009, V-CIRCOMLIB-PIC-010) that involves empty circuit templates that could potentially cause underconstrained errors when used, as well as optimizations on constraint size and documentations. In addition to the above-mentioned issues, we also formally verified (with machine-checkable proof in Coq) the functional correctness of the circuits with respect to their specifications written by 0xPARC Community and proved the absence of underconstrained issues.