一句话：提出 QED 2，结合 SMT 求解与轻量级唯一性推断，自动检测零知识证明算术电路中的欠约束漏洞。
随着零知识证明在区块链等场景中广泛应用，Circom 等 DSL 会编译生成有限域上的算术电路，但电路可能因程序或编译器缺陷而欠约束，导致同一输入存在多个 witness，攻击者可伪造证明。本文提出针对有限域多项式方程的语义推理方法，判断每个信号是否由输入唯一确定；其核心是将 SMT 求解与轻量级唯一性推断相结合。作者实现工具 QED 2，在 163 个 Circom 电路上评估，可成功处理 70% 基准，即验证输出信号唯一或找到反例 witness，并发现 8 个此前未知的广泛使用电路漏洞。
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 QED 2 and evaluate it on 163 Circom circuits. Our evaluation shows that QED 2 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, QED 2 has found 8 previously unknown vulnerabilities in widely-used circuits.
@article{paperbot1952,
title = {Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs},
author = {Shankara Pailoor and Yanju Chen and Franklyn Wang and Clara Rodríguez and Jacob Van Geffen and Jason Morton and Michael Chu and Brian Gu and Yu Feng and Işıl Dillig},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591282}
}