CISPA
Browse
cispa_all_3817.pdf (808.09 kB)

Automatic Detection of Speculative Execution Combinations

Download (808.09 kB)
conference contribution
posted on 2023-11-29, 18:23 authored by Xaver FabianXaver Fabian, Marco Guarnieri, Marco Patrignani
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. In this paper, we develop a framework for reasoning about composed speculative semantics that capture speculation due to different mechanisms and implement it as part of the Spectector verification tool. We implement novel semantics for speculating over store and return instructions and combine them with the semantics for speculating over branch instructions. Our framework yields speculative semantics for speculating over any combination of these instructions that are secure by construction, i.e., we obtain these security guarantees for free. The implementation of our novel semantics in Spectector let us verify programs that are vulnerable to Spectre v1, Spectre v4, and Spectre v5 vulnerabilities as well as new snippets that are only vulnerable to their compositions.

History

Preferred Citation

Xaver Fabian, Marco Guarnieri and Marco Patrignani. Automatic Detection of Speculative Execution Combinations. In: ACM Conference on Computer and Communications Security (CCS). 2022.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

ACM Conference on Computer and Communications Security (CCS)

Legacy Posted Date

2022-10-13

Open Access Type

  • Green

BibTeX

@inproceedings{cispa_all_3817, title = "Automatic Detection of Speculative Execution Combinations", author = "Fabian, Xaver and Guarnieri, Marco and Patrignani, Marco", booktitle="{ACM Conference on Computer and Communications Security (CCS)}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC