Resources

People often ask me "How did you learn how to hack?" The answer: by reading. This page is a collection of the blog posts and other articles that I have accumulated over the years of my journey. Enjoy!

Many security firms discuss how we found a bug completely automatically . However, there's a lot more to consider with LLMs than doing /goal Find bugs. In this article, they describe how, before the code review starts, they built custom tooling and format models to improve the review's quality and depth.

The target of this is the Miden VM, a ZK VM with its own custom assembly language and no developer tooling. So, they asked themselves: "what tooling what I like to have?" VS Code syntax highlighting for code review and code navigation are musts. From there, they asked what else they would need for reviews: they came up with a decompiler, and static analysis.

The static analysis tool did type verification for them on the assembly. This identified 400 locations where it could be improved and a single high-severity vulnerability where the remainder of the division wasn't properly verified for bounds.

What if this finds no bugs? For the client, it makes sense to deliver the generated code. The Miden VM was very possible to formally model: they claim this is because the instructions are small and side-effect-free. So, they created a representation in Lean! Claude built an automatic translator from MASM to Lean. They let the agent build the test, and then manually verified that the theorem statements were valid.

This resulted in 95 correctness proofs of small components of the code. Eventually, they found two bugs in this using the proofs. The first was an edge case in the 64-bit rotr instruction, where it behaved incorrectly on inputs larger than the Goldilocks prime and when the input was a multiple of 32. The second was the 256-bit multiplication instruction that dropped caller-owned values from the stack before returning. Yikes!

Building this tooling is costly but seems worth it. This type of coverage with proofs and custom tooling would have been impossible two years ago. Now, the LLM's can supercharge the reviews and speed things up dramatically. The Miden team actually uses the static analysis engine internally now. Overall, a great post on using security tooling for things than just finding bugs with /goal.