To thoroughly defend against Spectre, we should take the lessons learned about
similar problems in the non-speculative world and transfer those lessons into
the new speculative context. One key lesson is that language-based methods
provide an effective means to achieve efficient code with provable
security guarantees. For example, the security community turned to
language-based security to solidify intricate defense techniques—from SFI
enforcement on x86 processors [1]}, to information flow
control [2]}, to using constant-time
programming to eliminate traditional side-channel attacks [3]}.
Language-based methods are rooted in program semantics, which provide
rigorous models of program behavior, and serve as the basis for formal
security policies. These policies help us carefully and explicitly spell out
our assumptions about the attacker's strength, and to gain confidence that our
tools are sound with respect to this class of attackers—that standalone
Spectre vulnerability-detection tools find all of the vulnerabilities they
claim to, or that defense techniques (e.g., compiler passes) actually mitigate
the attacks they claim.
