Practical Security Analysis of Zero-Knowledge Proof Circuits

Practical Security Analysis of Zero-Knowledge Proof Circuits

Speakers: Hongbo Wen, PhD Student, UCSB PC Lab; Jon Stephens; Yanju Chen; Kostas Ferles; Shankara Pailoor; Kyle Charbonnet; Isil Dillig; Yu Feng

Conference: USENIX Security '24

YouTube: https://www.youtube.com/watch?v=Bo8pLGFWK6E

Overview

This talk by Hongbo Wen and his co-authors from UCSB PC Lab delves into the critical security challenges inherent in Zero-Knowledge Proof (ZKP) circuits. ZKP technologies are rapidly gaining prominence, particularly within the blockchain ecosystem, for their ability to enable privacy-preserving computations and enhance scalability by offloading heavy computational tasks off-chain while maintaining verifiability. The core premise is that a prover can convince a verifier of the correctness of a computation without revealing any underlying secret information, and crucially, without interaction in the case of ZK-SNARKs.

However, the practical implementation of ZKP circuits is fraught with potential vulnerabilities. The talk highlights a significant problem stemming from the semi-automatic nature of compiling high-level computations into ZKP-compatible circuits and their associated polynomial field equations. This manual intervention often leads to discrepancies between the intended computation and the actual constraints enforced, resulting in underconstrained circuits. Such flaws can be catastrophic, allowing malicious actors to generate bogus proofs that are accepted by the verifier, potentially leading to severe consequences like unauthorized token draining or double-spending on a blockchain.

The research presented addresses this pressing issue by introducing a novel static analysis approach centered around the Circuit Dependency Graph (CDG). This methodology aims to systematically identify and mitigate vulnerabilities arising from these compilation discrepancies, offering a scalable and precise detection mechanism. The work underscores the urgent need for robust security analysis in the burgeoning field of ZKP, providing developers and auditors with practical tools and insights to safeguard these complex systems.

Background

▶ Watch: Introduction to ZKP and blockchain adoption (0:00)

Zero-Knowledge Proofs (ZKPs) have emerged as a foundational technology for achieving both privacy and scalability in decentralized systems, especially blockchain. The core idea is simple yet powerful: a prover can demonstrate the truth of a statement to a verifier without revealing why it's true. Among various ZKP protocols, ZK-SNARKs (Zero-Knowledge Succinct Non-Interactive Argument of Knowledge) are particularly attractive due to their "non-interactive" nature, meaning the verification process can be completed without back-and-forth communication between the prover and verifier. This makes them ideal for on-chain verification of off-chain computations.

Constructing a ZK-SNARK for an arbitrary computation, let's say F(X), involves a multi-step process. First, the computation F must be translated into a ZK-SNARK circuit. This circuit encodes the logic of F, with inputs, outputs, and intermediate values represented as signals. Second, this circuit is compiled into a set of polynomial field equations, which mathematically represent the constraints that must hold true for the computation to be valid. Finally, the ZK-SNARK protocol itself is implemented for the prover and verifier, based on these equations.

The critical security vulnerability arises from a specific point in this process: the semi-automatic compilation from circuit logic to polynomial field equations. While much of the ZKP pipeline is automated, this particular step often requires manual intervention from developers. There are two primary reasons for this manual requirement:

1. Non-Expressible Computations: Some operations expressed at the circuit level, such as square roots, are not directly expressible as simple polynomial constraints. Developers must manually add auxiliary constraints to specify the relationship between inputs and outputs for these operations (e.g., output_squared = input).
2. Non-Trivial Constraint Inference: Even when computations are expressible, automatically inferring the correct and complete set of constraints from the circuit alone is a highly non-trivial task for compilers.

This manual intervention is the "root cause of the bug," as highlighted by the speakers. It introduces a significant risk of human error, leading to a state where the circuit and its corresponding field equations are not observationally equivalent. Observational equivalence means that for any input X, an output Z should satisfy the constraints if and only if Z is the actual output of the circuit given X. If this equivalence is broken, a malicious actor can craft bogus proofs that are accepted by the verifier, even though the underlying computation was invalid or produced an incorrect result.

The most common manifestation of this problem is underconstrained circuits. A circuit is underconstrained if its output signals are not uniquely determined by its input signals and the defined constraints. This allows an attacker to manipulate unspecified output values to generate a valid-looking proof for an invalid computation. The consequences are severe, as evidenced by real-world incidents involving token draining from protocols or enabling double-spending on blockchains.

To illustrate, the talk provides a concrete example of an underconstrained circuit due to semantic discrepancies in division. Consider a scenario where a circuit performs a division operation, but an attacker can set out_der = 0, in1 = -1, and in0 = 0. While the computation part (executed by the prover) might attempt in1 / in0, leading to an error or undefined state, the constraint part (evaluated by the verifier) might check conditions like out_der 2 = 0 and out1 0 = 0. In this specific case, the constraint out1 0 = 0 will always evaluate to true, regardless of the value of out1. This semantic gap between how division is handled in the computation versus how its constraints are formulated allows an attacker to pick any* value for out1 and still generate a proof that passes verification, effectively bypassing the intended logic. This discrepancy between division and multiplication when the denominator is zero perfectly encapsulates the type of subtle bug that manual constraint writing can introduce.

Key Findings

▶ Watch: Two reasons for non-automatic circuit compilation (3:00)

The central finding of this research is the identification of the semi-automatic compilation process as the primary source of critical vulnerabilities in Zero-Knowledge Proof (ZKP) circuits. Specifically, the manual addition of constraints by developers frequently leads to semantic discrepancies between the computation logic (executed by the prover) and the constraint logic (verified by the verifier), resulting in underconstrained circuits. These discrepancies enable attackers to forge valid proofs for invalid computations, posing a significant threat to the integrity and security of ZKP-enabled systems.

To address this, the authors propose a novel static analysis methodology that abstracts complex ZKP circuits into a Circuit Dependency Graph (CDG). This graph-based representation allows for a more scalable yet sufficiently precise detection of vulnerabilities, circumventing the limitations of traditional symbolic execution or fuzzing techniques which struggle with the extremely large search spaces inherent in ZKP circuits dueated to their use of large number fields.

Based on extensive analysis of common circuit errors, the research identifies three major categories of bugs that can be effectively detected using the CDG approach:

1. Non-deterministic signals: Output signals whose values are not uniquely determined by the circuit's inputs and constraints, allowing an attacker to choose arbitrary values.
2. Unsafe component usage: The misuse of standard arithmetic or logical operations in ways that create vulnerabilities, such as division by zero or implicit type conversions that lead to unexpected behavior in a finite field context.
3. Constraint computation discrepancies: Semantic mismatches between how a computation is performed and how its correctness is enforced by the corresponding constraints. This is epitomized by the division-by-zero example where out1 * 0 = 0 holds true for any out1, regardless of the actual division result.

To operationalize these findings, the authors developed a tool called Decap. Decap implements a series of nine detectors, designed to work on the CDG by querying it using a Vulnerability Description Language (VDL). The evaluation results demonstrate Decap's effectiveness: it was tested against 258 ZKP circuits from 17 popular open-source projects. Decap successfully identified 81 vulnerabilities across all defined bug categories, including several previously unknown bugs that were subsequently confirmed and fixed by the respective developers. Crucially, the tool exhibited a low false positive rate, indicating its practical utility for real-world security analysis.

Technical Deep Dive

▶ Watch: Consequences of under-constrained circuits: token draining, double spending (5:50)

The core of the proposed solution for analyzing ZKP circuit security lies in the Circuit Dependency Graph (CDG). Given the inherent complexity and vast search space of ZKP circuits—often operating over extremely large number fields—traditional dynamic analysis methods like symbolic execution or fuzzing become computationally intractable. The CDG offers a powerful abstraction that simplifies the circuit representation while retaining enough semantic information for effective static analysis.

A CDG is constructed from a ZKP circuit by modeling its fundamental components:

• Nodes: Each node in the CDG represents a signal within the circuit. Signals are the core symbols that carry data, representing inputs, outputs, and intermediate values of the computation. Nodes are typically labeled with their symbolic names.
• Edges: Edges in the CDG capture the relationships between signals. There are two primary types of edges:
• Computation Dependencies: These edges represent the data flow and operational relationships between signals as defined by the circuit's computation logic. For example, if C = A + B, there would be computation edges from A to C and from B to C.
• Constraint Dependencies: These edges represent the relationships enforced by the polynomial field equations (constraints). For instance, if a constraint states X * Y = Z, there would be constraint edges indicating this relationship.

By separating and explicitly representing both computation and constraint dependencies, the CDG provides a structured way to identify mismatches. The analysis focuses on examining pairs of computation and constraint edges between the same two nodes. For example, if a computation edge implies output = input_A / input_B, but the corresponding constraint edge only checks output * input_B = input_A, a discrepancy arises when input_B is zero. The CDG allows the static analysis engine to systematically compare the semantics of these expressions, looking for cases where they diverge, especially under edge conditions.

The authors designed a series of nine detectors, implemented within their tool Decap, to identify vulnerabilities based on the three major bug categories discussed earlier:

1. Non-deterministic Signals: Detectors for this category look for signals whose values are not uniquely determined by the combination of computation and constraint edges originating from their predecessors. This often involves identifying "dangling" signals or pathways where a computation result isn't fully constrained.
2. Unsafe Component Usage: This category targets common pitfalls in arithmetic operations within finite fields. For instance, a dedicated detector would identify potential division-by-zero scenarios by tracing input signals to division operations and checking if a zero value for the denominator is permissible under the existing constraints. Other detectors might look for implicit assumptions about data ranges or overflow conditions that are not properly enforced by constraints.
3. Constraint Computation Discrepancies: This is where the CDG's ability to represent both types of dependencies shines. Detectors here compare the semantic effects of computation edges versus constraint edges for the same logical operation. The division-by-zero example is a prime case: if the computation involves out1 = in1 / in0, but the constraint system only includes out1 in0 = in1 (or out1 0 = 0 in the problematic case), a detector can flag this discrepancy by identifying inputs (in0 = 0) that cause the constraint to be trivially satisfied while the computation part behaves differently. These detectors effectively look for cases where the "observational equivalence" between the circuit's functional behavior and its verification logic is broken.

These detectors are implemented using a Vulnerability Description Language (VDL), allowing Decap to perform declarative queries on the CDG. This approach makes the analysis both expressive and scalable. By leveraging the CDG, Decap avoids the combinatorial explosion of state that plagues more granular analysis techniques when dealing with the vast number fields common in ZKP. The static nature of the analysis also means it can provide comprehensive coverage without requiring specific test inputs, making it highly effective for pre-deployment security auditing.

Demo / Proof of Concept

▶ Watch: Example: Under-constrained circuit due to division by zero (6:10)

While the talk did not feature a live, interactive demonstration of the Decap tool in action, the speaker presented a clear and illustrative example of an underconstrained circuit resulting from constraint computation discrepancies. This example served as a compelling proof of concept for the type of vulnerability Decap is designed to detect and highlighted the fundamental problem in ZKP circuit security.

The scenario involved a circuit where the computation part might perform a division, while the constraint part, due to manual implementation, fails to correctly enforce the division's semantics under all conditions. Specifically, the speaker posited a case where certain input signals are assigned special values: out_der = 0, in1 = -1, and in0 = 0.

In this situation:

• Computation Part (Prover): The prover might attempt to execute an operation like out1 = in1 / in0. With in0 = 0, this operation is undefined or would typically result in an error in standard arithmetic.
• Constraint Part (Verifier): The verifier, however, checks a set of manually written constraints. The example provided showed constraints like out_der 2 = 0 and out1 0 = 0.

The critical flaw lies in the out1 0 = 0 constraint. Mathematically, this equation is true for any* value of out1. This means that if in0 is zero, the constraint system effectively loses control over the value of out1. An attacker could choose any arbitrary value for out1, generate a proof claiming that this out1 was the result of in1 / in0, and the verifier would accept it because out1 * 0 = 0 would hold true.

The speaker explicitly stated, "In this case any out1 and N value of the signal out1 could bypass the verification." This discrepancy arises from the "semantics between the division and multiple when the denominator is zero." This example vividly illustrates how a subtle difference in how an operation is handled (computationally undefined vs. trivially true constraint) can create a gaping security hole, allowing an attacker to generate bogus proofs that are accepted by the verifier. The CDG-based analysis of Decap would identify this semantic mismatch by comparing the computation path involving in0 and out1 with the corresponding constraint path, flagging the scenario where in0 = 0 leads to a non-deterministic out1.

Defensive Implications

▶ Watch: Decap tool, bug sources, and evaluation results (10:00)

The findings presented in "Practical Security Analysis of Zero-Knowledge Proof Circuits" carry significant implications for developers, auditors, and anyone involved in building or securing systems that leverage ZKP technology. The primary takeaway is the critical need to move beyond implicit trust in manually written constraints and adopt rigorous, automated security analysis.

Here are key defensive implications:

1. Prioritize Observational Equivalence: Developers must ensure that their ZKP circuits and the corresponding polynomial constraints are "observationally equivalent." This means that the constraints must precisely capture the intended functionality for all possible inputs, leaving no room for outputs to be underdetermined or for semantic discrepancies to emerge between the computation and verification logic.
2. Beware of Manual Constraint Writing: The semi-automatic compilation process, particularly the manual addition of constraints, is the root cause of many vulnerabilities. Developers should be highly cautious and meticulous when writing custom constraints, paying extreme attention to edge cases and potential semantic mismatches, especially for operations that behave differently in a finite field context (e.g., division, modulo, square roots).
3. Adopt Static Analysis Tools: Tools like Decap are indispensable for identifying subtle flaws that manual review or limited testing might miss. Integrating static analysis for ZKP circuits into the development pipeline should become a standard practice. This allows for early detection of:

• Non-deterministic signals: Ensure all output signals are uniquely determined by inputs and constraints.
• Unsafe component usage: Identify and mitigate risks associated with operations like division by zero, integer overflows/underflows in finite fields, or other arithmetic edge cases.
• Constraint-computation discrepancies: Systematically check for semantic mismatches between how the prover executes a computation and how the verifier checks its correctness.

1. Rigorous Testing and Formal Verification: While static analysis provides excellent coverage, it should be complemented by comprehensive testing, including property-based testing, to explore a wide range of inputs. For high-assurance systems, exploring formal verification methods that can mathematically prove the equivalence of circuits and constraints is also advisable, although often more resource-intensive.
2. Audit Existing Circuits: Given the prevalence of underconstrained circuits and the severe consequences they entail, existing ZKP circuits deployed in production systems should undergo thorough security audits using the principles and tools outlined in this research. This includes reviewing how complex operations are constrained and scrutinizing any manual constraint additions.
3. Education and Best Practices: Developers working with ZKP circuits need specialized training to understand the unique security implications of circuit design, finite field arithmetic, and constraint generation. Establishing and following best practices for circuit development, emphasizing clarity, completeness, and verifiability of constraints, is crucial.
4. Review Compiler Outputs: Even when using automated circuit compilers, it's beneficial to understand and critically review the generated constraints, especially for any warnings or non-standard constructions.

By proactively addressing these defensive implications, the ZKP ecosystem can mature with greater security and reliability, fostering broader adoption and trust in this transformative technology.

Key Takeaways

• Underconstrained ZKP circuits are a critical and common vulnerability: These flaws allow attackers to forge valid proofs for invalid computations, leading to severe consequences like token theft or double-spending.
• Manual constraint writing is the primary source of these bugs: The semi-automatic compilation of ZKP circuits, where developers must manually add constraints for complex operations, often introduces semantic discrepancies between computation and verification logic.
• Circuit Dependency Graph (CDG) enables scalable static analysis: By abstracting ZKP circuits into a CDG, which represents signals and their computational/constraint dependencies, the analysis can effectively overcome the extremely large search space of ZKP circuits in large number fields.
• Three major bug categories drive detection: The research identified non-deterministic signals, unsafe component usage (e.g., division by zero), and constraint computation discrepancies as the key vulnerability classes.
• Decap is a practical tool for automated detection: The developed tool, Decap, implements nine detectors based on these bug categories, successfully finding 81 vulnerabilities across 258 circuits from 17 projects, including previously unknown ones, with a low false positive rate.
• Developers must prioritize rigorous analysis: To ensure the security and integrity of ZKP systems, developers must adopt automated static analysis tools like Decap and commit to thorough auditing to guarantee "observational equivalence" between circuit functionality and its constraints.

About the Speaker(s)

The primary speaker for this presentation was Hongbo Wen, who introduced himself as a second-year PhD student from the UCSB PC Lab. While the talk focused on the collective work of the research team, Hongbo Wen was the presenter. The paper lists a team of co-authors, including Jon Stephens, Yanju Chen, Kostas Ferles, Shankara Pailoor, Kyle Charbonnet, Isil Dillig, and Yu Feng, suggesting a collaborative effort likely from the same academic institution or research group, focusing on advancements in program analysis and security, particularly in emerging fields like Zero-Knowledge Proofs.