AI 감사 도구, OpenVM ZkVM서 심각한 취약점 발견

This is the second post in the series. In case you have not read the first one on Cloudflare's CIRCL , it has more context on why we run these experiments and how our pipeline is set up. In this post, we pointed zkao , our AI auditor, at OpenVM's zkVM , and it found a critical soundness bug in its guest library openvm-pairing that lets a malicious prover forge any pairing equality. Note that this is not a soundness bug in the zkVM's proving system itself; it only affects code that uses the vulnerable library. The bug in this post was assigned CVE-2026-46669 and fixed in OpenVM 1.6.0. As far as we know, all partners building on OpenVM have since upgraded to that version. Note Clarification , same as in the first post: the AI produced a candidate finding, not a final report. Humans on our team then validated the issue, confirmed exploitability, understood the full impact and affected projects, and handled disclosure. In this case, a very quick manual triage was enough to decide it was worth sharing with the OpenVM team, thanks to the detailed report and a minimal PoC that zkao produced itself. How it happened Four months ago, we scanned OpenVM as part of our AI experiment, the same way we scan everything at first: an LLM with a simple prompt, and then an LLM with our expert-maintained skills. We ran it with Opus 4.6 and Codex 5.3. As soon as Opus 4.7 and Codex 5.4 came out, we ran them again. The candidate findings were all valid observations, and the models confidently labeled several of them as Critical or High, but none of them were actually exploitable. Our hypothesis was that a zkVM is simply too complex for a naive LLM setup to handle with 300K tokens or even 1M tokens of context. The dependencies between modules are far denser than in a typical library. A cryptography library can often be audited in parallel by simply handing each subagent a folder that maps to a single cryptographic primitive. Each subagent reads a small number of lines, applies only the relevant skills, writes its findings to a markdown file, and the main agent stitches those files together. All of this happens out of the box with popular agentic coding tools such as Claude Code and Codex, with little human steering. That approach does not transfer to a more complex codebase, like OpenVM. There, except for the low-hanging fruit, a subagent's useful output is not a list of bugs. You can have a provably secure module A and a provably secure module B whose composition is still not secure. So, hunting for bugs in that "isolated" mode cannot catch meaningful bugs. Instead, a subagent's output should be knowledge about a module: what it assumes, what it delegates to its callers, and what invariant it is silently relying on. However, representing that kind of output well is the hard part. Too short and it skips the implementation detail that the bug actually sits on. Too long and it overflows the main agent's context before it can be combined with anything else. From what we have seen, at least at the time of writing, this problem is not solved efficiently by the agentic coding tools mentioned above. With that hypothesis in mind, we decided to run zkao on OpenVM, even though our original rule for these experiments was to run zkao only after the plain LLMs had already found a real bug. We have spent a lot of time on context engineering for zkao, and we have encoded the working methods of our own experts into it as reusable flows for finding vulnerabilities, so it seemed like the right tool for exactly this situation. After more than nine and a half hours of scanning, it returned many findings. Similar to the prior experiment, we did not have time to go over every finding in depth. After a quick pass, one stood out immediately: a critical soundness bug in the pairing check in one of the guest libraries. Our hypothesis held up, and months of effort had paid off! Although there is only one bug to share, to stay consistent with the first post, here is the bug at a glance. Severities and fixes at a glance # Bug AI severity OpenVM severity Fix commit Found by 1 openvm-pairing pairing check missing proper subfield check on scaling factor Critical Critical a720e2c zkao This time, the AI severity and the maintainer severity agree. Bug 1: openvm-pairing pairing check missing proper subfield check on scaling factor Background Pairings are the engine under Groth16, PLONK with KZG, and BLS signatures. In all of these protocols, the verifier is usually not asking for one pairing value. It is asking whether a product of pairings is one: $$ \prod_i e(P_i, Q_i) = 1. $$ From that one yes-or-no answer, a verifier concludes that a SNARK proof is valid, that a KZG opening is correct, or that a signature verifies. So if a prover can make a false pairing product appear to be one, everything built on top of it is no longer sound. A pairing is a bilinear map $$ e : G_1 \times G_2 \to G_T, $$ where $G_1, G_2, G_T$ are abelian groups. In our case, $G_1$ and $G_2$ are elliptic-curve groups and $G_T$ is a multiplicative subgroup of $\mathbb{F}_{p^{12}}^{*}$. The most important property of pairing is bilinearity: $$ e([a]P, [b]Q) = e(P, Q)^{ab}. $$ This is why pairings are useful, but we will not actually need this property to understand the bug. So you can just ignore it. Computing a pairing $e(P, Q)$ has two main steps (except for Weil pairing). The first step is the Miller loop. It evaluates a Miller function $f_{r, Q}(P)$, which we can just view as a black box for simplicity. This stage outputs an element in $\mathbb{F}_{p^{12}}^{*}$. For a product of pairings, the circuit can run all the Miller loops and multiply their outputs together. Let us call that combined output $f$, i.e. $f = \prod_i f_{r, Q_i}(P_i)$. The catch is that $f$ is not the pairing product yet. It is only one representative of the equivalence class $\mathbb{F}_{p^{12}}^{*} / (\mathbb{F}_{p^{12}}^{*})^r$. This is one of the main observations from Novakovic and Eagen's paper : Miller-loop outputs are unique only up to multiplication by an $r$-th power. In other words, $f_1$ and $f_2$ stand for the same pairing whenever there is a non-zero $c$ with $f_1 = f_2 \cdot c^r$. That undetermined factor $c$ is what makes a direct equality check tricky. That is why the second step exists. The final exponentiation raises $f$ to $$ h = \frac{p^{12} - 1}{r}. $$ This removes the ambiguity, because for every non-zero $c$, we have: $$ (f \cdot c^r)^h = f^h \cdot c^{p^{12}-1} = f^h. $$ The last term disappears because every non-zero element of $\mathbb{F}_{p^{12}}$ satisfies $x^{p^{12}-1} = 1$. After this exponentiation, the result lands in $G_T$, the group of $r$-th roots of unity. So the real pairing-product check is: $$ f^h = 1. $$ The problem is that the exponent $h$ is far too expensive to raise to inside the circuit, while it is fine to let the prover compute $c$ outside the circuit and pass it in as a hint. Checking $f = c^r$ is much cheaper than computing the $f^h$ exponentiation. So to prove $\prod_i e(P_i, Q_i) = f^h = 1$, instead of computing $f^h$ directly, the prover only needs to provide a non-zero $c$ with $f = c^r$, which holds exactly when $f^h = 1$. This is the core idea behind the optimization. OpenVM implements it with the residue-witness trick from Novakovic and Eagen's paper : the prover supplies a few extra values and the circuit checks a cheap equation instead of running the full exponentiation. The actual optimized equation is slightly different from $f = c^r$: $$ f \cdot u = c^{\lambda} \wedge u^{d^i} = 1$$ Here $\lambda = m \cdot r$ is a curve-specific exponent whose structure lets the circuit evaluate $c^\lambda$ cheaply through the Frobenius map, and $u$ is called the scaling factor. In the OpenVM code this scaling factor is called u for BN254 and s for BLS12-381. The remaining symbols are $d = \gcd(m, h)$ and $i = v_d(h)$. The scaling factor is needed because $\lambda$ does not line up perfectly with the original $r$-residue che