Exploring nondeterminism.
Several Spectre analysis tools are built on some form of abstract execution:
They simulate speculative execution of the program
by tracking ranges or properties of different values.
By checking these properties throughout the program, they
determine if sensitive data can be leaked.
Standard tools for (non-speculative) abstract execution are
designed only to consider concrete execution paths; they must
be adapted to handle the many possible nondeterministic execution paths from speculation.
SpecuSym [1]}, KLEESpectre [2]}, and
AISE [3]} handle this nondeterminism by following an
always-mispredict strategy.
When they encounter a conditional branch, they first explore the
execution path which mispredicts this branch, up to a given speculation
depth.
Then, when they exhaust this path, they return to the correct branch.
This technique of course only handles the conditional branch
predictor; i.e., Spectre-PHT attacks.
Pitchfork [4]} and Binsec/Haunted [5]}
adapt the always-mispredict strategy to additionally account for
out-of-order execution and Spectre-STL.
Although
it may not be immediately clear that these always-mispredict
strategies are sufficient to prove security, especially when the attacker can
make any number of antagonistic prediction choices,
these strategies do indeed form a sound analysis [6]}, [4]}, [5]}.
