Academic research: Findings from our zero-knowledge research

Sep 10

| 6 min read

At Veridise, we combine cutting-edge academic research with the latest industry experience.

Along with our extensive experience auditing key blockchain infrastructure protocols, smart contracts, and zero-knowledge circuit implementations, many of our team members have academic research backgrounds.

In this blog post, we feature our research on zero-knowledge security and how it relates to work we are doing at Veridise.

We cover the following four ZK-related research papers:

Below, we’ve summarized each paper, along with their authors from the current Veridise team — click on each name to learn more about our team members!

Veridise’s academic research series:
📚 Part I: Findings from our smart contract research
📚 Part II:
Findings from our zero-knowledge research

Certifying Zero-Knowledge Circuits with Refinement Types

Veridise authors: Bryan Tan, Işıl Dillig

The paper addresses the challenge of verifying the correctness of zero-knowledge (ZK) proof systems, which are essential for secure applications like privacy-preserving apps and Layer 2 scaling solutions (ZK-Rollups).

ZK systems are highly prone to subtle bugs, which can allow attackers to exploit them without detection, making them particularly dangerous. Traditional defenses (e.g. runtime monitoring or sandboxing) are ineffective against such attacks because they leave no observable traces. This makes verification and static analysis the only viable solutions to prevent these silent exploits.

The paper introduces Coda, a statically-typed functional language that enables developers to formally specify and verify the correctness of ZK applications using a refinement type system. Refinement types augment traditional types with logical formulas, thereby allowing the specification of much more intricate correctness properties and enabling compile-time validation of those properties. Coda allows developers to write specifications as types and Coda’s type checker verifies that the implementation conforms to the given specification. Coda was used to re-implement 79 arithmetic circuits from widely-used Circom libraries and applications, an exercise which revealed six previously unknown vulnerabilities.

Overall, the Coda approach combines the benefits of static analysis with interactive theorem proving, making it a powerful tool for developers in the blockchain security domain. At Veridise, we have used the technique from Coda to formally define and verify the behavior of ZK circuits in auditing projects such as Circom-lib and Semaphore.

Automated Detection of Under-constrained Circuits in Zero-Knowledge Proofs

Veridise authors: Shankara Pailoor, Jacob Van Gaffen, Işil Dillig

This research paper addresses the issue of underconstrained arithmetic circuits in zero-knowledge proofs, which can lead to security vulnerabilities. These circuits, generated by domain-specific languages (DSLs) like Circom, can admit multiple witnesses for a given input, enabling malicious parties to create bogus proofs.

To combat this problem, the paper introduces QED2, a novel tool designed to automatically detect underconstrained circuits in zero-knowledge proof systems. QED2 combines lightweight Uniqueness Constraint Propagation (UCP) with SMT-based (Satisfiability Modulo Theory) reasoning to effectively verify whether a circuit is properly constrained.

The tool was tested on 163 real-world circuits from the Circom library. QED2 successfully solved 70% of these benchmarks, identifying eight previously unknown vulnerabilities in critical ZKP circuits. This demonstrates the potential of the tool to significantly enhance the security and reliability of zero-knowledge proof systems.

At Veridise, this research inspired the development of our in-house tool, Picus, designed to detect underconstrained circuits in zero-knowledge proofs. Picus has since undergone various improvements and has been extended to several additional ZK DSLs. Picus is frequently deployed in our ZK audits and has helped identify underconstrained circuits in a number of applications and languages.

Practical Security Analysis of Zero-Knowledge Proof Circuits

Veridise authors: Jon Stephens, Kostas Ferles, Shankara Pailoor, Işil Dillig

This research paper presents a lightweight technique for detecting vulnerabilities in zero-knowledge proof circuits, focusing on those written in Circom, a popular domain-specific language (DSL). The paper introduces a static analysis framework that uses a new program abstraction called Circuit Dependence Graph (CDG) to capture key properties of the circuit. The CDG abstraction facilitates efficient identification of whether a Circom program contains a vulnerability pattern.

The tool includes nine different detectors within this framework which were evaluated on over 258 circuits. The evaluation demonstrats that these detectors can identify vulnerabilities, including previously unknown ones, with high precision and recall, significantly improving the security analysis of ZKP circuits.

At Veridise, we have integrated this work into our Vanguard static analysis framework and have extended it to other ZK languages. It is frequently used in Veridise’s ZK audits and has identified several critical vulnerabilities.

Split Gröbner Bases for Satisfiability Modulo Finite Fields

Veridise authors: Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Işil Dillig

This research paper aims to improve the scalability of solvers used in the automated verification of cryptosystems by addressing the inefficiencies of previous solvers that build a full Gröbner basis (GB) for systems of field equations.

The paper proposes a new solver that uses multiple simpler GBs instead of one full GB, implemented within the cvc5 SMT (Satisfiability Modulo Theory) solver, and introduces specialized propagation algorithms for tasks such as understanding bitsums (common in ZKP circuits).

Experimental results demonstrate that this new solver significantly outperforms prior solvers in handling bitsum-heavy determinism benchmarks, without adding much overhead for other types of benchmarks.

The approach, called Split Gröbner Basis, avoids computing a full Gröbner Basis, and its instantiation, BitSplit, is particularly effective for bitsum-heavy queries. The method was also applied to ZKP compiler verification, showing promising results.

At Veridise, we’ve integrated the solver — enhanced with ideas from this paper — into Picus, our tool for detecting underconstrained ZK circuits. When a circuit is underconstrained, it translates into a satisfiability problem involving a system of polynomial equations. ZK circuits are often bitsum-heavy, making them ideal candidates for the Split Gröbner Basis approach proposed in this paper.

Conclusion

Our academic work in ZK has resulted in the following tools and advancements:

  • Coda, which revealed six previously unknown vulnerabilities in 79 Circom circuits. We have used Coda for formal verification in our auditing projects, such as Circom-lib and Semaphore.
  • QED², which successfully addressed 70% of 163 benchmarks and discovered eight new vulnerabilities in widely-used circuits. This paper initiated the development of our in-house tool Picus, which detects ZK circuit vulnerabilities.
  • ZKAP, our detectors identified vulnerabilities in 258 Circom projects with high precision and recall, including several previously unknown issues.
  • BitSplit, which significantly outperformed prior solvers in handling bitsum-heavy determinism benchmarks, demonstrating the effectiveness of using multiple simpler Gröbner bases.

At Veridise, we’re committed to combining academic research with industry practice to make zero-knowledge applications more robust and reliable.

Thank you for reading! If you haven’t had the chance yet, you can read our similar blog post on smart contract security research.

Veridise’s academic research series:
📚 Part I: Findings from our smart contract research
📚 Part II:
Findings from our zero-knowledge research

More by Veridise