Advanced Formal Verification of Zero-Knowledge Proofs: A Deep Analysis of Two ZK Vulnerabilities

撰文：CertiK

在之前的文章中，我们讨论了Zero knowledge proof的先进形式化验证：如何验证一条 ZK 指令。通过形式化验证每条 zkWasm 指令，我们能够完全验证整个 zkWasm 电路的技术Safety性和正确性。在本文中，我们将关注发现漏洞的视角，分析在审计和验证过程中发现的具体漏洞，以及从中得到的经验和教训。如要了解有关Zero knowledge proof（ZKP）Blockchain的先进形式化验证的一般讨论，请参见零知识证明Blockchain的先进形式化验证一文。

在讨论 ZK 漏洞之前，让我们先来了解 CertiK 是如何进行 ZK 形式化验证的。对于像 ZK 虚拟机（zkVM）这样的复杂系统，形式化验证（FV）的第一步是明确需要验证的内容及其性质。这需要对 ZK 系统的设计、代码实现和测试设置进行全面的审查。这个过程与常规的审计有所重合，但不同之处在于，审查后需要确立验证的目标和性质。在 CertiK，我们称其为面向验证的审计。审计和验证工作通常是一个整体。对于 zkWasm，我们对其同时进行了审计和形式化验证。

什么是 ZK 漏洞?

零知识证明系统的核心特征在于允许将离线或私密执行的计算（例如Blockchain交易）的简短加密证明传递给零知识证明验证器，并由其检查和确认，以确信该计算确已按声明的情况发生过。就此而言，ZK 漏洞将使得黑客可以提交用于证明虚假交易的伪造 ZK 证明，并让 ZK 证明检查器接受。

对于 zkVM 的证明器而言，ZK 证明过程涉及运行程序、生成每一步的执行记录，并把执行记录的数据转换成一组数字表格（该过程称为「算术化」）。这些数字之间必须满足一组约束（即「电路」），其中包括了具体表单元格之间的联系方程、固定的常数、表间的数据库查找约束，以及每对相邻表行间所需要满足的多项式方程（亦即「门」）。链上验证可以由此确认的确存在某张能满足所有约束的表，同时又保证不会看到表中的具体数字。

zkWasm 算术化表

每一个约束的准确性都至关重要。任何约束中的一个错误，无论是偏弱或是缺失，都可能使得黑客能够提交一个误导性的证明，这些表格看似代表了智能contract的一次有效运行，但实际并非如此。与传统 VM 相比，zkVM 交易的不透明性放大了这些漏洞。在非 ZK 链中，交易的计算细节是公开记录在区块之上的；而 zkVM 则不将这些细节存储于链上。透明度的缺失使得攻击的具体情况很难被确定，甚至连攻击是否已发生都很难确定。

执行 zkVM 指令规则的 ZK 电路极其复杂。对于 zkWasm 来说，其 ZK 电路的实现涉及超过 6,000 行的 Rust 代码和数百个约束。这种复杂性通常意味着可能存在多个漏洞正等待着被发现。

zkWasm 电路架构

的确，我们通过对于 zkWasm 审计和形式化验证发现了多个这样的漏洞。下面，我们将讨论两个具有代表性的例子，并讨论它们之间的差异。

代码漏洞：Load8 数据注入攻击

第一个漏洞涉及 zkWasm 的 Load8 指令。在 zkWasm 中，堆内存的读取是通过一组 LoadN 指令来完成的，其中 N 是要加载的数据的Xiaobai Navigation大小。例如，Load64 应该从 zkWasm 内存地址读出 64 位的数据。Load8 应该从内存中读出 8 位的数据（即一个字节），并用 0 前缀填充以创建一个 64 位的值。zkWasm 内部将内存表示为 64 位字节的数组，因此其需要「选取」内存数组的一部分。为此使用了四个中间变量（u16_cells），这些变量合起来构成了完整的 64 位加载值。

这些 LoadN 指令的约束定义如下：

这个约束分为 Load32、Load16 和 Load8 这三种情况。Load64 没有任何约束，因为内存单元正好就是 64 位的。对于 Load32 的情况，代码确保了内存单元中的高 4 个字节（32 位）必须为零。

对于 Load16 的情况，内存单元中的高 6 个字节（48 位）必须为零。

对于 Load8 的情况，应该要求内存单元中的高 7 个字节（56 位）为零。遗憾的是，在代码中并非如此。

正如你所见，只有高 9 至 16 位被限制为零。其他的高 48 位可以是任意值，却仍然可以伪装成「从内存中读取的」。

通过利用这个漏洞，黑客可以篡改一个合法执行序列的 ZK 证明，使得 Load8 指令的运行加载这些意外的字节，从而导致数据损坏。并且，通过精心安排周边的代码和数据，可能会触发虚假的运行和转账，从而steal取数据和资产。这种伪造的交易可以通过 zkWasm 检查器的检查，并被区块链错误地认定为真实交易。

修复这个漏洞实际上相当简单。

该漏洞代表了一类被称为「代码漏洞」的 ZK 漏洞，因为它们源于代码的编写，并可以通过较小的局部代码修改来轻松修复。正如你可能会同意的那样，这些漏洞也相对更容易被人看出来。

设计漏洞：伪造返回攻击

让我们来看看另一个漏洞，这次是关于 zkWasm 的调用和返回。调用和返回是基本的 VM 指令，它们允许一个运行的上下文（例如函数）去调用另一个，并在被调用者完成其执行后，恢复调用者上下文的执行。每次调用都预期稍后会返回一次。zkWasm 在调用和返回的生命周期中所追踪的动态数据被称为「调用帧（call frame）」。由于 zkWasm 按顺序执行指令，所有调用帧可以根据其在运行过程中的发生时间进行排序。下面是一个在 zkWasm 上运行的调用 / 返回代码示例。

用户可以调用 buy_token() 函数来购买Token（可能是通过支付或转移其他有价值的东西）。它的核心步骤之一是通过调用 add_token() 函数，实际将Token账户余额增加 1。由于 ZK 证明器本身并不支持调用帧数据结构，因此需要使用执行表（E-Table）和跳转表（J-Table）来记录和追踪这些调用帧的完整历史记录。

上图说明了 buy_token() 调用 add_token() 的运行过程，以及从 add_token() 返回到 buy_token() 的过程。可以看到，Token账户余额增加了 1。在执行表中，每个运行步骤占一行，其中包括当前执行中的调用帧编号、当前上下文函数名称（仅用于此处的说明）、该函数内当前运行指令的编号，以及表中所存的当前指令（仅用于此处的说明）。在跳转表中，每个调用帧占一行，表中存有其调用者帧的编号、调用者函数上下文名称（仅用于此处的说明）、调用者帧的下一条指令位置（以便该帧可以返回）。在这两个表中，都有一个 jops 列，它追踪当前指令是否为调用 / 返回（在执行表）以及该帧（在跳转表）发生的调用 / 返回指令总数。

正如人们所预期的，每次调用都应该有一次相应的返回，并且每一帧应该只有一次调用和一次返回。如上图所示，跳转表中第 1 帧的 jops 值为 2，与执行表中的第 1 行和第 3 行相对应，那里的 jops 值为 1。目前看起来一切正常。

但实际上这里有一个问题：尽管一次调用和一次返回将使帧的 jops 计数为 2，但两次调用或者两次返回也会使计数为 2。每帧有两次调用或两次返回听起来可能很荒谬，但要牢记的是，这正是黑客试图通过打破预期要做的事情。

你现在可能有点兴奋了，但我们真的找到问题了吗？

结果表明，两次调用并不是问题，因为执行表和调用表的约束使得两个调用无法被编码到同一帧的行中，因为每次调用都会产生一个新的帧编号，即当前调用帧编号加 1。

而两次返回的情况就没那么幸运了：由于在返回时不会创建新的帧，黑客确实有可能获取合法运行序列的执行表和调用表，并注入伪造的返回（以及相应的帧）。例如，先前执行表和调用表中 buy_token() 调用 add_token() 的例子可以被黑客篡改为以下情况：

黑客在执行表中原来的调用和返回之间注入了两次伪造的返回，并在调用表中增加了一个新的伪造的帧行（原来的返回和后续指令的运行步骤编号在执行表中则需要加 4）。由于调用表中每一行的 jops 计数均为 2，因此满足了约束条件，zkWasm 证明检查器将接受这个伪造的执行序列的「证明」。从图中可以看出，代币账户余额增加了 3 次而不是 1 次。因此，黑客能够以支付 1 个代币的价格获得 3 个代币。

解决这个问题有多种方法。一个明显的方法就是分别单独追踪调用和返回，并确保每一帧恰好有一次调用和一次返回。

你可能已经注意到，到目前为止我们尚未展示这个漏洞的哪怕一行代码。主流的原因是没有任何一行代码是有问题的，代码实现完全符合表格和约束设计。问题在于设计本身，而修复方法也是如此。

你可能认为，这个漏洞应该是显而易见的，但实际上并非如此。这是因为「两次调用或两次返回也会导致 jops 计数为 2」与「实际上两次返回是可能的」之间存在空白。后者需要对执行表和调用表中相关的各种约束进行详细、完整地分析，很难进行完整的非形式化推理。

两个漏洞的比较

对于「Load8 数据注入漏洞」和「伪造返回漏洞」，它们都可能导致黑客能够操纵 ZK 证明、创建虚假交易、骗过证明检查器，并进行窃取或劫持。 但他们的性质和被发现的方式却截然不同。

「Load8 数据注入漏洞」是在对 zkWasm 进行审计时发现的。这绝非易事，因为我们必须审查超过 6,000 行的 Rust 代码和上百条 zkWasm 指令的数百个约束。尽管如此，这个漏洞还是相对容易发现和确认的。由于这个漏洞在形式化验证开始之前就已被修复，所以在验证过程中并未遇到它。如果在审计过程中未发现该漏洞，我们可以预期在对 Load8 指令的验证中会发现它。

「伪造返回漏洞」是在审计之后的形式化验证中发现的。我们在审计中未能发现它的部分原因在于，zkWasm 中有一个同 jops 非常相似的机制叫做「mops」，其在 zkWasm 运行期间追踪每个内存单元历史数据对应的内存访问指令。mops 的计数约束确实是正确的，因为其只追踪了一种类型的内存指令，即内存写入；而且每个内存单元的历史数据都是不可变的，并只会写入一次（mops 计数为 1）。但即使我们在审计期间注意到了这个潜在的漏洞，如果不对所有的相关约束进行严格的形式化推理，我们将仍然无法轻易地确认或排除每一种可能情况，因为实际上没有任何一行代码是错误的。

总结来说，这两种漏洞分别属于「代码漏洞」和「设计漏洞」。代码漏洞相对较为浅显，更容易被发现（错误代码），并且更容易推理和确认；设计漏洞可能非常隐蔽，更难以发现（没有「错误」代码），更难以推理和确认。

发现 ZK 漏洞的最佳实践

根据我们在审计和形式化验证 zkVM 以及其他 ZK 及非 ZK 链的经验，下面是关于如何最好地保护 ZK 系统的一些建议。

检查代码以及设计

如前所述，ZK 的代码和设计中都可能存在漏洞。这两种类型的漏洞都可能导致 ZK 系统受到破坏，因此必须在系统投入运行之前消除它们。与非 ZK 系统相比，ZK 系统的一个问题是，任何攻击都更难揭露和分析，因为其计算细节没有公开或保留在链上。因此人们可能知道发生了黑客攻击，但却无法知道技术层面上是如何发生的。这使得任何 ZK 漏洞的成本都非常高。相应地，预先确保 ZK 系统Safety性的价值也非常高。

进行审计以及形式化验证

我们在这里介绍的两个漏洞分别是通过审计和形式化验证发现的。有人可能会认为，使用了形式化验证就不需要审计了，因为所有的漏洞都会被形式化验证发现。实际上我们的建议是两者都要进行。正如本文开头所解释的，一个高质量的形式化验证工作始于对代码和设计的彻底审查、检查和非正式推理；而这项工作本身就与审计重叠。此外，在审计期间发现并排除更简单的漏洞，将使形式化验证变得更加简单和高效。

如果要对一个 ZK 系统既进行审计又进行形式化验证，那么最佳时机是同时进行这两项工作，以便审计师和形式化验证工程师能够高效地协作（有可能会发现更多的漏洞，因为形式化验证的对象和目标需要高质量的审计输入）。

如果你的 ZK 项目已经进行了审计（赞）或多次审计（大赞），我们的建议是在此前审计结果的基础上对电路进行形式化验证。我们在 zkVM 以及其他 ZK 和非 ZK 项目的审计和形式化验证的经验一再表明，验证常常能捕捉到审计中遗漏而不易发现的漏洞。由于 ZKP 的特性，虽然 ZK 系统应该提供比非 ZK 解决方案更好的区块链Safety性和可扩展性，但其自身的Safety性和正确性的关键程度要远高于传统的非 ZK 系统。因此，对 ZK 系统进行高质量形式化验证的价值也远高于非 ZK 系统。

确保电路以及智能contract的安全

ZK 应用通常包含电路和智能合约两个部分。对于基于 zkVM 的应用，有通用的 zkVM 电路和智能合约应用。对于非基于 zkVM 的应用，有应用特定的 ZK 电路及相应部署在 L1 链或桥的另一端的智能合约。基于 zkVM 非基于 zkVM

我们对 zkWasm 的审计和形式验证工作只涉及了 zkWasm 电路。从 ZK 应用的整体安全性角度来看，对其智能合约进行审计和形式化验证也非常重要。毕竟，在为了确保电路安全方面投入了大量精力之后，如果在智能合约方面放松警惕，导致应用最终受到损害，那将是非常遗憾的。

有两种类型的智能合约值得特别关注。第一种是直接处理 ZK 证明的智能合约。尽管它们的规模可能不是很大，但它们的风险非常高。第二种是运行在 zkVM 之上的大中型智能合约。我们知道，它们有时会非常复杂，而其中最有价值的应该进行审计和验证，特别是因为人们无法在链上看到它们的执行细节。幸运的是，经过多年的发展，智能合约的形式化验证现在已经可以实用，并且为合适的高价值目标做好了准备。

让我们通过以下的说明来总结形式化验证（FV）对 ZK 系统及其组件的影响。

• FV 电路 + 非 FV 智能合约 = 非 FV 零知识证明

• 非 FV 电路 + FV 智能合约 = 非 FV 零知识证明

• FV 电路 + FV 智能合约 = FV 零知识证明

The article comes from the Internet:Advanced Formal Verification of Zero-Knowledge Proofs: A Deep Analysis of Two ZK Vulnerabilities

相关推荐: 了解 Mezo：Pantera 和 Multicoin 参投，构建比特币 L2 的经济层

Mezo所想构建的比特币L2不仅仅是是技术层面的关联，更多是经济层面的关联，即构建比特币的经济层。 撰文：Frost、Luccy 4 月 9 日，比特币二层网络 Mezo 完成 2100 万美元 A 轮融资，由 Pantera Capital 领投，Multi…