Welcome to the resource topic for 2025/2120
Title:
Language-Agnostic Detection of Computation-Constraint Inconsistencies in ZKP Programs via Value Inference
Authors: Arman Kolozyan, Bram Vandenbogaerde, Janwillem Swalens, Lode Hoste, Stefanos Chaliasos, Coen De Roover
Abstract:Zero-knowledge proofs (ZKPs) allow a prover to convince a verifier of a statement’s truth without revealing any other information. In recent years, ZKPs have matured into a practical technology underpinning major applications. However, implementing ZKP programs remains challenging, as they operate over arithmetic circuits that encode the logic of both the prover and the verifier. Therefore, developers must not only express the computations for generating proofs, but also explicitly specify the constraints for verification. As recent studies have shown, this decoupling may lead to critical ZKP-specific vulnerabilities.
Unfortunately, existing tools for detecting them are limited, as they:
(1) are tightly coupled to specific ZKP languages,
(2) are confined to the constraint level, preventing reasoning about the underlying computations,
(3) target only a narrow class of bugs,
and (4) suffer from scalability bottlenecks due to reliance on SMT solvers.
To address these limitations, we propose a language-agnostic formal model, called the Domain Consistency Model (DCM), which captures the relationship between computations and constraints. Using this model, we provide a taxonomy of vulnerabilities based on computation-constraint mismatches, including novel subclasses overlooked by existing models. Next, we implement a lightweight automated bug detection tool, called CCC-Check, which is based on abstract interpretation. We evaluate CCC-Check on a dataset of 20 benchmark programs. Compared to the SoTA verification tool CIVER, our tool achieves a 100-1000$\times$ speedup, while maintaining a low false positive rate. Finally, using the DCM, we examine six widely adopted ZKP projects and uncover 15 previously unknown vulnerabilities. We reported these bugs to the projects’ maintainers, 13 of which have since been patched. Of these 15 vulnerabilities, 12 could not be captured by existing models.
ePrint: https://eprint.iacr.org/2025/2120
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .