Spectre attacks have upended the foundations of computer
security [1]}—showing that attackers can violate
security boundaries and steal secrets despite countermeasures such as
process isolation [2]},
software fault isolation (SFI) [3]},
and control flow integrity (CFI) [4]}.
In response, the security community has been working on program analysis tools
to both find Spectre vulnerabilities and to guide mitigations (e.g., compiler
passes) that make real programs secure in the presence of this class of
attacks.
However, because Spectre attacks—and speculative execution in
general—violate our typical assumptions and abstractions, they have proven
particularly challenging to reason about and to defend against.
