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",
}