@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@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},
month = {June},
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.},
}