Introduction

Zero-Knowledge Proofs (ZKPs) enable individuals to prove that they know or possess a piece of information without revealing the actual data. In this process, a “prover” generates a proof based on their knowledge of the system’s inputs, while a “verifier” confirms the validity of the proof without accessing the underlying information.

zk-SNARKs (Succinct Non-interactive Arguments of Knowledge) are non-interactive protocols that allow a prover to generate a concise proof of knowledge. They are commonly used to prove that, for a given function f and a public input x, the prover knows a private input w (known as the witness), such that f(x, w) = y. This is done without disclosing any details about the private input, making zk-SNARKs highly valuable in a variety of applications, particularly in blockchain technology.

zk-SNARKs facilitate private transactions on public blockchains, such as Zcash, by ensuring that transaction details remain confidential. They are also used for compliance purposes, such as demonstrating that a private transaction adheres to banking laws or proving solvency without revealing sensitive information. Additionally, zk-SNARKs contribute to scalability by enabling privacy in zk-SNARK Rollups and supporting interoperability between blockchains through zk-Bridges.

In the previous post, we introduced Zekrom, an open-source library of arithmetization-oriented constructions for zk-SNARK circuits, which includes hash functions like Griffin, Neptune, Rescue Prime, and Reinforced Concrete. This library aims to analyze the performance of novel circuit constructions using modern frameworks such as arkworks-rs and Halo2, while also providing ready-to-use solutions for privacy-preserving applications.

In this post, we explore common vulnerabilities within zk-SNARK proof systems, focusing particularly on Halo2 proving system, and examine the risks associated with improper implementations. Additionally, we explore the security analysis tools available for Halo2 and evaluate their effectiveness.

Halo2

Halo2 is a zk-SNARK protocol that is part of the Zcash ecosystem. It is built upon the arithmetization of PLONK, specifically using an extended version known as UltraPLONK, which supports custom gates and lookup tables, features commonly referred to as “PLONKish.” One of the key advantages of Halo2 is that it does not require a trusted setup, and it supports recursive proof composition, making it particularly well-suited for use in Zcash digital currency.

In addition to its use in Zcash, Halo2 is widely adopted by various other organizations, including Protocol Labs, the Ethereum Foundation’s Privacy and Scaling Explorations (PSE), Scroll, and Taiko, among others. This broad adoption has made Halo2 one of the most popular zk-SNARK constructions in the industry today. A high-level overview of Halo2 is shown below:

UltraPLONK

PLONK is a zk-SNARK that is baed on polynomial IOPs (Interactive Oracle Proofs), and it is widely adopted in the industry due to its compact proof size (around 400 bytes) and fast verification time. UltraPLONK enhances PLONK by introducing support for custom gates and lookup tables, which further reduce the size of computation traces and improve the efficiency of the prover.

In PLONK, gates are primarily composed of multiplication and addition operations. Circuit constraints are expressed using the vanilla PLONK constraint, which can define both addition and multiplication gates.

where q_L, q_R, q_O, and q_M are preprocessed selector polynomials. Any circuit within a given proof system can be represented by this vanilla equation, supplemented by additional constraints derived from wiring.

Inner Product Argument

Polynomial Commitment Schemes (PCS) can generally be classified into several categories, including univariate polynomial commitments, multilinear commitments, vector commitments, and inner product arguments (IPA). A key advantage of PLONK is its flexibility, which allows it to be paired with any type of PCS to create a SNARK.

PLONK commonly uses a univariate polynomial commitment, such as the KZG polynomial commitment scheme, which relies on a universal trusted setup. However, a significant challenge with PLONK is the prover’s computational complexity due to its dependence on Fast Fourier Transforms (FFT), which requires the quasi-linear running time, a direct consequence of using univariate polynomials. HyperPlonk relies on multilinear polynomial commitments to eliminate the need for FFT and to support high degree custom gates.

Halo2 eliminates the need for a trusted setup by employing an Inner Product Argument (IPA) based on the Pedersen commitment scheme. Although IPA typically results in larger proofs than the PLONK SNARK, Halo2 mitigates this drawback through the use of Accumulation. This mechanism allows for the aggregation of multiple proof openings via recursive composition, resulting in an effective balance between proof size and the advantages of a trustless setup. By leveraging these techniques, Halo2 achieves a scalable zero-knowledge proof system without compromising on security or efficiency.

Common Vulnerabilities in Halo2 Proof System

Most Zero-Knowledge applications are not developed from scratch; instead, they often rely on forks of third-party code repositories or low-level libraries. As a result, many ZK development teams concentrate primarily on circuit design and business logic rather than building their own frameworks. Consequently, ZK audits tend to focus heavily on circuits, as they are the component of the stack most susceptible to bugs.

However, the ZKP stack encompasses far more than just circuit design, as illustrated below. A comprehensive ZK audit should therefore examine all aspects of the ZK stack, including the soundness of protocols, the secure implementation of cryptographic algorithms, the correct usage of parameters, and the dependencies involved.

Below, we present some examples of publicly disclosed vulnerabilities in Zero-Knowledge Proof systems. For a more comprehensive and up-to-date list, we recommend referring to the ZK Bug Tracker, a community-maintained resource dedicated to tracking vulnerabilities related to ZKP technologies.

Fiat-Shamir Transformation

The Fiat-Shamir (FS) transformation enables a prover to generate challenge values without interaction, replacing the need for verifier-supplied challenges. This is accomplished using a deterministic method, typically a cryptographic hash function, to produce the challenge value. While this transformation simplifies the interactive proof process, its practical implementation can be notably complex.

A critical aspect of the Fiat-Shamir transformation is the careful selection of inputs for the cryptographic hash function. The security of the proof system heavily depends on the correct choice of these inputs. Using incorrect or incomplete inputs can lead to vulnerabilities, often resulting in a broken proof system. For example, the Frozen Heart vulnerability may arise if portions of the public input are omitted from the FS transform. Similarly, the Last Challenge Attack may occur if parts of the transcript, beyond just the public input, are excluded when computing the final FS transform challenge.
Thus, careful consideration and rigorous analysis are required to ensure the transformation is implemented securely.

KZG’10 Commitment Scheme

The KZG’10 commitment scheme requires a one-time trusted setup before any KZG commitments can be computed. Once this trusted setup is completed, it can be reused to commit to and reveal as many different polynomials as needed. However, a critical aspect of this process is the secret parameter generated during the setup. This parameter must be securely discarded after the trusted setup ceremony to ensure that no one can determine its value.

Trusted setup ceremonies are typically conducted using established methods that rely on weak trust assumptions, such as the 1-out-of-N trust assumption, which can be achieved through multi-party computation (MPC). These methods help ensure that even if all but one participant is compromised, the setup remains secure. For more information on how trusted setups work, you can refer to this post by Vitalik Buterin.

Another potential vulnerability in the KZG scheme involves the incorrect computation of the Fiat-Shamir transform due to the omission of a non-input part of the full transcript. For more details, see this paper.

Although the original Halo2 protocol, as implemented in Zcash, doesn’t use KZG commitments, some variants of Halo2 utilize the KZG commitment scheme due to the need for smaller proofs and faster verification on resource-constrained hardware. For instance, the Aleph Zero proof system employs this approach.

Circom circuit

According to a survey paper, over 80% of findings in ZK audit reports are traced back to the circuit layer. One critical aspect of circuit auditing is ensuring that all inputs are properly used and constrained during proof generation. In Circom circuits, this means that every input must be involved in the creation of constraints to ensure the integrity of the proof.

Circuits that are under-constrained can cause verifiers to erroneously accept invalid proofs, compromising the system’s soundness. Conversely, over-constrained circuits can lead to honest provers or benign proofs being unjustly rejected, which impacts the completeness of the system.

Constraints in Circom are only generated using the === or <== operators. However, it is possible to mistakenly use the <-- operator, which does not create a constraint. An unconstrained <-- signal can be freely set to any value by a malicious prover, potentially compromising the security of the proof. Although this approach might sometimes be used for circuit optimization—such as reducing a ternary operator from two constraints to one—it poses a risk if not managed carefully.

If you encounter a <-- in Circom, it’s crucial to ensure that the subsequent signal is correctly constrained to prevent any exploitation by a malicious prover who could insert arbitrary values while still passing proof validation.

Arithmetic overflow/underflow

In ZKPs, Circom circuits operate over a scalar field, with all arithmetic operations performed modulo the field’s order. This modular arithmetic often causes overflow or underflow issues, which are not immediately apparent due to the inherent wrapping behavior.

To mitigate these risks, developers can utilize the LessThan and Num2Bits templates provided by Circomlib. These templates help enforce that values remain within specified bounds, effectively preventing overflows and underflows.

Missing constraints

In zk circuits, assignments are used to allocate values to variables during the proof generation process, but unlike constraints, they do not enforce proof validity on their own. If a necessary constraint is omitted in the configure function, a malicious prover could exploit this weakness by modifying the assign function to bypass or manipulate the missing constraint.

These discrepancies between assignment and constraint definitions create vulnerabilities, allowing a malicious actor to fork the code and adjust the assign function to exploit the absent constraint. This manipulation can lead to the generation of invalid proofs that appear valid, undermining the security and integrity of the zk circuit.

Security Analysis Tools

Static analysis

• Circomspect: Developed by Trail of Bits, Circomspect is a static analyzer and linter for the Circom programming language. It leverages code from the Rust-based Circom compiler built by iden3, providing insights into potential vulnerabilities and best practices in Circom code.
• ZKAP: A collection of static analysis detectors aimed at identifying bugs in Zero-Knowledge Proof (ZKP) implementations. This tool focuses on finding common pitfalls and errors within ZKP frameworks.
• Korrekt (Halo2-analyzer): Created by Quantstamp, this tool automatically verifies the correctness of the Halo2 proof system, which employs PLONKish arithmetization. It helps ensure the integrity of proofs generated within the Halo2 framework.
• Ecne: Ecne converts functions into Rank-1 Constraint System (R1CS) form, and it is used to verify that certain sets of R1CS constraints uniquely represent functions. This ensures that the cryptographic constraints accurately reflect the intended logic.
• Picus: Picus implements the QED tool to check various correctness notions, particularly focusing on detecting whether the resulting system is under-constrained. This helps in identifying potential security gaps in zk-SNARK circuits.
• Circomscribe: An online tool that shows which lines of Circom code generate specific constraints, if any. Circomscribe is a modified version of the Circom compiler, running in WebAssembly (WASM) and emitting detailed JSON-formatted information during the compilation process.

Dynamic Analysis

• ‍: SNARKProbe offers two subtools: ConstraintChecker and SnarkFuzzer. ConstraintChecker identifies errors in constraint flattening or gadget usage, while SnarkFuzzer is a smart fuzzing tool designed to uncover potential logical or software errors in zk-SNARK libraries. These tools assist in dynamically testing and validating the robustness of zk-SNARK implementations.

Post-quantum HALO2

Many existing zk-SNARKs, including widely deployed systems like Groth16, PLONK, Marlin, and Bulletproofs, are based on discrete logarithm and pairing-based cryptographic assumptions, which are susceptible to quantum attacks. To address this risk, considerable efforts are being taken to integrate post-quantum (PQ) cryptographic schemes, particularly to mitigate “intercept-now-decrypt-later” threats. However, the urgency to transition zk-SNARKs to quantum-resistant constructions is not as immediate as it is for public-key cryptographic schemes. This is because the security risks associated with SNARKs differ from those of encryption, where the primary concern is the potential for retrospective decryption of intercepted data.

Nevertheless, significant progress has been made in developing post-quantum zk-SNARKs, which rely on cryptographic hash functions or lattice-based cryptography. These approaches often come with the trade-off of larger proof sizes, which can result in slower verification times and increased gas costs on blockchains. Several post-quantum SNARKs have been constructed using hash-based Merkle commitments, such as STARKs, Ligero, Aurora, and Brakedown. While these systems offer quantum resistance, they tend to have relatively large proof sizes and require substantial memory resources when handling large statements.

Lattice-based zk-SNARKs are also advancing and show promising potential for more efficient, quantum-resilient proofs. Although not yet as competitive as hash-based systems, recent constructions like SLAP and LatticeFold indicate a path forward for lattice-based commitments in zk-SNARKs.

Despite these advancements, a significant challenge remains: post-quantum zk-SNARKs still suffer from substantial proof sizes compared to their pre-quantum counterparts. For example, Groth16 can produce proofs as compact as 128 bytes, whereas the most succinct post-quantum proofs can be up to 1000 times larger. This considerable difference underscores the efficiency trade-offs involved in achieving quantum resilience, and highlights the ongoing need for research and development to bridge this gap while maintaining practical performance for blockchain applications.

For quantum-resistent Halo2, a logical starting point would be to replace the discrete-logarithm-based commitment scheme with a post-quantum alternative, potentially leveraging lattice-based commitment schemes from recent advancements.
We will review the status of post-quantum zk-SNARKs and how they could be applied to Halo2 in the next post.

Conclusion

The recent advancements in Zero-Knowledge Proofs (ZKPs) and zk-SNARKs have brought a range of exciting applications, particularly within the blockchain industry. However, despite the progress in tools and methodologies, vulnerabilities can still emerge, especially given the complexity inherent in zk-SNARK systems.

By integrating these practices throughout the development lifecycle, we can enhance the security of Zero-Knowledge Proof systems, thereby advancing their effectiveness in privacy-preserving computations in blockchain.