Formal Synthesis of Efficient Verified Emulators

Abstract:

Two approaches to synthesizing verified machine code emulators by theorem proving will be described and contrasted. The initial motivation is to provide trustworthy and efficient execution of guest code binaries (e.g. for discontinued legacy hardware) on a different hose processor (e.g. current technology COTS), whilst retaining the soundness of original validations, and so reducing the effort needed for re-certification. Both approaches use formal models of the guest and host architectures. The first exploits just-in-time (JIT) compilation to translate each basic block of guest machine code into host machine code. Efficiency depends on how far the fetch-decode-execute loop of the emulated instruction set is partial evaluated on the actual binary code being emulated. The second approach uses static binary translation in which an entire program or module from one architecture is translated to run on another. This approach is partial, but when applicable it can result in better code. An initial case study will be outlined in the talk. Verified emulators for a legacy 32-bit ARM architecture (ARMv4) running on a 64-bit x86 are synthesized by mechanized proof using the HOL4 system. This work is a collaboration between Magnus Myreen, Anthony Fox, and Mike Gordon.

Biography:

Magnus Myreen received his BA in Computer Science from the University of Oxford, tutored by Dr. Jeff Sanders. During the summers of his undergraduate degree, he worked as a research assistant at Åbo Akademi University in Finland for Professor Ralph–Johan Back. Magnus completed his PhD on program verification in 2008 at the University of Cambridge, supervised by Professor Mike Gordon. Currently, Magnus is a research associate at the University of Cambridge.

Slide presentation will be available for download May 2012.