# A novel approach to automated vulnerability scanning for ZK circuits

The current ZK security landscape relies heavily on manual review of circuit synthesis code, requiring an experienced auditor to rigorously examine the circuit logic one constraint at a time. We are working towards the design and implementation of one of the first serious attempts at automating vulnerability analysis for ZK circuits.

## Introduction

ZK circuits function as arithmetic representations of a program. The proof for said circuit is a testament to the satisfaction of a set of assertions (constraints) imposed upon the program’s execution trace.

The circuit should therefore explicitly constrain all behavior that is expected of a valid execution trace of the program. Identifying a feature of the program that does not have a corresponding constraint in the circuit reveals a potential soundness error.

Our approach focuses on finding soundness issues due to underconstraints. For simplicity, we assume that completeness is determined beforehand through extensive traditional testing and other means.

Some distinguishing features of our approach are as follows:

- Relatively low computational requirements, making it scalable for larger circuits
- It is modular in nature and smaller sub circuits can be analyzed independently
- It does not require any patches to the target source code, and most of the setup code can be borrowed from tests.
- It provides 100% coverage for certain bug classes (though with a non zero false positive rate)
- It is agnostic to the proving system and framework/language used to implement a circuit
- The approach is extensible and provides a solid basis for future contributors to write their own analyzers for more bug classes.
- Given its statistical nature, this paradigm potentially opens avenues for ML based security analysis of ZK circuits

## Notation

Let $C$ be a circuit defined over a finite field $F$.

The set of circuit variables for $C$ is denoted $W(C)$.

We represent a trace with a vector $T \in F^n, n = |W(C)|$. We use the notation $T^{(i)}$ to access the ith index of a vector

A trace is said to be valid if the assignments satisfy all constraints in the circuit i.e can be used to generate a valid proof.

## Overview

The core idea is based on the following heuristic:

Suppose we are given a set $S$ of valid traces for a circuit $C$, with $S^{\mathrm{all}}$ denoting the set of all valid traces.
If some subset of circuit variables $W' \subseteq W(C)$ consistently follows some behavior $B$ over a large number of traces, then one of the following is true

1. $B$ holds for all traces, that is, $B$ is a characteristic of the underlying program.
2. $B$ holds with high probability for random traces in $S^{\mathrm{all}}$, but not for all.
3. The distribution $S$ is highly biased towards traces for which $B$ holds.

The second case occurs in particular for $B$ that are too unspecific, so such $B$ should be avoided[^FootnoteSecondCase]. The third case would in practice indicate missing test coverage, so is a useful finding in itself. From the perspective of searching for possible underconstraints associated with $B$, the second and third case represent false positives, but no underconstraints will be missed.

[^FootnoteSecondCase]: An example for a $B$ that is too unspecific would be "this circuit variable is *not* equal to 42". If the circuit variables is a uniformly random field element, then $B$ would not hold for all traces, yet would be true with high probability for a random trace. There are also instances of the second case that can not be rejected as easily as in this example, such as a circuit variable that is constrained to be the Boolean indicating whether the hash of some input is a particular value. This is highly unlikely, so with $B$ being "this circuit variable is 0", $B$ will be observed among valid traces with high likelihood, even though $B$ itself looks like a sufficiently specific property. In such cases, manual analysis is needed to understand such false-positives.

Our approach thus proceeds as follows
1. Fuzz a circuit with randomly generated benign inputs to generate valid circuit traces
2. Observe behavior of circuit variables across the traces and identify patterns that they follow
3. If a subset of circuit variables $W' \subseteq W(C)$ consistently follows behavior $B$, and behavior $B$ is specific enough to not be attributed to randomness, then it is likely to be a characteristic of the underlying program, or is a sign that the fuzzing in part 1 had insufficient coverage. Better fuzzing and a larger number of traces is useful for minimizing false positives in this step
5. Check if C enforces B by means of symbolic analysis on an analysis friendly representation of the circuit.

Making the tooling framework agnostic necessitates an analysis friendly Intermediate representation. Analyzers can then be implemented for this IR. Adding support for a new framework can thereafter be implemented with a frontend to parse it into the IR.

This splits the project into three major components

1. **IR design**: Designing an intermediate representation which is suitable for analysis and can encapsulate sufficient information for any arithmetization
2. **Trace analysis**: Analyzing traces to see what circuit variables follow a specific behavior
3. **Circuit analysis**: Analyzing circuit to see if that behavior is enforced for those variables

In principle, trace analysis is enough to flag all potential sources of bugs. Circuit analysis is responsible for filtering out false positives. The IR is the glue that makes both these components function efficiently.

## Concrete Analyzers

We present concrete analyzers for specific bug classes. The two vulnerability classes we target for our initial PoC are

1. Missing equality constraints: Values that are stored twice in the circuit for convenience but not constrained to be equal. e.g computed merkle root not equated against public input
2. Missing range checks: Values that are assumed to belong to a small range e.g circuit variables representing boolean or byte values, but not constrained so.

### Missing equality constraints
Suppose we are presented with a set of $m$ traces $S$.

We define the equivalence relation $R_S$ on the set of indices $i \in [0, n)$ (recall that $n$ was the number of circuit variables) as:
$(i, j) \in R_S \iff \forall\ T \in S:\ T^{(i)} = T^{(j)}$

The goal with the trace analysis is to find all the equivalence classes of the relation $R_S$.

For a random challenge $\gamma$, let $T_{\mathrm{RLC}} = \mathrm{RLC}_{\gamma}(S)$. Then with high probability $(i, j) \in R_S \iff T_{\mathrm{RLC}}^{(i)} = T_{\mathrm{RLC}}^{(j)}$. This follows from the Schwartz-Zippel lemma.

Therefore by computing a random linear combination of the set of traces, we can identify the equivalence classes simply by iterating through the aggregated vector with a hashmap

We can then apply symbolic analysis to the circuit graph to determine explicit and implicit equality constraints in the circuit. These constraints are represented as a graph where nodes correspond to circuit variables and edges correspond to explicit equality constraints. In order to be secure, each equivalence class identified in the trace analysis step must correspond to a connected component in circuit equality graph. If a particular class does not fit into a connected component, we flag it as a potential underconstraint.

Examples from the wild:
Findings 3.7 and 3.22 in [Scroll zkEVM part 2](https://github.com/Zellic/publications/blob/master/Scroll%20zkEVM%20-%20Part%202%20-%20Audit%20Report.pdf)

### Missing range checks

Suppose we are presented with a set of $m$ traces $S$.

Iterating over the set we compute the vector $M \in (F \times F)^n$ where $M^{(i)} = \left(\textrm{min}\left(\left\{T^{(i)}\ \middle\vert\ T \in S\right\}\right), \textrm{max}\left(\left\{T^{(i)}\ \middle\vert\ T \in S\right\}\right)\right)$.

$M$ can be referenced against common ranges such as Booleans, bytes, and 32 bit integers to guess the intended "type" of each variable.

Examples from the wild:
Finding 3.4 in [Scroll zkEVM part 1](https://github.com/Zellic/publications/blob/master/Scroll%20zkEVM%20-%20Part%201%20-%20Audit%20Report.pdf)

Finding 3.2, 3.4, 3.18 in [Scroll zkEVM part 2](https://github.com/Zellic/publications/blob/master/Scroll%20zkEVM%20-%20Part%202%20-%20Audit%20Report.pdf)

### Timeline estimates

For a production ready MVP, we propose an estimate of 4 engineer months split across 2-3 engineers