ZK-ProVer: Proving Programming Verification in Non-interactive Zero-Knowledge Proofs

Haoyu Wei

doi:10.1007/978-981-95-4213-0_12

2026-01-01

PRE

DOI：10.1007/978-981-95-4213-0_12

原文链接

原文求助

摘要

En 中文

程序验证通过形式化方法确保软件正确性，但会产生巨大的计算开销。它通常将程序执行编码为公式，并使用SAT求解器及其扩展进行验证。然而，这一过程会暴露敏感的程序细节，且在多方需要验证正确性时需要冗余计算。为克服这些限制，零知识证明（ZKPs）生成紧凑、可复用的证明，具有快速的验证时间，同时可证明地隐藏程序的内部逻辑。我们提出了一种两阶段零知识协议，在验证过程中隐藏程序实现细节。在第一阶段，采用零知识虚拟机（zkVM），该虚拟机采用HyperPlonk作为底层协议。该zkVM能够将程序编码为布尔可满足性（SAT）公式，同时严格避免披露程序的语义信息。第二阶段通过PLONKish电路对UNSAT实例的解析证明和SAT实例的满足性赋值验证电路进行编码。在Boolector基准测试上的评估表明，我们的方法在UNSAT实例上实现了与子句宽度无关的高效验证时间，在SAT实例上与公式大小无关。由此产生的ZKPs能够在提供强端到端隐私保证的同时，实现程序属性的高效验证。

Keyword:

program verification

zero-knowledge proofs

SAT

PLONKish

zkVM