Paper 2023/1051
Automated Analysis of Halo2 Circuits
, Polytechnique Montréal, Quantstamp, Inc., Aarhus University, Quantstamp, Inc., Quantstamp, Inc., Quantstamp, Inc., Quantstamp, Inc.Abstract
Zero-knowledge proof systems are becoming increasingly prevalent and being widely used to secure decentralized financial systems and protect the privacy of users. Given the sensitivity of these applications, zero-knowledge proof systems are a natural target for formal verification methods. We describe methods for checking one such proof system: Halo2. We use abstract interpretation and an SMT solver to check various properties of Halo2 circuits. Using abstract interpretation, we can detect unused gates, unconstrained cells, and unused columns. Using an SMT solver, we can detect under-constrained (in the sense that for the same public input they have two efficiently computable satisfying assignments) circuits. This is the first work we are aware of that applies lightweight formal methods to PLONKish arithmetization and Halo2 circuits.
Metadata
- Available format(s)
-
PDF
- Category
- Applications
- Publication info
- Published elsewhere. Satisfiability Modulo Theories 2023 (SMT 2023)
- Keywords
- Zero-Knowledge ProofsHalo2Formal MethodsAbstract InterpretationSMT
- Contact author(s)
-
fatemeh heidari-soureshjani @ polymtl ca
mathias @ hall-andersen dk
mohammad @ quantstamp com
jeffrey @ quantstamp com
j gorzny @ gmail com
mohsen @ quantstamp com - History
- 2023-07-05: approved
- 2023-07-05: received
- See all versions
- Short URL
- https://ia.cr/2023/1051
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2023/1051,
author = {Fatemeh Heidari Soureshjani and Mathias Hall-Andersen and MohammadMahdi Jahanara and Jeffrey Kam and Jan Gorzny and Mohsen Ahmadvand},
title = {Automated Analysis of Halo2 Circuits},
howpublished = {Cryptology {ePrint} Archive, Paper 2023/1051},
year = {2023},
url = {https://eprint.iacr.org/2023/1051}
}
