Paper 2023/1051 Original: eprint.iacr.org/2023/1051 ↗
Automated Analysis of Halo2 Circuits
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
- Preprint.
- History
- 2023-07-05: last updated
- 2023-07-05: published
- Short URL
- https://ia.cr/2023/1051
- License
- https://creativecommons.org/licenses/by/4.0/
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}
}