CISPA
Browse
cispa_all_3820.pdf (228.82 kB)

Formal Verification of Spectres Combination

Download (228.82 kB)
conference contribution
posted on 2023-11-29, 18:19 authored by Xaver FabianXaver Fabian, Koby Chan, Marco Patrignani
Speculative execution allows CPUs to improve performance by using prediction mechanisms that predict the outcome of branching and other instructions without waiting for the correct result. When the prediction is wrong, the CPU rolls back the effects of the speculatively-executed instructions on the architectural state (i.e., memory, registers). However, the side effects on the microarchitectural state, which includes the cache and buffers, are not rolled back and thus can leak possible confidential data that was speculatively accessed (Listing 1). Spectre attacks [1–4] demonstrate that most modern CPUs are affected by this speculation-based vulnerability.

History

Preferred Citation

Xaver Fabian, Koby Chan and Marco Patrignani. Formal Verification of Spectres Combination. In: Workshop on Programming Languages and Analysis for Security (PLAS). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Workshop on Programming Languages and Analysis for Security (PLAS)

Legacy Posted Date

2022-10-13

Open Access Type

  • Green

BibTeX

@inproceedings{cispa_all_3820, title = "Formal Verification of Spectres Combination", author = "Fabian, Xaver and Chan, Koby and Patrignani, Marco", booktitle="{Workshop on Programming Languages and Analysis for Security (PLAS)}", year="2021", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC