ZKSMT: A VM for Proving SMT Theorems in Zero Knowledge
发表信息
作者
- Daniel Luick
- John C. Kolesar
- Timos Antonopoulos
- William R. Harris
- James Parker
- Ruzica Piskac
- Eran Tromer
- Xiao Wang
- Ning Luo
笔记
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 does not support 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.
程序安全性验证通常可以简化为证明可满足性模理论(Satisfiability Modulo Theories, SMT)中公式的不可满足性(即有效性)：这种理论将布尔逻辑与形式化任意一阶片段的理论相结合。零知识(Zero-knowledge, ZK)证明允许在不向其他方透露底层公式或其证明的情况下验证SMT公式，这是证明专有程序安全性的关键构建模块。最近，Luo等人(CCS 2022)研究了证明纯布尔公式不可满足性这一较简单的问题，但不支持由SMT求解器生成的证明。本文提出了ZKSMT，这是一个在零知识环境下证明SMT公式有效性的新型框架。我们设计了一个虚拟机(Virtual Machine, VM)，专门用于在零知识环境中高效表示SMT有效性证明的验证过程。我们的虚拟机在证明程序安全性时可以支持绝大多数流行的理论，同时保持完备性和可靠性。为了证明这一点，我们在虚拟机中实例化了常用的相等性理论和线性整数算术理论，并针对在零知识环境中证明这些理论进行了理论特定的优化。即使在处理由软件验证常用工具Boogie生成的实际SMT公式时，ZKSMT也能实现高度的实用性。与在通用零知识系统中执行证明验证代码的基准相比，它实现了三个数量级的性能提升。