301 Scalable Verification of Zero Knowledge Protocols MIGUEL ISABEL MÁRQUEZ

### Overview Zero-knowledge (ZK) protocols allow a prover to convince a verifier that a statement is true without revealing any secret information beyond the statement's validity. These protocols rely on completeness, soundness, and zero knowledge. Typically, statements are represented as arithmetic circuit satisfiability problems composed of addition and multiplication gates and encoded as quadratic constraint systems over large finite fields. A major source of vulnerabilities in ZK protocols is underconstrained bugs, where required constraints are omitted, enabling a malicious prover to produce verifiable proofs for invalid statements. This presentation introduces Cyber, a formal verification tool designed to automatically detect underconstrained bugs and verify Circom circuits against pre- and post-condition specifications.

### Key Topics - **Zero-Knowledge Circuit Constraints**: Circuit representations in ZK systems strictly require quadratic constraints. In domain languages like Circom, developers work across symbolic constraint systems and executable witness generation code using different operators (`===`, `<--`, and `<==`). Improper combination can lead to circuits compiling successfully while generating empty or incomplete constraint systems. - **Limitations of Existing Tools**: Existing verification techniques include syntactic checkers (Circom compiler inspect flag, Circomspect, Ecne) that only recognize standard surface patterns, and semantic tools (such as Picus) that suffer from scalability bottlenecks on large circuits and lack pre- and post-condition specification support. - **Circom Tags**: Circom's type tagging mechanisms (e.g., specifying a binary signal tag) only enforce syntactic propagation checks during compilation rather than proving semantic satisfaction via actual constraints.

### Technical Details Verification of ZK constraint systems faces two core challenges: reasoning over large finite fields involving nonlinear arithmetic operations, and scaling to circuits containing thousands to millions of constraints. Cyber overcomes these via two primary mechanisms:

1. **Transformation and Deduction Rules**: Standard SMT solvers (like Z3) frequently time out when handling nonlinear operations over finite fields. Cyber applies deduction and algebraic transformations to simplify operations before passing them to the solver. For example, quadratic equations like $a \cdot b = 0$ are rewritten into disjunctions ($a = 0 \lor b = 0$), and modulo operations are substituted with auxiliary variables ($k$) accompanied by computed tight bounds to constrain the search space. 2. **Modular Hierarchical Verification**: Instead of evaluating an entire flattened circuit containing millions of constraints simultaneously, Cyber leverages the circuit's hierarchical template structure. It verifies child components individually against their specifications, abstracts those subcomponents by replacing their internal constraint systems with their specification summaries, and uses those abstractions during parent component verification.

Formally, verification is cast as a satisfiability query: given circuit constraints $P$ and target specifications, the solver checks whether there exists an assignment that violates the specification (returning `sat` with a counterexample) or proves no violation is possible (`unsat`).

### Takeaways Cyber was evaluated against widely used, real-world benchmarks, including production libraries such as `circomlib`, `zk-email`, and the `Dark Forest` game circuit codebase, as well as `B-Stark` (under development). Some evaluated circuits scaled up to 11 million constraints. Cyber verified most circuits with very few timeouts (which primarily occurred on complex mathematical structures such as elliptic curves). The tool identified previously undetected critical bugs, such as an underconstrained integer division bug in Dark Forest where the remainder was missing a constraint forcing it to be positive, allowing negative remainder counterexamples. Future work aims to extend Cyber to other ZK frameworks (Noir, Halo 2), alternative proving systems (Plonk), circuits defined solely as flat constraint systems, and extension fields.