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供应商与系统集成商之间由此产生的信任僵局，需要新颖的隐私保护验证技术。然而，现有的隐私保护硬件验证方法均基于模拟，无法提供形式化保证。本文提出ZK-CEC，首个用于硬件形式化验证的隐私保护框架。通过结合形式化验证与零知识证明，ZK-CEC为在不泄露设计机密性的前提下形式化验证IP正确性与安全性奠定了基础。我们观察到，现有的形式化验证零知识协议旨在证明公开公式的陈述。然而，在公式保密的隐私保护验证场景中，这些协议无法阻止恶意证明者伪造公式，从而破坏验证的可靠性。为弥补这些不足，我们首先提出了证明秘密设计相对于公开约束不可满足性的蓝图，该蓝图可广泛应用于软件、硬件及信息物理系统的属性证明。基于所提蓝图，我们构建了ZK-CEC，使证明者能在零知识条件下使验证者确信秘密IP的功能与公开规范完全一致，仅需披露证明的长度与宽度。我们实现了ZK-CEC，并在包括算术单元和密码组件在内的多种电路上评估其性能。实验结果表明，ZK-CEC能在实际时间限制内成功验证如AES S盒等实际设计。