MTZK: Testing and Exploring Bugs in Zero-Knowledge (ZK) Compilers

MTZK: Testing and Exploring Bugs in Zero-Knowledge (ZK) Compilers

Speakers: Dongwei Xiao

Conference: NDSS Symposium

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

Overview

Dongwei Xiao's talk, "MTZK: Testing and Exploring Bugs in Zero-Knowledge (ZK) Compilers," presented at the NDSS Symposium, addresses a critical and emerging security challenge in the rapidly evolving landscape of zero-knowledge proofs (ZKPs). The presentation details a novel methodology for automatically testing ZK compilers, which are foundational components in systems leveraging zero-knowledge technology. By identifying and highlighting vulnerabilities in these compilers, the research underscores the potential for severe security breaches and financial losses in applications where ZKPs are used, such as high-value blockchain systems.

The core of the talk revolves around the design and implementation of MTZK, a system that employs two distinct mutation-based testing strategies tailored specifically to the unique properties of ZKPs: satisfiability invariants and information visibility. These strategies enable the systematic discovery of semantic discrepancies between high-level ZK programs and their compiled low-level circuits. The findings from this research are significant, revealing 21 bugs across four mainstream ZK compilers, many of which have since been fixed. This work represents a pioneering effort in the security analysis of ZK compilers, emphasizing the urgent need for robust verification and testing practices in this complex domain.

The importance of this research cannot be overstated. As zero-knowledge proofs move from theoretical concepts to practical applications, securing their underlying infrastructure, particularly the compilers responsible for translating high-level logic into cryptographic circuits, becomes paramount. A single compiler bug can undermine the very privacy and integrity guarantees that ZKPs are designed to provide, leading to catastrophic consequences in systems managing billions of dollars or sensitive personal data. MTZK provides a much-needed framework for ensuring the reliability and trustworthiness of these critical components.

Background

▶ Watch: Introduction to zero-knowledge proofs and privacy (0:40)

Zero-knowledge proofs (ZKPs) are cryptographic protocols that allow one party (the prover) to convince another party (the verifier) that a statement is true, without revealing any information beyond the validity of the statement itself. This property, often referred to as "zero-knowledge," is revolutionary for privacy-preserving applications. A common illustrative example involves a bank account application: a prover wants to demonstrate they meet an income requirement (e.g., earning over $2,000 per month) without disclosing their exact salary. The verifier (the bank) receives a proof that the condition is met, but never learns the actual salary figure.

In practical ZKP systems, the constraints or rules governing a statement (like the income requirement) are typically expressed using specialized programming languages known as domain-specific languages (DSLs) for ZK programs. These programs allow developers to define logic, declare variables, and specify visibility modifiers—designating whether inputs are public (visible to both prover and verifier) or private (known only to the prover). For instance, a tax allowance might be public, while gross income is private. Assert statements are used to enforce constraints, such as assert(net_income > 2000).

The challenge then becomes how to translate these high-level programs into a format suitable for cryptographic proof generation. This is where ZK circuits come into play. For efficiency, the mathematical puzzles underlying ZKPs are typically encoded into specialized arithmetic circuits, often in forms like Rank-1 Constraint Systems (R1CS). These circuits represent the program's logic as a series of gates and wires, where each gate performs a basic arithmetic operation (e.g., addition, multiplication) over a finite field.

The crucial component facilitating this translation is the ZK compiler. Unlike traditional compilers that target machine code, ZK compilers translate high-level ZK programs into low-level ZK circuits. This process is highly complex, requiring specialized optimizations unique to zero-knowledge proof systems. The correctness of ZK compilers is absolutely essential for the security and integrity of any application built upon ZKPs. A bug in a ZK compiler can have devastating consequences: an unqualified applicant might be mistakenly classified as qualified, or an attacker could exploit a flaw to bypass critical security checks. The speaker highlighted that several major blockchain systems, which rely on ZK compilers to secure billions of dollars, have already suffered from such bugs, underscoring the real-world impact of this problem.

The fundamental difficulty in testing ZK compilers lies in the "ground truth problem." How can one definitively determine if a compiler has correctly translated a high-level program into an equivalent low-level circuit? Correctness in this context means that the compiled circuit must maintain the exact same semantics as the original high-level program. Any semantic discrepancy constitutes a compiler bug. Proving semantic equivalence between a high-level program and its corresponding circuit is a notoriously hard problem, generally intractable for arbitrary ZK programs. This inherent challenge necessitates alternative, pragmatic approaches to ensure compiler reliability, which MTZK aims to provide.

Key Findings

▶ Watch: Why ZK compiler correctness is critical (4:50)

Given the inherent difficulty of proving semantic equivalence for arbitrary ZK programs, the MTZK research proposes an innovative approach: instead of directly proving equivalence, they compare the compiler with itself. This methodology sidesteps the ground truth problem by introducing controlled mutations and observing their effects across compilation. The core idea is to predesign a set of relations that should always hold true for the original program and its mutated variants. These programs are then compiled into ZK circuits. If the compiler is correct, these predefined relations should also hold true for the compiled circuits. If a relation fails to hold in the circuit, it indicates a semantic discrepancy—and thus, a compiler bug.

The research introduced two distinct mutation strategies specifically designed to exploit the unique characteristics of zero-knowledge proof systems:

1. Inserting Always-Satisfying Constraints (Satisfiability Invariants): This strategy involves adding constraints to the high-level ZK program that are logically tautological—meaning they should always be satisfied regardless of the input values. If, after compilation, an input can be found that violates these "always true" constraints in the generated circuit, it signifies a compiler bug. The compiler has failed to correctly translate or preserve the semantic intent of the constraint.
2. Mutating Information Visibility: ZKPs inherently differentiate between public and private information. ZK compilers are responsible for handling these distinctions, often applying specific optimizations based on visibility. This mutation strategy involves altering the visibility of inputs (e.g., changing a public constant to a private input or vice-versa) while ensuring the program's output logic remains unchanged. If the compiled circuit, after such a visibility mutation, produces a different output or behaves unexpectedly, it reveals a bug in how the compiler manages information visibility and its associated optimizations.

To validate their methodology, the MTZK team evaluated four mainstream ZK compilers. These compilers are critical components in high-value blockchain systems, securing substantial financial assets. Through their systematic testing, MTZK successfully discovered a total of 21 bugs across these four compilers. Crucially, the majority of these identified bugs have since been fixed by the respective compiler developers, demonstrating the practical impact and effectiveness of the MTZK approach in improving the security posture of the ZK ecosystem. This work represents the first systematic study to uncover bugs in ZK compilers, establishing a foundational step towards more robust and secure zero-knowledge applications.

Technical Deep Dive

▶ Watch: MTZK's core idea: comparing compiler with itself (6:00)

The MTZK methodology's strength lies in its two specialized mutation strategies, each targeting different aspects of ZK compiler functionality.

Satisfiability Invariants

The first mutation technique focuses on satisfiability invariants, or tautological constraints. The premise is simple: insert constraints into the high-level ZK program that are logically always true. These constraints should never be violated, regardless of the input data. The MTZK system then compiles both the original and the mutated programs. If the compiled circuit for the mutated program can be violated by some input, it proves a compiler bug. The compiler has failed to correctly encode the always-true constraint, leading to a semantic discrepancy.

Examples of such tautological constraints include:

• Data Type Bounds: Asserting that a variable X must be less than or equal to the maximum value of its data type (e.g., X <= MAX_INT). This should always hold true by definition, assuming X is within its declared type.
• Arithmetic Identities: Constraints like X == X * 1 or X == X + 0. These are fundamental mathematical identities that should always hold.
• Random Profiling-based Assertions: The system can even perform random profiling of a program's execution to determine a value V for a variable X at a specific program line L for a given input. It then inserts an assertion like assert(X == V) at line L. While not a universal tautology, this constraint should hold for that specific execution path and input. If the compiled circuit allows X to be different from V at that point, given the same input, it indicates an issue.
• Double Negation: Applying double negation to an existing boolean expression (!!(condition)) should retain its original truth value. If the compiler mishandles this, the invariant is broken.
• Conjunctions: Combining multiple simple tautologies using logical AND operators can create more complex invariants, further stressing the compiler's logical translation capabilities.

By iteratively applying these mutations, MTZK can generate highly complex ZK programs. These programs serve as thorough stress tests for ZK compiler implementations, probing their ability to correctly translate various forms of logical and arithmetic constraints into circuits. The ability to find an input that violates these invariants in the compiled circuit, even when they are trivially true in the source code, clearly points to a compiler defect.

Information Visibility Mutations

The second mutation technique leverages the unique concept of information visibility inherent to ZKPs. In ZK, inputs are explicitly categorized as either public (plaintext, known to both prover and verifier) or private (encrypted, known only to the prover). ZK compilers play a critical role in distinguishing between these and applying corresponding optimizations, as public inputs can often be handled more efficiently.

The mutation strategy here involves exchanging the visibility of inputs in a way that should not affect the program's final output semantics. For example:

• A public constant in the original program might be replaced with a public input variable of the same value.
• A public constant might even be substituted with a private input variable, with the expectation that the compiler's handling of privacy should still yield the same logical outcome, albeit potentially with different performance characteristics.

The critical check is: if the program's output, as determined by the compiled circuit, changes after such a visibility mutation, then a compiler bug exists. This indicates that the compiler is mishandling the semantics of information visibility, either failing to correctly apply optimizations or, worse, altering the program's logic based on an input's declared visibility where it shouldn't. This type of bug can be particularly insidious, as it might subtly alter the behavior of a ZKP system in production, potentially leading to incorrect proofs or privacy leaks.

Examples of Discovered Bugs

The talk highlighted two critical bugs uncovered by MTZK:

1. Constraint Bypass due to MAX_INT Mishandling: In a bank scenario, a common constraint is that a withdrawal amount cannot exceed savings (withdrawal_amount <= savings). MTZK found a critical bug where a ZK compiler mishandled this constraint. After compilation, for certain public finite field data types, the compiler would incorrectly input the maximum integer value (MAX_INT) into the circuit for the savings variable, regardless of the actual savings amount. This effectively bypassed the withdrawal_amount <= savings constraint, allowing users to withdraw arbitrary amounts. This bug arose from the compiler's incorrect handling of public finite field data types during the compilation process, leading to a catastrophic security vulnerability where financial limits could be ignored.

1. Division by Zero Mishandling and Backdoor Potential: Another bug related to the handling of division by zero. In ZK systems, division by zero is typically an undefined operation that should ideally trigger an error. However, MTZK discovered a compiler bug where, instead of throwing an error, the compiler would silently set the result of a division by zero operation to zero. For instance, if an average_salary was calculated by dividing total_salary by number_of_employees, and number_of_employees was zero, the compiler would set average_salary to zero. This seemingly benign behavior could be exploited. The speaker described a scenario where a subsequent constraint, like assert(average_salary >= required_minimum), would then always pass if average_salary was forced to zero, regardless of the actual intent. An attacker could compose a backdoor by crafting specific inputs (e.g., a "magic password" that causes a division by zero in an internal calculation), triggering this bug, and then being classified as a "low incomer" to receive unwarranted benefits. This bug highlights how subtle arithmetic mishandling can lead to severe logical flaws and potential exploits.

Demo / Proof of Concept

▶ Watch: Mutation strategy 1: Inserting always-true constraints (6:50)

While the talk did not feature a live, interactive demonstration of the MTZK tool in action, the entire presentation served as a comprehensive proof of concept for its methodology. The speaker detailed how the mutation strategies work, provided concrete examples of the types of mutations applied, and most importantly, presented the results of the tool's application. The discovery of 21 unique bugs across four widely used ZK compilers, including critical vulnerabilities like constraint bypasses and division by zero mishandling, unequivocally demonstrates the effectiveness and practical utility of MTZK's approach. These discovered bugs, with specific examples like the MAX_INT mishandling and the average salary division-by-zero flaw, act as direct proof points of the methodology's ability to uncover real-world security vulnerabilities in complex ZK compiler implementations. The fact that many of these bugs were subsequently fixed further validates the impact of this research.

Defensive Implications

▶ Watch: Mutation strategy 2: Testing information visibility handling (8:50)

The findings presented by Dongwei Xiao carry profound defensive implications for the entire zero-knowledge ecosystem, from compiler developers to application builders and users of ZKP-enabled systems.

For ZK Compiler Developers:

• Prioritize Rigorous Testing: The discovery of 21 bugs in mainstream compilers underscores that existing testing methodologies are insufficient. Compiler developers must integrate more comprehensive, systematic, and automated testing frameworks, such as mutation-based testing akin to MTZK.
• Focus on Semantic Preservation: The core issue is semantic discrepancy. Developers need to pay extreme attention to ensuring that the translation from high-level ZK programs to low-level circuits is semantically faithful under all conditions, especially concerning edge cases and complex interactions.
• Careful Data Type Handling: The MAX_INT mishandling bug highlights the critical importance of correctly implementing and translating data types, especially finite field arithmetic and integer bounds, across the compilation pipeline.
• Robust Arithmetic Operations: The division-by-zero bug illustrates the need for precise and secure handling of all arithmetic operations, ensuring that undefined behaviors are consistently handled (e.g., by throwing errors) rather than silently leading to incorrect results that can be exploited.
• Thorough Visibility Management: ZK compilers must meticulously manage the distinction between public and private inputs. Any optimizations or transformations based on visibility must be proven to not alter the program's core logic or introduce new vulnerabilities.

For ZK Application Developers:

• Compiler Awareness: Developers building ZK applications for areas like blockchain, finance, or regulatory compliance must be acutely aware of the specific ZK compiler they are using. They should understand its known limitations, bug history, and the robustness of its testing.
• Layered Security: Relying solely on the cryptographic guarantees of ZKPs is insufficient if the underlying compilation process is flawed. Application developers should consider implementing additional checks or redundant logic where critical constraints are involved, if feasible, or at least be prepared to manually audit the generated circuits for critical sections.
• Stay Updated: Regularly monitor security advisories and updates from ZK compiler projects. Promptly patch and upgrade compilers to fixed versions.
• Input Sanitization and Validation: While ZKPs provide privacy, robust input sanitization and validation on the prover's side (before proof generation) and potentially on the verifier's side (for public inputs) remain crucial to prevent malformed inputs from triggering compiler bugs or other vulnerabilities.

For Organizations and Users of ZKP Systems:

• Demand Transparency and Audits: Organizations deploying ZKP-enabled systems, especially those securing significant assets or sensitive data, should demand transparency regarding the ZK compilers used. Regular, independent security audits of these compilers are essential.
• Risk Assessment: Understand that even with strong cryptographic primitives, the implementation layer (compilers) introduces a new attack surface. Conduct thorough risk assessments that include the potential for compiler-induced vulnerabilities.
• Contribute to Open Source: Where ZK compilers are open source, contributing to their testing, formal verification, and development can strengthen the entire ecosystem.

Ultimately, the talk serves as a stark reminder that the security of complex systems is only as strong as their weakest link. In the world of zero-knowledge proofs, the ZK compiler is a foundational and often overlooked component whose correctness is paramount to upholding the privacy and integrity guarantees of the entire system.

Key Takeaways

• ZK Compiler Correctness is Critical: The security and privacy guarantees of zero-knowledge proof systems fundamentally rely on the correct functioning of ZK compilers, which translate high-level programs into low-level cryptographic circuits.
• MTZK is a Pioneering Testing Framework: MTZK is the first systematic work to study and uncover bugs in mainstream ZK compilers, addressing the challenging "ground truth problem" of compiler verification.
• Novel Mutation Strategies: The research introduced two effective mutation-based testing techniques tailored for ZKPs: inserting always-satisfying constraints (satisfiability invariants) and mutating information visibility of inputs.
• Significant Bug Discovery: MTZK successfully discovered 21 bugs across four mainstream ZK compilers, many of which were critical vulnerabilities leading to constraint bypasses or incorrect program semantics.
• Real-World Impact: Examples like the MAX_INT mishandling and division-by-zero flaws demonstrate how compiler bugs can lead to severe security breaches, financial losses, and potential backdoor creation in high-value blockchain and other ZKP applications.
• Call for Enhanced Security Practices: The findings highlight an urgent need for compiler developers to adopt more rigorous, automated testing, and formal verification methods, and for application developers to be acutely aware of compiler risks to build more robust and secure ZKP systems.

About the Speaker(s)

The talk was presented by Dongwei Xiao. The transcript and metadata do not provide further details about their title or affiliation beyond their name.