Proving Circuit Functional Equivalence in Zero Knowledge

This paper introduces ZK-CEC, the first privacy-preserving framework that combines formal verification and zero-knowledge proofs to mathematically guarantee the functional equivalence of secret hardware designs against public specifications without revealing the underlying proprietary IP.

The Gist

Imagine you are a famous chef (the IP Vendor) who has invented a secret, world-changing recipe for a new type of pizza. You want to sell this recipe to a massive restaurant chain (the System Integrator).

However, there's a problem:

1. The Chef's Fear: If you show the restaurant the full recipe, they might steal it, copy it, and sell it themselves.
2. The Restaurant's Fear: If they just take your word for it, you might be selling them a fake recipe that looks good on paper but actually contains a "Trojan horse"—maybe a hidden ingredient that makes the pizza taste terrible only on Tuesdays, or a secret switch that lets you remotely control the oven.

They are stuck in a trust deadlock. They need to know the recipe works perfectly without seeing the secret ingredients.

The Old Way: The "Taste Test" (Simulation)

Previously, to solve this, the restaurant would ask the chef to bake a few pizzas using random ingredients (test cases). If the pizzas tasted good, the restaurant assumed the recipe was safe.

• The Flaw: This is like testing a bridge by driving one car over it. It doesn't prove the bridge won't collapse if a truck drives over it, or if it rains, or if an earthquake happens. A clever bad actor could hide a flaw that only triggers under very specific, rare conditions.

The New Way: The "Magic Black Box" (ZK-CEC)

This paper introduces ZK-CEC, a new method that acts like a magic black box. It allows the chef to prove, mathematically and with 100% certainty, that their secret recipe produces the exact same result as the restaurant's public standard recipe, without ever revealing a single ingredient.

Here is how it works, broken down into simple steps:

1. The "Miter" Machine (The Comparison Engine)

Imagine building a machine that takes the Chef's secret recipe and the Restaurant's public recipe and tries to find any scenario where they produce different pizzas.

• If the machine finds a difference, it rings a bell (the circuit is "Satisfiable" or broken).
• If the machine tries every possible combination of ingredients and temperatures and cannot find a single difference, it proves the two recipes are identical (the circuit is "Unsatisfiable").

2. The Problem with Magic

Usually, to prove the machine found no differences, you have to show your work (the math). But if you show the work, you reveal the secret recipe.

• The Trap: If the chef just says, "Trust me, I ran the math," a dishonest chef could lie and say, "I ran the math on a fake recipe that I made up to look perfect," and the restaurant would have no way to know.

3. The Solution: The "Blueprint"

The authors created a General Blueprint to fix this. They split the problem into two parts:

• The Public Part: The restaurant's standard recipe (which everyone can see).
• The Secret Part: The chef's secret recipe (which is hidden).

The magic trick is to prove three things simultaneously without revealing the secret:

1. The Public Recipe is Real: The restaurant confirms the standard recipe is valid.
2. The Secret Recipe Exists: The chef proves they actually have a valid recipe (it's not a contradiction like "add salt and don't add salt").
3. They Don't Mix: The chef proves that the only place the two recipes touch is at the "entrance" (ingredients) and "exit" (finished pizza). The secret internal steps of the chef's recipe never leak into the public recipe.

Once these three locks are secured, the system runs the "Miter Machine." If the machine proves it's impossible to find a difference between the two, the restaurant knows the secret recipe is perfect, but they still don't know what the secret ingredients are.

The "Speed Up" Trick

Proving this mathematically is like trying to solve a massive maze. Sometimes the maze is so big that the proof takes forever to write down.

• The Optimization: The authors realized that in many mazes, you only need to check the "turning points" (key junctions) rather than every single step. They found a way to compress the proof, skipping redundant steps.
• The Result: This made the process up to 2.88 times faster, making it practical for real-world use (like verifying the complex math inside an AES encryption chip).

Why This Matters

This isn't just about pizza. It's about the entire hardware supply chain.

• Smartphones, Cars, Power Grids: All rely on chips made by different companies.
• The Benefit: Chip designers can now sell their "black box" designs to buyers with mathematical guarantees that there are no hidden backdoors or bugs, without fear of their intellectual property being stolen.

In a nutshell: ZK-CEC is a trust machine. It lets you prove your secret is safe and correct by showing you can't find a single flaw, all while keeping your secret ingredients locked in a vault that only the math can open.

Technical Summary

1. Problem Statement

The modern integrated circuit (IC) supply chain relies heavily on third-party intellectual property (3PIP). This creates a "trust deadlock":

• IP Vendors fear that revealing their designs to buyers for verification will lead to IP piracy.
• System Integrators (Buyers) fear that hidden malicious logic (e.g., hardware Trojans, backdoors, or logic bugs) exists in the IP, which simulation-based verification often fails to detect due to the inability to cover all corner cases.

The Core Challenge: How to formally verify that a secret circuit implementation ($C_{impl}$) is functionally equivalent to a public specification ($C_{spec}$) without revealing the internal structure of $C_{impl}$, while ensuring the verification is mathematically exhaustive (formal) rather than probabilistic (simulation).

Limitations of Existing Solutions:

• Simulation-based ZK (e.g., zkVMs): These rely on test vectors and cannot guarantee the absence of malicious logic in untested scenarios.
• Existing Formal ZK (e.g., ZKUNSAT): These protocols are designed to prove the unsatisfiability (UNSAT) of a public formula. If applied directly to a secret formula, a malicious prover could forge a proof for a different, fake formula, breaking the soundness of the verification.

2. Methodology: ZK-CEC Framework

The authors propose ZK-CEC, the first privacy-preserving framework for hardware formal verification. It combines Combinational Equivalence Checking (CEC) with Zero-Knowledge Proofs (ZKP) based on Vector Oblivious Linear Evaluation (VOLE).

A. The Core Insight: A New Blueprint

The authors identify that ZKUNSAT fails for secret formulas because the verifier cannot ensure the secret formula matches the intended system. They propose a General Blueprint for secret formula property checking:

1. Partitioning: Split the verification problem into a Secret System ($\Phi_{sys}$) and a Public Property ($\Phi_{prop}$).
2. Goal: Prove that $\Phi_{sys} \land \Phi_{prop}$ is Unsatisfiable (UNSAT).
3. Soundness Guarantees: To prevent forgery, the protocol enforces four constraints:
   • P1 (Public Correctness): The public property must be correctly formed and satisfiable.
   • P2 (Global UNSAT): The conjunction of the secret and public parts is UNSAT.
   • P3 (Secret Satisfiability): The secret system itself must be satisfiable (it is not internally contradictory).
   • P4 (Variable Isolation): The secret system and public property only interact through defined interface variables; they do not share internal secret variables.

B. Technical Implementation

The protocol ($\Pi_{ZK-CEC}$) is constructed using four sub-protocols based on VOLE-based ZK commitments:

1. Encoding Scheme:

   • Boolean clauses are encoded as univariate polynomials over a finite field $\mathbb{F}$.
   • Literals are mapped to field elements. Public literals use direct indexing; secret literals use a keyed hash function ($H_k$) to hide polarity and prevent the verifier from inferring the literal's value.
   • Clauses are represented as polynomials where roots correspond to literals.

2. Sub-Protocol $\Pi_{P1}$ (Public Verification):

   • The verifier reconstructs the public specification and miter circuit logic.
   • The prover opens commitments to prove the public clauses match the specification.

3. Sub-Protocol $\Pi_{P2}$ (UNSAT Proof):

   • Adapts the ZKUNSAT protocol to prove the miter circuit (representing $C_{impl} \neq C_{spec}$) is UNSAT.
   • Uses a ROM (Read-Only Memory) functionality to verify a sequence of resolution steps (a refutation proof) without revealing the intermediate clauses.
   • The prover commits to the refutation proof steps, and the verifier checks the logical consistency of the resolution chain ending in the empty clause ($\bot$).

4. Sub-Protocol $\Pi_{P3}$ (Secret Satisfiability):

   • The prover proves that the secret formula $\Phi_{sec}$ is satisfiable by providing a satisfying assignment.
   • Uses polynomial evaluation to show that for every clause in the secret formula, at least one literal in the assignment evaluates to true (making the clause true).

5. Sub-Protocol $\Pi_{P4}$ (Variable Isolation):

   • Proves that the secret formula does not contain any literals from the public set (except the interface).
   • Uses a "non-zero proof" technique: The prover commits to the inverse of the polynomial evaluation of a public literal against a secret clause. If the result is 1, the evaluation was non-zero, proving the literal is not in the clause.

C. Optimization

The authors introduce a Resolvent Compression optimization. Instead of storing every intermediate step of the resolution proof in the ROM, they store only "learned clauses" (sub-trees). This reduces the number of permutation checks required, significantly speeding up the protocol while maintaining security (the verifier cannot reconstruct the full formula from the compressed structure due to factorial complexity).

3. Key Contributions

1. First Privacy-Preserving Formal Hardware Verification: ZK-CEC is the first framework to provide formal guarantees (exhaustive verification) for hardware equivalence without revealing the design.
2. General Blueprint for Secret Formulas: They resolve the soundness gap in existing ZKUNSAT protocols by introducing a method to verify secret formulas against public constraints, applicable to software and cyber-physical systems.
3. Protocol Design: A complete protocol ($\Pi_{ZK-CEC}$) composed of four sub-protocols that satisfy completeness, soundness, and zero-knowledge properties.
4. Practical Implementation & Optimization: Implementation using the EMP-toolkit and VOLE, with a compression optimization that yields up to 2.88x speedup.

4. Experimental Results

The authors evaluated ZK-CEC on 37 combinational circuits, including arithmetic units (adders, multipliers), control logic, and cryptographic components (AES, SM4, Ascon S-Boxes).

• Performance:
  • Verification of practical designs (e.g., AES S-Box) is feasible within reasonable time limits (e.g., ~4.9 seconds for AES S-Box).
  • The UNSAT proof ($\Pi_{P1} + \Pi_{P2}$) is the dominant bottleneck, scaling with the size of the refutation proof (which can grow exponentially).
  • The SAT proof ($\Pi_{P3}$) and Isolation proof ($\Pi_{P4}$) scale linearly with circuit size and are negligible in cost compared to UNSAT.
• Optimization Impact:
  • The resolvent compression optimization reduced total proving time significantly.
  • Speedup ranged from 1.16x to 2.88x, with higher gains observed in larger, more complex circuits.
• Scalability: The framework is currently limited by the memory required to store large refutation proofs for very complex circuits (out-of-memory errors occurred for the largest benchmarks), but it successfully handles practical industrial-scale components.

5. Significance

• Trust in Supply Chains: ZK-CEC enables a "fair exchange" model where IP vendors can prove their designs are Trojan-free and functionally correct without exposing their IP, solving a critical bottleneck in the semiconductor industry.
• Beyond Simulation: It moves hardware verification from probabilistic simulation (which misses rare bugs/Trojans) to mathematical formal verification, providing absolute guarantees.
• Foundational Work: The proposed blueprint for "Secret Formula Property Checking" provides a theoretical foundation for applying formal methods to any system where the logic is private but the requirements are public, extending beyond hardware to software and AI model verification.