An abstract semantics of speculative execution for reasoning about security vulnerabilities

Robert J. Colvin, Kirsten Winter

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 o…