Speculative execution is inherently
nondeterministic: Any given branch in a program may
proceed either correctly or incorrectly, regardless of the actual condition value.
More generally, predictors such as the BTB can send execution to an entirely indeterminate location.
The semantics in tab:mechanics all allow these nondeterministic
choices to be actively adversarial—for instance, given by attacker-specified
directives [1]}, [2]},
or, equivalently, by consulting an abstract
oracle [3]}, [4]}, [5]}, [6]}.
These semantics
all (conservatively) assume that the attacker has full control
of microarchitectural prediction and scheduling; we explore
the different techniques they use to verify or enforce security
in the face of adversarial nondeterminism.
