漏洞披露：Cairo VM中潜在的排序器-证明器不一致性问题

概述

在1月26日星期日，Starkware告知我们，他们在Cairo VM中发现了一个关键问题，该问题与一个能够在虚拟机上成功执行但会违反AIR约束的程序有关。该漏洞是在调查第三方报告的其他问题时发现的，修复已在一个PR中实现。PR已合并，并已发布最新版，目前已更新。你可以在这里阅读Starkware的披露帖。

技术实现

在拉取请求#1925中的修复添加了两个更改：

• 在解码指令时进行额外验证
• 对verify_secure_runner进行额外验证。

指令解码 : 调用指令

调用指令大致执行以下操作：

1. 将当前帧指针保存到[ap]
2. 将调用返回地址保存到[ap + 1]
3. 更新fp和ap为ap + 2，跳过保存的数据。
4. 将pc更新为目标函数的起始位置

由于调用指令的一些标志是固定的，我们可以验证：

• dst寄存器保存ap+0，其中当前帧指针将被存储。

dst_register == AP
dst_offset   == 0

• op0寄存器保存ap+1，其中调用返回地址将被存储。

op0_register == AP
op0_offset   == 1

• fp和ap都更新为ap+2：

ap_update == Add2
fp_update == APPlus2

如果这些条件未满足，则解码失败。

指令解码 : 返回指令

返回指令大致执行以下操作：

1. 恢复之前的帧指针（在[fp - 2]）
2. 跳转到调用返回地址（在[fp - 1]）

由于返回指令的一些标志是固定的，我们可以验证：

• 程序计数器以绝对跳转更新

pc_update == Jump

• 跳转位置取自res，其等于fp-1：

res_logic   == Op1
op1_offset  == -1
op1_address == FP

• 下一个帧指针取自dst，其等于fp-2

fp_update    == Dst
dst_register == FP
dst_offset   == -2

如果这些条件未满足，则解码也失败。

条件跳转

该PR还强制规定，当pc_update等于4（条件跳转）时，res_logic必须等于0（这意味着忽略该字段）。

这一行为在Cairo白皮书第33页中有文档记录：

if pc_update == 4:
    if res_logic == 0 && opcode == 0 && ap_update != 1:
        res = Unused
    else:
        Undefined Behavior

安全运行者验证

verify_secure_runner函数验证在运行者中完成的运行是否安全，可以被重新定位并被其他Cairo程序使用。

PR验证最终帧指针与调用者的帧指针一致，存储在[initial_frame_pointer - 2]。

• 当使用ExecutionMode::ProofModeCanonical时，整个地址必须匹配。
• 当使用ExecutionMode::RunnerMode时，只有偏移量必须匹配。

影响分析

正如Starkware在发布中提到的：

"由于缺少的检查在sequencer中而不是在prover中，因此这对Starknet的正确性或安全性没有任何影响。理论上，它可能会导致一种情况，表面上已经通过的交易会在以后被撤销（重组）"

主要风险在于Cairo0合约的交易在sequencer上执行并撤销，而不是被证明。因为该交易不会通过prover，因此没有不正确的交易被证明，但撤销会影响用户体验。

结论

正如我们之前所说，这种问题在复杂软件中总是可能和常见，突显了让多个团队关注安全性、密切合作、拥有简单代码库以及详细检查组件之间交互的重要性。

非常感谢Starkware的通知和快速修复！

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