Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation (Extended Version)
Davide Davoli, Martin Avanzini, Tamara Rezk
TL;DR
This work formalizes kernel safety under memory-separated execution and shows that KASLR offers probabilistic protection in classic attacker models. It then demonstrates that in the Spectre era, layout randomization alone is insufficient due to side-channel leakage and speculative execution, introducing side-channel layout non-interference as a sufficient condition (though often impractical). To address this, the authors prove that transforming a classically kernel-safe kernel into a speculative-safe one using program transformations preserves semantics and enforces speculative kernel safety, and they implement three LLVM-based transformations. An extensive experimental evaluation on Linux shows that optimized fencing achieves modest overheads on compute-heavy tasks and acceptable costs on many workloads, indicating practical viability with future hardware support. Overall, the paper advances a formal framework and practical tools for enforcing kernel safety in the presence of speculative and side-channel vulnerabilities beyond traditional layout-randomization-based protection.
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 enforcement mechanisms that can guarantee speculative kernel safety for safe system calls in the Spectre era. We implement three suitable mechanisms and we evaluate their performance overhead on the Linux kernel.