Axiom Halo2 电路深入研究

在我们密码学团队审查的众多高度复杂、前沿的项目中，2023 年的一个项目脱颖而出。经过 两 次 审计，我们审查了由 Axiom 开发的一个区块链系统，该系统允许计算以太坊的整个历史记录，所有这些都通过链上的零知识证明 (ZKP) 进行验证，使用 ZK 验证的椭圆曲线和 SNARK 递归操作。该系统是使用 Halo2 框架构建的——一种复杂、新兴的技术，在构建安全应用程序时提出了许多挑战，包括由其底层 API 导致的潜在的约束不足问题。

自从我们的审计结束以来，这个库已经被重新用于 Axiom 更通用的 OpenVM 产品，这是一个 ZK 虚拟机，允许为任意 Rust 程序生成 ZK 证明。

这篇文章提供了我们审查过程的见解；发现的结果，包括几个可能破坏系统安全性的可靠性和约束不足的错误；以及 Axiom 在采纳我们的建议后所采取的步骤。由于 Axiom 系统的庞大规模和 Halo2 框架的新颖性，这次审计大大增强了我们已经广泛的 ZKP 系统测试知识。我们赞赏 Axiom 如此积极地合作，并努力与我们合作以确保他们的系统安全。

“在审查我们的 Halo2 电路时，Trail of Bits 团队的技术严谨性和安全意识给我们留下了深刻的印象。他们在审查过程中系统而周到，尤其是在我们系统中更复杂的密码学领域，这让我们对最终的系统安全性更有信心。”——Axiom 联合创始人 Yi Sun

Axiom 系统

Axiom 设计了一个系统，允许访问 EVM 应用程序的历史区块链数据。EVM 合约本身只能访问它们自己的当前账户状态；它们无法查看过去的状态、交易状态或其他账户的状态。为了实现这种访问，Axiom 使用 ZKP 简洁地验证了对历史交易和状态的灵活查询。具体来说，他们使用 Halo2 ZKP 框架允许用户读取和信任历史数据，例如 headers、状态和交易。

为了构建这样一个系统，Axiom 必须使用 Halo2 电路对以太坊数据、交易、状态等进行建模。这需要为底层 primitives 编写 Halo2 电路，例如椭圆曲线密码学，以及更高级别的数据结构，如 Merkle 树和以太坊区块。由于现有的 Halo2 电路库非常有限，因此许多这些 primitives 必须作为 Axiom 的 halo2-base 和 halo2-ecc 库的一部分进行开发，并在 snark-verifier 库中用于 SNARK 递归。除了自定义的底层库之外，Axiom 还使用了修改版的 Halo2 证明系统本身。一些 Axiom 电路包括关于可变长度数组的证明，这些数组从多阶段电路中受益匪浅，这些电路在 Privacy & Scaling Explorations 的 Halo2 分支中作为一项实验性功能实现。

Axiom 已经指出，自从审计结束以来，他们已经关闭了 ZK 协处理器产品（最初 ZK 电路是为该产品设计的），并且 Axiom 现在将它们用作 OpenVM 项目 中的依赖项，OpenVM 是一个模块化且高性能的基于 ZK 的虚拟机，允许在 ZK 应用程序中使用 arbitrary Rust crates，但有一些限制。

安全评估过程

Trail of Bits 密码学团队致力于通过两次单独的评估来审查 Axiom 的 Halo2 电路。我们的 第一个项目 从 2023 年 2 月 10 日到 5 月 17 日进行，重点关注底层的 Halo2 primitives (PSE 的 Halo2 分支)，例如椭圆曲线算术和哈希函数，以及 Axiom 的一些业务逻辑。第二次审计 从 2023 年 9 月 11 日到 9 月 29 日进行，重点关注 Axiom 从第一次评估中所做的更改/升级，以及对 SNARK 验证逻辑的更深入审查。

由于这些项目的性质，我们的大部分工作都包括对 Halo2 电路进行深入的手动审查。幸运的是，我们的密码学团队已经审查了多个使用 Halo2 框架的项目，因此我们维护了内部笔记和文档，其中包含与 Halo2 应用程序相关的尖锐问题和常见陷阱，我们在与 Axiom 的整个项目中不断利用（和更新）这些笔记和文档。为了有效地审查这个系统，我们需要通过审查他们的文档并通过 Slack 和每周的电话会议与 Axiom 工程师保持公开对话来广泛地研究 Axiom 系统。

即使这些项目主要是手动工作，我们也利用工具来自动化我们的一些分析。我们使用了一些 Rust 实用程序工具，如 cargo-audit 和 Clippy 来查找过时的依赖项和常见的 Rust 问题，并且我们使用 Semgrep 来查找更常见的 Rust 问题和 Axiom 特定的逻辑问题。通过使用 Semgrep，我们已经能够开发针对 Halo2 的自定义分析；具体来说，当我们识别出一个可能出现在其他位置的 Halo2 安全问题时，我们使用 Semgrep 来执行变体分析并识别和修复所有类似的问题。

审查 Halo2 的乐趣

为了创建能够证明特定程序执行的 ZKP，必须以 ZKP 系统可以使用的格式（电路）对程序进行建模。Halo2（以及其他如 Circom、Cairo 和 Noir）是由 ZCash 团队开发的库，它可以让你做到这一点；具体来说，它允许你指定由有选择地激活的多项式方程（称为“gates”）、充当这些 gates 之间“wires”的相等约束以及被称为“lookups”的子集包含约束组成的电路。从本质上讲，你的电路是一个巨大的方程组，其中每个方程都是几个特定的“gate”方程之一，可能具有不同的常数值。这些方程中的变量代表整个计算过程中使用的不同值，例如你的输入、中间值和输出。这种电路定义风格被称为“plonkish”，因为它概括了 PLoNK 证明系统首先推广的 gates-and-wires 算术电路类型。电路通常不是直接计算结果，而是检查所有这些值是否与程序的正确执行相匹配。完整的细节要复杂得多，但是如果你感到好奇，可以查看 Halo2 book。

对于 ZKP 电路来说，最常见和最严重的错误类别之一被称为“约束不足”的可靠性错误。当电路中的一个变量可以采用多个可能的值时，该变量就会受到约束不足的影响，其中一些值违反了电路其余部分的假设。当直接计算被检查替换时，通常会发生这种情况。例如，如果你在普通程序中运行 x = sqrt(9)，则 x 将始终等于一个值，通常为 3。但是，如果你在电路中用更有效的检查来替换它（即，不直接计算 x，而是让 prover 为 x 选择某个值，然后检查 x^2 == 9），那么恶意的 prover 可以选择将 x 设置为 3 或 -3。有时，这种灵活性是不可利用的——但是在严重的情况下，恶意的 prover 本质上可以生成伪造的证明，在这些证明中，他们执行非常不正确或无效的计算，但是他们仍然会生成一个验证为正确的 ZKP。

Halo2 提供了一个非常底层的 API 来定义电路。这允许团队开发自定义的约束集，从而可以针对其特定需求进行优化，并为生成 ZKP 实现更好的性能。但是，这是一把双刃剑，因为每种类型的约束也会引入新的风险，并且不同约束的相互作用会使引入安全漏洞变得更加容易。我们尤其在具有不同类型数据的电路中发现了“约束不足”的错误。由于 Halo2 电路中的每个变量都是一个有限域元素，因此实现者需要处理许多额外的约束，以确保变量具有更受限制的值集——例如，表示真值的变量仅为 0 或 1。由于每个约束都很昂贵，因此实现者会尽量避免冗余约束，但是有时可以跳过约束的原因分散在十几个文件和数千行代码中，并且错误可能非常难以察觉。

有一些很好的资源可以用来学习 Halo2，例如 Halo2 book，但是这些资源存在局限性。特别是，如果你打开 Halo2 book，你会注意到存在很多 TODO (在我们与 Axiom 合作时，TODO 的数量甚至更多)。除此之外，一旦你开始深入研究 Halo2，你会很快注意到有很多尖锐的问题，这就是为什么我们觉得需要维护内部文档和 Halo2 使用指南。为了让你对此有所了解，以下是从我们的内部文档中提取的几个注意事项：

• API 符号可能不一致。特别是，Region::assign_advice 不会创建约束，但是 Region::assign_advice_from_instance 和 Region::assign_advice_from_constant 会创建约束。如果你将这些混淆，并认为 Region::assign_advice 分配了一个约束，那么你可能引入了一个严重的欠约束的错误。

• 正确的约束需要多次 API 调用。复制约束（允许你复制电路中的值）是通过调用 AssignedCell::copy_advice 引入的。但是，要实际强制执行复制约束，你需要使用对 ConstraintSystem::enable_equality 的调用来为给定的列启用置换检查。

我们有一个类似于这些的完整注意事项列表。请记住，对 Halo2 的工具支持非常有限，因此验证所有这些细微之处主要是一个手动过程。

主要发现

我们对 Axiom Halo2 电路的两次安全评估总共发现了 35 个安全问题。其中，有四个是高危漏洞，与可靠性或约束不足问题有关，可能会完全破坏系统的安全性。以下是这四个问题的快速摘要：

• TOB-AXIOM-3: idx_to_indicator 电路受到约束不足的影响。该电路应该输出一个全零和一的向量，其中向量中的每个元素都为零，除了 idx 的位置，该位置应该为一。由于缺少约束，全零向量将始终被视为正确的答案，因此恶意的 prover 可以插入该值并创建经验证为正确的错误计算。

• TOB-AXIOM-13: 两个标量乘法电路可能会返回约束不足的结果。如果被利用，这将允许恶意的 prover 生成将被视为有效的错误标量乘法结果。这可能会对使用这些操作的操作（例如签名验证（即，签名伪造））产生影响。

• TOB-AXIOM-19: assert_equal 函数中的一个小的但具有灾难性的拼写错误意味着它实际上并没有断言相等。从本质上讲，该函数应该比较两个值是否相等，但是它改为将第一个值与其自身进行比较。这个小错误可能会产生巨大的后果，因为该函数在许多关键位置使用，例如证明验证，并且会破坏证明的可靠性。

• TOB-AXIOMv2-3: range_check 方法应该将一个整数值约束为低于某个范围，但是这是通过 debug_assert 而不是实际约束来强制执行的。这意味着在测试期间会捕获大值，但是一旦部署，恶意的 prover 可能会生成恶意值，并且 ZKP 不会捕获这些值。幸运的是，根据它的使用方式，它在 Axiom 系统中是不可利用的，但是如果它以其他方式使用，可能会出现问题。

其他值得注意的发现包括对椭圆曲线运算中无穷远点等极端情况的不正确处理，以及可能引入系统漏洞的危险假设区域。

除了这些安全问题之外，我们还提出了一些我们称之为代码质量问题的问题。这些问题本身并不代表直接的安全问题，但是我们仍然提出它们，因为它们可能会导致以后的安全问题，或者代表了使代码库更具可读性或效率的机会。在两次评估中，我们总共提出了 25 个与诸如不正确的注释和冗余的 Rust 调用等问题相关的代码质量问题。

建议：前进的道路

当我们与 Axiom 合作时，他们正处于开发的早期阶段。特别是，我们在第一个项目中审查的 Halo2 电路在当时才刚刚开发出来，并且在这个项目之后，Axiom 继续开发其他电路，我们在第二次评估中对其进行了审查。这就是为什么当你阅读我们的安全报告时，你会看到我们的代码库成熟度评估给 Axiom 在诸如文档和测试等领域中最低的薄弱/缺失评级。

虽然文档和测试对于任何安全关键项目都是必不可少的，但在处理具有许多尖锐问题的底层复杂框架（例如 Halo2）时尤其如此。测试和文档对于一些原因是最重要的，例如更好的可读性/可审计性，防止回归以及确认预期的行为。这就是为什么在我们两次评估之后，我们都向 Axiom 提出了长期性的战略性建议，以改善他们的测试和文档，以及修复我们报告的 35 个问题的建议。

我们很高兴看到 Axiom 听取了这些建议，并在两个方面都做出了重大改进。他们在我们的第一次和第二次评估之间开发了一个端到端测试套件，并在完成两次审计后扩展了测试套件。

总结

我们与 Axiom 的合作是使用 Halo2 构建应用程序所面临的挑战、正确保护它们所需的承诺以及为什么安全审查是开发周期中如此重要的组成部分的绝佳示例。特别是，通过在开发生命周期的早期与我们互动，Axiom 能够对其安全状况进行非常有影响力的长期改进。这与我们在 对 Ockam 系统进行设计审查时 看到的的影响非常相似。

我们再次感谢 Axiom 团队为该项目所做的出色工作；他们非常乐于合作、反应迅速，并在我们的项目完成后积极采纳了我们的见解。如果你正在构建像 Axiom 这样的复杂密码系统，并且需要安全方面的帮助，请 联系 我们的密码学团队！

• 原文链接： blog.trailofbits.com/202...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～