Auditing in the age of (good enough) AI
AI-assisted tooling built for the Miden zkVM uncovered a high-severity Falcon signature forgery flaw and produced 95 Lean correctness proofs. Trail of Bits used AI agents to build an LSP server, decompiler, static analysis engine, and Lean model for the Miden VM. The static analysis found a high-severity flaw in mod_12289 enabling Falcon signature forgery and fund theft. Formal modeling produced 95 correctness proofs and found two additional bugs.
Detection / Hunteropenrouter
Immediate Actions
- Patch the
mod_12289procedure to validate the remainder before use. - Audit all prover-supplied advice values in Miden core library procedures.
Key Takeaways
- High-severity flaw in
mod_12289allows malicious provers to forge Falcon signatures. - AI agents built an LSP server, decompiler, and static analysis engine for MASM.
- Lean formal verification produced 95 machine-checked correctness proofs.
- Formal modeling found two bugs missed by unit tests:
rotrandwrapping_mul. - Static analysis identified over 400 locations needing type validation improvements.
Attack Chain
- Initial Access: Attacker acts as a malicious prover interacting with the Miden VM.
- Execution: Attacker supplies underconstrained advice values (quotient and remainder) to the
mod_12289procedure. - Bypass: The remainder bypasses validation before being passed to
u32overflowing_sub. - Impact: Attacker forges Falcon signatures and drains funds from Miden accounts.
Affected Systems
- Miden VM
- Miden core library
- Falcon signature implementation in Miden
Detection Availability
No detection rules or queries are published in the source article.
Detection Engineering Assessment
Hypotheses are starting points derived from the article, not findings about your environment; validate against your own telemetry.
| Dimension | Rating | Rationale |
|---|---|---|
| EDR Visibility | None | The vulnerability is in cryptographic code logic, not endpoint malware behavior. |
| Network Visibility | None | Exploitation occurs within the VM execution logic, not via network traffic. |
| Detection Difficulty | Hard | Requires understanding of Miden assembly and zero-knowledge proof internals to detect. |
Hunting Hypotheses
| Hypothesis | Telemetry | Stage | FP Risk |
|---|---|---|---|
Hunt for Miden transactions where prover-supplied advice values to mod_12289 produce unexpected remainders. | Miden VM execution traces | Execution | Medium — requires custom VM instrumentation to monitor. |
Required Log Sources
- Miden VM execution logs
- Miden transaction logs
Key Behavioral Indicators
- Prover-supplied remainder values in
mod_12289bypassing validation. - Falcon signature verification succeeding with anomalous
mod_12289outputs.
Control Gaps
- Standard EDR products lack visibility into Miden VM execution.
- Network monitoring cannot inspect cryptographic proof logic.
False Positive Assessment
Low — The vulnerability is specific to the mod_12289 procedure and requires precise conditions.
Recommendations
Suggestions to evaluate against your own environment, tooling, and incident-response procedures — not directives.
Infrastructure Hardening
- Deploy the updated Miden static analysis engine in CI/CD pipelines.
- Integrate the MASM linter into the Miden VM build process.
User Protection
- Rotate Falcon key pairs for Miden accounts if exploitation is suspected.
Plain-Language Summary
Security researchers used AI to build custom tools for reviewing the Miden virtual machine, a new system for privacy-preserving computations. These tools found a serious flaw where an attacker could forge digital signatures and steal funds. The AI also generated mathematical proofs confirming that many core parts of the system work correctly. Organizations using Miden should ensure they have applied fixes for these identified issues.
Additional IOCs
- File Paths:
falcon512_poseidon2.masm- Miden assembly file containing the vulnerable mod_12289 procedure.
- filenamefalcon512_poseidon2.masmMiden assembly file containing the vulnerable mod_12289 procedure.