Automated Analysis of Halo2 Circuits

TY - GEN

T1 - Automated Analysis of Halo2 Circuits

AU - Soureshjani, Fatemeh Heidari

AU - Hall-Andersen, Mathias

AU - Jahanara, MohammadMahdi

AU - Kam, Jeffrey

AU - Gorzny, Jan

AU - Ahmadvand, Mohsen

PY - 2023

Y1 - 2023

N2 - 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 circuits (in the sense that for the same public input they have two efficiently computable satisfying assignments). This is the first work we are aware of that applies lightweight formal methods to PLONKish arithmetization and Halo2 circuits.

AB - 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 circuits (in the sense that for the same public input they have two efficiently computable satisfying assignments). This is the first work we are aware of that applies lightweight formal methods to PLONKish arithmetization and Halo2 circuits.

KW - Abstract Interpretation

KW - Formal Methods

KW - Halo2

KW - SMT

KW - Zero-Knowledge Proof Systems

UR - https://www.scopus.com/pages/publications/85166017565

M3 - Article in proceedings

VL - 3429

SP - 3

EP - 17

BT - Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), Rome, Italy, July, 5-6, 2023

A2 - Graham-Lengrand, Stéphane

A2 - Preiner, Mathias

PB - CEUR-WS.org

ER -