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

我们开源了Amarna，这是我们为Cairo编程语言开发的新静态分析器和linter工具。Cairo是一种编程语言，为多个拥有数百万美元资产的交易交易所（如由StarkWare驱动的dYdX）提供支持，并且是StarkNet合约的编程语言。但与其他语言一样，它也有其奇怪的特性和陷阱。因此，我们将首先简要概述该语言、其生态系统以及开发人员应注意的一些语言陷阱。然后，我们将介绍Amarna，讨论其工作原理、它能发现什么，以及我们计划在未来实现的功能。

Cairo简介

为什么需要Cairo？

Cairo及其类似语言（如Noir和Leo）的目的是编写“可验证程序”，其中一方运行程序并创建证明，证明在给定特定输入时程序返回特定输出。

假设我们希望将程序的计算外包给某个（可能不诚实的）服务器，并需要保证结果的正确性。使用Cairo，我们可以获得程序输出正确结果的证明；我们只需要验证证明，而不是自己重新计算函数（这首先就违背了外包计算的目的）。

总结来说，我们采取以下步骤：

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

Cairo编程语言

正如我们刚才解释的，Cairo编程模型涉及两个关键角色：证明者（prover），运行程序并创建程序返回特定输出的证明；验证者（verifier），验证证明者创建的证明。

然而，在实践中，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
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19


# compute the program's hash
$ cairo-hash-program --program compiled.json
0x3c034247e8bf20ce12c878793cd47c5faa6f5470114a33ac62a90b43cfbb494
# compute program fact
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执行的！

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

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

那么如何修复它？

每当我们看到非确定性跳转时，