Auditing in the age of (good enough) AI

What it is

A Trail of Bits engagement report on auditing the Miden zkVM's core cryptographic library, written in the stack-machine assembly language MASM. The distinct value beyond the summary is the mechanism of the findings and the methodology reasoning — the summary names the bugs but not why they occur or why the approach was newly feasible.

The high-severity bug, mechanically

The mod_12289 procedure reduces a 64-bit value modulo 12289, taking a quotient and remainder as prover-supplied advice values (precomputed inputs pushed via a separate advice stack). The quotient is validated as a proper 64-bit value (two 32-bit limbs); the remainder is not validated before being passed to the u32overflowing_sub instruction. By jointly varying quotient and remainder so they still satisfy the subtraction's constraints, an attacker can make mod_12289 return a value that is not the true remainder — enough to forge Falcon signatures and drain any Miden account controlled by a Falcon key pair. The 400+ type-validation findings share a root cause noted in a footnote: nearly all core-library procedures are part of the public API, so third-party callers reach them without validation.

The two Lean-caught arithmetic bugs

• rotr (64-bit right-rotation): incorrect on inputs greater than the Goldilocks prime when the rotational shift is a multiple of 32.
• wrapping_mul (256-bit multiplication): dropped caller-owned values from the stack before returning.

Both were missed by the existing unit-test suite.

Why the abstract-interpretation results are trustworthy

The static analysis tracks the types of possible stack values (e.g. "32-bit integer," "unknown") and iterates to a fixpoint, always over-approximating. Because it never drops a possible case, a passing check is guaranteed to hold on every real run — soundness, not sampling. Conversely, the decompiler was deliberately restricted to a well-defined MASM subset because faithful decompilation of arbitrary hand-written MASM is intractable: procedures lack declared signatures and calling conventions, while-loops need not be stack-neutral, and conditional branches can have differing stack effects, so any analysis failure propagates up the call chain.

Methodology worth reproducing

Six months of pre-audit prep, agent-built: an LSP server + VS Code extension (working prototype in days), a decompiler (100+ AI commits over months — the reusable payoff was its IR and analysis framework, not the full pipeline), an abstract-interpretation engine with concrete passes, and a Lean executor model with an automatic MASM→Lean translator. Workflow alternated Claude (planning/development) with Codex (review); decompiler regressions were caught by diffing agent decompilations of randomized procedures against source and filing failures as regression tests. Lean proofs were validated by the kernel, so humans only audited theorem statements. The stated enabling shift: agents are now cheap enough to carry speculative side projects under light supervision — "a failed side project only costs tokens" — which previously couldn't be sold to clients in advance. Miden has adopted the static analysis engine for ongoing use.