Axiom系统

Axiom设计了一个允许EVM应用访问历史区块链数据的系统。原生状态下，EVM合约只能访问自身当前账户状态，无法查看过去状态、交易状态或其他账户状态。为实现这一功能，Axiom使用零知识证明（ZKPs）对历史交易和状态进行简洁的灵活查询验证。具体而言，他们采用Halo2 ZKP框架，使用户能够读取并信任历史数据（如区块头、状态和交易记录）。

构建此类系统需要Axiom使用Halo2电路对以太坊数据、交易和状态等进行建模。这涉及为底层原语（如椭圆曲线密码学）以及高层数据结构（如Merkle树和以太坊区块）编写Halo2电路。由于现有Halo2电路库非常有限，许多原语必须作为Axiom的halo2-base和halo2-ecc库的一部分进行开发，并用于snark-verifier库中的SNARK递归操作。除了自定义底层库外，Axiom还使用了修改版的Halo2证明系统本身。多个Axiom电路包含对可变长度数组的证明，这些证明极大地受益于多阶段电路——该功能在Privacy & Scaling Explorations的Halo2分叉中作为实验性特性实现。

Axiom指出，自审计结束后，他们已关闭ZK协处理器产品（ZK电路最初为此设计），现在将其作为OpenVM项目的依赖项使用。OpenVM是一个模块化、高性能的基于ZK的虚拟机，允许在有限制条件下将任意Rust crate用于ZK应用。

安全评估流程

Trail of Bits密码学团队通过两次独立评估对Axiom的Halo2电路进行了审查。首次项目（2023年2月10日至5月17日）专注于底层Halo2原语（PSE的Halo2分叉），如椭圆曲线算术和哈希函数，以及部分Axiom业务逻辑。第二次审计（2023年9月11日至29日）则重点关注Axiom自首次评估后的变更/升级，并对SNARK验证逻辑进行了更深入的审查。

由于项目性质，我们的大部分工作涉及对Halo2电路的深度手动审查。幸运的是，我们的密码学团队已审查过多个使用Halo2框架的项目，因此我们维护了关于Halo2应用常见陷阱的内部笔记和文档，并在与Axiom的合作中持续利用（和更新）这些资源。有效审查该系统要求我们通过查阅文档并与Axiom工程师通过Slack和每周会议保持开放对话，深入研究Axiom系统。

尽管这些项目主要是手动工作，我们也利用工具自动化部分分析。我们使用cargo-audit和Clippy等Rust工具查找过时依赖和常见Rust问题，并使用Semgrep寻找更常见的Rust问题及Axiom特定逻辑问题。通过Semgrep，我们开发了针对Halo2的自定义分析；特别是当发现可能存在于其他位置的Halo2安全问题时，我们使用Semgrep进行变体分析以识别和修复所有类似问题。

审查Halo2的乐趣

为创建证明特定程序执行的ZKPs，必须将程序建模为ZKP系统可用的格式（电路）。Halo2（及其他如Circom、Cairo和Noir）是由ZCash团队开发的库，专门用于指定由选择性激活多项式方程（称为"门"）、充当门间"导线"的等式约束以及称为"查找"的子集包含约束组成的电路。本质上，电路是一个庞大的方程系统，每个方程是少数特定"门"方程之一，可能具有不同的常数值。这些方程中的变量代表整个计算中使用的不同值，如输入、中间值和输出。这种电路定义风格被称为"plonkish"，因为它推广了由PLoNK证明系统首次普及的门线算术电路类型。电路通常不直接计算结果，而是检查所有这些值是否与程序的正确执行匹配。完整细节更为复杂，但如果您好奇，可以查阅Halo2书籍。

ZKP电路最常见和最严重的错误类型之一是"约束不足"的正确性错误。当电路中的变量可以取多个可能值（其中一些违反电路其余部分的假设）时，该变量即为约束不足。这通常发生在直接计算被检查替代时。例如，如果在正常程序中运行x = sqrt(9)，x将始终等于一个值（通常为3）。但如果在电路中用更高效的检查替代（即不让直接计算x，而是让证明者选择某个x值，然后检查x^2 == 9），恶意证明者可以选择将x设为3或-3。有时这种灵活性不可利用，但在严重情况下，恶意证明者基本上可以生成虚假证明，执行完全错误或无效的计算，但仍生成验证为正确的ZKP。

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

有一些学习Halo2的好资源（如Halo2书籍），但这些资源存在局限性。特别是，如果您打开Halo2书籍，会注意到存在相当多的TODO项（在我们与Axiom合作时甚至更多）。除此之外，一旦开始深入研究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位置应为1外，向量中的每个元素都应为零。由于缺少约束，全零向量始终被视为正确答案，因此恶意证明者可以插入此值并创建验证为正确的不正确计算。
• TOB-AXIOM-13：两个标量乘法电路可能返回约束不足的结果。如果被利用，这可能允许恶意证明者生成被视为有效的错误标量乘法结果。这可能对使用这些操作的操作（如签名验证，即签名伪造）产生影响。
• TOB-AXIOM-19：assert_equal函数中的一个微小但灾难性的拼写错误意味着它实际上没有断言相等。本质上，该函数应该比较两个值是否相等，但它反而将第一个值与自身进行比较。这个小小的错误可能产生严重后果，因为该函数在许多关键位置（如证明验证）使用，这会破坏证明的正确性。
• TOB-AXIOMv2-3：range_check方法应该将整数值约束在特定范围内，但这通过debug_assert而不是实际约束强制执行。这意味着大值在测试期间会被捕获，但一旦部署，恶意证明者可以生成恶意值，而这不会被ZKP捕获。幸运的是，基于使用方式，这在Axiom系统中不可利用，但如果以其他方式使用可能会出现问题。

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

除了这些安全问题，我们还提出了许多我们称为代码质量的问题。这些问题本身不代表直接的安全问题，但我们仍然提出它们，因为它们要么可能导致未来的安全问题，要么代表使代码库更可读或更高效的机会。在两次评估中，我们共提出了25个代码质量问题，涉及诸如不正确注释和冗余Rust调用等问题。

建议：前进之路

当我们与Axiom合作时，他们处于开发生命周期的相当早期阶段。特别是，我们在第一个项目中审查的Halo2电路在当时刚刚开发完成，在此项目之后，Axiom继续开发了额外电路，我们在第二次评估中审查了这些电路。这就是为什么当您阅读我们的安全报告时，会看到我们的代码库成熟度评估在文档和测试等领域给Axiom提供了弱/缺失的最低评级。

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

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

总结

我们与Axiom的合作是使用Halo2构建应用程序挑战、适当保护它们所需承诺以及为什么安全审查是开发周期如此重要部分的一个很好的例子。特别是，通过在开发生命周期早期与我们接触，Axiom能够对其安全状况进行非常有影响力的长期改进。这与我们在对Ockam系统的设计审查中看到的影响非常相似。

我们再次感谢Axiom团队在这个项目上的出色工作；他们高度协作、响应迅速，并在项目完成后积极采纳我们的见解。如果您正在构建像Axiom这样的复杂密码系统并需要安全援助，请联系我们的密码学团队！