Formal Verification of Zero-Knowledge Circuits

Autor:	Coglio, Alessandro, McCarthy, Eric, Smith, Eric W.
Rok vydání:	2023
Předmět:	Computer Science - Logic in Computer Science Computer Science - Cryptography and Security Computer Science - Symbolic Computation
Zdroj:	EPTCS 393, 2023, pp. 94-112
Druh dokumentu:	Working Paper
DOI:	10.4204/EPTCS.393.9
Popis:	Zero-knowledge circuits are sets of equality constraints over arithmetic expressions interpreted in a prime field; they are used to encode computations in cryptographic zero-knowledge proofs. We make the following contributions to the problem of ensuring that a circuit correctly encodes a computation: a formal framework for circuit correctness; an ACL2 library for prime fields; an ACL2 model of the existing R1CS (Rank-1 Constraint Systems) formalism to represent circuits, along with ACL2 and Axe tools to verify circuits of this form; a novel PFCS (Prime Field Constraint Systems) formalism to represent hierarchically structured circuits, along with an ACL2 model of it and ACL2 tools to verify circuits of this form in a compositional and scalable way; verification of circuits, ranging from simple to complex; and discovery of bugs and optimizations in existing zero-knowledge systems. Comment: In Proceedings ACL2-2023, arXiv:2311.08373
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2311.08858 Zobrazit plný text záznamu View this record from Arxiv