Logo image
Back
Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs
Journal article   Open access   Peer reviewed

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

Shankara Pailoor, Yanju Chen, Franklyn Wang, Clara Rodríguez, Jacob Van Geffen, Jason Morton, Michael Chu, Brian Gu, Yu Feng and Işıl Dillig
Proceedings of ACM on programming languages, v 7(PLDI), pp 1510-1532
06 Jun 2023
DOI: https://doi.org/10.1145/3591282
url
https://doi.org/10.1145/3591282View
Published, Version of Record (VoR) Open

Abstract

Automated reasoning Cryptographic protocols Program analysis Program verification Theory of computation
As zero-knowledge proofs gain increasing adoption, the cryptography community has designed domain-specific languages (DSLs) that facilitate the construction of zero-knowledge proofs (ZKPs). Many of these DSLs, such as Circom, facilitate the construction of arithmetic circuits, which are essentially polynomial equations over a finite field. In particular, given a program in a zero-knowledge proof DSL, the compiler automatically produces the corresponding arithmetic circuit. However, a common and serious problem is that the generated circuit may be underconstrained, either due to a bug in the program or a bug in the compiler itself. Underconstrained circuits admit multiple witnesses for a given input, so a malicious party can generate bogus witnesses, thereby causing the verifier to accept a proof that it should not. Because of the increasing prevalence of such arithmetic circuits in blockchain applications, several million dollars worth of cryptocurrency have been stolen due to underconstrained arithmetic circuits. Motivated by this problem, we propose a new technique for finding ZKP bugs caused by underconstrained polynomial equations over finite fields. Our method performs semantic reasoning over the finite field equations generated by the compiler to prove whether or not each signal is uniquely determined by the input. Our proposed approach combines SMT solving with lightweight uniqueness inference to effectively reason about underconstrained circuits. We have implemented our proposed approach in a tool called QED2 and evaluate it on 163 Circom circuits. Our evaluation shows that QED2 can successfully solve 70% of these benchmarks, meaning that it either verifies the uniqueness of the output signals or finds a pair of witnesses that demonstrate non-uniqueness of the circuit. Furthermore, QED2 has found 8 previously unknown vulnerabilities in widely-used circuits.

Metrics

21 Record Views
12 citations in Web of Science
9 citations in Scopus

Details

InCites Highlights

Data related to this publication, from InCites Benchmarking & Analytics tool:

Collaboration types
Domestic collaboration
International collaboration
Web of Science research areas
Computer Science, Software Engineering
Logo image