Cryptology ePrint Archive: Report 2019/310
A Formal Approach to Secure Speculation
Kevin Cheang and Cameron Rasmussen and Sanjit Seshia and Pramod Subramanyan
Abstract: Transient execution attacks like Spectre, Meltdown and Foreshadow have shown that combinations of microarchitectural side-channels can be synergistically exploited to create side-channel leaks that are greater than the sum of their parts. While both hardware and software mitigations have been proposed against these attacks, provable security has remained elusive. This paper introduces a formal methodology for enabling secure speculative execution on modern processors. We propose a new class of of information flow security properties called trace property-dependent observational determinism (TPOD). We use this class to formulate a secure speculation property. Our formulation precisely characterises all transient execution vulnerabilities. We demonstrate its applicability by verifying secure speculation for several illustrative programs.
Category / Keywords: implementation / speculation, transient execution, formal methods, formal verification, model checking, observational determinism
Original Publication (with minor differences): 32nd IEEE Computer Security Foundations Symposium
DOI: 10.1109/CSF.2019.00027
Date: received 18 Mar 2019, last revised 26 Oct 2019
Contact author: spramod at cse iitk ac in
Available format(s): PDF | BibTeX Citation
Note: Minor typos fixed + additional discussion of Spectector in the related work.
Version: 20191026:061616 (All versions of this report)
Short URL: ia.cr/2019/310
[ Cryptology ePrint archive ]