AI与密码学相遇2：AI在OpenVM的zkVM中发现了什么

这是本系列的第二篇文章。 如果你还没有阅读 关于 Cloudflare CIRCL 的第一篇文章，那篇文章提供了更多关于我们为什么进行这些实验以及我们的工作流是如何设置的背景信息。 在这篇文章中，我们将 zkao，我们的人工智能审计师，指向了 OpenVM 的 zkVM，它在其客库 openvm-pairing 中发现了一个关键的可靠性 bug，该 bug 允许恶意证明者伪造任何配对等式。 请注意，这不是 zkVM 证明系统本身的可靠性 bug；它只影响使用该易受攻击库的代码。

本文中的 bug 被分配为 CVE-2026-46669，并在 OpenVM 1.6.0 中修复。 据我们所知，所有基于 OpenVM 构建的合作伙伴都已升级到该版本。

澄清说明，与第一篇文章相同：人工智能生成了一个候选发现，而不是最终报告。 我们团队的人类随后验证了该问题，确认了可利用性，了解了完整影响和受影响的项目，并负责了披露。 在这种情况下，由于详细的报告和 zkao 自身生成的最小化 PoC，非常快速的人工分类就足以决定值得与 OpenVM 团队分享。

它是如何发生的

四个月前，作为我们人工智能实验的一部分，我们扫描了 OpenVM，这与我们最初扫描所有内容的方式相同：先是一个带简单提示的 LLM，然后是一个带我们专家维护的技能集的 LLM。 我们使用 Opus 4.6 和 Codex 5.3 运行了它。 一旦 Opus 4.7 和 Codex 5.4 发布，我们又重新运行了它们。 候选发现都是有效的观察结果，模型自信地将其中几个标记为严重或高，但没有一个是真正可利用的。

我们的假设是，对于一个简单的 LLM 设置来说，一个 zkVM 过于复杂，无法处理 30 万个 token 甚至 100 万个 token 的上下文。 模块之间的依赖关系比典型库中密集得多。 密码学库通常可以并行审计，只需将每个子代理分配给一个映射到单个密码原语的文件夹。 每个子代理读取少量代码行，只应用相关技能，将发现写入一个 markdown 文件，然后主代理将这些文件拼接在一起。 所有这些都可以使用流行的代理编码工具（如 Claude Code 和 Codex）开箱即用，几乎不需要人工引导。

这种方法不适用于更复杂的基础代码库，比如 OpenVM。 在那里，除了低垂的果实，子代理的有用输出不是 bug 列表。 你可以有一个可证明安全的模块 A 和一个可证明安全的模块 B，但它们的组合仍然不安全。 因此，在这种“隔离”模式下寻找 bug 无法捕获有意义的 bug。 相反，子代理的输出应该是关于一个模块的 知识：它假设了什么，它委托给调用者什么，以及它默默依赖的不变量是什么。 然而，良好地表示这种输出是困难的部分。 太短会忽略 bug 实际所在的实现细节。 太长会在与其他信息结合之前溢出主代理的上下文。 根据我们所看到的，至少在撰写本文时，上述代理编码工具并没有有效解决这个问题。

考虑到这个假设，我们决定在 OpenVM 上运行 zkao，尽管我们这些实验的原始规则是只有在普通 LLM 已经发现一个真正的 bug 之后才运行 zkao。 我们在 zkao 的上下文工程上花费了大量时间，并将我们自己的专家的工作方法编码为可重用的流程来寻找漏洞，所以它似乎是针对这种情况的正确工具。 经过九个多小时的扫描，它返回了许多发现。 与之前的实验类似，我们没有时间深入检查每个发现。 经过快速筛选后，一个发现立即脱颖而出：在其中一个客库中配对检查的关键可靠性 bug。 我们的假设成立，数月的努力得到了回报！

虽然只有一个 bug 要分享，但为了与第一篇文章保持一致，以下是该 bug 的概览。

严重性和修复概览

这次，AI 严重性和维护者严重性一致。

Bug 1：openvm-pairing 配对检查缺少对缩放因子的适当子域检查

背景

配对是 Groth16、带 KZG 的 PLONK 以及 BLS 签名背后的引擎。 在所有这些协议中，验证者通常不是询问一个配对值。 而是询问配对的乘积是否等于 1：

∏ie(Pi,Qi)=1。

根据这个是或否的答案，验证者得出结论，SNARK 证明有效，KZG 打开正确，或签名验证通过。 因此，如果证明者可以使一个假的配对乘积看起来为 1，那么构建在其上的所有东西都不再可靠。

配对是一个双线性映射

e:G1×G2→GT，

其中 G1、G2、GT 是阿贝尔群。在我们的例子中，G1 和 G2 是椭圆曲线群，GT 是 Fp12∗ 的一个乘法子群。

配对最重要的性质是双线性：

e([a]P,[b]Q)=e(P,Q)ab。

这就是配对有用的原因，但我们实际上不需要这个性质来理解这个 bug。所以你可以忽略它。

计算配对 e(P,Q) 有两个主要步骤（除了 Weil 配对）。

第一步是米勒循环。 它计算一个米勒函数 fr,Q(P)，为了简单起见，我们可以将其视为一个黑盒。 此阶段输出 Fp12∗ 中的一个元素。 对于多个配对的乘积，电路可以运行所有米勒循环并将它们的输出相乘。 让我们称那个组合输出为 f，即 f=∏ifr,Qi(Pi)。

问题是，f 还不是配对乘积。 它只是等价类 Fp12∗/(Fp12∗)r 的一个代表。 这是来自 Novakovic 和 Eagen 的 论文 的主要观察之一：米勒循环输出仅在乘以一个 r 次幂的意义上是唯一的。 换句话说，每当存在非零的 c 使得 f1=f2⋅cr 时，f1 和 f2 代表相同的配对值。 那个未确定的因子 c 正是使直接等式检查变得棘手的原因。

这就是为什么 第二步 存在的原因。最终指数运算将 f 提升到

h=p12−1r。

这消除了歧义，因为对于每个非零 c，我们有：

(f⋅cr)h=fh⋅cp12−1=fh。

最后一项消失，因为 Fp12 中每个非零元素都满足 xp12−1=1。 在这个指数运算之后，结果落在 GT 中，即 r 次单位根群。 所以真正的配对乘积检查是：

fh=1。

问题在于指数 h 在电路内部计算成本太高，而让证明者在电路外部计算 c 并作为提示传入则是可以的。 检查 f=cr 比计算 fh 指数运算要便宜得多。 因此，为了证明 ∏ie(Pi,Qi)=fh=1，证明者不需要直接计算 fh，只需要提供一个非零的 c 满足 f=cr，这正好在 fh=1 时成立。

这就是优化背后的核心思想。 OpenVM 使用来自 Novakovic 和 Eagen 的 论文 的残差-见证技巧来实现这一点：证明者提供几个额外值，电路检查一个便宜的方程，而不是运行完整的指数运算。

实际的优化方程与 f=cr 略有不同：

f⋅u=cλ ∧ udi=1

这里 λ=m⋅r 是一个曲线特定的指数，其结构允许电路通过 Frobenius 映射便宜地计算 cλ，而 u 被称为缩放因子。 在 OpenVM 代码中，对于 BN254 这个缩放因子被称为 u，对于 BLS12-381 被称为 s。 其余符号是 d=gcd(m,h) 和 i=vd(h)。

需要缩放因子是因为 λ 与原始的 r-残差检查并不完美对齐。 论文的定理 3 通过要求缩放因子满足一个小单位根关系来弥合这一差距，即上面的 udi=1 条件。

对于这些特定的曲线，论文给出了一条更便宜的路径：不是直接检查 udi=1，而是足以将缩放因子限制在适当的子域 Fp6⊂Fp12 中。 而这个检查非常便宜。 OpenVM 将一个 Fp12 元素存储为六个 Fp2 系数：

[c0,c1,c2,c3,c4,c5]。

位于 Fp6 子域意味着奇数索引的系数为零：

c1=c3=c5=0。

因此，整个安全关键的子域测试只是三个等式检查。

Bug

回顾检查的形式。 电路有一个组合的米勒循环输出 f，并且只有当配对乘积在经过最终指数运算后变为 1 时才应接受。 OpenVM 通过检查优化关系避免了那个昂贵的指数运算：

f⋅u=cλ。

但这个关系只有在 u 被限制在正确子域时才正确。 OpenVM 只检查了提示 c 非零，然后就没有了。 它没有检查缩放因子是否在 Fp6 中。 以下是修复前的 BLS12-381 代码路径：

// guest-libs/pairing/src/bls12_381/pairing.rs
let (c, s) = Self::pairing_check_hint(P, Q);
// ... 没有检查 s 是否在 Fp6 中 ...
let c_conj = c.conjugate();
if c_conj == Fp12::ZERO {   // 仅拒绝 c == 0
    return None;
}

BN254 有 相同的模式，只是用了 if c == Fp12::ZERO { return None; }。 因此，电路拒绝零 c，但接受任何缩放因子。

此时，优化方程不再证明真正的配对检查。 对于任何米勒输出 f，即使是来自虚假配对等式的输出，证明者可以设置：

c=1, u=f−1。

那么 cλ=1，被检查的关系变为：

f⋅f−1=1=cλ。

检查通过。 相同的替换在两条曲线上都有效：BN254 上 c=1,u=f−1，BLS12-381 上 c=1,s=f−1。

通常 f−1 是一个完整的 Fp12 元素，而不是 Fp6 子域的元素。这正是子域检查会拒绝该伪造的原因。

还有一个细微的控制流细节。 因为优化例程返回成功，所以将执行完整最终指数运算的较慢回退路径永远不会被触发。

影响

伪造任意配对检查破坏了众多事物所依赖的密码学基础：

• 在 BLS12-381 上，证明者可以伪造 KZG 打开证明，这破坏了数据可用性、 blob 验证以及 PLONK 或 KZG 验证器背后的多项式承诺方案。
• 在 BN254 上，同样的伪造破坏了 Groth16 SNARK 验证器、BLS 签名检查以及任何依赖配对等式的桥接或协议。
• 任何通过 OpenVM 的配对检查模拟以太坊地址 0x08 的 ecPairing 预编译的 zkVM 客程序都会产生伪造的结果，导致不正确的 EVM 执行。

因此，任何在 OpenVM 客程序内部验证配对的 L2 Rollup、桥接或隐私协议都继承了该问题。 zkao 将其评为严重，OpenVM 维护者确认其为严重。

修复

修复方法是添加缺失的子域成员资格测试。它断言缩放因子的奇数索引系数为零：

// 只有缩放因子位于子域 Fp6 时，它才是一个诚实的提示
for i in [1, 3, 5] {
    if s.c[i] != Fp2::ZERO {
        return None;
    }
}

像 f−1 这样的缩放因子通常具有非零的奇数系数，因此它被拒绝，伪造消失。 该修复位于提交 a720e2c 中，并在 OpenVM 1.6.0 中发布。

我们学到的一些东西

一个简单的 LLM 在一个复杂代码库上仍然会遇到瓶颈。 这是我们开头所做的观察，实验证实了这一点：在两个模型代次中，普通 LLM 传递在 OpenVM 上产生的发现全部被分类为信息性。 原因如上所述。 一个 zkVM 不像库那样可以分解为独立的原语，因此代理必须向上传递的工作单元是 关于一个模块的知识，而这确实难以表示。

缩小这一差距正是 zkao 上下文工程的大部分内容，我们通过启发式方法（编码我们专家在许多过去手动审计中如何实际阅读代码）和系统化方法（工具如何在代理之间移动信息而不会溢出任何单个上下文窗口）来处理它。 zkao 通过一个名为 cryptopsy 的流程发现了这个 bug。 我们将把这个流程如何工作的细节留给未来的博客文章，但基本上它结合了综合分析以及在实现与背后的学术文献（已知攻击、陷阱、密码分析结果等）之间的来回验证。 这模拟了我们手动审计过程的一小部分。

分类不能仅仅要求 LLM 生成一个可工作的 PoC。 我们最早尝试自动化分类的方法之一是询问 LLM 是否可以将自己的报告转换为可工作的 PoC。 想法很简单：如果 PoC 运行，则 bug 是真实的。 在实践中，该信号实际上比看起来弱得多。 模型非常擅长生成通过的 PoC，即使报告的问题不是真实的。 足够多的无意义注释、隐藏假设、打补丁的辅助函数、禁用的检查、模拟的状态以及可疑的运行标志可以使几乎任何利用看起来成功。 验证这些 PoC 最终花费的时间比分类原始报告还要多。 这就是为什么此后我们在 zkao 上投入了大量时间，并改进了其分类过程以减少误报。 在另一篇文章中，我们将讨论我们如何实现这一点，以及 zkao 如何从分类 bug 的用户那里学习，从而在项目中的前几次分类后进一步减少误报。

下一步

感谢 OpenVM 团队，他们快速分类并修复了此问题，并在 1.6.0 中发布了修复。 我们感谢 Axiom 联合创始人 Yi Sun 对这篇博客文章的宝贵反馈。 在此报告之后，我们与 OpenVM 团队合作，为 OpenVM 2.0 版本进行了更有针对性的参与。zkao 在那里发现了额外的高影响问题，一旦细节准备好分享，我们将在未来的博客中撰写这些内容。

这是本系列的第二篇文章。随着其他项目的确认 bug 得到解决，我们将继续发布，特别是当它们教会我们一些有用的东西时：人工智能审计在哪些地方有效，哪些地方仍然失败，以及需要什么样的人工审查。

如果你维护一个 zkVM 或密码学项目，并且对此感兴趣，我们非常乐意与你一起研究，以便在严重 bug 发布之前发现并修复它们。 这种持续的 AI 覆盖正是 zkao 的构建目标。 请通过 zksecurity.xyz/contact 联系我们。

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