Proving Circuit Functional Equivalence in Zero Knowledge

✨

这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

Each language version is independently generated for its own context, not a direct translation.

这篇论文提出了一种名为 ZK-CEC 的新技术，旨在解决芯片设计行业中的一个核心难题：如何在“不泄露商业机密”的前提下，证明一个芯片设计是安全且正确的。

为了让你轻松理解，我们可以把整个芯片供应链想象成一个**“神秘大厨”和“挑剔食客”**的故事。

1. 背景：信任危机与“黑盒”困境

现状：现在的芯片（比如手机里的处理器）太复杂了，就像一道超级大餐。没人能从头到尾自己种菜、养猪、做调料。所以，系统集成商（食客）会买很多“预制菜包”（第三方 IP 核，由供应商提供），拼在一起做成最终产品。
问题：
- 供应商的担忧：如果我把我的独家秘方（芯片设计图）完全给你看，你学会了怎么办？或者你转手卖给别人怎么办？（知识产权泄露风险）
- 食客的担忧：如果我不看你的秘方，我怎么知道你在菜里没下毒（硬件木马）？或者你是不是偷工减料，把“红烧肉”做成了“红烧豆腐”？（安全隐患风险）
过去的尝试：
- 模拟测试：就像食客让厨师做几道菜尝尝。但这只能尝到“运气好”遇到的情况，如果毒药只在“下雨天吃红烧肉”这种极罕见情况下才发作，模拟测试就发现不了。
- 形式化验证：这是一种数学证明，能 100% 保证逻辑正确。但以前这通常需要把设计图公开，导致供应商不敢用。

2. 核心突破：零知识证明（ZK）

这篇论文引入了零知识证明（Zero-Knowledge Proof, ZKP）。

通俗比喻：
想象有一个**“魔法隧道”**。
- 供应商（证明者）：手里拿着一份绝密的食谱（芯片设计）。
- 买家（验证者）：手里拿着一份公开的菜单要求（比如：这道菜必须包含牛肉，不能有毒）。
- 目标：供应商要证明“我的绝密食谱做出来的菜，完全符合你的菜单要求”，但他绝对不能把食谱本身给买家看。

以前的零知识证明技术，只能证明“我确实知道一个解”，但如果连“题目”（验证规则）都是秘密的，这就容易出漏洞：坏人可以随便编一个题目，然后证明“我解开了这个假题目”，从而蒙混过关。

3. 论文的创新：ZK-CEC 的“三步走”策略

作者提出了一种新的**“蓝图”，解决了上述漏洞，让验证既安全又严谨。我们可以把它比作“双重保险锁”**：

第一步：公开部分与秘密部分分离

比喻：
- 公开部分（Public）：买家提供的“菜单要求”（比如：输入是 1，输出必须是 0）。这是大家都知道的。
- 秘密部分（Secret）：供应商的“绝密食谱”（芯片内部逻辑）。这是只有供应商知道的。
- 接口（Interface）：两者连接的地方（输入输出端口）。

第二步：构建“矛盾检测器”（Miter Circuit）

比喻：
想象把“公开菜单”和“秘密食谱”强行拼在一起，看它们会不会打架。
- 如果食谱是安全的，它应该能完美满足菜单要求，两者和谐共处，没有任何矛盾。
- 如果食谱里有木马或错误，它和菜单要求就会产生逻辑冲突（比如菜单说“要牛肉”，食谱里却只有“豆腐”且无法变出牛肉）。
- 数学原理：在数学上，我们要证明这种“冲突”是不可能发生的（即“不可满足”UNSAT）。如果能证明“无论怎么尝试，都找不到一个让两者冲突的情况”，那就说明食谱是安全的。

第三步：零知识“无懈可击”的证明

作者设计了四个小协议（子步骤）来确保万无一失：

确认菜单是真的：买家先证明自己的要求是合理的。
证明食谱本身没自相矛盾：供应商证明自己的食谱逻辑是自洽的（不是乱写的）。
证明“不越界”：供应商证明他的秘密部分和公开部分，除了接口外，没有偷偷混入其他变量（防止作弊）。
核心证明（ZKUNSAT）：使用一种特殊的数学方法（基于 VOLE 技术），向买家证明：“虽然我没给你看食谱，但我能证明，我的食谱和你的菜单永远不可能产生冲突。”

关键点：在这个过程中，买家只知道“证明成功了”，除了知道这个芯片大概有多大（门电路数量）和证明有多长之外，完全无法还原出供应商的原始设计图。

4. 实际效果：快得像变魔术

实验结果：作者真的把这个系统做出来了，并测试了各种复杂的电路（比如加密芯片 AES、加法器、乘法器）。
性能：
- 对于像 AES 加密盒 这样复杂的电路，系统能在合理的时间内完成验证。
- 他们还做了一个优化（“压缩证明”），就像把一本厚厚的证明书压缩成几页摘要，让验证速度提升了 2.88 倍。
意义：这是世界上第一个能在不泄露设计细节的情况下，用数学方法100% 保证芯片逻辑正确性的框架。

5. 总结：为什么这很重要？

这就好比：

以前：要么你信任供应商（可能被骗），要么你把秘方交出来（可能被盗）。
现在（ZK-CEC）：供应商可以自信地说：“看，我用魔法证明了我的菜没问题，而且我不用给你看食谱，你也不用担心我下毒。”

这项技术为芯片供应链建立了一座**“信任桥梁”**，让全球芯片产业可以在保护知识产权的同时，彻底消除硬件木马和逻辑错误的隐患。这对于国家安全、金融安全和日常电子设备的安全都至关重要。

Each language version is independently generated for its own context, not a direct translation.

这是一份关于论文《Proving Circuit Functional Equivalence in Zero Knowledge》（零知识下电路功能等价性证明）的详细技术总结。

1. 研究背景与问题 (Problem)

背景：
现代集成电路（IC）生态系统高度依赖第三方知识产权（3PIP）集成。这种模式引入了严重的安全风险，如硬件木马（Hardware Trojans）、安全漏洞和逻辑错误。然而，IP 供应商（Prover）不愿公开其专有设计以防知识产权（IP）被盗，而系统集成商（Verifier）需要验证设计的安全性以防被欺骗。这导致了供应链中的“信任死锁”。

现有方案的局限性：

基于模拟的验证： 现有的隐私保护硬件验证方法（如使用同态加密或零知识虚拟机 zkVM 进行模拟）只能提供概率性的保证，无法覆盖所有边界情况（Corner Cases），特别是那些仅在罕见条件下触发的隐蔽硬件木马。
形式化验证的缺失： 形式化验证（如组合等价性检查 CEC）能提供数学上的完备性保证，但现有的零知识证明（ZKP）协议（如 ZKUNSAT）主要针对公开公式的不可满足性（UNSAT）证明。
核心矛盾： 如果直接将待验证的公式作为私有输入，现有的 ZKUNSAT 协议会面临健全性（Soundness）漏洞：恶意证明者可以伪造一个与原始设计无关的公式并证明其不可满足，从而欺骗验证者。

核心问题：
如何在不泄露电路设计细节的前提下，利用形式化验证（而非模拟）来证明私有 IP 电路的功能与公开规范完全等价，同时确保协议的健全性？

2. 方法论 (Methodology)

作者提出了 ZK-CEC，这是首个用于硬件形式化验证的隐私保护框架。其核心思想是将形式化验证与零知识证明相结合，并设计了一套新的协议蓝图。

2.1 核心蓝图：私有公式属性检查 (Blueprint for Secret Formula Property Checking)

为了解决 ZKUNSAT 在私有公式场景下的健全性问题，作者提出将公式划分为两部分：

私有部分 ( $\Phi_{sys}$ )：代表 IP 供应商的电路实现（秘密）。
公共部分 ( $\Phi_{prop}$ )：代表待验证的属性或规范（公开）。

验证目标： 证明私有系统模型与公共属性违规条件的合取是不可满足的（ $\Phi_{sys} \land \Phi_{prop} \models \bot$ ）。

确保健全性的三个关键检查：

属性正确性： 公共部分 $\Phi_{prop}$ 必须正确描述属性且是可满足的。
系统可满足性： 私有部分 $\Phi_{sys}$ 必须是可满足的（证明者不能提供一个自相矛盾的电路）。
变量隔离： 私有变量集与公共变量集除了定义的接口外必须互不相交。

通过零知识证明这三个条件，结合 ZKUNSAT 证明合取公式的不可满足性，从而在保持隐私的同时保证逻辑的严密性。

2.2 协议架构 ( $\Pi_{ZK-CEC}$ )

协议基于 VOLE（向量 oblivious 线性评估）构建的零知识证明后端，主要包含四个子协议：

$\Pi_{P1}$ (公共部分验证)： 验证公共规范（ $\Phi_{pub}$ ）的编码正确性，确保其符合电路规范且结构正确。
$\Pi_{P2}$ (不可满足性证明)： 基于 ZKUNSAT 的改进版。证明者提交一个归谬证明（Refutation Proof），证明 $\Phi_{miter}$ （由公共规范和私有实现构成的异或电路）是不可满足的。利用 ZK-ROM（零知识只读内存）优化证明过程。
$\Pi_{P3}$ (私有可满足性证明)： 证明私有公式 $\Phi_{sec}$ 本身是可满足的（即电路内部没有逻辑矛盾），防止证明者提交一个自相矛盾的电路来通过验证。
$\Pi_{P4}$ (变量隔离证明)： 证明私有公式中的文字（Literals）与公共公式中的文字（除接口外）没有交集，防止证明者通过共享变量“作弊”。

2.3 编码与优化

多项式编码： 将布尔子句编码为单变量多项式，利用多项式运算（如根的存在性、整除性）来验证逻辑关系。
自适应文字编码： 使用哈希函数对私有文字进行编码，防止验证者通过编码值推断文字的正负极性。
性能优化： 提出了一种**归结压缩（Resolvent Compression）**优化。将多次使用的中间归结子句合并，减少 ZK-ROM 的访问次数和置换检查开销。该优化在不显著泄露证明结构信息的前提下，显著提升了证明速度。

3. 主要贡献 (Key Contributions)

通用蓝图： 提出了一个通用的隐私保护形式化验证蓝图，通过将公式划分为私有和公共部分并施加交叉约束，解决了在零知识环境下证明私有公式属性的健全性问题。
首个 ZK-CEC 协议： 设计了首个用于组合等价性检查（CEC）的零知识协议。它允许供应商证明其私有 IP 与公开规范在功能上完全等价，提供了针对硬件木马和设计错误的形式化保证。
实现与评估： 基于 EMP-toolkit 实现了该协议，并在 37 种不同类型的电路（包括算术单元、加密组件如 AES S-Box、控制逻辑等）上进行了评估。
性能优化与泄漏分析： 提出了一种优化方案，将证明时间加快了 2.88 倍。同时进行了泄漏分析，证明优化引入的额外信息（证明树结构长度）不足以让验证者重构原始公式。

4. 实验结果 (Results)

验证对象： 包括加法器、乘法器、比较器、FSM、以及 AES/SM4/Ascon/Present 等加密组件的 S-Box。
性能表现：
- 主要瓶颈： 验证不可满足性（ $\Pi_{P1} + \Pi_{P2}$ ）占据了大部分执行时间，这与 UNSAT 是 co-NP 完全问题的性质一致。随着电路规模增大，归谬证明的长度呈指数级增长。
- 优化效果： 引入归结压缩优化后，在大规模电路（如 6x6 乘法器、AES S-Box）上实现了 1.83x 到 2.88x 的加速。
- 具体案例： 对于 AES S-Box（211 个变量，700 个子句），未优化总时间约为 4951 秒，优化后约为 1763 秒，加速比达到 2.81 倍。
可扩展性限制： 对于极大规模电路，归谬证明的爆炸式增长导致了内存溢出（OOM）和超时，这是当前框架的主要瓶颈。

5. 意义与影响 (Significance)

填补技术空白： 这是首个将形式化验证（Formal Verification）引入隐私保护硬件验证的框架。它克服了传统模拟方法无法覆盖所有边界情况的缺陷，提供了数学上的完备性保证。
解决信任死锁： 为 IP 供应商和系统集成商之间建立信任提供了新的技术路径。供应商无需公开源代码即可证明其设计无木马且符合规范，买家无需担心 IP 泄露即可获得形式化保证。
通用性潜力： 提出的“私有公式属性检查”蓝图不仅适用于硬件，还可扩展至软件验证和物理信息系统（Cyber-Physical Systems）的隐私保护验证。
推动 ZKP 发展： 解决了现有 ZKUNSAT 协议在处理私有输入时的健全性漏洞，为构建更复杂的隐私保护形式化验证工具奠定了基础。

总结：
ZK-CEC 通过创新的协议设计和多项式编码技术，成功在零知识环境下实现了电路功能等价性的形式化验证。它在保护 IP 隐私的同时，提供了比传统模拟方法更严格的安全保证，是硬件供应链安全领域的一项重要突破。