Visible to the public A Formal Approach to Secure Speculation

TitleA Formal Approach to Secure Speculation
Publication TypeConference Paper
Year of Publication2019
AuthorsCheang, Kevin, Rasmussen, Cameron, Seshia, Sanjit, Subramanyan, Pramod
Conference Name2019 IEEE 32nd Computer Security Foundations Symposium (CSF)
Date Publishedjun
Keywordscompositionality, formal, formal approach, formal verification, Formal-Verification, hyperproperty, information flow security properties, information-flow, Kernel, Linux, meltdown, Metrics, microarchitectural side-channels, microarchitecture, mitigation, observational-determinism, out-of-order-execution, Program processors, provable security, pubcrawl, resilience, Resiliency, safety-property, secure speculation property, secure speculative execution, security, security of data, side-channel, SMT, software mitigations, Spectre, speculation, trace property-dependent observational determinism, trace-property, Transient analysis, transient execution attacks, transient-execution, uclid5, verification
AbstractTransient 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 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.
Citation Keycheang_formal_2019