A Formal Approach to Secure Speculation

Kevin Cheang, Cameron Rasmussen, Sanjit A. Seshia, and Pramod Subramanyan. A Formal Approach to Secure Speculation. In Proceedings of the Computer Security Foundations Symposium (CSF), June 2019.

Download

[pdf] 

Abstract

Transient execution attacks like Spectre, Meltdown and Foreshadow have shown that combinations of microarchitectural side-channels can be 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 property formulation and associated adversary models help formalize the class of transient execution vulnerabilities. We demonstrate applicability of our methodology by verifying secure speculation for several illustrative programs.

BibTeX

@inproceedings{cheang-csf19,
  author    = {Kevin Cheang and Cameron Rasmussen and Sanjit A. Seshia and Pramod Subramanyan}, 
  title     = {A Formal Approach to Secure Speculation},
  booktitle = {Proceedings of the Computer Security Foundations Symposium (CSF)},
  year      = {2019},
  abstract  = {Transient execution attacks like Spectre, Meltdown 
and Foreshadow have shown that combinations of microarchitectural 
side-channels can be 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 property 
formulation and associated adversary models help formalize 
the class of transient execution vulnerabilities. We demonstrate 
applicability of our methodology by verifying secure speculation  
for several illustrative programs.},
}