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系统。

尽管这些项目主要是手动工作，我们也利用工具自动化部分分析。我们使用了一些Rust实用工具，如cargo-audit和Clippy，来发现过时的依赖和常见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位置应为