Language-Agnostic Detection of Computation-Constraint Inconsistencies in ZKP Programs via Value Inference
Arman Kolozyan
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 an IR-based bug detection tool, called CCC-Check, which is based on abstract interpretation. Our evaluation shows that CCC-Check is, on average, two orders of magnitude faster than the SoTA verification tool CIVER, while achieving comparable precision. 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.
Bio:
Arman is a recent graduate in Computer Science with research experience in applied cryptography, currently interning at the Max Planck Institute for Security and Privacy (MPI-SP) under the guidance of Prof. Carmela Troncoso. He received his Masters degree from Vrije Universiteit Brussel where he worked with Janwillem Swalens and Stefanos Chaliasos. Before that, he completed a research internship at KU Leuven's COSIC group under the supervision of Prof. Bart Preneel and Prof. Dave Singelée, where he analyzed the security of the Matter standard for smart home devices.