(2019) Efficient Information-Flow Verification under Speculative Execution.
|
Text
main.pdf Download (389kB) | Preview |
Abstract
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.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Swen Jacobs (SJ) |
| Conference: | ATVA International Symposium on Automated Technology for Verification and Analysis |
| Depositing User: | Swen Jacobs |
| Date Deposited: | 17 Nov 2019 16:46 |
| Last Modified: | 04 Jun 2021 08:37 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/2954 |
Actions
Actions (login required)
 |
View Item |