Formal Verification of Spectres Combination

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.