在之前的文章中，我们深入探讨了零知识证明的高级形式化验证方法，特别是如何验证单条ZK指令的技术细节。通过逐条验证zkWasm指令，我们能够全面确保整个zkWasm电路的技术安全性和正确性。本文将转换视角，重点分析在审计和验证过程中发现的具体漏洞案例，并分享从中获得的宝贵经验。如需了解零知识证明（ZKP）区块链形式化验证的总体讨论，可以参考我们此前发布的《零知识证明区块链的先进形式化验证》一文。
在深入探讨ZK漏洞之前，有必要先了解CertiK进行ZK形式化验证的方法论。面对像ZK虚拟机（zkVM）这样复杂的系统，形式化验证的第一步是明确验证对象及其特性。这需要对ZK系统的整体设计、代码实现和测试环境进行全面审查。虽然这个过程与常规审计有所重叠，但其独特之处在于需要在此基础上确立具体的验证目标和特性。在CertiK，我们将这种方法称为”面向验证的审计”。对于zkWasm项目，我们采取了审计与形式化验证并行的策略，确保全方位的安全保障。
深入理解ZK漏洞
零知识证明系统的核心价值在于，它允许将离线或私密执行的计算（如区块链交易）生成简短的加密证明，并由验证器进行确认，而无需透露具体计算内容。在这个机制中，ZK漏洞可能导致严重后果——攻击者可以伪造证明来验证虚假交易，而验证器却无法识别。
在zkVM的证明生成过程中，程序执行会产生详细的执行记录，这些记录随后被转换为数字表格（称为”算术化”过程）。这些数字必须满足一系列严格的约束条件（即”电路”），包括表单元格间的关联方程、固定常数、表间查找约束，以及相邻表行间的多项式方程（即”门”）。链上验证通过确认这些约束的满足来保证表格的有效性，同时确保具体数值的隐私性。
zkWasm算术化表示例
每一个约束条件的准确性都至关重要。任何约束中的缺陷，无论是强度不足还是完全缺失，都可能为攻击者打开后门，使他们能够提交看似合法实则虚假的执行证明。与传统的虚拟机相比，zkVM交易的不透明性进一步放大了这些漏洞的风险。在非ZK链上，交易计算细节公开可见；而zkVM则将这些细节隐藏在链下，这使得识别攻击行为变得异常困难，有时甚至无法判断攻击是否已经发生。
实现zkVM指令规则的ZK电路极其复杂。以zkWasm为例，其电路实现涉及超过6,000行Rust代码和数百个约束条件。这种复杂性往往意味着系统中可能存在多个潜在漏洞点。在我们的审计和形式化验证过程中，确实发现了多个此类漏洞。接下来，我们将重点分析两个具有代表性的案例，探讨它们的差异和启示。
代码层面的漏洞：Load8数据注入攻击
第一个漏洞出现在zkWasm的Load8指令实现中。zkWasm通过一组LoadN指令来处理堆内存读取操作，其中N表示要加载的数据大小。例如，Load64指令负责从内存地址读取64位数据，而Load8指令则应读取8位数据（1个字节）并用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指令加载非预期的字节，导致数据损坏。通过精心构造周边代码和数据，甚至可能触发虚假交易，窃取数据和资产。这种伪造的交易能够通过zkWasm检查器的验证，被区块链误认为是合法交易。
修复这个漏洞的方案相对简单直接：
这类漏洞属于”代码漏洞”，源于具体的代码实现问题，通常可以通过局部代码修改来修复。正如案例所示，这类漏洞相对容易被识别和确认。
设计层面的漏洞：伪造返回攻击
第二个漏洞涉及zkWasm的调用和返回机制。作为虚拟机的基本指令，调用和返回允许执行上下文（如函数）相互调用并在完成后恢复执行。每次调用都应有对应的返回，zkWasm通过”调用帧”来追踪这些动态数据。由于指令按顺序执行，所有调用帧可以根据时间顺序排列。以下是zkWasm中调用/返回的示例：
在这个示例中，buy_token()函数通过调用add_token()来实现代币账户余额的增加。由于ZK证明器本身不支持调用帧数据结构，需要使用执行表（E-Table）和跳转表（J-Table）来记录完整的调用历史：
图中展示了buy_token()调用add_token()并返回的完整过程。执行表中每行代表一个执行步骤，包含当前调用帧编号、函数名、指令位置等信息；跳转表中每行代表一个调用帧，记录调用者信息等关键数据。两表都包含jops列，用于追踪调用/返回指令的数量。
表面上看，每次调用对应一次返回，每帧应该只有一次调用和一次返回。但问题在于：虽然一次调用加一次返回会使jops计数为2，但两次调用或两次返回同样会产生这个结果。虽然两次调用由于会生成新帧编号而难以实现，但两次返回却可能被攻击者利用。
攻击者可以在合法执行序列中注入伪造的返回指令：
如图所示，攻击者在原有调用和返回之间插入了两次伪造返回，并在跳转表中添加了新的伪造帧行。由于每行的jops计数仍为2，约束条件得到满足，zkWasm验证器会接受这个伪造的执行证明。结果导致代币账户余额增加了3次而非预期的1次，使攻击者能够以支付1个代币的代价获取3个代币。
这个漏洞的特殊之处在于，没有任何一行代码存在错误——代码完全按照设计要求实现。问题出在设计本身，因此解决方案也需要从设计层面着手，例如分别追踪调用和返回次数，确保每帧恰好各有一次。
两类漏洞的对比分析
“Load8数据注入”和”伪造返回”这两个漏洞虽然都能导致相似的安全后果，但它们的性质和发现过程却截然不同。前者是在审计过程中发现的代码级漏洞，虽然需要审查大量代码，但相对容易被识别；后者则是在形式化验证阶段发现的设计级漏洞，需要对整个约束系统进行全面分析才能确认。
这个对比凸显了ZK系统安全评估的复杂性——既需要关注代码实现细节，也需要审视整体设计方案。这也解释了为什么对ZK系统而言，审计和形式化验证都是不可或缺的安全措施。
ZK系统安全最佳实践
基于对zkVM及其他ZK/非ZK链的审计和验证经验，我们总结出以下保护ZK系统的关键建议：
全面审查代码与设计
ZK系统中，代码和设计层面的漏洞都可能造成严重后果。由于ZK系统的不透明性，攻击行为往往难以追溯和分析，这使得预防性安全措施显得尤为重要。在系统上线前彻底消除各类漏洞，对ZK系统而言具有极高的安全价值。
结合审计与形式化验证
我们的案例表明，不同类型的漏洞可能需要不同的发现方法。虽然形式化验证能够发现许多深层问题，但审计在识别明显漏洞方面效率更高。理想情况下，两项工作应该协同进行，使审计师和验证工程师能够优势互补，提高漏洞发现效率。
确保电路与智能合约的双重安全
ZK应用通常包含电路和智能合约两部分。虽然我们对zkWasm的验证主要关注电路部分，但智能合约的安全同样重要。特别是直接处理ZK证明的合约和运行在zkVM上的复杂合约，都应该接受严格的安全审查和验证。
通过以下图示，我们可以更直观地理解形式化验证对ZK系统各组件的影响：
声明：文章不代表CHAINTT观点及立场，不构成本平台任何投资建议。投资决策需建立在独立思考之上，本文内容仅供参考，风险 自担！转载请注明出处：https://www.chaintt.cn/14165.html