Formal Verification of Spectres Combination

Fabian, Xaver and Chan, Koby and Patrignani, Marco
(2021) Formal Verification of Spectres Combination.
In: PLAS 2021, 7 Dec 2021, Online.
Conference: PLAS Workshop on Programming Languages and Analysis for Security

PLAS_Workshop_paper_Spectre___combined (8).pdf

Download (234kB) | Preview


Speculative execution allows CPUs to improve performance by using prediction mechanisms that predict the outcome of branching and other instructions without waiting for the correct result. When the prediction is wrong, the CPU rolls back the effects of the speculatively-executed instructions on the architectural state (i.e., memory, registers). However, the side effects on the microarchitectural state, which includes the cache and buffers, are not rolled back and thus can leak possible confidential data that was speculatively accessed (Listing 1). Spectre attacks [1–4] demonstrate that most modern CPUs are affected by this speculation-based vulnerability.


Actions (login required)

View Item View Item