Axiom系统架构

Axiom构建了一个允许EVM应用访问以太坊历史链数据的系统。通过Halo2框架，他们实现了对历史交易和状态的零知识证明验证，包括：

• 使用halo2-base/halo2-ecc库开发底层椭圆曲线密码学原语
• 构建Merkle树和以太坊区块等高层数据结构
• 采用PSE分叉版Halo2的多阶段电路特性处理变长数组证明
• 最终演变为支持任意Rust程序的ZK虚拟机OpenVM

安全审计方法论

审计团队通过两次深度评估（2023年2-5月，9月）采用：

1. 手动代码审查：基于内部Halo2安全笔记（含常见陷阱清单）
2. 自动化辅助：
   • cargo-audit/Clippy检查Rust依赖
   • Semgrep定制化分析工具（针对Halo2特定模式）
3. 持续知识更新：与Axiom工程师通过Slack/周会保持技术对话

Halo2审查技术要点

核心挑战

• 低层级API风险：需手动管理约束条件，易引入未约束漏洞
• 字段元素限制：所有变量均为有限域元素，需额外约束确保语义正确性（如布尔值仅0/1）
• 文档缺口：官方Halo2手册存在大量TODO项

典型陷阱案例

1
2
3
4
5
6
7

1. API不一致性：
   - `Region::assign_advice` 不创建约束
   - `Region::assign_advice_from_constant` 却会创建约束

2. 约束生效机制：
   - 复制约束需先调用`AssignedCell::copy_advice`
   - 再通过`ConstraintSystem::enable_equality`激活置换检查

关键漏洞发现

改进建议与成果

1. 测试体系强化：

   • 审计间期建立了端到端测试套件
   • 覆盖椭圆曲线边界情况（如无穷远点处理）

2. 文档规范化：

   • 修复35处代码注释错误
   • 建立约束条件追踪文档

3. 长期策略：

   • 实施Semgrep规则进行变体分析
   • 引入约束有效性证明机制

合作价值

通过早期介入的安全审计，Axiom在系统成熟度（原评估为"weak/missing"）方面实现了显著提升，包括：

• 业务逻辑测试覆盖率提升至92%
• 关键密码学操作文档完整度达100%
• 所有高危漏洞在部署前完成修复

“Trail of Bits团队在Halo2电路审查中展现了卓越的技术深度，特别是在密码学复杂领域的方法系统性，这使我们最终系统的安全性获得了质的飞跃” —— Axiom联合创始人Yi Sun