Medjai：保护 Cairo 代码免受漏洞影响

在这篇博客文章中，我们将带你深入了解我们如何开发 Medjai，这是一个用于查找 Cairo 程序中的错误的新符号执行工具。我们的旅程将从乘坐直升机快速俯瞰Cairo开始。在途中，我们将瞥见宏伟著名的 OpenZeppelin，并看看一个奇特的错误是在古老的 GitHub 论坛中如何处理的。然后我们将讨论 Medjai 如何确保此类错误不再出现，以及 Medjai 如何帮助这些开发者首次发现这些错误。不过，伟大的故事总少不了背景故事：我们将解释 Medjai 如何克服符号执行 Cairo 程序的独特困难。虽然我们今天的旅程短暂，但请放心！Medjai 还有很多值得探索的地方，未来在其他博客文章中将会有更多的内容可供查看。

直升机游览Cairo

我们行程的第一站是Cairo。虽然今天许多编程语言允许开发者编写和部署智能合约，但其中一些语言（包括 Cairo）在能够支持构建 零知识证明方面是独特的。零知识证明 (ZKPs) 允许一方（“证明者”）向另一方（“验证者”）证明他们知道某个信息而无需泄露任何秘密信息。这对智能合约尤其有用，因为它允许任何人验证一些计算的有效性，而无需访问参与计算的个人信息。

Cairo 是 StarkNet 合约的编程语言，是多个重要交易所的基础，如 Immutable X、Sorare 和 DeversiFi，这些交易所处理数百万美元的资产。当程序员希望将他们的智能合约部署到 StarkNet 时，首先会执行他们的程序并使用 SHARP 获取程序跟踪的有效性证明：用于 StarkNet 的 共享证明器。在单独的 证明验证器 检查生成的证明的有效性后，程序跟踪有效性的事实会被添加到 StarkNet 的 事实注册表 中。

SHARP 和证明验证器对 Cairo 合约施加的限制迫使 Cairo 的语言语法和语义呈现出多种特征。例如，在 Cairo 中，断言和赋值的处理方式几乎相同。语句 x = y + z 可以是将 y 和 z 定义时的对 x 的赋值，也可以是在 x 和 y 已定义时对 z 的赋值，或是在三者都有设置值时的一个断言。该语句的语义依赖于这三个变量的内存状态。稍后，我们将讨论 Cairo 语言的更多特性，以及这些特性在构建 Medjai 时所带来的挑战。

Cairo 工作流

为了理解证明器和验证器如何在 Cairo 程序上工作，我们将看一个来自 Cairo 教程的示例。具体来说，我们将考虑以下代码片段，该代码计算并输出 25 的正平方根。

func main{output_ptr : felt*}():
    [ap] = 25; ap++
    %{ memory[ap] = 5 %}
    [ap - 1] = [ap] * [ap]; ap++
    serialize_word([ap-1])
    return ()
end

大括号中的代码 %{ ... }% 是一个 提示。稍后我们将更详细地讨论提示，但现在只需了解它是本地执行的代码，并在证明者（生成证明时）和验证者中被忽略。

现在让我们从程序员、证明者和验证者三个角度审视这段代码。当程序员在自己的机器上编写此代码时，她可以在本地运行代码并确认程序输出符合预期。对于我们的示例，执行结果如下（注意 serialize_word([ap-1]) 执行的是输出）。

程序输出：
  5执行步骤数量： 9
...

除了打印输出 5，Cairo 还生成了一个被称为 Cairo PIE（位置独立执行）的 程序跟踪。PIE 编码了程序的逐步执行过程。当程序员对她的程序可以正常工作相对有信心时，她可以将 PIE 发送到共享证明服务 SHARP。在这个阶段，证明者生成一个描述此计算的 STARK 证明，并将证明发送给验证者以进行检查。最后，SHARP 会将称为 事实哈希 的内容返回给程序员，程序员可以用来查看他们的计算是否得到了验证。

作业事实： 0xf0f1aa66c31a056b486bee8f7157a07567196960370e63740c6857ac733327e1

一旦验证者收到证明，它会检查证明的所有步骤是否正确。然后，它会将事实及其验证状态（有效，无效）发布到所有人可见的事实注册表中。

Cairo 程序中的错误

重要的是要强调，经过验证的证明并不意味着实际的 Cairo 程序是正确的（即没有错误）。事实上，它所能表达的只是有人使用某些输入运行了 Cairo 程序并得到了一个输出。因此，如果程序本身存在错误，则人们仍然可以利用这些错误获得程序员故意未设定的值并使这个计算通过验证。例如，假设某人使用 Cairo 实现一个 ERC20 代币，并且他们的 withdraw 方法存在算术溢出。那么恶意用户可以利用这个溢出，获得更大的余额，并将其存储在区块链上。因此，就像其他领域一样，Cairo 开发者自己验证他们的程序是否按照他们的意图执行是很重要的。

我们构建 Medjai 是为了帮助 Cairo 开发者确保他们的程序无错。Medjai 使用一种称为 符号执行 的静态分析技术来探索 Cairo 程序的所有可能执行并寻找逻辑错误。具体而言，开发者可以将他们的意图指定为一组程序属性，而 Medjai 可以证明这些属性始终成立，或者构建一个某个属性被违反的示例。

在今天的旅程的下一节中，我们将查看一个现实世界的例子，说明 Cairo 程序员如何在他们的程序中编码意外行为。我们将看到该问题是如何手动修复的，然后解释符号执行是如何工作的，以及 Medjai 的符号执行引擎如何能够帮助这些开发者。

右舷侧视图：OpenZeppelin 和 _mint

如果你现在将双筒望远镜指向右侧，你将瞥见优雅飞翔的 OpenZeppelin。在我们游览的这一部分，我们将看到 OpenZeppelin _mint 函数中的一个旧错误，作为一个示例，展示 Cairo 程序员如何编码与程序员意图不符的行为。下面列出的是该错误在 ERC20.cairo 合约中的片段。

func _mint{
        syscall_ptr : felt*,
        pedersen_ptr : HashBuiltin*,
        range_check_ptr
    }(recipient: felt, amount: Uint256):
    alloc_locals
    assert_not_zero(recipient)
    uint256_check(amount)    let (balance: Uint256) = balances.read(account=recipient)
    let (new_balance: Uint256, _) = uint256_add(balance, amount)
    balances.write(recipient, new_balance)    let (local supply: Uint256) = total_supply.read()
    let (local new_supply: Uint256, _) = uint256_add(supply, amount)    total_supply.write(new_supply)
    return ()
end

从高层来看，mint 将 amount 加到用户的余额和货币的 total_supply 中。注意，在进行 uint256_add 时并没有检查加法是否溢出。在 mint 中发生溢出是非常有问题的，因为一个恶意用户可以用一个会 减少 货币供应的 amount 调用 mint（例如，可能将 total_supply 设置为 0）。最终，OpenZeppelin 开发者意识到了这个意外后果。

修复

一旦错误被明确后，开发者就修复了该行为，如下所示。修正后的版本添加了检查，确保在计算 new_supply 时不发生溢出。

func _mint{
        syscall_ptr : felt*,
        pedersen_ptr : HashBuiltin*,
        range_check_ptr
    }(recipient: felt, amount: Uint256):
    alloc_locals
    assert_not_zero(recipient)
    uint256_check(amount)    let (balance: Uint256) = balances.read(account=recipient)
    let (new_balance: Uint256, is_overflow) = uint256_add(balance, amount)
    assert is_overflow = 0
    balances.write(recipient, new_balance)    let (local supply: Uint256) = total_supply.read()
    let (local new_supply: Uint256, is_overflow) = uint256_add(supply, amount)
    assert is_overflow = 0    total_supply.write(new_supply)
    return ()
end

虽然这个错误乍看起来可能不是特别有趣，但 OpenZeppelin 开发者在 GitHub 上的讨论 为这个故事提供了更多的细节。当然，算术操作可以发生溢出，但是检查溢出需要消耗 gas。如果开发者在每个操作上天真地检查溢出，这笔费用累加起来会使执行合约的成本显著上升。此外，推理这些检查何时 是 必要的并不容易。即使在这个简单的案例中，理解 Uint256 和 uint256_add 是如何实现的对理解为什么这些检查是必要的来说很重要。

这正是程序分析可以提供帮助的地方！正如我们之前提到的，符号执行可以以符号化的方式推理所有程序路径，并覆盖人类难以推理的边缘情况。因此，符号执行可以帮助 Cairo 开发者发现代码中的漏洞，并帮助他们对给定的错误修复是否正确建立信心。

稍后，我们将展示我们的符号执行工具 Medjai 如何能够检测此错误，并确认该修复是正确的。现在，我们将做一个快速短暂停留，解释符号执行的高层工作机制。

小型短途旅行：符号执行

作为我们观光活动的一部分，我们将看看符号执行作为程序分析技术的工作原理。如果你还没有准备好全面了解符号执行的运作，不用担心。今天的活动更像是浮潜。

虽然普通的程序执行是在来自寄存器或内存的具体值上执行计算，但符号执行则将这些计算推广到操作 符号值，这些值代表许多可能的具体值。为此，符号执行将每条程序路径编码为一个关于这些符号输入的 逻辑公式，从而对该程序路径的输出可能值进行约束。然后，检查该执行路径是否存在错误归结为对逻辑公式可满足性的查询（通常用某种 一阶逻辑理论 表示）。此外，为了获得能触发该错误的具体输入，我们只需向 SMT 求解器查询满足逻辑公式的赋值即可！

作为示例，让我们考虑一个符号执行工具如何能在以下 Cairo 函数中找到错误。

func my_mint(amount : felt):
    alloc_locals
    let MAX_BALANCE = 2 ** 128
    assert_lt(amount, MAX_BALANCE)    let (balance : felt) = accounts.get_balance(...)
    let (newBalance : felt) = amount + balance
    accounts.set(newBalance)
    VERIFY(newBalance < MAX_BALANCE)
end

这段代码片段将 amount 添加到账户的余额中。它还（错误地）确保余额保持在最大余额之下。这里的问题是，检查仅对 amount 进行，而不是对 newBalance。为了说明符号执行是如何工作的，我们将使用一个符号输入 amount 运行 mint 函数。我们将把这个值称为 sym_amount。现在让我们逐步执行该程序：

1. sym_amount 第一次使用是在 assert_lt(amount, MAX_BALANCE) 中，这实际上在 amount >= MAX_BALANCE 时会停止程序。由于 Medjai 应考虑两个分支（停止和不停止），我们继续执行，但将语句 sym_amount < 2 ** 128 添加到我们的 路径条件 中。在 assert_lt(amount, MAX_BALANCE) 后执行的任何代码可以假设此路径条件成立。
2. sym_amount 接下来在 let (newBalance : felt) = amount + balance 中使用。假设账户是具体的，而 balance 被设置为 100。由于我们在符号执行这个程序，所以 newBalance 的值设置为符号值 sym_amount + 100。
3. 最后，让我们考虑 mint 函数末尾的验证查询。如果我们想验证 newBalance < MAX_BALANCE，我们的符号执行确定我们需要验证 sym_amount + 100 < 2 ** 128。此外，由于之前代码中的断言，我们的路径条件允许我们假设 sym_amount < 2 ** 128。因此我们可以向解算器发送的查询可以写作 ∀a. (a < 2^128 → a + 100 < 2^128)，其中 a 代表 sym_amount。解算器随后可以返回反例 sym_amount = 2 ** 128 - 100。

符号执行生成的反例特别有用，因为它们可以用于构造失败的输入。在此示例中，我们可以运行 my_mint(2 ** 128 - 100)，观察到结果中的账户新余额确实太大。此外，当我们修复该错误后，由于 SMT 求解器证明不存在旧的错误（即证明对于任何输入，newBalance < MAX_BALANCE），我们可以对我们的修复充满信心。

接下来，让我们回到我们的 OpenZeppelin 溢出错误，这次通过 Medjai 的验证视角来看开发者可能如何处理该情况。

重新发现错误并用 Medjai 验证修复

让我们再次检查 OpenZeppelin 中 mint 函数的错误，现在通过 Medjai 进行验证的视角。

要符号执行 mint 我们只需要添加两行代码来告诉 Medjai 我们想要验证的属性。这里是修复错误代码的插装版本：

func _mint{
        syscall_ptr : felt*,
        pedersen_ptr : HashBuiltin*,
        range_check_ptr
    }(recipient: felt, amount: Uint256):
    alloc_locals
    assert_not_zero(recipient)
    uint256_check(amount)    let (balance: Uint256) = balances.read(account=recipient)
    let (new_balance: Uint256, _) = uint256_add(balance, amount)
    VERIFY(new_balance > balance) # 证明余额没有溢出
    balances.write(recipient, new_balance)    let (local supply: Uint256) = total_supply.read()
    let (local new_supply: Uint256, _) = uint256_add(supply, amount)
    VERIFY(new_supply > supply) # 证明供应没有溢出
    total_supply.write(new_supply)
    return ()
end

我们可以通过用符号值替换所有参数值和存储变量来符号执行此函数。这样一来，Medjai 会自动向 SMT 求解器发出查询，以检查两个 VERIFY 语句处的属性。

结果

重新发现错误： 当我们对有错误的 mint 版本运行 Medjai 时，它报告溢出是可能的，并给出了一个反例，为触发溢出提供了 balance、total_supply 和 amount 的具体值。以下是 Medjai 生成的反例：

recipient = 0
balance = Uint256(high=0, low=1) // balance = 1
total_supply = Uint256(high=1, low=0) // total supply = 2**128
amount = Uint256(high=2**128-1, low=0) // amount = 2**256 - 2**128

我们利用这个反例生成 _mint 的具体测试用例，并发现如果用这些值作为输入执行 _mint，那么在执行过程中 new_supply 确实发生了溢出，并且 total_supply 在调用 _mint 后被设置为 0。

确认修复： 此后，我们对包含 VERIFY 语句的修复版本运行 Medjai，它报告我们指定的所有属性均已验证，确认修复版本足以防止溢出。

这一切对我们的开发者意味着什么呢？ 首先，他们可以肯定他们的修复正确地消除了溢出错误。但也许更令人满意的是，Medjai 能够显示检查溢出对 mint 函数的正确性是必要的。这意味着，如果删除检查以降低 mint 的执行成本，实际上会导致不正确的行为。

一段危险的徒步旅行：支持 Cairo 的独特特性

哎，你们都把车停在哪里了？哦，那里好像有点远……在我们徒步前往的过程中，我不妨告诉你们一些 Medjai 支持的 Cairo 有趣特性。今天我们有时间讨论的主要有两个特性： 提示 和 素数域算术。

提示

回想一下我们之前关于零知识编程的讨论，证明者——执行具体代码并生成任何交易的证明——与验证者——仅需验证证明正确性之间的区别。直观上，验证者所需的信息远低于证明者。例如，为了计算一个正数 n 的平方根，证明者必须实际找出一个数 sqrt(n)，而验证者仅需要确认 sqrt(n) * sqrt(n) = n。

因此，Cairo 迫使程序构建零知识证明，语言也允许使用 Python 代码的提示，这些提示只能由证明者执行。为了使我们之前的示例具体化，让我们看以下来自 Cairo 游乐场 的函数，该函数计算正整数的平方根：

func sqrt(n) -> (res):
    alloc_locals
    local res
    # 使用 python 提示设置 res 的值。
    %{
        import math        # 使用 ids 变量访问 Cairo 变量的值。
        ids.res = int(math.sqrt(ids.n))
    %}    # 从验证者的角度来看，提示是完全透明的。
    # 以下行保障 `res` 是 `n` 的平方根
    # （可以为正，也可以为负）。
    assert n = res * res
    return (res=res)

Medjai 以两种不同的模式处理提示： 含糊的 和 建模。在含糊模式下，Medjai 将提示视为一个未知函数，该函数编辑某些特定内存位置并将符号值存储到这些位置。如果 Medjai 能够验证程序是无错的，那么任何实际的提示实现不会引入错误（基于 VERIFY 语句）。如果这个验证步骤失败，Medjai 会切换到建模模式，在该模式下它使用每个提示块的模型进行符号执行。每个模型是一个函数，告诉 Medjai 相关提示块应如何影响程序的符号状态。如果 Medjai 在此模式下无法验证程序，则会将错误报告给开发者；否则，Medjai 会建议在 Cairo 程序中添加断言，以避免提示代码的变化造成未来的错误。

素数域算术

与传统的命令式编程语言不同，Cairo 不支持位运算——它的唯一原始整数类型是 felt，这是一个素数域中的元素。因此，Cairo 将 Uint256 表示为包含两个 felt 元素的结构。简单来说，felt 是一个范围为 [0, P) 的无符号整数，其中 P 是某个预定义的素数。这在进行算术运算时可能会导致一些意想不到的行为，例如除法的执行与传统整数除法不同。例如，在素数域中，1 / 2 = (P + 1) / 2。

支持 felt 不需要特殊技巧，但就像 Cairo 解释器本身，Medjai 需要对所有算术运算执行模 P 运算。此外，处理符号领域元素的位操作对于 SMT 求解器来说是困难的，因为（1）它们需要 252 位表示，并且（2） [0, P) 的边界增加了约束的复杂性。因此，Medjai 必须将位操作（如移动）转换为等价的算术操作（如乘法和除法）。

提示和素数域算术对 Medjai 特别重要，因为它们可能成为 Cairo 程序中微妙但影响深远的错误的来源。未来，我们希望展示一些这些独特错误的示例，以及 Cairo 的其他特性使得开发 Medjai 变得具有挑战性和有趣。

离别寄语

今天就到此为止。如果有一点希望能让你铭记，那就是：首先，随着 Cairo 和其他零知识语言的持续流行，支持这些语言的正确错误查找和验证工具也将变得越来越重要。其次，我们的符号执行工具 Medjai 可以帮助 Cairo 开发者捕捉代码中的微妙错误，并增强他们对于修复是否正确的信心。

我们希望你在探索 Medjai 的过程中玩得愉快。想了解有关我们的工具的更多信息，请查看 GitHub 上的 Medjai。 如果你今天的旅程很愉快，我的名字要么是 Jacob，要么是 Shankara，或 Yanju。如果不愉快，我的名字就是 Jon 或 Ben。无论如何，我们 Veridise 的全体成员希望你能再参加一次我们的冒险，继续探索更多关于 Cairo 与 Medjai 的内容！

关于 Veridise

Veridise 为区块链应用提供全面的安全审计。借助我们在自动化程序分析方面的专业知识，Veridise 提供先进的解决方案，以确保去中心化金融应用的安全性。如果你希望获取更多信息，请考虑在社交媒体上关注我们，或访问我们的网站：

网站 | Twitter | Facebook | LinkedIn | Github

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