SoK: Practical Foundations for Software Spectre Defenses
- 1 May 2022
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE) in 2022 IEEE Symposium on Security and Privacy (SP)
Abstract
Spectre vulnerabilities violate our fundamental assumptions about architectural abstractions, allowing attackers to steal sensitive data despite previously state-of-the-art countermeasures. To defend against Spectre, developers of verification tools and compiler-based mitigations are forced to reason about microarchitectural details such as speculative execution. In order to aid developers with these attacks in a principled way, the research community has sought formal foundations for speculative execution upon which to rebuild provable security guarantees.This paper systematizes the community’s current knowledge about software verification and mitigation for Spectre. We study state-of-the-art software defenses, both with and without associated formal models, and use a cohesive framework to compare the security properties each defense provides. We explore a wide variety of tradeoffs in the expressiveness of formal frameworks, the complexity of defense tools, and the resulting security guarantees. As a result of our analysis, we suggest practical choices for developers of analysis and mitigation tools, and we identify several open problems in this area to guide future work on grounded software defenses.Keywords
Funding Information
- Semiconductor Research Corporation
- Office of Naval Research
This publication has 50 references indexed in Scilit:
- ret2specPublished by Association for Computing Machinery (ACM) ,2018
- Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”Published by Institute of Electrical and Electronics Engineers (IEEE) ,2018
- On Subnormal Floating Point and Abnormal TimingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2015
- System-level Non-interference for Constant-time CryptographyPublished by Association for Computing Machinery (ACM) ,2014
- RockSaltPublished by Association for Computing Machinery (ACM) ,2012
- Codejail: Application-Transparent Isolation of Libraries with Tight Program InteractionsLecture Notes in Computer Science, 2012
- Object Capabilities and Isolation of Untrusted Web ApplicationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2010
- Language-based information-flow securityIEEE Journal on Selected Areas in Communications, 2003
- Efficient software-based fault isolationPublished by Association for Computing Machinery (ACM) ,1993
- The equational theory of pomsetsTheoretical Computer Science, 1988