Formally verified binaries were a distant dream for decades; now it’s clear they will be central to the future of secure software, and that future is very near!
Can we use any compilation pipeline we want to produce efficient machine code, then apply formal methods to show that this code behaves in a certain way?View quoted post on X
This has long been a dream – a gold standard of formal verification, verifying programs at the assembly level – but was considered to be too difficult due to the loss of structure when going from a high level language to machine code.
Can AI bash through this problem? Apparently yes!
The basic idea I’ve been playing with is to write an interpreter of the target instruction set in an interactive theorem prover such as Lean or Bend. We can then prove that some compiled program conforms to a given specification by writing a proof that connects the machine code, interpreter, and some desired behavior of that code.
Why is this useful? It helps resolve 2 tradeoffs:
- When we write programs in a high level language designed for native execution rather than theorem proving, we get great performance, but are unable to formally reason about how that code behaves.
- On the other hand, when writing programs in a language like Lean, we can write proofs to reason about its behavior, but get poor native performance.
We can try and solve this tension by extracting a program written in something like Rust into Lean, but this tooling is complex, limited, and can introduce bugs!
Or, we can develop theorem provers that can compile to efficient native code. This is what Bend hopes to accomplish. Today, both of these techniques are limited, so proving at the assembly or bytecode level seems like a good solution.
What is the downside then? Well, formally reasoning about an instruction set is much harder than high level code. You have to consider registers, stack machines, and other low level semantics that are not particularly relevant to showing the correctness of a given algorithm. You also lose a great deal of information during compilation, making reasoning about it more difficult.
However, if you happen to be proving correctness over the instruction set you actually intend to run, you get *very* good correctness guarantees, as you don't even need to consider compiler bugs in your threat model.
So far, I have experimented with verifying simple algorithms compiled to both RISC-V and WASM32, and have gotten some surprisingly good initial results! LLMs handle writing tedious proofs, and all I do is verify a small set of invariants defining how the code should behave. Interestingly enough, WASM seems to be much easier to reason about, as the instruction set has some higher level semantics, such as local variables and functions. When proving RISC-V, we have to contend with reasoning about things like function dispatch and parameter encoding, which makes life much harder!
Anyways, stay tuned for some more updates on this as I try to see just how far we can push this technique!
