Zero-knowledge proofs (ZKPs) have evolved from being a theoretical concept providing privacy and verifiability to having practical, real-world implementations. Some of the most common use-cases are for private transactions in blockchains (e.g., Zcash), blockchains with private smart contract capabilities (e.g., Aleo, scalability through off-chain validity proofs (e.g., zk-rollups), infrastructure for secure non-custodial authentication (e.g., zkLogin), and private-focused applications such as ZKEmail. All of those examples are build on top of SNARKs.

In the past year, at zkSecurity, we have worked on auditing diverse applications that either use ZKPs or even auditing implementations of ZKPs. Further, we have been doing research on developing safer DSLs for writing circuits, and better understanding security issues in the ZKP ecosystem. Finally, we have also developed tools to help both developers and auditors when working with ZKPs.

In this article, we will briefly discuss where vulnerabilities can be introduced when using ZKPs, and then we will discuss the state of security tools for finding vulnerabilities in ZKPs.

Layers of SNARKs

In a recent work where we systemized the knowledge of security vulnerabilities in SNARKs, we provided a concrete system model for SNARKs. Part of the model is to break the implementation and use of SNARKs into layers. The following figure, depicts the main layers.

We have the following layers. For each layer, we also provide the the respective component/tool for the Semaphore protocol.

• Circuit Layer: Developers have to write a circuit that represents their logic in a SNARK-friendly program using a DSL or an eDSL (e.g., Circom or Halo2). The circuit has a dual purpose: first, to compute values and fill the witness (prover job) and, secondly, to constrain/assert that the witness is correct (verifier logic) – e.g., semaphore.circom.
• Frontend Layer: The frontend typically includes a compiler that takes the circuit as input and extracts the constraints in an arithmetization (e.g., R1CS). Furthermore, the frontend also provides a witness generation function that takes some public (and private) inputs and produces a witness based on the logic described in the circuit – e.g., the circom compiler.
• Backend Layer: The backend implements the three main functions of a SNARK, i.e., Setup, Prove, Verify – e.g., the snarkjs toolchain.
• Integration Layer: Beyond the circuit and the infrastructure required to prove a witness and verify its proof, applications typically require some auxiliary code that interacts with the SNARK components. A typical example in the blockchain world is the smart contract that interacts with the on-chain verifier to verify submitted proofs and implement the respective logic depending on the verifier’s outcome. This code might require performing non-trivial operations such as enforcing some assertions before interacting with the SNARK, or implementing critical logic that is complementary to the ZKPs, such as handling of nullifiers – e.g., the semaphore.sol solidity smart contract.

It is critical to note that a vulnerability in any layer can break the properties provided by the ZKP. Furthermore, a vulnerability in the Frontend or Backend layers could break any applications built on top of them, even if the circuit is correct.

Vulnerabilities in SNARKs

Vulnerabilities in SNARKs could break the main properties provided by the ZKPs:

• Breaking Soundness: A prover can convince a verifier of a false statement.
• Breaking Completeness: Cannot verify proofs for valid statements or cannot produce proofs for valid statements.
• Breaking Zero-Knowledge: Information leakage about the private witness.

Security Tools for Detecting Circuit Bugs

Recently, a lot of effort from both practitioners and researchers has been made into developing tools for finding vulnerabilities in the Circuit layer. This is expected, as most of the reported ZKP-related vulnerabilities are in that layer, but also most of the audits are circuit audits. The main vulnerabilities that can occur in this layer are:

• Underconstrained Vulnerabilities: Arises from insufficient constraints and typically lead to critical soundness errors.
• Overconstrained Vulnerabilities: Circuits can be over-constrained, leading to the rejection of valid witnesses by honest provers or benign proofs from honest verifiers.
• Computation/Hints Errors: Occurs when the computational part of a circuit is erroneous.

So far, almost all forms of formal methods have been used to detect circuit vulnerabilities. Below, we briefly describe the main techniques used to detect circuit vulnerabilities.

Static Analysis and Symbolic Execution

Static analysis involves examining the code without executing it to identify potential vulnerabilities. This method relies on patterns and heuristics to detect common issues that could lead to vulnerabilities. Examples are Circomspect and ZKAP for Circom and halo2-analyzer for Halo2 circuits. Current approaches are limited in the sense that they can detect only very specific vulnerability patterns and can analyze only programs written in a specific DSL or eDSL. In principle, some of the techniques could work on more than one DSL. These tools are typically used during development or in the initial phase of an audit to detect potential vulnerabilities. We are still in the preliminary stages of developing static analysis tools for ZKPs compared to other industries. For instance, static analyzers for smart contracts have become highly sophisticated, capable of detecting critical vulnerabilities effectively.

Symbolic execution is a program analysis technique that examines possible execution paths of a program by treating inputs as symbolic variables rather than concrete values. This technique systematically explores all potential paths the program can take, looking for bugs and vulnerabilities by analyzing how different variables affect program behavior. Symbolic execution for bug finding, as opposed to formal verification, is still underutilized in this field. This approach is particularly useful for detecting underconstrained and overconstrained bugs in circuits. Despite its potential, symbolic execution has not yet been widely exploited to detect circuit vulnerabilities, beyond some initial formal verification efforts (as we will see below).

Dynamic Analysis and Fuzzing

Dynamic analysis involves executing the code and observing its behavior in real-time to identify potential vulnerabilities. Fuzzing, a subset of dynamic analysis, involves providing the program with a wide range of random inputs to see how it handles unexpected or extreme cases. The only existing tool for dynamic analysis is SnarkProbe, a security analysis framework for SNARKs that can analyse R1CS-based libraries and applications to detect various issues, such as edge case crashing, cryptographic operation errors, and/or inconsistencies with protocol descriptions. This tool requires some ideal functionality files provided by the users and then it tries to detect inconsistencies. Although SnarkProbe is an interesting first approach, there is still a missing opportunity in using dynamic analysis tools for bug finding in this space similar to other fields. Note that some efforts have been made to apply traditional fuzzers to detect issues in SNARKs, but typically those tools struggle as they cannot solve the oracle problem required to detect important vulnerabilities for SNARKs, such as underconstrained bugs that can break the soundness of an application.

Formal Verification

Formal verification involves mathematically proving that a system adheres to certain properties. This technique provides assurance about the correctness and security of a system by rigorously checking against a formal specification or some rules. Specifically, formal verification is a process that uses mathematical and logical reasoning to ensure that a system’s design satisfies certain correctness properties. Unlike traditional testing methods, which can only detect the presence of bugs, formal verification can prove the absence of specific types of errors. This makes it a useful tool for ensuring the security of systems. However, formal verification often poses significant challenges due to the need for accurate formal specifications, and it can struggle to scale effectively, often resulting in timeouts. For a comprehensive overview of formal verification for ZKPs, you can refer to this article. Below, we provide a brief discussion on the current state of formal verification for circuits.

Different Approaches: Using a Proof Assistant vs. Without Using a Proof Assistant

• Using a Proof Assistant: Proof assistants like Coq and Lean provide an interactive environment for developing formal proofs. These tools allow users to write specifications and proofs in a formal language, which the proof assistant then checks for correctness. Using proof assistants requires significant expertise and effort to use effectively. Recently, there have been some efforts on automated that process through transpilation of programs.
• Without Using a Proof Assistant: This approach involves using automated tools like SMT solvers (e.g., Z3 and CVC4) and other automated reasoning tools to verify properties of the system.

Formal Verification for Circuits

In the context of ZKP circuits, formal verification ensures that circuits correctly implement the intended logic without introducing vulnerabilities. This involves verifying that constraints are correctly implemented and that the circuit behaves as expected under all possible inputs.

Several existing open-source, end-to-end tools and techniques for formal verification of circuits include:

• Picus: Uses an advanced symbolic execution approach to verify that Circom circuits are not under-constrained. This tool leverages static analysis and SMT solver to ensure that every part of the circuit is adequately constrained.
• CIVER: Employs a modular technique based on the application of transformation and deduction rules to verify properties of Circom circuits using pre- and post-conditions. This method provides a structured way to reason about the correctness of circuit components.
• horus-checker: performs formal verification of Cairo smart contracts with language annotations using SMT solvers.
• Medjai: A symbolic evaluator for Cairo that checks whether certain properties hold on Cairo programs.
• DSLs like Coda and Leo: These domain-specific languages support formal verification of circuits using synthesis, aiding developers in creating more secure circuits. They integrate formal verification techniques directly into the development process, making it easier to ensure correctness from the outset.
• Transpiler from Gnark to Lean: A library that compiles zero-knowledge circuits from Gnark to the Lean theorem prover to formally verify the circuit.

Despite these advancements, significant limitations remain. Tools relying on SMT solvers, like Picus, face challenges due to limited support and efficiency in handling finite field arithmetic, leading to performance bottlenecks. These tools, while powerful, are often constrained by the underlying solvers’ capabilities, which can limit their applicability to more complex circuits. Recent works by Ozdemir et al. have attempted to improve SMT solvers for ZKPs. Proof assistant languages, particularly for cryptographic protocols, still face limitations in expressivity. There are few tools capable of directly proving theorems about cryptographic protocols. Multiple efforts have been made to overcome these hurdles, but formally verify ZKP circuit remains a challenging task. Despite the impressive efforts towards formal verification for ZKPs, it should be accompanied by a holistic security approach to ensure security. End-to-end formal verification is a complex task and often relies on user input and other software, which means that in practise is difficult to be certain for the absense of bugs.

Testing Tools

Furthermore, in the circuit development process, we have found a major issue: the lack of robust testing frameworks. Developers often use testing frameworks from host languages in eDSLs or creating custom toolchains when using DSLs. However, there is limited support for effectively writing unit and integration tests for circuits, particularly for testing soundness vulnerabilities. A critical missing piece of infrastructure is property-based testing, similar to QuickCheck or Foundry, which is essential for thorough property testing.

Additionally, debugging circuits in most DSLs is a challenging task, presenting another area in need of improvement. To address this, we developed Circomscribe, a tool for debugging constraints in Circom circuits. Moving forward, we plan to release more tools to aid developers and auditors in the testing and debugging of circuits, enhancing the overall development process and ensuring higher security and reliability of ZKP implementations.

Overview

In the following table, we provide an overview of the existing open-source tooling:

UC: Underconstrained, OC: Overconstrained, CE: Computational Error, SA: Static Analysis, FV: Formal Verification, DA: Dynamic Analysis

Frontend and Backend

The infrastructure layer, comprising the frontend and backend of SNARK systems, has largely been overlooked by security researchers. Ozdemir et al. recognized that a flaw in a ZKP compiler could undermine the integrity of a ZKP and took initial steps to mitigate such risks by partially verifying a key compiler pass in the CirC compiler. SNARKProve implements a fuzzing framework that can be configured with custom files (i.e., ideal files) to test specific cryptographic properties of the backends and frontends. In its initial version, it has been successful in detecting issues in the Setup phase of the backend.

Some initial work has been done on verifying the verifier, i.e., ensuring that the implementation of the verification algorithm is correct. Additionally, practitioners have employed fuzzing tools like AFL to identify bugs in these layers. However, these tools are somewhat limited in scope, typically only capable of detecting crashes and potentially missing more subtle but critical vulnerabilities such as miscompilations. Detecting bugs in these layers is of paramount importance as any exploitable bug could affect the entire stack. For example, even if a circuit is formally verified, a frontend vulnerability could render its deployment unsound. Thus, ensuring the security and correctness of both the frontend and backend layers is crucial for the overall integrity of ZKP systems.

What’s Next

Security tools for ZKPs are in the early stages of development, but they hold great promise for the future. These tools can significantly aid developers and should ideally become an integral part of the development lifecycle, used before auditing. Auditing remains primarily a manual effort, as most of the protocols using ZKPs require domain expertise into understanding their logic and the implementation.

At zkSecurity, we are dedicated to developing and publicly sharing tools to assist both auditors and developers. Tools like Circomspect are part of our efforts to improve the debugging of ZKP circuits. We are also focused on categorizing ZK vulnerabilities and providing insights to improve and develop new tools to detect them. Check out our blog post on Boomerang vulnerabilities and our paper on analyzing SNARK vulnerabilities for more information.

If you’re passionate about zero-knowledge proofs and security, consider joining us on this exciting journey. You can apply by taking our zkBank challenge here! For those interested in security tools for ZKPs and seeking an internship to work on interesting problems, consider applying here.