Microarchitectural attacks, such as Spectre and Meltdown, illustrate that artifacts of hardware implementations (like speculative and out-of-order execution) can result in measurable side-effects on program execution time that attackers can exploit to compromise a system’s security. These attacks arise from emerging behaviors obtained when combining hardware and software. Building systems that are resistant against these attacks requires fundamentally rethinking the design of existing security mechanisms.

In this talk, I will focus on speculative execution attacks–a specific class of microarchitectural attacks–and I will illustrate a principled approach for reasoning about security against these attacks. The key component of this approach is aleakage contract, a formal ISA-level specification of the information that may be leaked through microarchitectural side-effects. Concretely, I will present (1) how to model the information flows at the core of Spectre-style attacks, (2) how to formalize leakage contracts, and (3) how to use contracts to reason about the security of hardware and software.