一句话：提出首个零知识框架 ZSafe，在不泄露专有硬件设计的情况下向验证者证明其形式安全性。
第三方硬件验证要求不可信验证者审查专有设计，但现有混淆、水印、设计加密及隐私保护验证方法或不适配、或依赖可信第三方、或缺乏可扩展的形式保证。ZSafe 是首个为专有硬件设计提供形式安全保证的零知识框架。它引入硬件设计编码方案与 ZK 友好约束系统，将设计及其公式表示绑定；提出高效 ZKP 协议验证逻辑蕴含，通过概率检查避免公式翻译的过高开销；并设计共享结构不可满足性证明协议，高效处理相互关联的验证检查。作者实现 ZSafe，在 69 个改编自 HWMCC'24 的硬件验证基准上评估，设计规模最高达 30 万门，90% 实例可在一小时内完成证明，展示了实际可扩展性。
Protecting the confidentiality of hardware designs is essential, especially during third-party verification, where proprietary designs must be examined by potentially untrusted verifiers. Existing approaches, such as obfuscation, watermarking, design encryption, and prior privacy-preserving verification techniques, are either not applicable, rely on trusted third parties, or lack scalable formal guarantees. We present ZSafe, the first zero-knowledge (ZK) framework to provide formal safety guarantees for proprietary hardware designs. ZSafe enables a designer to prove the safety of confidential hardware to a verifier without revealing the design. Our approach introduces (i) an encoding scheme for hardware design, and a ZK-friendly constraint system that binds hardware design and its formula representation, (ii) an efficient ZKP protocol for validating logical implication, avoiding the prohibitive overhead of formula translation by using probabilistic checking, and (iii) a shared-structure unsatisfiability proof protocol to handle interrelated verification checks efficiently. We implement ZSafe and evaluate it on 69 adapted HWMCC’24 hardware verification benchmarks with up to 300,000 gates. The results demonstrate practical scalability: 90% of instances are proven within an hour.
@article{paperbot12086,
title = {ZSafe: Proving the Safety of Proprietary Hardware Designs in Zero Knowledge},
author = {Zhaoxiang Liu and James Parker and Ning Luo},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839517}
}