Name:Dr. Anthony Fox
Designation:Senior Research Associate
Title:Applied Theorem Proving: Modelling Instruction Sets and Decompiling Machine Code

Abstract: There are number of safety and security critical applications where there is a call for reasoning about low-level machine-code. These “high-assurance” applications include the formal verification of micro-kernels (e.g. seL4) and compilers (e.g. Compcert and CakeML). This talk will discuss recent work on formally specifying Instruction Set Architectures (ISAs) using a domain specific language, L3, which provides facilities for generating specifications as Standard ML and HOL4. Models of ARM, MIPS and x86-64 have been developed and validated. Automated reasoning tools have been developed within the HOL4 interactive theorem prover, providing facilities for “certifiably decompiling” machine-code into mathematical functions.

Biography: Dr Anthony Fox studied computer science at Swansea University and his thesis was on the correctness of microprocessor designs.  After a short stint at Dera (now QinetiQ), he joined the Cambridge University Computer Laboratory working for Professor Mike Gordon.  Having completed a formal verification of the ARM6 micro-architecture using the HOL4 interactive theorem prover, he has subsequently worked on developing models and tools for machine-code verification.  Recently his focus has been on designing and using a custom ISA specification language, called L3.

Formal Verification Seminar Presentation                                                                                    Video Presentation