Matt Griffin
Academic and research departments
Computer Science Research Centre, Surrey Centre for Cyber Security.About
My research project
Verifying Hyperproperties for SecurityHyperproperties allow us to capture security policies such as non interference and non determinism across multiple execution traces. Formal modelling and automatic verification of select hyperproperties can be achieved by using the Isabelle proof assistant.
Supervisors
Hyperproperties allow us to capture security policies such as non interference and non determinism across multiple execution traces. Formal modelling and automatic verification of select hyperproperties can be achieved by using the Isabelle proof assistant.
University roles and responsibilities
- Lab Assistant
- Course Representative - CS PGR
Teaching
COM3026: Distributed Systems (2020/21)
COM3014: Advanced Challenges in Web Technologies (2020/21)
COM3018: Practical Business Analytics (2021/22)
COMM051: Database Systems (2021/22)
COMM034: Cloud Computing (2021/22)
Publications
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.