Formal foundations don't just help us make sure our Spectre defenses are
secure, they also help improve the performance of our tools.
Without formalizations, Spectre defenses are usually either overly
conservative (unnecessarily flagging code as vulnerable, which ultimately
leads to unnecessary and slow mitigations) or overly aggressive (and thus
vulnerable).
For example, speculative load hardening [1]} is safe—it safely
eliminates Spectre-PHT attacks—but is overly conservative: It assumes that
all array indexing operations must be hardened.
Aggressive techniques like oo7 [2]} are both inefficient and
unsafe—they impose unnecessary restrictions yet also miss vulnerable code
patterns.
Foundations allow us to craft defenses that are, in some sense, minimal
(e.g., they target the precise locations where vulnerabilities
exist [3]}, [4]}) while still being provably
secure.
