2025/11/18 by John Derrick, Brijesh Dongol, Chelsea Edmonds +3 · 1 voice
Computer Science · Social Sciences · #Security and Verification in Computing #Information and Cyber Security #Access Control and Trust
paper · pdf · doi:10.1007/s10817-025-09744-7
openalex created_date 2025/11/18 · openalex publication_date 2025/11/18 · openalex updated_date 2026/07/23
Abstract Meltdown and Spectre are vulnerabilities known as transient execution vulnerabilities, where an attacker exploits speculative execution (a semantic optimization present in most modern processors) to break confidentiality. We introduce relative security , a general notion of information-flow security that models this type of vulnerability by contrasting the leaks that are possible in a “vanilla” semantics with those possible in a different semantics, often obtained from the vanilla semantics via some optimizations. We describe incremental proof methods, in the style of Goguen and Meseguer’s unwinding, both for proving and for disproving relative security, and deploy these to formally establish the relative (in)security of some standard Spectre examples. Both the abstract results and the case studies have been mechanized in the Isabelle/HOL theorem prover. This paper is an extension of an earlier conference paper that provides significantly more detail on the Isabelle formalization and the unwinding proof process.