CISPA
Browse
- No file added yet -

Efficient Information-Flow Verification under Speculative Execution

Download (380.15 kB)
conference contribution
posted on 2023-11-29, 18:11 authored by Roderick Bloem, Swen JacobsSwen Jacobs, Yakir Vizel
We study the formal verification of information-flow properties in the presence of speculative execution and side-channels. First, we present a formal model of speculative execution semantics. This model can be parameterized by the depth of speculative execution and is amenable to a range of verification techniques. Second, we introduce a novel notion of information leakage under speculation, which is parameterized by the information that is available to an attacker through side-channels. Finally, we present one verification technique that uses our formalism and can be used to detect information leaks under speculation through cache side-channels, and can decide whether these are only possible under speculative execution. We implemented an instance of this verification technique that combines taint analysis and safety model checking. We evaluated this approach on a range of examples that have been proposed as benchmarks for mitigations of the Spectre vulnerability, and show that our approach correctly identifies all information leaks.

History

Preferred Citation

Roderick Bloem, Swen Jacobs and Yakir Vizel. Efficient Information-Flow Verification under Speculative Execution. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). 2019.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Symposium on Automated Technology for Verification and Analysis (ATVA)

Legacy Posted Date

2019-11-17

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_2954, title = "Efficient Information-Flow Verification under Speculative Execution", author = "Bloem, Roderick and Jacobs, Swen and Vizel, Yakir", booktitle="{International Symposium on Automated Technology for Verification and Analysis (ATVA)}", year="2019", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC