You are looking at a specific version 20190320:103921 of this paper. See the latest version.

Paper 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, provably 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.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Preprint. MINOR revision.
Keywords
speculationtransient executionformal methodsformal verificationmodel checkingobservational determinism
Contact author(s)
spramod @ cse iitk ac in
History
2019-10-26: last of 2 revisions
2019-03-20: received
See all versions
Short URL
https://ia.cr/2019/310
License
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.