Automatic Detection of Speculative Execution Combinations
Xaver Fabian, Marco Guarnieri, Marco Patrignani · Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security · 2022
Modern processors employ different speculation mechanisms to speculate over different kinds of instructions. Attackers can exploit these mechanisms simultaneously in order to trigger leaks of speculatively-accessed data. Thus, sound reasoning about such speculative leaks requires accounting for all potential speculation mechanisms. Unfortunately, existing formal models only support reasoning about fixed, hard-coded speculation mechanisms, with no simple support to extend said reasoning to new mechanisms.