Amarna：Cairo程序的静态分析工具

我们开源了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已初始化，assert语句断言a和b相等。

尽管Cairo的语法和关键字细节很有趣，但本文不会涵盖这些主题。官方Cairo文档和Perama的Cairo笔记是了解更多信息的好起点。

设置和运行Cairo代码

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20


# 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 %}

    # computes the Pedersen hash of the tuple (input, 1)
    let (hash) = hash2{hash_ptr=pedersen_ptr}(input, 1)

    # prints the computed hash
    serialize_word(hash)

    return ()
end

要设置Cairo工具，我们使用Python虚拟环境：

1
2


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

然后，我们编译程序：

1
2
3


# compile the validate_hash.cairo file,
# writing the output to compiled.json
$ cairo-compile validate_hash.cairo --output compiled.json

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

1
2
3
4


# run the program
$ cairo-run --program=compiled.json --print_output --layout small
Program output:
  1524309693207128500197192682807522353121026753660881687114217699526941127707

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

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

1
2
3


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

验证者为什么会相信我们？嗯，我们可以证明我们知道隐藏值，该值将使程序返回该输出！

要生成证明，我们需要计算程序的哈希以生成程序事实。此哈希不依赖于输入值，因为赋值在提示内部（这是Cairo的一个怪癖，我们将在本文后面讨论）：

1
2
3


# compute the program's hash
$ cairo-hash-program --program compiled.json
0x3c034247e8bf20ce12c878793cd47c5faa6f5470114a33ac62a90b43cfbb494

计算程序事实：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15


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

# hash and output computed above
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’d的！

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17


%builtins output

from starkware.cairo.common.serialize import serialize_word

func main{output_ptr:felt*}():

    # arbitrary python code
    %{
       import os
       os.system('whoami')
    %}

    # prints 1
    serialize_word(1)

    return ()
end

1
2
3
4
5


$ 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的平方根：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18


func sqrt(n) -> (res):
    alloc_locals
    local res

    # Set the value of res using a python hint.
    %{
        import math

        # Use the ids variable to access the value
        # of a Cairo variable.
        ids.res = int(math.sqrt(ids.n))
    %}

    # The following line guarantees that
    # `res` is a square root of `n`
    assert n = res * res
    return (res)
end

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

约束不足结构

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63


%builtins output

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

# Fills `new_array` with the squares of the
# first `length` elements in `array`.
func _inner_sqr_array(array : felt*, new_array : felt*,
                                        length : felt):
    # recursion base case
    if length == 0:
        return ()
    end

    # recursive case: the first element of the new_array will
    # be the first element of the array squared
    # recall that the assert will assign to the
    # `new_array` array at position 0
    # since it has not been initialized
    assert [new_array] = [array] * [array]

    # recursively call, advancing the arrays
    # and subtracting 1 to the array length
    _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
    # allocates an arbitrary length array
    let (local res_array) = alloc()

    # fills the newly allocated array with the squares
    # of the elements of array
    _inner_sqr_array(array, res_array, length)
    return (res_array)
end

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

    # Allocate a new array.
    let (local array) = alloc()

    # Fill the new array with field elements.
    assert [array] = 1
    assert [array + 1] = 2
    assert [array + 2] = 3
    assert [array + 3] = 4

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

    # prints the array elements
    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函数以零长度调用会发生什么？

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18


func main{output_ptr : felt*}():
    alloc_locals
    # Allocate a new array.
    let (local array) = alloc()
    # Fill the new array with field elements.
    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。

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

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

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

1
2
3


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

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

1
2
3
4
5
6


# hash and output computed above
program_hash = 0x01eb05e1deb7ea9dd7bd266abf8aa8a07bf9a62146b11c0bd1da8bb844ff2479
program_output = [1, 3, 3, 7]

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

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

那么这里发生了什么？

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

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15


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

    %{  # write on the result array if the length is 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是否相等：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16


func are_equal(x, y) -> (eq):
    # sets the ap register to True or False depending on
    # the equality of x and y
    %{ memory[ap] = ids.x == ids.y %}

    # jump to the label equal if the elements were equal
    jmp equal if [ap] != 0; ap++

    # case x != y
    not_equal:
    return (0)

    # case x == y
    equal:
    return (1)
end

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10


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

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

1
2


    %{ 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)）提供证明。

那么我们如何修复它？

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21


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

    # case x != y
    not_equal:
    # we are in the not_equal case
    # so we can't have equal x and y
    if x == y:
	# add unsatisfiable assert
        assert x = x + 1
    end
    return (0)

    # case x == y
    equal:
    # we are in the equal case
    # so x and y must equal
    assert x = y
    return (1)
end

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

1
2
3
4
5
6
7


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中，使用VSCode的SARIF Viewer扩展，并在代码中查看带下划线的警告：带有带下划线死存储的Cairo代码（左）和SARIF Viewer扩展显示Amarna的结果（右）。

Amarna如何工作？

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

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

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19


class ArithmeticOperationsRule(GenericRule):
    """
    Check arithmetic operations:
        - reports ALL multiplications and divisions
        - reports ONLY addition and subtraction that
          do not involve a register like [ap - 1]
    """

    RULE_TEXT = "Cairo arithmetic is defined over a finite field and has potential for overflows."
    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）：

虽然这些规则大多数属于信息类别，但它们肯定具有安全含义：例如，未能检查函数的返回代码可能非常严重（想象一下该函数是签名验证）；错误代码规则将找到其中一些实例。

未使用参数规则将找到函数参数在它们出现的函数中未使用，这是通用编程语言linter中的常见模式；这通常表明有使用参数的意图，但从未实际使用，这也可能具有安全含义。该规则本可以在几个月前在OpenZeppelin合约中发现此错误，该错误是由于未检查的nonce（作为参数传递给execute函数）造成的。

未来计划

由于Cairo仍然是一个发展中的生态系统，枚举所有易受攻击的模式可能很困难。我们计划将来添加更多规则，并在中期/长期计划中添加更复杂的分析功能，例如数据流分析。

同时，如果你有任何易受攻击代码模式的想法，我们非常乐意审查功能请求、新规则、错误修复、问题以及来自社区的其他贡献。

Cairo静态分析工具Amarna：发现智能合约中的安全隐患

本文详细介绍Trail of Bits开源的Cairo静态分析工具Amarna，探讨Cairo语言特性、常见安全陷阱及静态分析规则，帮助开发者识别智能合约中的潜在漏洞。