|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.