我们正在开源 Amarna，这是我们用于 Cairo 编程语言的新静态分析器和 linter（检查代码风格/错误的小工具）。 Cairo 是一种编程语言，为拥有数百万美元资产的多个交易交易所提供支持（例如由 StarkWare 驱动的 dYdX），并且是 StarkNet 合约的编程语言。但是，与其他语言不同，它也有一些奇怪的功能。因此，我们将首先简要概述该语言、其生态系统以及开发人员应注意的该语言中的一些漏洞。然后，我们将介绍 Amarna 并讨论它是如何工作的？

为什么我们需要Cairo？

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

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

总之，我们采取了以下步骤：

1.导出我们要计算的函数。

2.使用的具体输入在工作设备上运行该函数，获得结果，并生成计算有效性的证明。

3.通过验证证明来验证计算。

Cairo编程语言

如上所述，Cairo 编程模型涉及两个关键角色：运行程序并创建程序返回特定输出的证明的验证程序，以及验证验证程序创建的证明的验证程序。

然而，在实践中，Cairo 程序员实际上不会自己生成或验证证明。相反，生态系统包括以下三个部分：

1.SHARed Prover (SHARP) 是一个公共验证程序，它为用户发送的程序跟踪生成有效性证明。

2.证明验证程序合约验证程序执行的有效性证明。

3.可以查询事实注册合约来检查某个事实是否有效。

事实注册表是一个数据库，用于存储程序事实，或从程序及其输出的哈希计算的值；创建程序事实是将程序绑定到其输出的一种方法。

这是Cairo的基本工作流程：

1.用户编写程序并将其跟踪提交给 SHARP（通过 Cairo Playground 或命令 cairo-sharp）。

2.SHARP 为程序跟踪创建一个 STARK 证明，并将其提交给证明验证程序合约。

3.证明验证程序合约验证证明，如果有效，则将程序事实写入事实注册表。

4.任何其他用户现在都可以查询事实注册表合约以检查该程序事实是否有效。

还有两件事要记住：

Cairo 的内存是一次性写入的：一个值写入内存后，就无法更改。

assert语句assert a = b的行为会根据a是否被初始化而不同：如果 a 未初始化，则 assert 语句将 b 分配给 a；如果 a 被初始化，assert 语句断言 a 和 b 相等。

尽管 Cairo 的语法和关键字的细节很有趣，但我们不会在这篇文章中讨论这些主题。

设置和运行Cairo代码

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

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

然后，我们编译程序：

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

这个值就是(4242, 1)的Pedersen hash对应的字段元素。

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

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

为了生成证明，我们需要计算程序的哈希来生成程序事实。这个哈希值不依赖于输入值，因为赋值是在一个提示中进行的(这是Cairo的一个奇怪设置，我们将在本文后面讨论)：

然后，我们可以通过使用事实注册表合约并以程序事实作为输入调用 isValid 函数来检查程序事实的有效性：

调用 isValid 函数检查程序事实有效性的结果。

概括地说，我们运行了程序，SHARP创建了一个可以在事实注册表中查询的证明，以检查其有效性，证明我们确实知道将导致程序输出该值的输入。

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

Cairo功能

Cairo有几个奇怪功能，新的Cairo程序员可能还使不习惯。我们将描述三个容易被滥用并导致安全问题的 Cairo 习惯：Cairo 提示、递归和欠约束结构之间的相互作用以及非确定性跳转。

提示

提示是特殊的 Cairo 语句，基本上使验证程序能够编写任意 Python 代码。是的，以 Cairo 提示编写的 Python 代码实际上是被执行的！

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

因为 Cairo 可以在提示中执行任意 Python 代码，所以你不应该在自己的设备上运行任意 Cairo 代码，这样做可以将你的设备的完全控制权授予编写代码的人。

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

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

Underconstrained结构

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

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

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

基本上，会发生以下情况：

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的值是未知的：

按原样运行上述代码后出现的错误。

但是，请记住，通常你不会运行代码。你将验证程序输出某些值的证据。而且我实际上可以向你证明该程序可以输出你想要的任何四个值！

下面的事实将该程序与输出[1,3,3,7]绑定：

根据事实注册合同，这一事实是有效的：

事实注册表对程序事实的验证。

可以看到，由于返回的数组只是分配的，从不写入（因为它的长度为0，所以递归一开始就停止），验证程序可以在提示中写入数组，提示代码不会影响程序的哈希！

恶意的 sqr_array 函数实际上如下：

简而言之，如果有一些错误使数组的长度为0，恶意验证程序可以创建他想要的任意结果。

你可能会有疑问，恶意验证程序不能简单地在程序末尾添加一个提示来以他希望的任何方式更改输出。好吧，他可以，只要之前没有写过那个内存；这是因为 Cairo 的内存是一次性写入的，所以每个内存单元只能写入一个值。

由于Cairo中内存的工作方式，这种创建最终结果数组的模式是必要的，但它也存在安全问题的风险：跟踪该数组长度的一个简单的错误可能允许恶意验证程序任意控制数组内存。

非确定性跳跃

对于第一次阅读Cairo的程序员来说，非确定性跳跃是另一种看起来不自然的代码模式。它们结合提示和条件跳跃来重定向带有某个值的程序控制流。验证程序可以不知道这个值，因为验证程序可以在提示中设置它。

例如，我们可以编写一个程序，检查两个元素x和y是否相等，方法如下：

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

然而，这个函数实际上很容易受到恶意验证程序的攻击。注意跳跃指令如何仅依赖于提示中的值：

而且我们知道提示完全可以由验证程序控制！这意味着验证程序可以在该提示中编写任何其他代码。事实上，不能保证验证程序确实检查了 x 和 y 是否相等，甚至不能保证 x 和 y 以任何方式使用过。由于没有其他检查，该函数可以返回验证程序想要的任何内容。

正如我们之前看到的，程序哈希不考虑提示中的代码；因此，验证程序无法知道是否执行了正确的提示。恶意验证程序可以通过更改提示代码并将每个证明提交到SHARP。

那么我们如何解决这个问题呢？

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

在本例中，该函数足够简单，代码只需要一个if语句：

在审核Cairo代码时，我们注意到除了VScode中的语法高亮显示外，基本上没有任何形式的语言支持。然后，当我们在代码中发现问题时，我们希望确保类似的模式不会出现在代码库的其他地方。

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

Amarna 将其静态分析结果导出为 SARIF 格式，使我们能够使用 VSCode 的 SARIF Viewer 扩展轻松地将它们集成到 VSCode 中，并查看代码中带下划线的警告：

带有下划线的dead store（左）和显示来自 Amarna 的结果的 SARIF Viewer 扩展的 Cairo 代码（右）。

Amarna是如何工作的？

Cairo 编译器是用 Python 编写的，它使用解析工具包 lark 来定义语法并构建其语法树。使用 Lark 库，可以直接为程序的抽象语法树构建访问者。从这里开始，编写规则就是对要在树中找到的内容进行编码。

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

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

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

1.本地规则独立分析每个文件。上述用于查找文件中所有算术运算的规则是本地规则的一个示例。

2.收集规则独立地分析每个文件，并收集供后处理规则使用的数据。例如，我们有收集所有声明函数和所有调用函数的规则。

3.在分析所有文件并使用收集规则收集的数据之后，将运行后处理规则。例如，在收集规则找到文件中所有声明的函数和所有调用的函数之后，后处理规则可以通过标识声明但从未调用的函数来找到所有未使用的函数。

到目前为止，我们已经实施了 10 条规则，其影响范围从帮助我们审核代码的信息性规则（标记为 Info）到可能对安全敏感的代码模式（标记为警告）：

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

未使用的参数规则可以找到函数中没有使用的参数，这是通用编程语言linter 中的常见模式；这通常表明存在使用该参数的某种意图，但从未实际使用过，这也可能具有安全隐患。

本文翻译自：https://blog.trailofbits.com/2022/04/20/amarna-static-analysis-for-cairo-programs/如若转载，请注明原文地址