Zisk二进制文件和主审查

总结 类型： zkVM/电路 时间线： 从 2025-10-13 → 2025-11-14

语言： PIL2

发现

问题总数：13 (0 已解决)

严重：1 (0 已解决) · 高：2 (0 已解决) · 中：1 (0 已解决) · 低：3 (0 已解决)

笔记和附加信息

提出了 4 个笔记 (0 已解决)

关注点

OpenZeppelin 对 0xPolygonHermez/zisk 仓库的 5104c56 commit 进行了审查。

我们的审查集中在以下文件：

 state-machines
├── binary/pil
│   ├── binary.pil
│   ├── binary_add.pil
│   ├── binary_extension.pil
│   ├── binary_extension_table.pil
│   └── binary_table.pil
└── main/pil
    └── main.pil

系统概述

Zisk 是一个通用、开源的 zkVM，专为计算和证明程序而设计。Zisk 使用一个名为 Zisk ISA 的自定义 ISA。虽然这个 ISA 是自定义的，但 Zisk 团队创建了一个编译器，可以将 RISC-V 指令转换为 Zisk 指令。因此，任何可以编译为 RISC-V 的源代码都可以通过 Zisk 进行证明。例如，Zisk 团队最近在证明以太坊区块方面展示了有希望的结果。

与其他 zkVM 类似，Zisk 具有仿真步骤和证明步骤。Zisk 中的仿真步骤是在 Rust 中实现的，以保证兼容性和效率。证明步骤需要获取从仿真中创建的执行跟踪，并满足定义 Zisk ISA 的电路约束。虽然这些约束可以用各种不同的电路语言编写，但 Zisk 选择使用 PIL2 语言来实现。我们的审查重点是这些 PIL2 约束。

本次审查分为两个范围。第一个范围包含 binary 文件夹中的所有 PIL2 文件。这些文件与 MIN、MAX、LT、GT、EQ、ADD、SUB、LE、AND、OR、XOR、SLL、SRL、SRA、SE 等操作有关。为了确保这些指令的正确性，它们会根据一个查找表进行验证，该表包含每个操作的所有 1 字节（8 位）组合。由于 Zisk 使用 8 字节（64 位）的输入，因此两个输入之间的每个操作都会根据这个预定的表逐字节查找，以确定正确的输出。本次审查的重点是预定表值的正确性，以及将这些字节拼接在一起的约束的正确性。

第二个范围围绕 main.pil 文件展开。该文件从程序的执行跟踪中获取每个指令，并将其定向到不同指令的各种约束。构成程序的指令集是可信的，并从 ROM（只读存储器）中获取。ROM 是可信的，因为它是一个公共输入，并且由证明者提交。main.pil 还处理寄存器的读写，输入和输出的操作都存储在寄存器中。类似地，该文件还负责将内存的写入和读取定向到内存约束，并通过更新程序计数器来维护程序的控制流。

Zisk 的一项创新是通过将执行分解为更小的片段，并为每个片段生成一个证明，从而避免为执行创建单一的证明。main.pil 文件提供了约束，以保证一个片段的结束和另一个片段的开始之间，以及属于一个片段的不同步骤之间的一致性。main.pil 还可以选择证明使用栈的执行跟踪。然而，由于该文件的这部分目前不打算用于生产，因此在与 Zisk 团队讨论后，将其排除在审查范围之外。因此，除了与栈相关的部分外，main.pil 已被完全审查。

开源审查

本次审查是 OpenZeppelin 帮助保护具有强大开源 DNA 的有前景的年轻项目的一部分工作，符合我们帮助保护开放经济的使命。

严重缺陷

不正确的二进制操作码评估

has_initial_carry 见证 未受约束。这允许所有相关的二进制操作码都以相反的进位位执行，从而产生一个相差一的错误。特别是，当处理最低有效字节时，进位位被设置为 has_initial_carry * INITIAL_CARRY_LT_ABS。对于 LT_ABS 系列的操作码，进位位在取反负数输入时使用，应设置为 1。如果设置为 0，则取反将计算出一个错误递减的值，可能导致不正确的比较。

另一方面，所有其他操作码都应以 0 的初始进位位开始。如果 has_initial_carry 设置为 INITIAL_CARRY_LT_ABS 的倒数，则会导致初始进位位设置为 1，这可能导致不正确的计算。

考虑约束 has_initial_carry，使其对于 LT_ABS 系列的操作码为 1，否则为 0。

高危风险

LE[U] 操作码的二进制表不正确

LE[U] 二进制表部分 用于确认 a <= b，其中 a 和 b 是两个 8 字节的数字。与该表中的所有记录一样，它只对 a 和 b 的一个字节进行操作。因此，总体结果应通过组合各种 1 字节的结果从外部确定。

当 a 和 b 的最高有效字节相等时，该表断言 条件成功，这意味着 a 不大于 b。但是，结果实际上取决于前一个查找（对于第二个最高有效字节）是否得出 a 不大于 b 的结论。例如，当 a = 0x0002000000000000 且 b = 0x0001000000000000 时，该表将得出 a <= b 为 true 的结论。

考虑引入一个进位位以解释上述情况。

32 位模式下的无效的最后进位校正

二进制比较操作输出一个布尔值，这需要设置最低有效字节。由于结果直到处理最高有效字节后才知道，因此结果保存在最高有效字节中，然后在二进制处理器中校正输出。

但是，这种技术有一个不必要的步骤，并且对于 32 位操作码的实现不正确。特别是，结果写入字节 3，但校正应用于字节 7。由于最后进位已经编码了输出布尔值，因此无需保存然后清除结果。

对于使用最后进位作为结果的操作，考虑简单地在二进制表的每个步骤中输出 0，然后通过将最后的 cout 添加到最低有效位来纠正此问题。

中危风险

非对称读取和存储：存储忽略高 32 位

main.pil 将间接加载地址 addr1 计算为 b_offset_imm0 + b_src_ind * (a[0] + 2**32 * a[1])。但是，它将间接存储地址 addr2 计算为 store_offset + store_ind * a[0]，忽略 a[1]。

对加载和存储使用不同的地址计算允许在存储时截断指针，而加载使用完整的 64 位地址。这意味着当 a 超过 32 位时，读取和写入可能发生在两个不同的地址。

考虑将间接存储的 addr2 计算为 store_offset + store_ind * (a[0] + 2**32 * a[1])，以匹配加载路径，包括任何栈偏移逻辑。或者，考虑在读取时将地址限制为 32 位。

低危风险

缺少 ; 导致编译错误

在 binary_extension_table.pil 中，多行末尾缺少 ;，例如第 144 行，第 156 行 和第 168 行。由于 PIL2 语言要求所有语句都以 ; 结尾，因此这会导致编译错误。

考虑在每个受影响的行的末尾添加 ;，以确保代码成功编译。

缺少且具有误导性的文档

在整个代码库中，发现了多个缺少和/或具有误导性的文档的实例：

• 文件 binary_add.pil 没有任何文档指定见证的预期大小。但是，它期望 a、b 和 c_chunk 具有特定的大小，否则会导致此约束失败。
• 预填充的 binary_table.pil 中的 GT 操作 仅适用于有符号比较。考虑记录不应将其用于无符号比较。
• binary_table.pil 的第 71 行 可以使用注释 // EXT_32 来指定它用于哪个操作码。
• 此注释 说“……和 c[input_chunks-1] = cout”，而它应该说“……和 c[input_chunks-1] = cout * factor。”
• 在 binary_extension.pil 的第 75 行 中，注释表明 in2_low 是 5 位或 6 位。但是，这意味着只有最低有效 5 位或 6 位与表相关。
• 在 main.pil 的第 318 行 中，注释说“大于”，而它应该说“之前”。
• 考虑使用数字分隔符 (_) 来提高整个代码库中大数值的视觉清晰度，例如这些。
• binary_extension.pil 的第 4 行中的注释 使用了 "standard" 一词，而应使用 "extended"。
• main.pil 的第 137-138 行中的注释 应为 "[is_external_op == 0 && op == 0] ==> c = 0, flag = 1" 和 "[is_external_op == 0 && op == 1] ==> b = c, flag = 0."
• main.pil 的第 159-160 行中的注释 已被翻转。

考虑添加缺少的注释并修改上述注释，以提高一致性并更准确地反映已实现的逻辑。这样做将使审计员和其他检查代码的各方更容易理解代码的每个部分的设计目的。

预计算查找表中的重复行

二进制查找表的 EXT_32 操作码部分分为四个部分，通过 index_offset 值 0、1、2、3 来区分。

• 索引偏移量 0 导致 op_is_min_max = 0 和 result_is_a = 0，生成一个 FLAGS 值 为 0。
• 索引偏移量 1 导致 op_is_min_max = 1 和 result_is_a = 0，从而导致 FLAGS 值为 2。
• 索引偏移量 3 导致 op_is_min_max = 1 和 result_is_a = 1，从而导致 FLAGS 值为 6。

但是，索引偏移量 2 导致 op_is_min_max = 0 和 result_is_a = 0，这与索引偏移量 0 完全相同。查找值 因此是相同的和不必要的。

考虑删除上述额外的行以提高存储和计算性能。

笔记和附加信息

常量问题

在整个代码库中，发现了多个实例，其中可以使用、更好地定义或删除常量。

例如，以下常量未使用：

• binary.pil 中的 LTU_OP
• main.pil 中的 REG_BASE_ADDR

考虑删除上面列出的常量以提高代码清晰度。

在以下实例中，可以使用常量而不是无法解释的文字（“魔法数字”）：

• 在 binary_extension_table.pil 的第 99 行 中，可以使用 常量 bits 而不是 64。
• binary_extension_table.pil 的第 136 行 可以定义一个常量而不是 32。
• binary_extension.pil 的第 87-88 行 可以使用常量而不是 2**8、2**16 和 2**24。
• binary_extension.pil 的第 106 行 可以使用常量而不是 2**24 - 1。
• main.pil 的第 297 行 可以使用 RC 而不是 2。

考虑定义和使用常量以避免使用魔法数字，这可能会在将来修改代码时引起问题和混乱。

在以下实例中，可以使用全大写定义常量，以提高代码清晰度：

• 在 binary_extension_table.pil 的第 47-48 行 中，bits 和 bytes 可以用大写字母书写。

考虑用大写字母定义所有变量以提高代码清晰度。

代码简化

在整个代码库中，发现了多个代码简化的机会：

• binary_add.pil 的第 21 行 可用于简化前一行。
• binary_table.pil 的第 118-122 行 可以使用三元运算符简化。
• binary.pil 中的此循环 分为四个互斥且顺序执行的块。相反，它可以重构为两个不同的循环（其中字节 0、3 和 7 作为单独的语句处理）。
• 在多个地方，例如在 binary_extension_table.pil 的第 98 行 中，非二进制值被视为 true。虽然大于 0 的任何值都为真，但明确说明这一点可能会更清楚。
• 在 main.pil 中，stack_enabled 在某些部分作为布尔值进行测试，而在其他部分，它明确地与 1 进行比较。这意味着如果一个值设置为大于 1 的值，则在同一 main 实例的不同部分中，它将被视为 true 和 false。考虑一致地定义 if 语句。
• SE_W 操作码没有显式处理 当 offset > 3 时的案例。考虑明确处理这种情况，以与其他操作码的逻辑保持一致，例如这个 和这个。
• OP_IS_SHIFT 列在 binary_extension_table.pil 中定义，但在 binary_extension.pil 使用它之前，它一直未使用。考虑从表中删除此列，并在 binary_extension.pil 中处理此逻辑。

考虑修改上述代码以提高一致性并简化已实现的逻辑。这样做将使审计员和其他检查代码的各方更容易理解代码的每个部分的设计目的。

三元运算符的一致性

在 GT 操作码中，三元运算符 用于有符号比较读取 c = (b & 0x80) ? 1 : 0;。但是，对于文件中所有其他有符号比较，例如此行 上的比较，该条件基于 a & 0x80。

考虑更新此行代码以读取 c = (a & 0x80) ? 0 : 1;，以保持一致性和易于推理。如果需要重构，这将对系统的未来发展尤其有利。

排版错误

在整个代码库中，发现了多个排版错误的实例：

• 在 main.pil 的第 33 行 中，"inicial_pc" 应为 "initial_pc"。
• 在 main.pil 的第 113 行 和第 128 行 中，"a immediate" 应为 "an immediate"。
• 在 main.pil 的第 131 行 中，"form" 应为 "from"。
• 在 main.pil 的第 198 行 中，"de" 应为 "the"。
• 在 main.pil 的第 225 行 中，"sizeo_of_instance" 应为 "size_of_instance"。
• 在 main.pil 的第 230 行 中，"máximum" 应为 "maximum"。
• 在 main.pil 的第 423 行 中，"isn't send to closed the cycle" 应为 "is not sent to close the cycle"。
• 在 main.pil 的第 432 行 中，"it will the previous access" 应为 "it will be the previous access"。
• 在 main.pil 的第 433 行 中，"must not be send" 应为 "must not be sent"。 LT_ABS 操作码族使用两个进位来处理每个字节。但是，在构造标志位图时，它假设只有一个进位。这导致操作进位被错误地解释为 op_is_min_max 标志。

考虑扩展 flags 位图，以便为“操作进位”标志设置一个专用位置。

程序计数器在段开始时未受约束

分段延续逻辑确保（1，2）segment_initial_pc 值与前一个段一致。但是，段中的第一个 pc 值没有被约束为与此值匹配。这意味着 prover 可以在段之间引入无效跳转。

考虑约束每个段中的第一个 pc 值等于 segment_initial_pc。

结论

Zisk 是一种新颖的开源 zkVM，能够证明任何可以编译为 RISC-V 的程序。由于约束是用一种新的编程语言 PIL2 编写的，因此特别注意学习这种语言并确保适当的约束到位。

审查发现了多个问题，严重程度从注意级别到严重级别不等。最值得注意的是，存在约束不足的子电路和二进制表的一些不正确的逻辑。

感谢 Zisk 团队努力维护开源代码库，及时、清晰地回答我们的问题，并花时间引导我们了解他们的系统。这些努力使代码库更具弹性，并且团队很高兴与他们合作完成这个里程碑。

附录

问题分类

OpenZeppelin 将智能合约漏洞分为 5 个级别：

• 严重
• 高
• 中
• 低
• 注意/信息

严重程度

当问题的影响是灾难性的，威胁到客户的声誉和/或导致客户或用户遭受严重的财务损失时，应用此分类。利用的可能性可能很高，需要迅速响应。严重问题通常涉及重大风险，例如大量用户敏感资产的永久丢失或锁定，或者核心系统功能出现故障且没有可行的缓解措施。由于这些问题可能严重损害系统完整性或用户信任，因此需要立即关注。

高严重程度

这些问题的特点是可能对客户的声誉产生重大影响和/或导致相当大的财务损失。利用的可能性很大，需要迅速响应。此类问题可能包括大量用户敏感资产的暂时丢失或锁定，或者关键系统功能中断，尽管存在潜在但有限的缓解措施。重点在于对系统运营或资产安全的重大但不总是灾难性的影响，因此需要及时有效的补救措施。

中等严重程度

被归类为中等严重程度的问题可能会对客户的声誉产生明显的负面影响和/或造成适度的财务损失。如果不加以处理，此类问题有中等可能性被利用或可能导致系统中出现不良副作用。这些问题通常仅限于一小部分用户的敏感资产，或者可能涉及与指定系统设计方案的偏差，这些偏差虽然在性质上并非直接是财务上的，但会损害系统完整性或用户体验。这里的重点是构成真实但受控风险的问题，需要及时关注以防止升级。

低严重程度

低严重程度的问题是指对客户的运营和/或声誉影响较小的问题。这些问题可能代表客户特定业务模型的小风险或低效率。它们被确定为可以改进的领域，如果加以解决，虽然不紧急，但可以增强代码库的安全性和质量。

注释和附加信息严重程度

此类别是为那些影响最小但仍需要解决的问题保留的。解决这些问题有助于提高整体安全态势和代码质量，但不需要立即采取行动。它反映了对维护高标准和持续改进的承诺，即使在没有直接风险的领域也是如此。

准备好保护你的代码了吗？

请求审计 →

• 原文链接： openzeppelin.com/news/zi...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～