Scalable Verification of Zero-Knowledge Protocols

Scalable Verification of Zero-Knowledge Protocols

Speakers: Miguel Isabel, Clara Rodríguez-Núñez, Albert Rubio

Conference: IEEE S&P

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

Overview

This talk, presented by Clara Rodríguez-Núñez alongside Miguel Isabel and Albert Rubio from the University of Complutense Madrid, delves into the critical challenge of verifying Zero-Knowledge Protocols (ZKPs). Specifically, it addresses the pervasive issue of under-constraint bugs in arithmetic circuits, which form the computational backbone of many ZKPs. These vulnerabilities can have severe security implications, potentially allowing malicious actors to forge valid proofs for false statements, thereby undermining the integrity and trustworthiness of ZKP-based systems.

The speakers introduce Cyber, a novel tool designed to provide scalable and semantic verification for these complex circuits. Cyber tackles two primary hurdles: the use of large finite fields in ZKP arithmetic, which complicates formal reasoning, and the immense size of modern ZKP circuits, often comprising millions of constraints. By leveraging a combination of innovative transformation rules and modular reasoning, Cyber offers a robust solution where existing syntactic-based tools fall short and prior semantic approaches struggle with scalability.

The significance of this work cannot be overstated in the burgeoning landscape of privacy-preserving technologies and decentralized applications. ZKPs are fundamental to scaling blockchains, enabling confidential transactions, and ensuring data privacy across various domains. The security of these protocols directly hinges on the correctness of their underlying arithmetic circuits. Cyber represents a significant step forward in ensuring this correctness, providing developers with a powerful mechanism to detect and mitigate critical vulnerabilities that could otherwise compromise entire systems.

Background

▶ Watch: Introduction to Zero-Knowledge Protocols and verification problem (0:00)

Zero-Knowledge Protocols (ZKPs) are a class of cryptographic protocols enabling a prover to convince a verifier that a statement is true, without revealing any information beyond the veracity of the statement itself. This property is crucial for privacy and efficiency in many modern applications, from blockchain scaling solutions to secure multi-party computation. ZKPs must satisfy three core properties: completeness (an honest prover can always convince the verifier), soundness (a dishonest prover cannot convince the verifier of a false statement), and zero-knowledge (the verifier learns nothing beyond the statement's truth).

In the context of ZKPs, the statements being verified are typically modeled as an arithmetic circuit satisfiability problem. This involves representing computations as circuits composed of multiplication and addition gates, defined over large finite fields. These circuits are then translated into constraint systems, specifically requiring quadratic constraints, where each constraint is a polynomial of degree at most two. The prover's task is to demonstrate knowledge of private inputs that satisfy this circuit, generating a proof that the verifier can efficiently check.

A critical and prevalent vulnerability in ZKP circuit design is the under-constraint bug. This occurs when the constraint system generated from a circuit does not fully capture the intended logical behavior of the statement. Consequently, a malicious prover can exploit these missing constraints to generate a verifiable proof for an incorrect or unintended state, effectively bypassing the security guarantees of the ZKP. Such bugs are particularly common in languages like Circom and Halo 2, where users explicitly define constraints, often leading to subtle errors when complex logic is translated into quadratic forms.

Existing tools for verifying ZKP constraint systems have significant limitations. Tools like the flag in the Circom compiler, Circom SMT, and Circom SP primarily perform syntactic checks. They look for predefined patterns that might indicate an under-constraint bug but are incapable of detecting more complex, semantic vulnerabilities that don't fit these patterns. On the other end of the spectrum, tools like Picus attempt semantic checks, offering a more thorough analysis. However, Picus suffers from severe scalability issues, rendering it impractical for the large, real-world circuits common in ZKP applications, which can contain thousands or even millions of constraints. Furthermore, no existing tool effectively handles formal specifications defined using pre-conditions and post-conditions, which are essential for rigorous verification. The core challenges, therefore, are reasoning efficiently about constraints defined over large finite fields and managing the sheer complexity of enormous circuit structures.

Key Findings

▶ Watch: Current tools' limitations and verification challenges (3:30)

The central contribution of this work is the introduction of Cyber, a novel verification tool designed to address the aforementioned shortcomings in ZKP circuit analysis. Cyber provides a scalable and semantic approach to detecting under-constraint bugs, offering a significant advancement over existing methods.

The key findings and contributions of Cyber are:

• Semantic Verification with Formal Specifications: Cyber introduces a language for precisely specifying the expected behavior of ZKP circuits using preconditions and postconditions. This allows developers to formally define what a circuit should achieve, including expected ranges for signals and specific output values, enabling a much deeper, semantic verification than purely syntactic checks.
• Addressing Large Finite Fields: To overcome the difficulty of reasoning about constraints defined over large finite fields, Cyber employs a sophisticated set of transformation and deduction rules. These rules systematically minimize the number of nonlinear operations within the constraint system, making the problem more tractable for standard SMT solvers like Z3.
• Scalability through Modular Reasoning: For handling the immense size of real-world ZKP circuits (some benchmarks exceeding 11 million constraints), Cyber implements a modular reasoning approach. It leverages the inherent hierarchical structure of circuit definitions, allowing individual components to be verified in isolation. The specifications of child components are then used to abstract their behavior when verifying parent components, drastically reducing the number of constraints that need to be considered at any single step.
• Successful Real-World Application: Cyber has been rigorously tested on a suite of real-world circuits from widely used libraries and projects, including circomlib, circomlib-rs, Dark Forest, and ZK-Stark. The tool successfully verified a majority of these complex circuits.
• Discovery of Critical Bugs: Crucially, Cyber demonstrated its efficacy by identifying critical under-constraint bugs in production-level projects that could not be detected using previous approaches. This highlights Cyber's ability to uncover subtle, yet exploitable, vulnerabilities that escape the notice of syntactic checkers.
• Public Availability: The tool, Cyber, is publicly available on GitHub, encouraging broader adoption and contributing to the open-source security ecosystem for ZKP development.

In essence, Cyber represents a paradigm shift in ZKP circuit verification, moving beyond superficial syntactic checks to provide deep, semantic guarantees of correctness, even for the most complex and large-scale applications.

Technical Deep Dive

▶ Watch: Cyber tool's modular reasoning for scalable verification (4:35)

The core of the problem addressed by Cyber lies in the intricate process of defining and compiling arithmetic circuits for Zero-Knowledge Proofs, particularly within the Circom language. Circom is widely used for modeling these circuits, and its compiler generates both a symbolic representation (the constraint system) and an executable file for witness generation. Understanding the nuances of Circom's operators is crucial to grasping how under-constraint bugs arise.

Circom provides three primary operators for defining circuit logic, each with distinct implications for the generated constraint system and executable code:

1. Equality Operator (===): This operator is used to add a constraint directly to the constraint system. The expression on the left-hand side must be quadratic (polynomial of degree at most two). If a non-quadratic expression is used, the Circom compiler will throw an error. This operator primarily works at the symbolic level, ensuring the mathematical properties of the circuit.
2. Single Arrow Operator (=): This operator performs an assignment to a signal, adding a line of code to the executable file that simulates the circuit's behavior. Unlike the equality operator, it does not add any constraints to the constraint system, and thus, there is no quadratic expression requirement. It operates purely at the computational level, defining how values are computed.
3. Double Arrow Operator (<==): This operator combines both functionalities: it adds a constraint to the constraint system and an assignment to the executable file. Similar to the equality operator, expressions used with the double arrow must be quadratic. Ideally, for generating equivalent symbolic and computational representations, developers would exclusively use <==. However, as the talk elucidates, this is not always possible for expressing more complex logic.

The danger arises when developers, particularly beginners, attempt to implement complex logic. A common scenario involves conditional statements or non-quadratic expressions. For instance, a circuit checking if an input in is zero, setting out to 1 if in is zero and 0 otherwise, cannot be directly expressed using out <== (in == 0 ? 1 : 0) because the comparison in == 0 is non-quadratic in a finite field context (it's essentially a disjunction, which translates to a high-degree polynomial). A typical, yet dangerous, "fix" is to replace <== with =, e.g., out = (in == 0 ? 1 : 0). While this compiles without error and the executable code might behave as expected, it adds no constraints to the constraint system. The result is an empty constraint system, meaning any input/output combination could be proven valid, leading to a severe under-constraint bug. The correct approach, as demonstrated, involves a combination of operators to construct an equivalent quadratic representation, often requiring auxiliary signals and multiple constraints (e.g., in out === 0 and (1 - in) (1 - out) === 0 for a binary in and out).

Furthermore, the talk highlights the limitations of Circom tags. These are annotations (e.g., binary) that users can add to signals to indicate expected properties. While the newest version of Circom includes these tags, the compiler only performs syntactic checks. It ensures, for example, that a signal tagged binary is only assigned to another binary signal. However, it performs no semantic checks to ensure that the underlying constraints actually enforce the binary property (e.g., out * (1 - out) === 0). This leaves another vector for under-constraint bugs.

Cyber's approach to verification tackles these issues head-on. It frames the verification problem as a satisfiability query. Given the circuit's constraints P and the target property (specification) T, Cyber checks if there exists any solution to P that does not satisfy T. This is expressed as checking the satisfiability of constraints(P) AND NOT(specification(T)). If this query is satisfiable, Cyber returns a counter-example, indicating a bug.

To make this query tractable for SMT solvers, Cyber employs two main strategies:

1. Transformation and Deduction Rules: SMT solvers like Z3 struggle with nonlinear operations over finite fields. Cyber introduces a set of rules to simplify these expressions. For example:

• A * B === 0 can be transformed into A === 0 OR B === 0.
• Modulo operations, such as A % B === C, are rewritten as A === K * B + C, where K is an integer variable. Crucially, Cyber also computes tight bounds for K based on the context of the expression, significantly aiding the SMT solver's performance. These transformations reduce the complexity to more linear or disjunctive forms that SMT solvers handle more efficiently.

1. Modular Reasoning: To manage the immense size of circuits, Cyber leverages their hierarchical structure. Instead of feeding the entire circuit's constraints to the SMT solver, it verifies each component individually. When a component is composed of sub-components (children), Cyber substitutes the child's internal constraint system with its pre-defined specification. This means that when verifying a parent component, the SMT solver only needs to consider the parent's specific constraints and the abstracted specifications of its children, drastically reducing the number of variables and constraints in each satisfiability query. This modularity allows Cyber to scale to circuits with millions of constraints that would otherwise overwhelm SMT solvers.

By combining these technical innovations, Cyber effectively bridges the gap between the complex mathematics of ZKP circuits and the practical limitations of formal verification tools, enabling robust security analysis.

Demo / Proof of Concept

▶ Watch: Detailed explanation of Circom's constraint operators (6:20)

While the presentation did not feature a live, interactive demo, the speakers provided compelling evidence of Cyber's capabilities through extensive experimental results and a detailed case study of a bug found in a real-world ZKP project.

Cyber was applied to a suite of widely used and complex real-world circuits, serving as benchmarks for its performance and efficacy. These included:

• circomlib and circomlib-rs: Libraries of common Circom templates, many of which are in production.
• Dark Forest: A decentralized game built on ZKPs, also in production.
• ZK-Stark: A project currently under development.

Some of these benchmarks contained huge circuits, with up to 11 million constraints, demonstrating the significant scale at which Cyber can operate. The evaluation showed that Cyber was able to verify most of these circuits successfully. For the few cases where timeouts occurred, they were typically associated with circuits modeling highly complex mathematical structures, such as elliptic curves, which are inherently challenging for current SMT solvers even with Cyber's optimizations. Crucially, Cyber's analysis led to the discovery of critical under-constraint bugs in these projects, some of which could not have been found using existing, purely syntactic verification techniques.

A specific example presented was a bug found in the Dark Forest Library, within a circuit designed to perform integer division and calculate the remainder and quotient of two values (dividend and divisor). The expected behavior of such a circuit dictates that the remainder must always be non-negative. However, Cyber, when used to verify the original implementation against this specification, produced a counter-example. This counter-example demonstrated a valid assignment of inputs and outputs within the circuit that resulted in a negative remainder value, directly violating the expected behavior. This indicates an under-constraint bug, as the circuit's constraints did not enforce the non-negativity of the remainder.

The fix, as shown, involved adding a simple yet critical constraint: explicitly forcing the remainder signal to be positive (e.g., remainder >= 0). Once this constraint was added, Cyber was able to successfully verify the corrected circuit, confirming that it now satisfied the specified property. This real-world example vividly illustrates how Cyber can pinpoint subtle logical flaws that have profound security implications, providing developers with actionable insights to harden their ZKP implementations.

Defensive Implications

▶ Watch: Practical example: identifying an under-constraint bug in Circom (7:50)

The findings presented in "Scalable Verification of Zero-Knowledge Protocols" carry significant defensive implications for developers, auditors, and practitioners working with Zero-Knowledge Proofs. The prevalence and criticality of under-constraint bugs necessitate a proactive and robust approach to circuit verification.

Here are key defensive implications:

• Prioritize Semantic Verification: Developers must move beyond relying solely on syntactic checks provided by compilers like Circom. While these checks prevent basic errors, they are insufficient for detecting deep logical flaws that lead to under-constraint bugs. Integrating tools like Cyber that perform semantic verification is crucial for ensuring the true correctness and soundness of ZKP circuits.
• Formal Specification is Paramount: The ability to express circuit behavior using preconditions and postconditions is a powerful defensive mechanism. Developers should formally specify the expected properties of their circuits, including signal ranges, output values, and critical relationships. This not only aids automated verification but also improves clarity and understanding of the circuit's intended logic.
• Understand Circom Operator Nuances: A deep understanding of the === (equality), = (assignment), and <== (double arrow) operators in Circom is essential. Developers must be acutely aware that using = for critical logic instead of === or <== can silently lead to an empty constraint system and severe under-constraint vulnerabilities. Complex conditional logic or non-quadratic expressions require careful translation into multiple quadratic constraints.
• Do Not Over-rely on Circom Tags: While Circom tags (e.g., binary) can be useful for documentation and some basic syntactic checks, defenders should be aware that the Circom compiler does not perform semantic checks on these tags. A signal tagged binary is not necessarily enforced to be binary by the constraints unless explicitly added by the developer. Semantic verification tools are needed to validate these properties.
• Integrate Verification into CI/CD: To ensure continuous security, ZKP circuit verification tools should be integrated into the continuous integration and continuous deployment (CI/CD) pipelines. This ensures that every code change is automatically checked for under-constraint bugs before deployment, catching issues early in the development lifecycle.
• Auditing Complex Mathematical Structures: Circuits involving complex mathematical structures, such as elliptic curves or intricate number theory operations, are particularly prone to subtle errors and can be challenging for even advanced verification tools. These components warrant extra scrutiny, manual review, and dedicated verification efforts.
• Contribute to Open-Source Tooling: The public availability of tools like Cyber provides an opportunity for the community to contribute to its development, extend its capabilities to other languages (like Noir and Halo 2) and formats (like Plonk), and ensure its long-term maintenance and improvement.

By adopting these defensive strategies, the ZKP ecosystem can significantly enhance the security and trustworthiness of privacy-preserving applications, mitigating the risks posed by under-constraint vulnerabilities.

Key Takeaways

• Under-constraint bugs are a critical and pervasive threat in Zero-Knowledge Proof (ZKP) arithmetic circuits, potentially allowing malicious provers to generate valid proofs for false statements.
• Existing verification tools are largely insufficient, with syntactic checkers failing to find complex semantic bugs and prior semantic approaches like Picus struggling with the scalability required for real-world ZKP circuits.
• Cyber introduces a novel, scalable, and semantic verification approach by leveraging transformation rules to simplify nonlinear operations over finite fields and modular reasoning to handle circuits with millions of constraints.
• Formal specification using preconditions and postconditions is a powerful feature of Cyber, enabling developers to precisely define and automatically verify the intended behavior of their ZKP circuits.
• Cyber has successfully identified critical, previously undetected bugs in production-level ZKP projects like Dark Forest, demonstrating its practical utility and superior bug-finding capabilities.
• ZKP developers must adopt robust semantic verification tools and practices, understand the nuances of circuit definition languages like Circom, and formally specify circuit properties to mitigate the significant security risks posed by under-constraint vulnerabilities.

About the Speaker(s)

The work on "Scalable Verification of Zero-Knowledge Protocols" was presented by Clara Rodríguez-Núñez, and co-authored by Miguel Isabel and Albert Rubio. All three speakers are affiliated with the University of Complutense Madrid. Their research focuses on enhancing the security and reliability of Zero-Knowledge Protocols through advanced verification techniques.