An Abstract Semantics of Speculative Execution for Reasoning About Security Vulnerabilities
| Autor: | Robert Colvin, Kirsten Winter |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Class (computer programming)
Correctness Programming language Semantics (computer science) Computer science Speculative execution 020207 software engineering 02 engineering and technology computer.software_genre 020202 computer hardware & architecture 0202 electrical engineering electronic engineering information engineering Cache State (computer science) computer Language construct |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030549961 FM Workshops (2) |
| Popis: | Reasoning about correctness and security of software is increasingly difficult due to the complexity of modern microarchitectural features such as out-of-order execution. A class of security vulnerabilities termed Spectre that exploits side effects of speculative, out-of-order execution was announced in 2018 and has since drawn much attention. In this paper we formalise speculative execution and its side effects as an extension of a framework for reasoning about out-of-order execution in weak memory models. Our goal is to allow speculation to be reasoned about abstractly at the software level. To this end we encode speculative execution explicitly using a novel language construct and modify the definition of conditional statements correspondingly. Underlying this extension is a model that has sufficient detail to enable specification of the relevant microarchitectural features. We add an abstract cache to the global state of the system, and derive some general refinement rules that expose cache side effects due to speculative loads. The rules are encoded in a simulation tool, which we use to analyse an abstract specification of a Spectre attack and vulnerable code fragments. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|