This thesis sheds light on the key aspects of verifying binary analysis.

Binary analysis refers to the process of analysing binaries without the need for high-level source code. The Binary Analysis Platform (BAP) is a widely used tool for performing binary analysis for a wide range of languages (C, C++, Rust), toolchains (LLVM, Ghidra) and target architectures (x86, RISC-V), achieved through lifting to an intermediate language named BIL (BAP Intermediary Language). Unfortunately, BAP lacks a verification component crucial for ensuring both provable correctness and security.

In response, we present IsaBIL, a binary analysis framework within Isabelle/HOL based upon BAP. Specifically, we formalise BIL, inheriting the full flexibility of BAP.

To make verification tractable, we develop several automation and optimisation techniques that alleviate the proof burden. Most notably, IsaBIL includes a verified Isabelle/ML parser for BIL programs, allowing one to automatically generate the associated Isabelle/HOL program locale from a BAP output. Taken together, IsaBIL provides a highly flexible user-friendly proof environment for program binaries.

To motivate the effectiveness of IsaBIL, we integrate it with Hoare logic (to enable proofs of correctness) as well as O’Hearn’s logic (to enable proofs of incorrectness). We prove (in)correctness for key examples drawn from the Joint Strike Fighter coding standards and the MITRE database.

Our subsequent work concerns verifying (in)security, specifically Transient Execution Vulnerabilities like Spectre, Meltdown and Foreshadow. Generic compiler mitigations for Spectre are known to be insufficient for eliminating vulnerabilities. Moreover, these mitigation techniques often overprescribe speculative fences, causing the performance of the programs to suffer.

Cheang et al. introduced operational semantics of program execution capable of characterising speculative executions and a novel class of information flow hyperproperties termed TPOD that ensure secure speculation. We encode Cheang et al.’s operational semantics in IsaBIL, providing a framework for verifying TPOD using Isabelle/HOL. Through powerful unwinding proofs, our framework can prove the existence of vulnerabilities and correctness of secure speculation. We exemplify our framework by proving (in)security for 20 examples, uncovering fundamental limitations in the TPOD hyperproperty leading to the misclassification of so-called ”conditionally secure" examples.

In our culminating work, we overcome the limitations of TPOD by introducing Relative Security, a more general hyperproperty. We instantiate Relative Security within the IsaBIL framework and, using the incremental proof methods described for TPOD, prove relative (in)security across the same Spectre examples, including the ”conditionally secure"

example.