Machine code, formal verification and functional programming

Magnus Myreen, University of Cambridge

Tuesday, May 28th, 2013 at 10:30.

Polacksbacken, room 1145

All programs run in the form of machine code. Ultimately, all formal software verification ought to reach down to this concrete form of execution and prove theorems about the actual ARM, x86 or PowerPC machine instructions that pass through the processor.

This talk presents techniques and tools that aid both verification of existing machine code (e.g. as produced by gcc) and tools that synthesise correct-by-construction machine code from high-level specifications (functions in logic). All of these tools have been implemented and used within the HOL4 theorem prover.

For post hoc verification, I describe a proof-producing decompiler that, given concrete machine code, returns a clean logic function describing the effect of executing that machine code. The decompiler is proof producing, i.e. for each run it proves that the generated function is correct w.r.t. specification of the underlying machine language (instruction set architecture).

For synthesis, I turn the decompiler around into a tool that generates correct machine code from functions in logic. This technique has been successfully applied in projects that construct verified implementations of Lisp (and soon ML). The most sophisticated verified Lisp implementation has decent efficiency due to its ability to perform verified dynamic compilation at runtime. Support for the dynamic compilation requires reasoning about self-modifying x86 code.

The talk includes a number of short demos and is meant to be accessible to people unfamiliar with machine code or theorem proving.