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

TL;DR

This paper analyzes kernel safety in the context of Spectre vulnerabilities, proposing a new condition that guarantees safety without relying solely on layout randomization, and discusses enforcement mechanisms for safe system calls.

Contribution

It introduces a formal condition ensuring kernel safety against Spectre-style attacks, extending prior models to realistic OS scenarios with memory separation.

Findings

Layout randomization offers comparable safety guarantees under relaxed assumptions.

Side-channels and speculative execution threaten kernel safety.

A new formal condition can guarantee kernel safety without layout randomization.

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.