ZKSMT: A VM for Proving SMT Theorems in Zero Knowledge

Daniel Luick; John Kolesar; Timos Antonopoulos; William R. Harris; James Parker; Ruzica Piskac; Eran Tromer; Xiao Wang; Ning Luo

Paper 2023/1762

ZKSMT: A VM for Proving SMT Theorems in Zero Knowledge

Daniel Luick, Yale University

John Kolesar, Yale University

Timos Antonopoulos, Yale University

William R. Harris, Galois (United States)

James Parker, Galois (United States)

Ruzica Piskac, Yale University

Eran Tromer, Boston University

Xiao Wang, Northwestern University

Ning Luo, Northwestern University

Abstract

Verification of program safety is often reducible to proving the unsatisfiability (i.e., validity) of a formula in Satisfiability Modulo Theories (SMT): Boolean logic combined with theories that formalize arbitrary first-order fragments. Zero-knowledge (ZK) proofs allow SMT formulas to be validated without revealing the underlying formulas or their proofs to other parties, which is a crucial building block for proving the safety of proprietary programs. Recently, Luo et al. (CCS 2022) studied the simpler problem of proving the unsatisfiability of pure Boolean formulas, but it does not support safety proofs generated by SMT solvers. This work presents ZKSMT, a novel framework for proving the validity of SMT formulas in ZK. We design a virtual machine (VM) tailored to efficiently represent the verification process of SMT validity proofs in ZK. Our VM can support the vast majority of popular theories when proving program safety while being complete and sound. To demonstrate this, we instantiate the commonly used theories of equality and linear integer arithmetic in our VM with theory-specific optimizations for proving them in ZK. ZKSMT achieves high practicality even when running on realistic SMT formulas generated by Boogie, a common tool for software verification. It achieves a three-order-of-magnitude improvement compared to a baseline that executes the proof verification code in a general ZK system.

Note: We changed the contact information of one author.

Metadata

Available format(s): PDF
Category: Cryptographic protocols
Publication info: Preprint.
Keywords: Zero-knowledge proof Formal methods
Contact author(s): daniel luick @ yale edu
john kolesar @ yale edu
timos antonopoulos @ yale edu
bll hrris @ gmail com
james @ galois com
ruzica piskac @ yale edu
tromer @ bu edu
wangxiao @ northwestern edu
ning luo @ northwestern edu
History: 2023-11-28: revised; 2023-11-15: received; See all versions
Short URL: https://ia.cr/2023/1762
License: CC BY

BibTeX

@misc{cryptoeprint:2023/1762,
      author = {Daniel Luick and John Kolesar and Timos Antonopoulos and William R. Harris and James Parker and Ruzica Piskac and Eran Tromer and Xiao Wang and Ning Luo},
      title = {ZKSMT: A VM for Proving SMT Theorems in Zero Knowledge},
      howpublished = {Cryptology ePrint Archive, Paper 2023/1762},
      year = {2023},
      note = {\url{https://eprint.iacr.org/2023/1762}},
      url = {https://eprint.iacr.org/2023/1762}
}