一句话：提出 ConsCS 框架，用电路推理规则与二叉属性图加速 Circom 欠约束电路验证，并以领域信息引导 SMT 求解。
Circom 是编写算术电路的流行语言，其电路被编译为 R1CS 以生成 zk-SNARK 证明。R1CS 电路的一大挑战是欠约束问题：约束不足会使错误计算通过验证，造成安全漏洞。本文提出自动验证 Circom 电路的框架 ConsCS，贡献有三：1）提出新的电路推理规则，缩小电路规模并比现有工作提取更全面的信息；2）引入二叉属性图（Binary Property Graph, BPG）作为高效推理引擎，在有效性与效率上优于现有工具；3）利用细粒度领域特定信息引导 SMT 求解以处理非线性约束，将现有工作的 SMT 查询成功率从 2.68% 提升到 48.84%。实验表明 ConsCS 将现有工作的求解率从约 50–60% 提升至 80% 以上。
Circom is a popular programming language for writing arithmetic circuits that can be used to generate zero-knowledge proofs (ZKPs) like zk-SNARKS. ZKPs have received tremendous attention in protocols like zkRollups. The Circom circuits are compiled to Rank-1 Constraint Systems (R1CS) circuits, based on which zk-SNARK proofs are generated. However, one major challenge associated with R1CS circuits is the problem of under-constrained circuits, which are susceptible to allowing incorrect computations to pass verification due to insufficient constraints, potentially leading to security vulnerabilities. In this paper, we propose a novel framework CONSCS to automatically verify Circom circuits. Our contributions are threefold: 1) we propose novel circuit inference rules to help reduce the size of circuits and to extract more comprehensive information than existing works; 2) we introduce the novel Binary Property Graph (BPG) as a highly efficient reasoning engine, outperforming all existing tools in effectiveness and efficiency; 3) we leverage fine-grained domain-specific information to guide the SMT solving to address non-linear constraints, increasing the success rate of SMT queries of existing works from 2.68% to 48.84%. We conduct experiments to show that CONSCS enhances the solved rate of existing works from around 50-60% to above 80%.
DOI 原文 ·
@inproceedings{paperbot8872,
title = {ConsCS: Effective and Efficient Verification of Circom Circuits},
author = {Jinan Jiang and Xinghao Peng and Jinzhao Chu and Xiapu Luo},
booktitle = {ICSE},
year = {2025},
doi = {10.1109/icse55347.2025.00200}
}