Trail of Bits Used Six Months of Agent-Built MASM Tooling and Lean Proofs to Audit the Miden zkVM
- Trail of Bits found a real bug during its Miden VM review: an unvalidated prover-supplied input that would let a malicious prover forge Falcon signatures and steal funds from Miden account holders.
- Before the review even started the team spent six months having agents build an LSP server (masm-lsp), a decompiler (masm-decompiler), a static analysis engine (masm-analysis), and a Lean model of the VM executor from scratch, since Miden assembly (MASM) had almost no developer tooling.
- The Lean work produced 95 machine-checked correctness proofs covering a large component of the Miden core library, where cryptographic primitives are hand-written in MASM.
- Claude built a working masm-lsp prototype within a few days with syntax highlighting, goto definition, reference finding, docstring hover, plus inline instruction documentation and per-instruction stack effects.
- Decompiling hand-written MASM stays hard because most core library procedures have no declared signatures, calls follow no calling convention so net stack effects cannot be computed statically and failures propagate up the call chain, and while-loops need not be stack neutral so loop conditions can sit in different stack slots per iteration.
Hacker News opinions
This is a great example of AI making the work better instead of just making it faster.
I'd say the difference is mostly semantics. With AI I can do in one day what would have taken me a week, so the result is better while my time spent stays constant.
Good enough AI for security auditing feels like asking for 'good enough' brakes. There is no room for complacency.
Not sure I follow the analogy. We do have standards for brakes that are good enough without being brake-maxxers, and a verified implementation with correctness proofs and a tiny trusted translator seems close to good enough here. A lot rides on the Claude-built translator though.
I don't get the analogy either. Brakes that are good enough for a Honda Civic are not good enough for a fire truck or a race car, but standards that are 'good enough' exist for all of those.
There is one area where AI audits really add value: the huge number of companies that have never looked at security at all, the small businesses.
It's basically over for security people. Assume you are 100% going to get pwned eventually and start rethinking your architecture around that.
FHE would be nice, but plenty of products could be E2EE today and a lot of breaches are just server-side files and dumps. For remote attack security I'd rank clients: GrapheneOS, iOS/iPadOS, stock Pixel Android, ChromeOS, macOS, Windows, desktop Linux, and with AI I can audit a native client's source as often as I want thanks to reproducible builds.