The modern integrated circuit ecosystem is increasingly reliant on third-party intellectual property integration, which introduces security risks, including hardware Trojans and security vulnerabilities. Addressing the resulting trust deadlock between IP vendors and system integrators without exposing proprietary designs requires novel privacy-preserving verification techniques. However, existing privacy-preserving hardware verification methods are all simulation-based and fail to offer formal guarantees. In this paper, we propose ZK-CEC, the first privacy-preserving framework for hardware formal verification. By combining formal verification and zero-knowledge proof (ZKP), ZK-CEC establishes a foundation for formally verifying IP correctness and security without compromising the confidentiality of the designs. We observe that existing zero-knowledge protocols for formal verification are designed to prove statements of public formulas. However, in a privacy-preserving verification context where the formula is secret, these protocols cannot prevent a malicious prover from forging the formula, thereby compromising the soundness of the verification. To address these gaps, we first propose a blueprint for proving the unsatisfiability of a secret design against a public constraint, which is widely applicable to proving properties in software, hardware, and cyber-physical systems. Based on the proposed blueprint, we construct ZK-CEC, which enables a prover to convince the verifier that a secret IP's functionality aligns perfectly with the public specification in zero knowledge, revealing only the length and width of the proof. We implement ZK-CEC and evaluate its performance across various circuits, including arithmetic units and cryptographic components. Experimental results show that ZK-CEC successfully verifies practical designs, such as the AES S-Box, within practical time limits.

翻译：现代集成电路生态系统日益依赖第三方知识产权（IP）集成，这引入了包括硬件木马和安全漏洞在内的安全风险。在无需暴露专有设计的前提下，解决IP供应商与系统集成商之间的信任僵局需要新颖的隐私保护验证技术。然而，现有隐私保护硬件验证方法均基于仿真，无法提供形式化保证。本文提出ZK-CEC，这是首个面向硬件形式化验证的隐私保护框架。通过结合形式化验证与零知识证明（ZKP），ZK-CEC为在不损害设计机密性的前提下形式化验证IP正确性与安全性奠定了基础。我们观察到，现有用于形式化验证的零知识协议旨在证明公开公式的陈述。但在公式为机密的隐私保护验证场景中，这些协议无法阻止恶意证明者伪造公式，从而破坏验证的可靠性。为填补这些空白，我们首先提出一种蓝图，用于证明秘密设计对公共约束的不可满足性，该蓝图可广泛应用于软件、硬件及信息物理系统中属性的证明。基于所提蓝图，我们构建了ZK-CEC，它使证明者能够零知识地说服验证者：秘密IP的功能与公共规范完全一致，仅泄露证据的长度与宽度。我们实现了ZK-CEC，并在包括算术单元和密码组件在内的多种电路上评估其性能。实验结果表明，ZK-CEC能在实际时间内成功验证如AES S-Box等实用设计。