深入解析 Cairo 静态分析工具 Amarna：安全编程新利器
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 哈希函数并在控制台输出结果：
使用 Python 虚拟环境设置 Cairo 工具：
然后编译程序：
最后运行程序，将输出以下值：
该值是对应(4242, 1)的 Pedersen 哈希的域元素。
现在假设我们将输入从 4242 改为某个隐藏值，并向验证者提供以下输出：
验证者为何相信我们？我们可以证明我们知道会使程序返回该输出的隐藏值！
要生成证明，需要计算程序哈希以生成程序事实。此哈希不依赖输入值，因为赋值在提示内（Cario 的一个特性，后文讨论）：
然后可使用事实注册合约，以程序事实作为输入调用 isValid 函数来检查程序事实的有效性：调用 isValid 函数检查程序事实有效性的结果。
回顾一下，我们运行了程序，SHARP 创建了可在事实注册库中查询有效性的证明，证明我们确实知道会导致程序输出此值的输入。
现在我可以告诉你我使用的输入是 71938042130017，你可以去检查结果是否匹配。
你可以在 Cairo 区块链开发文档和 StarkWare 的这篇文章中了解更多关于此过程细节及事实注册库的信息。
Cairo 特性与易错点
Cairo 有几个可能让新 Cairo 程序员困惑的特性和易错点。我们将描述三个容易被误用导致安全问题的 Cairo 特性：Cairo 提示、递归与约束不足结构的相互作用，以及非确定性跳转。
提示
提示是特殊的 Cairo 语句，基本上允许证明者编写任意 Python 代码。是的，用 Cairo 提示编写的 Python 代码字面上是 exec 执行的！
提示写在%{ %}内。我们在第一个示例中已使用它们为输入变量赋值：
由于 Cairo 可以在提示中执行任意 Python 代码，你不应在自己的机器上运行任意 Cairo 代码——这样做可能让代码编写者获得对你机器的完全控制。
提示通常用于编写仅由证明者执行的代码。证明验证者甚至不知道提示存在，因为提示不会改变程序哈希。以下来自 Cairo playground 的函数计算正整数 n 的平方根：
程序使用提示中的 Python 数学库计算 n 的平方根。但在验证时，此代码不运行，验证者需要检查结果确实是平方根。因此，函数在返回结果前包含检查 n 是否等于 res * res。
约束不足结构
Cairo 缺乏对 while 和 for 循环的支持，迫使程序员使用传统的递归进行迭代。考虑 Cairo playground 的"动态分配"挑战。挑战要求我们编写函数，给定元素列表，将平方这些元素并返回包含这些平方元素的新列表：
运行此代码将按预期输出数字 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，为程序的任何可能输出值((0, 0), (1, 1), (0, 1), 或(1, 0))提供证明。
那么如何修复它？每当看到非确定性跳转时，我们需要确保跳转有效，验证者需要在每个标签中验证跳转：
在这种情况下，函数足够简单，代码只需要 if 语句：
Amarna：我们的 Cairo 静态分析器
在审计 Cairo 代码时，我们注意到基本上没有任何语言支持，除了 VScode 中的语法高亮。然后，当我们在代码中发现问题时，我们希望确保代码库中其他位置不存在类似模式。
我们决定构建 Amarna，一个 Cairo 静态分析器，使我们能够创建自己的规则并搜索我们感兴趣的代码模式——不一定是安全漏洞，而是任何需要分析或在审查代码时需要更多关注的安全敏感操作。
Amarna 将其静态分析结果导出到 SARIF 格式，使我们能够使用 VSCode 的 SARIF Viewer 扩展轻松集成它们，并在代码中查看带下划线的警告：带下划线死存储的 Cairo 代码（左）和显示 Amarna 结果的 SARIF Viewer 扩展（右）。
Amarna 如何工作？
Cairo 编译器使用 Python 编写，使用 lark（解析工具包）定义语法并构建其语法树。使用 lark 库，构建程序抽象语法树的访问者很简单。从这里开始，编写规则就是在树中编码你想要找到的内容。
我们编写的第一个规则是突出显示所有算术操作+、-、*和/的使用。当然，并非所有除法使用都不安全，但通过这些操作的下划线，开发者被提醒 Cairo 算术在有限域上工作，并且除法不是像其他编程语言中的整数除法。域算术下溢和溢出是开发者需要注意的其他问题。通过突出显示所有算术表达式，Amarna 帮助开发者和审阅者快速聚焦代码库中可能在这方面有问题的位置。
检测所有除法的规则非常简单：它基本上只是创建带有文件位置的结果对象并将其添加到分析结果中：
当我们寻找更复杂的代码模式时，我们开发了三类规则：
本地规则：独立分析每个文件。上述查找文件中所有算术操作的规则是本地规则的示例。
收集器规则：独立分析每个文件并收集数据供后处理规则使用。例如，我们有规则收集所有声明函数和所有调用函数。
后处理规则：在所有文件分析后运行，并使用收集器规则收集的数据。例如，在收集器规则找到文件中所有声明函数和所有调用函数后，后处理规则可以通过识别声明但从未调用的函数来找到所有未使用函数。
Amarna 发现什么？
到目前为止，我们已经实现了 10 条规则，其影响范围从帮助我们审计代码的信息性规则（标记为 Info）到潜在安全敏感的代码模式（标记为 Warning）：
虽然这些规则大多属于信息性类别，但它们肯定有安全影响：例如，未能检查函数的返回代码可能相当严重（想象如果函数是签名验证）；错误代码规则将找到其中一些实例。
未使用参数规则将找到函数参数在出现的函数中未使用，这是通用编程语言 linter 中的常见模式；这通常表明有使用参数的意图，但从未实际使用，这也可能有安全影响。该规则本可以在几个月前在 OpenZeppelin 合约中发现由于未检查 nonce（作为参数传递给 execute 函数）导致的错误。
未来规划
由于 Cairo 仍是一个发展中的生态系统，枚举所有易受攻击模式可能很困难。我们计划未来添加更多规则，并在中期/长期计划中添加更复杂的分析功能，如数据流分析。
同时，如果你有任何易受攻击代码模式的想法，我们非常乐意审查功能请求、新规则、错误修复、问题以及来自社区的其他贡献。
如果你喜欢这篇文章，请分享：TwitterLinkedInGitHubMastodonHacker News
页面内容近期文章使用 Deptective 调查依赖项系好安全带，Buttercup，AIxCC 评分轮正在进行中！使智能合约超越私钥风险成熟 Go 解析器中意外的安全陷阱我们审查首批 DKLs23 库的收获来自 Silence Laboratories 的 23 个库© 2025 Trail of Bits.使用 Hugo 和 Mainroad 主题生成。更多精彩内容 请关注我的个人公众号 公众号（办公 AI 智能小助手）公众号二维码
还未添加个人签名 2021-05-19 加入
还未添加个人简介
评论