ConsCS: Effective and Efficient Verification of Circom Circuits
This program is tentative and subject to change.
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%.
This program is tentative and subject to change.
Wed 30 AprDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 17:30 | Formal Methods 2Research Track / New Ideas and Emerging Results (NIER) / Journal-first Papers at 103 | ||
16:00 15mTalk | ConsCS: Effective and Efficient Verification of Circom Circuits Research Track Jinan Jiang The Hong Kong Polytechnic University, Xinghao Peng , Jinzhao Chu The Hong Kong Polytechnic University, Xiapu Luo Hong Kong Polytechnic University | ||
16:15 15mTalk | Constrained LTL Specification Learning from Examples Research Track Changjian Zhang Carnegie Mellon University, Parv Kapoor Carnegie Mellon University, Ian Dardik Carnegie Mellon University, Leyi Cui Columbia University, New York, Romulo Meira-Goes The Pennsylvania State University, David Garlan Carnegie Mellon University, Eunsuk Kang Carnegie Mellon University | ||
16:30 15mTalk | LLM-aided Automatic Modeling for Security Protocol Verification Research Track Ziyu Mao Zhejiang University, Jingyi Wang Zhejiang University, Jun Sun Singapore Management University, Shengchao Qin Xidian University, Jiawen Xiong East China Normal University | ||
16:45 15mTalk | Model Assisted Refinement of Metamorphic Relations for Scientific Software New Ideas and Emerging Results (NIER) Clay Stevens Iowa State University, Katherine Kjeer Iowa State University, Ryan Richard Iowa State University, Edward Valeev Virginia Tech, Myra Cohen Iowa State University | ||
17:00 15mTalk | Precisely Extracting Complex Variable Values from Android Apps Journal-first Papers | ||
17:15 7mTalk | A Unit Proofing Framework for Code-level Verification: A Research Agenda New Ideas and Emerging Results (NIER) Paschal Amusuo Purdue University, Parth Vinod Patil Purdue University, Owen Cochell Michigan State University, Taylor Le Lievre Purdue University, James C. Davis Purdue University Pre-print | ||
17:22 7mTalk | Automated Testing Linguistic Capabilities of NLP Models Journal-first Papers Jaeseong Lee The University of Texas at Dallas, Simin Chen University of Texas at Dallas, Austin Mordahl The University of Texas at Dallas, Cong Liu University of California, Riverside, Wei Yang UT Dallas, Shiyi Wei University of Texas at Dallas | ||