Matt Griffin

Matt Griffin

Postgraduate Research Student


My research project

University roles and responsibilities

  • Lab Assistant
  • Course Representative - CS PGR



    Matt Griffin, Brijesh Dongol (2021) Verifying Secure Speculation in Isabelle / HOL

    Secure speculation is an information flow security hyperproperty that prevents transient execution attacks such as Spectre, Meltdown and Foreshadow. Generic compiler mitigations for secure speculation are known to be insufficient for eliminating vulnerabilities. Moreover, these mitigation techniques often overprescribe speculative fences, causing the performance of the programs to suffer. Recently Cheang et al. have developed an operational semantics of program execution capable of characterising speculative executions as well as a new class of information flow hyperproperties named TPOD that ensure secure speculation. This paper presents a framework for verifying TPOD using the Isabelle/HOL proof assistant by encoding the operational semantics of Cheang et al. We provide translation tools for automatically generating the required Isabelle/HOL theory templates from a C-like program syntax, which

    speeds up verification. Our framework is capable of proving the existence of vulnerabilities and correctness of secure speculation. We exemplify

    our framework by proving the existence of secure speculation bugs in 15 victim functions for the MSVC compiler as well as correctness of

    some proposed fixes.