Proving Circuit Functional Equivalence in Zero Knowledge

TL;DR

This work addresses the trust gap in third-party IP verification by introducing ZK-CEC, a privacy-preserving framework that combines formal hardware verification with zero-knowledge proofs to establish circuit functional equivalence without revealing secret designs. It develops a general blueprint for privacy-preserving property checking, partitioning formulas into secret and public parts and enforcing cross-constraints to maintain soundness. Building on this blueprint, the authors present four sub-protocols and compose them into the main protocol Pi_ZK-CEC, proving completeness, soundness, and zero-knowledge, and implement it in the EMP-toolkit with a VOLE-based ZK backend. Evaluations across diverse circuits (including AES S-Box) show practical proving times and a substantial speedup (up to 2.88x) with optimizations, while discussing leakage and fair-exchange aspects. The work offers a path toward formal guarantees in confidential hardware verification, enabling trust between IP vendors and system integrators without disclosing proprietary designs.

Abstract

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.

Figures (14)

• Figure 1: A miter circuit constructed by $C_\text{spec}$ and $C_\text{impl}$.
• Figure 2: An AND gate and its corresponding CNF formula.
• Figure 3: Functionality for ZKPs of elements in $\mathbb{F}$.
• Figure 4: Functionality for ZKPs of univariate polynomials.
• Figure 5: Functionality for clause operations in ZK.

Theorems & Definitions (3)

• Lemma 4.1
• Lemma 5.1
• Theorem 5.1