深入解析Cairo静态分析工具Amarna：安全编程新利器

原创

qife122

发布于 2025-08-27 17:51:58

11400

代码可运行

运行总次数：0

代码可运行

Amarna：Cairo程序的静态分析工具 - Trail of Bits博客

Filipe Casal

2022年4月20日

密码学, 静态分析

我们正式开源Amarna——针对Cairo编程语言的新型静态分析器和linter工具。Cairo是驱动多个资产规模达数百万美元的交易交易所（如StarkWare推出的dYdX）的编程语言，也是StarkNet合约的编程语言。但与其他语言类似，它也存在一些奇特功能和易错点。因此我们将首先简要介绍该语言、其生态系统以及开发者应注意的语言陷阱，随后介绍Amarna的工作原理、检测能力及未来规划。

Cairo语言介绍

为什么需要Cairo？

Cairo及类似语言（如Noir和Leo）旨在编写"可证明程序"，即一方运行程序并生成证明，证实程序在给定特定输入时返回特定输出。

假设我们需要将程序计算外包给某个（可能不可信的）服务器，并需保证结果正确。使用Cairo，我们可以获得程序输出正确结果的证明；只需验证证明而无需重新计算函数（这违背了外包计算的初衷）。

总结步骤如下：

编写要计算的函数
在工作机上使用具体输入运行函数，获取结果并生成计算有效性证明
通过验证证明来验证计算

Cairo编程语言

如前所述，Cairo编程模型涉及两个关键角色：证明者（运行程序并创建证明）和验证者（验证证明者创建的证明）。

但在实践中，Cairo程序员实际上不会自己生成或验证证明。生态系统包含三大支柱：

共享证明器（SHARP）：公共证明器，为用户发送的程序轨迹生成有效性证明
证明验证合约：验证程序执行的有效性证明
事实注册合约：可查询以检查特定事实是否有效

事实注册库是存储程序事实（或从程序及其输出哈希计算的值）的数据库；创建程序事实是将程序与其输出绑定的方式。

这是Cairo的基本工作流程：

用户编写程序并将其轨迹提交给SHARP（通过Cairo playground或cairo-sharp命令）
SHARP为程序轨迹创建STARK证明并提交给证明验证合约
证明验证合约验证证明，若有效则将程序事实写入事实注册库
其他用户现在可查询事实注册合约检查该程序事实是否有效

还需注意两点：

Cairo内存为一次性写入：值写入内存后不可更改
assert语句assert a = b的行为取决于a是否初始化：若a未初始化，assert语句将b赋值给a；若a已初始化，则断言a和b相等

虽然Cairo语法和关键字细节很有趣，但本文不涵盖这些主题。官方Cairo文档和Perama的Cairo笔记是很好的入门资料。

设置和运行Cairo代码

现在简要概述Cairo语言后，让我们讨论如何设置和运行Cairo代码。考虑以下简单Cairo程序，该函数计算数字对(input, 1)的Pedersen哈希函数并在控制台输出结果：

# validate_hash.cairo
%builtins output pedersen

from starkware.cairo.common.cairo_builtins import HashBuiltin
from starkware.cairo.common.hash import hash2
from starkware.cairo.common.serialize import serialize_word

func main{output_ptr:felt*, pedersen_ptr : HashBuiltin*}():
    alloc_locals
    local input
    %{ ids.input = 4242 %}

    # 计算元组(input, 1)的Pedersen哈希
    let (hash) = hash2{hash_ptr=pedersen_ptr}(input, 1)

    # 打印计算的哈希值
    serialize_word(hash)

    return ()
end

使用Python虚拟环境设置Cairo工具：

$ mkvirtualenv cairo-venv
(cairo-venv)$ pip3 install cairo-lang

然后编译程序：

# 编译validate_hash.cairo文件，
# 输出写入compiled.json
$ cairo-compile validate_hash.cairo --output compiled.json

最后运行程序，将输出以下值：

# 运行程序
$ cairo-run --program=compiled.json --print_output --layout small
Program output:
  1524309693207128500197192682807522353121026753660881687114217699526941127707

该值是对应(4242, 1)的Pedersen哈希的域元素。

现在假设我们将输入从4242改为某个隐藏值，并向验证者提供以下输出：

$ cairo-run --program=compiled.json --print_output --layout small
Program output:
  1134422549749907873058035660235532262290291351787221961833544516346461369884

验证者为何相信我们？我们可以证明我们知道会使程序返回该输出的隐藏值！

要生成证明，需要计算程序哈希以生成程序事实。此哈希不依赖输入值，因为赋值在提示内（Cario的一个特性，后文讨论）：

# 计算程序哈希
$ cairo-hash-program --program compiled.json
0x3c034247e8bf20ce12c878793cd47c5faa6f5470114a33ac62a90b43cfbb494

# 计算程序事实
from web3 import Web3

def compute_fact(program_hash, program_output):
    fact = Web3.solidityKeccak(['uint256', 'bytes32'],
                               [program_hash, Web3.solidityKeccak(['uint256[]'], [program_output])])

    h = hex(int.from_bytes(fact, 'big'))
    return h

# 上面计算的哈希和输出
program_hash = 0x3c034247e8bf20ce12c878793cd47c5faa6f5470114a33ac62a90b43cfbb494
program_output = [1134422549749907873058035660235532262290291351787221961833544516346461369884]

print(compute_fact(program_hash, program_output))
# 0xe7551a607a2f15b078c9ae76d2641e60ed12f2943e917e0b1d2e84dc320897f3

然后可使用事实注册合约，以程序事实作为输入调用isValid函数来检查程序事实的有效性：调用isValid函数检查程序事实有效性的结果。

回顾一下，我们运行了程序，SHARP创建了可在事实注册库中查询有效性的证明，证明我们确实知道会导致程序输出此值的输入。

现在我可以告诉你我使用的输入是71938042130017，你可以去检查结果是否匹配。

你可以在Cairo区块链开发文档和StarkWare的这篇文章中了解更多关于此过程细节及事实注册库的信息。

Cairo特性与易错点

Cairo有几个可能让新Cairo程序员困惑的特性和易错点。我们将描述三个容易被误用导致安全问题的Cairo特性：Cairo提示、递归与约束不足结构的相互作用，以及非确定性跳转。

提示

提示是特殊的Cairo语句，基本上允许证明者编写任意Python代码。是的，用Cairo提示编写的Python代码字面上是exec执行的！

提示写在%{ %}内。我们在第一个示例中已使用它们为输入变量赋值：

%builtins output

from starkware.cairo.common.serialize import serialize_word

func main{output_ptr:felt*}():

    # 任意Python代码
    %{
       import os
       os.system('whoami')
    %}

    # 打印1
    serialize_word(1)

    return ()
end

$ cairo-compile hints.cairo --output compiled.json
$ cairo-run --program=compiled.json --print_output --layout small
fcasal
Program output:
  1

由于Cairo可以在提示中执行任意Python代码，你不应在自己的机器上运行任意Cairo代码——这样做可能让代码编写者获得对你机器的完全控制。

提示通常用于编写仅由证明者执行的代码。证明验证者甚至不知道提示存在，因为提示不会改变程序哈希。以下来自Cairo playground的函数计算正整数n的平方根：

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)
end

程序使用提示中的Python数学库计算n的平方根。但在验证时，此代码不运行，验证者需要检查结果确实是平方根。因此，函数在返回结果前包含检查n是否等于res * res。

约束不足结构

Cairo缺乏对while和for循环的支持，迫使程序员使用传统的递归进行迭代。考虑Cairo playground的"动态分配"挑战。挑战要求我们编写函数，给定元素列表，将平方这些元素并返回包含这些平方元素的新列表：

%builtins output

from starkware.cairo.common.alloc import alloc
from starkware.cairo.common.serialize import serialize_word

# 用`array`前`length`个元素的平方填充`new_array`
func _inner_sqr_array(array : felt*, new_array : felt*,
                                        length : felt):
    # 递归基本情况
    if length == 0:
        return ()
    end

    # 递归情况：new_array的第一个元素将是array第一个元素的平方
    # 回忆assert将赋值给new_array数组位置0，因为它尚未初始化
    assert [new_array] = [array] * [array]

    # 递归调用，推进数组并减去1到数组长度
    _inner_sqr_array(array=array + 1,
                     new_array=new_array + 1,
                     length=length - 1)
    return ()
end

func sqr_array(array : felt*, length : felt) ->
                                          (new_array : felt*):
    alloc_locals
    # 分配任意长度数组
    let (local res_array) = alloc()

    # 用array元素的平方填充新分配的数组
    _inner_sqr_array(array, res_array, length)
    return (res_array)
end

func main{output_ptr : felt*}():
    alloc_locals

    # 分配新数组
    let (local array) = alloc()

    # 用域元素填充新数组
    assert [array] = 1
    assert [array + 1] = 2
    assert [array + 2] = 3
    assert [array + 3] = 4

    let (new_array) = sqr_array(array=array, length=4)

    # 打印数组元素
    serialize_word([new_array])
    serialize_word([new_array + 1])
    serialize_word([new_array + 2])
    serialize_word([new_array + 3])

    return ()
end

运行此代码将按预期输出数字1、4、9和16。

但如果发生错误（或差一错误）导致sqr_array函数以零长度调用会发生什么？

func main{output_ptr : felt*}():
    alloc_locals
    # 分配新数组
    let (local array) = alloc()
    # 用域元素填充新数组
    assert [array] = 1
    assert [array + 1] = 2
    assert [array + 2] = 3
    assert [array + 3] = 4

    let (new_array) = sqr_array(array=array, length=0)
    serialize_word([new_array])
    serialize_word([new_array + 1])
    serialize_word([new_array + 2])
    serialize_word([new_array + 3])

    return ()
end

基本上发生以下情况：

sqr_array函数将分配res_array并调用_inner_sqr_array(array, res_array, 0)
_inner_sqr_array将长度与0比较并立即返回
sqr_array将返回已分配但从未写入的res_array

那么当你在new_array的第一个元素上调用serialize_word时会发生什么？

这取决于...按原样运行代码将导致错误，因为new_array的值未知：按原样运行上述代码后发生的错误。

但请记住，通常你不会运行代码；你将验证程序输出某些值的证明。我实际上可以向你提供证明，该程序可以输出你想要的任何四个值！你可以自己计算所有这些来确认我没有作弊：

$ cairo-compile recursion.cairo --output compiled.json
$ cairo-hash-program --program compiled.json
0x1eb05e1deb7ea9dd7bd266abf8aa8a07bf9a62146b11c0bd1da8bb844ff2479

以下事实将此程序与输出1, 3, 3, 7绑定：

# 上面计算的哈希和输出
program_hash = 0x01eb05e1deb7ea9dd7bd266abf8aa8a07bf9a62146b11c0bd1da8bb844ff2479
program_output = [1, 3, 3, 7]

print(compute_fact(program_hash, program_output))
# 0x4703704b8f7411d5195e907c2eba54af809cb05eebc65eb9a9423964409a8a4d

根据事实注册合约，此事实有效：事实注册库对程序事实的验证。

那么这里发生了什么？

由于返回的数组仅分配但从未写入（因为其长度为0，递归一开始就停止），证明者可以在提示中写入数组，而提示代码不会影响程序的哈希！

"邪恶"的sqr_array函数实际上是以下内容：

func sqr_array(array : felt*, length : felt) ->
                                           (new_array : felt*):
    alloc_locals
    let (local res_array) = alloc()

    %{  # 如果长度为0，写入结果数组
        if ids.length == 0:
            data = [1, 3, 3, 7]
            for idx, d in enumerate(data):
                memory[ids.res_array + idx] = d
    %}

    _inner_sqr_array(array, res_array, length)
    return (res_array)
end

简而言之，如果某些错误使数组长度为0，恶意证明者可以创建他想要的任何任意结果。

你可能还会问，为什么一般来说恶意证明者不能简单地在程序末尾添加提示以任何他希望的方式更改输出。嗯，他可以，只要该内存之前没有被写入过；这是因为Cairo内存是一次性写入的，所以你只能向每个内存单元写入一个值。

由于Cairo内存的工作方式，创建最终结果数组的这种模式是必要的，但它也带有安全风险：跟踪此数组长度的简单差一错误可能允许恶意证明者任意控制数组内存。

非确定性跳转

非确定性跳转是另一种可能让首次阅读Cairo的程序员感到不自然的代码模式。它们结合提示和条件跳转，用某个值重定向程序的控制流。该值对验证者可能是未知的，因为证明者可以在提示中设置它。

例如，我们可以以下列刻意的方式编写检查两个元素x和y是否相等的程序：

func are_equal(x, y) -> (eq):
    # 根据x和y的相等性设置ap寄存器为True或False
    %{ memory[ap] = ids.x == ids.y %}

    # 如果元素相等，跳转到equal标签
    jmp equal if [ap] != 0; ap++

    # 情况x != y
    not_equal:
    return (0)

    # 情况x == y
    equal:
    return (1)
end

运行此程序将返回预期结果（不同值返回0，相等值返回1）：

func main{output_ptr : felt*}():

    let (res) = are_equal(1, 2)
    serialize_word(res) # -> 0

    let (res) = are_equal(42, 42)
    serialize_word(res) # -> 1

    return()
end

然而，此函数实际上易受恶意证明者攻击。注意跳转指令仅依赖提示中写入的值：

    %{ memory[ap] = ids.x == ids.y %}
    jmp equal if [ap] != 0; ap++

我们知道提示完全由证明者控制！这意味着证明者可以在该提示中编写任何其他代码。实际上，无法保证证明者确实检查了x和y是否相等，甚至x和y是否以任何方式使用。由于没有其他检查，函数可以返回证明者希望的任何内容。

如前所述，程序哈希不考虑提示中的代码；因此，验证者无法知道是否执行了正确的提示。恶意证明者可以通过更改提示代码并将每个证明提交给SHARP，为程序的任何可能输出值((0, 0), (1, 1), (0, 1), 或(1, 0))提供证明。

那么如何修复它？

每当看到非确定性跳转时，我们需要确保跳转有效，验证者需要在每个标签中验证跳转：

func are_equal(x, y) -> (eq):
    %{ memory[ap] = ids.x == ids.y %}
    jmp equal if [ap] != 0; ap++

    # 情况x != y
    not_equal:
    # 我们在not_equal情况中
    # 所以不能有相等的x和y
    if x == y:
	# 添加不可满足的断言
        assert x = x + 1
    end
    return (0)

    # 情况x == y
    equal:
    # 我们在equal情况中
    # 所以x和y必须相等
    assert x = y
    return (1)
end

在这种情况下，函数足够简单，代码只需要if语句：

func are_equal(x, y) -> (eq):
    if x == y:
        return (1)
    else:
        return (0)
    end
end

Amarna：我们的Cairo静态分析器

在审计Cairo代码时，我们注意到基本上没有任何语言支持，除了VScode中的语法高亮。然后，当我们在代码中发现问题时，我们希望确保代码库中其他位置不存在类似模式。

我们决定构建Amarna，一个Cairo静态分析器，使我们能够创建自己的规则并搜索我们感兴趣的代码模式——不一定是安全漏洞，而是任何需要分析或在审查代码时需要更多关注的安全敏感操作。

Amarna将其静态分析结果导出到SARIF格式，使我们能够使用VSCode的SARIF Viewer扩展轻松集成它们，并在代码中查看带下划线的警告：带下划线死存储的Cairo代码（左）和显示Amarna结果的SARIF Viewer扩展（右）。

Amarna如何工作？

Cairo编译器使用Python编写，使用lark（解析工具包）定义语法并构建其语法树。使用lark库，构建程序抽象语法树的访问者很简单。从这里开始，编写规则就是在树中编码你想要找到的内容。

我们编写的第一个规则是突出显示所有算术操作+、-、*和/的使用。当然，并非所有除法使用都不安全，但通过这些操作的下划线，开发者被提醒Cairo算术在有限域上工作，并且除法不是像其他编程语言中的整数除法。域算术下溢和溢出是开发者需要注意的其他问题。通过突出显示所有算术表达式，Amarna帮助开发者和审阅者快速聚焦代码库中可能在这方面有问题的位置。

检测所有除法的规则非常简单：它基本上只是创建带有文件位置的结果对象并将其添加到分析结果中：

class ArithmeticOperationsRule(GenericRule):
    """
    检查算术操作：
        - 报告所有乘法和除法
        - 仅报告不涉及像[ap - 1]这样的寄存器的加法和减法
    """

    RULE_TEXT = "Cairo算术在有限域上定义并有潜在溢出风险。"
    RULE_PREFIX = "arithmetic-"

    def expr_div(self, tree: Tree) -> None:
        result = create_result(
            self.fname,
            self.RULE_PREFIX + tree.data,
            self.RULE_TEXT,
            getPosition(tree)
        )
        self.results.append(result)

当我们寻找更复杂的代码模式时，我们开发了三类规则：

本地规则：独立分析每个文件。上述查找文件中所有算术操作的规则是本地规则的示例。
收集器规则：独立分析每个文件并收集数据供后处理规则使用。例如，我们有规则收集所有声明函数和所有调用函数。
后处理规则：在所有文件分析后运行，并使用收集器规则收集的数据。例如，在收集器规则找到文件中所有声明函数和所有调用函数后，后处理规则可以通过识别声明但从未调用的函数来找到所有未使用函数。

Amarna发现什么？

到目前为止，我们已经实现了10条规则，其影响范围从帮助我们审计代码的信息性规则（标记为Info）到潜在安全敏感的代码模式（标记为Warning）：

	规则	发现内容	影响	精度
1	算术操作	所有算术操作+、-、*、/的使用	Info	High
2	未使用参数	函数参数在出现的函数中未使用	Warning	High
3	未使用导入	未使用的导入	Info	High
4	错误类型装饰器	错误类型的代码装饰器	Info	High
5	未使用函数	从未调用的函数	Info	Medium
6	错误代码	具有必须检查返回值的函数调用	Info	High
7	不一致断言使用	以不同方式使用相同常量的断言（如assert_le(amount, BOUND)和assert_le(amount, BOUND - 1))	Warning	High
8	死存储	在返回语句前赋值但未使用的变量	Info	Medium
9	潜在未检查溢出	忽略返回溢出标志的函数调用（如uint256_add）	Warning	High
10	调用者地址返回值	对get_caller_address函数的函数调用	Info	High