Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Kernel's Safety in the Spectre Era (Extended Version)

Davide Davoli, Martin Avanzini, Tamara Rezk

TL;DR

This work formalizes kernel safety in the Spectre era by first proving that kernel-layout-randomization yields probabilistic kernel safety under a classic attacker model with memory separation. It then shows that speculative execution and side-channels break these guarantees unless a stronger property, speculative layout non-interference, is adopted; it also introduces a semantics-preserving program transformation to enforce speculative kernel safety for systems that are already kernel-safe in the classic model. The results establish a formal foundation linking kernel safety to spatial-memory safety and CFI while proposing practical instrumentation (fences) to mitigate speculative leaks. Overall, the paper advances kernel security beyond layout randomization by combining formal models, non-interference concepts, and enforceable transformations, paving the way for robust defenses in the Spectre era.

Abstract

The efficacy of address space layout randomization has been formally demonstrated in a shared-memory model by Abadi et al., contingent on specific assumptions about victim programs. However, modern operating systems, implementing layout randomization in the kernel, diverge from these assumptions and operate on a separate memory model with communication through system calls. In this work, we relax Abadi et al.'s language assumptions while demonstrating that layout randomization offers a comparable safety guarantee in a system with memory separation. However, in practice, speculative execution and side-channels are recognized threats to layout randomization. We show that kernel safety cannot be restored for attackers capable of using side-channels and speculative execution and introduce a new condition, that allows us to formally prove kernel safety in the Spectre era. Our research demonstrates that under this condition, the system remains safe without relying on layout randomization. We also demonstrate that our condition can be sensibly weakened, leading to enforcement mechanisms that can guarantee kernel safety for safe system calls in the Spectre era.

On Kernel's Safety in the Spectre Era (Extended Version)

TL;DR

This work formalizes kernel safety in the Spectre era by first proving that kernel-layout-randomization yields probabilistic kernel safety under a classic attacker model with memory separation. It then shows that speculative execution and side-channels break these guarantees unless a stronger property, speculative layout non-interference, is adopted; it also introduces a semantics-preserving program transformation to enforce speculative kernel safety for systems that are already kernel-safe in the classic model. The results establish a formal foundation linking kernel safety to spatial-memory safety and CFI while proposing practical instrumentation (fences) to mitigate speculative leaks. Overall, the paper advances kernel security beyond layout randomization by combining formal models, non-interference concepts, and enforceable transformations, paving the way for robust defenses in the Spectre era.

Abstract

The efficacy of address space layout randomization has been formally demonstrated in a shared-memory model by Abadi et al., contingent on specific assumptions about victim programs. However, modern operating systems, implementing layout randomization in the kernel, diverge from these assumptions and operate on a separate memory model with communication through system calls. In this work, we relax Abadi et al.'s language assumptions while demonstrating that layout randomization offers a comparable safety guarantee in a system with memory separation. However, in practice, speculative execution and side-channels are recognized threats to layout randomization. We show that kernel safety cannot be restored for attackers capable of using side-channels and speculative execution and introduce a new condition, that allows us to formally prove kernel safety in the Spectre era. Our research demonstrates that under this condition, the system remains safe without relying on layout randomization. We also demonstrate that our condition can be sensibly weakened, leading to enforcement mechanisms that can guarantee kernel safety for safe system calls in the Spectre era.
Paper Structure (39 sections, 23 theorems, 182 equations, 11 figures)

This paper contains 39 sections, 23 theorems, 182 equations, 11 figures.

Table of Contents

  1. Introduction
  2. Motivation
  3. The Language
  4. Syntax
  5. Semantics
  6. Layouts
  7. Randomization scheme
  8. Small step operational semantics
  9. Threat Model
  10. Classic Threat Model
  11. Relation of kernel safety with security
  12. Final remarks
  13. Speculative Threat Model
  14. The Speculative Execution Model
  15. Victim Language and Semantics
  16. ...and 24 more sections

Key Result

Lemma 1

Let ${\color{codefn}{\mathtt{s}}}$ be a system call of a layout non-interfering system $\sigma=(\tau_{}, \gamma, \xi)$, and let $\mathsf{refs}_\sigma(\gamma({\color{codefn}{\mathtt{s}}}))\setminus \mathsf{Sys}=\{{\color{codefn}{\mathtt{id}}}_1, \dots, {\color{codefn}{\mathtt{id}}}_h\}$ be identifier

Figures (11)

  • Figure 1: System Calls vulnerable to memory corruption
  • Figure 2: Syntax of the language. Here, $v$ is a value, $x$ a register, ${\color{codefn}{\mathtt{a}}}$ an array identifier, ${\color{codefn}{\mathtt{f}}}$ a procedure identifier, and ${\color{codefn}{\mathtt{op}}}$ is an operator.
  • Figure 3: Semantics w.r.t. system $\sigma=(\tau_{},\gamma,\xi)$, first part.
  • Figure 4: Semantics w.r.t. system $\sigma=(\tau_{},\gamma,\xi)$, second part.
  • Figure 5: Speculative semantics, excerpt.
  • ...and 6 more figures

Theorems & Definitions (84)

  • Definition 1: Kernel safety
  • Definition 2: Layout non-interference
  • Lemma 1
  • proof : Proof sketch of \ref{['lemma:onsyscall']}
  • Lemma 2
  • proof : Proof Sketch of \ref{['lemma:onsyscallterm']}
  • Theorem 1
  • proof
  • Definition 3: Speculative kernel safety
  • Definition 4: Speculative layout non-interference
  • ...and 74 more