# Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation

Davide Davoli, Martin Avanzini, Tamara Rezk

► To cite this version:

Davide Davoli, Martin Avanzini, Tamara Rezk. Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation. ACM Transactions on Privacy and Security, 2025, 10.1145/3743678. hal-05173527

HAL Id: hal-05173527

https://hal.science/hal-05173527v1

Submitted on 21 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Comprehensive Kernel Safety in the Spectre Era: Mitigations
and Performance Evaluation

DAVIDE DAVOLI, Inria, Université Côte d'Azur, France

MARTIN AVANZINI, Inria, Université Côte d'Azur, France

TAMARA REZK, Inria, Université Côte d'Azur, France

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.

CCS Concepts: • **Security and privacy** → **Formal security models**; **Operating systems security**; *Side-channel analysis and countermeasures*.

Additional Key Words and Phrases: Speculative execution; layout randomization; memory safety; control flow integrity; kernel safety

**ACM Reference Format:**

Davide Davoli, Martin Avanzini, and Tamara Rezk. 2025. Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation. *ACM Trans. Priv. Sec.* 1, 1, Article 1 (January 2025), 39 pages. https://doi.org/10.1145/3743678

# 1 Introduction

Memory safety violations on kernel memory can result in serious ramifications for security, such as e.g. arbitrary code execution, privilege escalation, or information leakage. In order to mitigate safety violations, operating systems such as Linux employ address space layout randomization [32, 33, 47, 62, 63, 68]. This protection measure can prevent attacks that depend on knowledge of specific data or procedure location, as it introduces randomization of these addresses.

On the one hand, the efficacy of layout randomization has been formally demonstrated in Abadi et al.'s line of work [2-4], as a protective measure within a *shared-memory model* between the attacker and the victim. These results, however, are contingent on specific assumptions regarding victim programs, notably the absence of pointer arithmetic, introspection, or indirect jumps. These precise constraints shaped a controlled environment where memory safety could be enforced effectively via layout randomization. However, operating systems employing layout randomization on kernel (a.k.a. KASLR in Linux e.g. [33]) diverge from these assumptions. Notably, they operate on a separate memory model, wherein, kernel code—acting as the victim—resides on kernel memory, while user

Authors' Contact Information: Davide Davoli, Inria, Université Côte d'Azur, Sophia Antipolis, France, davide.davoli@inria.fr; Martin Avanzini, Inria, Université Côte d'Azur, Sophia Antipolis, France, martin.avanzini@inria.fr; Tamara Rezk, Inria, Université Côte d'Azur, Sophia Antipolis, France, tamara.rezk@inria.fr.

<figure><img src="image_2.png" /></figure>

This work is licensed under a Creative Commons Attribution 4.0 International License.

© 2025 Copyright held by the owner/author(s).

ACM 2471-2574/2025/1-ART1

https://doi.org/10.1145/3743678
code—acting as the potential attacker—resides in user space. The interaction between the two
occurs through a limited set of procedures provided via system calls [77]. In the operating system's
realm, system calls may be written in C and assembly code, further deviating from the restricted
conditions outlined by Abadi et al. This introduces a distinction not only in the expressiveness of
victim code considered but also in the underlying memory model.

Hence, our first research question emerges: can we relax the language assumptions proposed by Abadi et al. [2-4] while concurrently demonstrating that layout randomization offers a comparable safety guarantee in a system with memory separation? We affirmatively respond to this question by showcasing that layout randomization probabilistically ensures kernel safety within a classic attacker model, where users of an operating system execute without privileges and victims can feature pointer arithmetic, introspection, and indirect jumps.

On the other hand, in the current state-of-the-art of security, often referred to as the Spectre era, speculative execution and side-channels are well known to be effective vectors for compromising layout randomization [14, 41, 43, 53, 57, 58]. Indeed, our first result neglects the impact of speculative execution and side-channels. Recognizing this limitation, our second research question arises: can we restore a similar safety result in the Spectre era?

In this regard, we formally acknowledge that by relying solely on layout randomization it is not
possible to restore kernel safety. We then introduce a new condition, called *side-channel layout non-interference* akin to speculative constant-time [16], which intuitively asserts that victims should
not unintentionally leak information on the kernel’s layout through side-channels. Our research
formally demonstrates that under this assumption, the system is safe, and perhaps surprisingly,
without the necessity of layout randomization. Later, we show that side-channel layout non-
interference is not a necessary requirement, and this motivates us to study how safety can be
enforced without requiring that property.

Our third contribution is to show that kernels can be protected even without requiring *side-channel layout non-interference*. We do so by relating safety in the classic execution model to the speculative one. Specifically, we show that a kernel that is safe against classic attackers can be protected against speculative attackers by applying specific program transformations. However, the initial safety requirement that we impose on the kernel cannot be granted solely by layout randomization. Finally, we show the soundness of three such transformations, and we implement them in order to evaluate their overhead in terms of performance.

This marks the first formal step toward strengthening kernel safety in the presence of speculative
and side-channel vulnerabilities, and the surpassing of layout randomization as a system level
protection mechanism. In summary, our contributions are:

* We formally demonstrate the effectiveness of layout randomization to provide kernel safety for a classic operating system scenario, with system calls offered as interfaces to attackers and different privilege execution modes, as well as kernel and user memory separation.

* We empower the attackers of our first scenario to execute side-channel attacks and control speculative execution. We demonstrate that kernel safety is not maintained under this more potent attacker model, and we subsequently present a sufficient condition to ensure kernel safety.

* We show that it is possible to enforce safety against speculative attackers on a system that enjoys weaker security guarantees by the application of specific program transformations.

* We implement these transformations, and we measure their overhead on the Linux kernel. The experimental evaluation shows that they impose low performance overheads on computationally heavy user-space tasks.
- This paper is an extended version of the ACM CCS conference paper [30] on kernels' safety in the presence of speculative execution. The additional material in this work, compared to the conference version, is the following:

* We model indirect branch prediction, related to Spectre v2, significantly strengthening the attack model compared to the conference paper (Section 6). Incorporating indirect branch prediction required extending the attacker's language with controls over branch targets, and adapting our speculative semantics accordingly. To contrast unwanted indirect branch predictions, we modeled a class of jump instructions whose targets cannot be speculative, and that are crucial for the effectiveness of the mitigations in Section 8. This addition does not affect sections where speculative execution is not considered, notably Sections 3 and 5.

* We review state-of-art mitigations against speculative execution attacks, showing that none of them can easily be adopted to enforce kernel's safety in the presence of speculative execution (Section 7).

* We extend the transformation given in the conference version of this paper [30, Section 7] to protect against indirect branch speculation.

* We define two additional transformations. The first one is an optimized version of the transformation given in the conference version of this paper [30, Section 7], and the other one blocks all forms of *kernel-space* speculation taken into account in this work (Section 8).

* We implement the transformations as LLVM passes, and we offer them as open source [29].

* We evaluate the performance overhead of these transformations on computationally heavy *user-space* and *kernel-space* tasks, and on I/O-bound *user-space* workloads.

The paper is structured as follows: in Section 2, we give an overview of the contributions of this paper, motivated by a concrete example. In Section 3, we introduce our execution model by giving its language and semantics; in Section 4, we establish threat models. Section 5 is devoted to showing that layout randomization protects against attacks that do not rely on speculative execution and side-channel observations. In Section 6, we extend the model of Section 3 with side-channel info leaks and speculative execution, and we show that layout randomization is not a viable protection mechanism in this scenario. State-of-art mitigations against speculative attacks are reviewed in Section 7. In Section 8, we show that any system that is safe against classic attackers can be transformed into an equivalent system that is safe against speculative attackers, and we propose three suitable program transformations for this task. In Section 9, we estimate the overhead of this transformation on real hardware. Finally, we discuss related work in Section 10, and we conclude in Section 11. Omitted proofs are available in the extended version of this paper [31].

## 2 Overview

Each year, dozens of vulnerabilities are found in commodity operating systems' kernels, and the majority of them are memory corruption vulnerabilities [74]. A kernel suffers a memory corruption vulnerability when an unprivileged user-space program, acting as the attacker, can trigger it to read or write its memory in an *unexpected* way, usually, by issuing a sequence of system calls with maliciously crafted arguments. In Figure 1, we show a pair of system calls of a hypothetical operating system that are subject to this vulnerability. The *recv* and *send* system calls are meant to implement a simple message passing protocol. The implementation supports up to K sockets, each socket can buffer up to H messages. A user can send messages by invoking the system call *send*, and read them with the system call *recv*. These system calls employ a shared buffer *buf* that stores messages, together with a hook for a customizable callback pointed by *buf[K][0]*. If specified, this callback is executed after a message is sent. Such a callback may, for instance, inform the sender on whether the message was sent correctly.
```c
int buf[K+1][H];
int recv(socket* s, size_t idx) {
    if (valid(s, idx))
        return buf[*s][idx];
    return -1;
}

void send(socket* s, size_t idx, int msg) {
    if (valid(s, idx)) {
        buf[*s][idx] = msg;
        if (buf[K][0] != NULL)
            (*buf[K][0])(s, idx);
    }
}
```

<caption>Fig. 1. System calls vulnerable to memory corruption</caption>

These system calls are meant to interact only with the memory containing the buffer, the code of the called procedures and with the resources that these procedures access. In the following, we will refer to the set of memory resources that a system call may access rightfully as the *capabilities* of that system call. Depending on the implementation of the procedure `valid`, these system calls can suffer from memory corruption vulnerabilities. For instance, if the `valid` function does not perform bound checks on the value of `idx`, these two system calls can be used to perform arbitrary read and write operations by a malicious user-space program, acting as an attacker against the victim kernel. In particular, the `recv` system call can be used to perform an unrestricted memory read operation by supplying an out-of-bounds value for `idx`. Similarly, the `send` system call can be used to overwrite any value of kernel memory and, in particular, to overwrite the pointer to the callback that is stored within the buffer. This means that a malicious user-space program, acting as an attacker, can turn this memory-vulnerability into a *control flow integrity* (CFI) violation [1], as it can deviate the control flow from its intended paths.

However, if the system that implements these system calls is protected with layout randomization—like many commodity operating systems do [32, 33, 47, 62, 63, 68]— exploiting these vulnerabilities is not straightforward. In Linux, for instance, one of the viable ways to mount a privilege-escalation attack is to disable the *Supervisor Mode Execution Prevention* (SMEP) by running the `native_write_cr4` procedure. When this protection is disabled, the kernel is allowed to run any *payload* stored in user-space. The attacker can trigger the system to execute the *payload* by exploiting the vulnerability of the `send` system call twice: the first time to run the `native_write_cr4` procedure, and the second time to run the *payload*. However, in order to do so, the attacker has to infer the address of `native_write_cr4`. In the absence of info-leaks, an attacker can only guess such address and, due to layout randomization, the probability of success is low. Section 5 is devoted to showing that without side-channel leaks (and speculative execution), if a system is protected with layout randomization, the probability that an unprivileged attacker leads the system to perform an unsafe memory access is very low, provided the address space is sufficiently large. Of course, the precise probability depends on the concrete randomization scheme. This result is compatible with the large number of kernel attacks that break Linux's kernel layout randomization, e.g. by means of heap overflows [73], as the distribution of Linux's heap addresses lacks entropy [37]. In consequence, the probability of mounting a successful attack is relatively high.

Although it was already well known that layout randomization can provide security guarantees [2–4], one of the main novelties of Section 5 is showing that these guarantees are valid even if
victims can perform pointer arithmetic and indirect jumps. Despite this positive result, the threat model considered in Section 5 is unrealistic nowadays. In particular, it does not take into account the ability of the attackers to access side-channel info-leaks and to steer speculative execution. There is evidence that, by leveraging similar features, the attackers can leak information on the kernel's layout [14, 43, 46, 53, 58] and compromise the security guarantees offered by layout randomization [41, 57].

In particular, if the victim system suffers from side-channel info-leaks that involve the layout, an attacker may break the protection offered by randomization. For instance, suppose the system contains the following system call:

```c
void sc_leak(x){
    if ((void*) x == (void*) native_write_cr4)
    for(int i = 0; i < K; i++);
}
```

By measuring the execution time of the system call, an attacker may deduce information on the location of `native_write_cr4`. If, for some address a, the invocation call `sc_leak(a)` takes sensibly longer to execute, the attacker can deduce that a corresponds to the address of `native_write_cr4`. Then, the attacker can disable the SMEP protection via the vulnerable system call `send`.

Side-channel leaks can also be triggered with the help of speculative execution: in our example from Figure 1, an attacker can use the `recv` primitive to probe for readable data without crashing the system. This can be done by supplying to the system call arguments `s` and `idx` such that `valid(s, idx)` returns false—ideally, causing out of bound accesses when the return value is fetched from memory. If the attacker manages in mis-training the branch predictor, the access to `buf[*s][idx]` is performed after a wrong prediction, i.e., in *transient execution*. Depending on the allocation state of the address referenced by `buf[*s][idx]`, two cases arise. If that address does not store any readable data, the memory violation is not raised to the architectural state, because it occurred during transient execution. However, if that address stores writable data, the load operation inserts a new line in the system's cache and, when the system detects the mis-prediction, the execution backtracks to the latest architecturally valid state. After the backtrack, the insertion of a new line in the cache can be detected from user-space. Thus, the attacker can infer that the address referenced by `buf[*s][idx]` contains readable data, and it can exploit the vulnerabilities of the `send` and the `recv` system calls to read or write the content of that memory address. This form of *speculative probing* is very similar to what happens, for instance, in the *BlindSide* attack [41] that effectively defeats Linux's KASLR.

The reader may observe that such attacks rely on the attacker's ability to reconstruct the kernel's memory layout by collecting side-channel info-leaks. For this reason, a natural question is whether these attacks can be prevented by imposing that no information on the layouts leaks to the architectural and the micro-architectural state during the execution of system calls. It turns out that this is the case, as we show in Section 6. In practice, this mitigation is of little help though, as it would effectively rule out all system calls that access memory at runtime.

However, we show that any operating system can be pragmatically turned into another system that is functionally equivalent to the original one for user-space programs, but that is not subject to vulnerabilities due to transient execution. This can be achieved with program transformations. With such an approach, showing that a kernel is safe in the speculative execution model boils down to showing that the kernel under consideration is safe in the classic execution model. Concretely, a suitable program transformation could block the speculative attack to the `recv` system call we described above by disallowing the transient execution of the unsafe load operation with a
```
Expr   ⊃ E, F ::= v | x | a | f | op(E₁, ..., Eₙ)
```

```
Instr ⊃ I, J ::= skip | x := E | x := *E | *E := F | call F(E₁, ..., Eₙ) | syscall s(E₁, ..., Eₙ) |
           if E then C else D fi | while E do C od
```

```
Cmd   ⊃ C, D ::= ε | I; C
```

<caption>Fig. 2. Syntax of the language. Here, v is a value, x a register, a an array identifier, f a procedure identifier, and op is an operator.</caption>

speculation barrier: an instruction that stops speculative execution. The efficacy of this technique is formally shown in Section 8.

Although partially blocking kernel-space speculative execution can have deleterious ramifications for performance, computer systems' execution takes place mostly in user space, amortizing the overhead that the system encounters in kernel-space. An experimental evaluation given in Section 9 confirms this claim.

# 3 Language

In this section, we introduce the language that we employ throughout the following to study the effectiveness of kernel address space layout randomization. We are considering a simple imperative while language. The address space is explicit, and segregated into user and kernel space. We start by describing the syntax.

## 3.1 Syntax

The set `Cmd` of commands is given in Figure 2. Memories may store procedures and arrays, i.e., sequences of values $v \in Val$ organized as a contiguous region. The set of values is left abstract, but we assume that it encompasses at least Boolean values `Bool` $\triangleq \{true, false\}$, (memory) addresses `Addr`, modeled as non-negative integers, and an undefined value `null`. Within expressions, $x \in Reg$ ranges over registers, `a` $\in$ `ArrId` and `f` $\in$ `Procld` over array and procedure identifiers respectively; `op` $\in$ `Ops` ranges over operators. Identifiers `Id` $\triangleq$ `ArrId$\cup$` `Procld` are mapped to addresses at runtime, as governed by a layout randomization scheme. The size (length) of an array `a` is denoted by `size(a)` and is fixed for simplicity, i.e., we do not model dynamic allocation and deallocation.

A command `C` $\in$ `Cmd` is a sequence of instructions, evaluated in-order. The instruction `x := E` stores the result of evaluating `E` within register `x` $\in$ `Reg`. To keep the semantics brief, expressions neither read nor write to memory. Specifically, addresses are dereferenced explicitly. To this end, the instruction `x := *E` performs a memory read from the address given by `E`, and stores the corresponding value in register `x`. Dually, the instruction `*E := F` stores the value of `F` at the address given by `E`. The instruction `call F(E₁, ..., Eₙ)` invokes the procedure residing at address `F` in memory, supplying arguments `E₁, ..., Eₙ`. Likewise, `syscall s(E₁, ..., Eₙ)` invokes a system call `s` from a finite set of system call names `Sys` with arguments `E₁, ..., Eₙ`. The execution of a system call engages the *privileged execution mode* and thereby the accessible address space changes. To this end, the address space `Addr` is partitioned into $\kappa_u$ *user-space* addresses `Addr_u` = {0, ..., $\kappa_u$ - 1}, visible in unprivileged mode, and $\kappa_k$ *kernel-space* addresses `Addr_k` = {$\kappa_u$, ..., $\kappa_u$ + $\kappa_k$ - 1}, visible in unprivileged mode. The remaining constructs are standard.

*Stores.* Let `Arr` denote the set of arrays, i.e., finite sequences of values $\vec{v}$ of fixed length $|\vec{v}|$. A *store* is a (well-sorted) mapping $\tau: \text{Id} \to \text{Arr} \cup \text{Cmd}$, mapping array identifiers `a` to arrays $\tau(a) \in \text{Arr}$ of length `size(a)` and procedure identifiers `f` to their implementation $\tau(f) \in \text{Cmd}$. Let $\text{Id}_u \psi \text{Id}_k = \text{Id}$ be a partitioning of identifiers into *user-space* and *kernel-space* identifiers, respectively. This distinction
will signify the intended location of the corresponding objects within the memory address space. We write $\text{Procld}_k \subseteq \text{Id}_k$ and $\text{Procld}_u \subseteq \text{Id}_u$ for the *kernel-space* and *user-space procedure idenitifiers*; similarly, we use $\text{Arrld}_k \subseteq \text{Id}_k$ and $\text{Arrld}_u \subseteq \text{Id}_u$ to denote *kernel-space* and *user-space array idenitifiers*, respectively. Given a store $\tau$, we always assume that the address space is sufficiently large to hold $\tau$; that is, for every $b \in \{u, k\}$, $\kappa_b \ge \sum_{id \in \text{Id}_b} \text{size}(id)$. Here, by convention, $\text{size}(f) \triangleq 1$. In the following, we often work with pairs of stores that associate a set of identifiers to the same values—e.g., containing identical procedures. We write $\tau =_{\text{Id}} \tau'$ if $\tau$ and $\tau'$ coincide on $\text{Id} \subseteq \text{Id}$.

*Capabilities.* To model safety, each system call *s* is associated with a fixed set of identifiers defining the memory regions it can access. We refer to this set as the *capabilities of s*.

*Systems.* In our model, kernels are modeled as triples defining system calls, the content of kernel space memory, and the capabilities associated with every system call. Let Sys denote a (finite) set of system call identifiers. A system for Sys is a tuple $\sigma = (\tau, \gamma, \xi)$, consisting of:

* an initial store $\tau: \text{Id} \rightarrow \text{Arr} \cup \text{Cmd}$, relating identifiers to their initial value;

* a system call map $\gamma: \text{Sys} \rightarrow \text{Cmd}$ associating system calls to their implementation; and

* a capability map $\xi: \text{Sys} \rightarrow \mathcal{P}(\text{Id}_k)$ associating system calls with their capabilities.

We require that the code $\tau(f)$ associated with user space identifiers $f \in \text{Procld}_u$ is *unprivileged*, i.e. ids($\tau(f)$) $\subseteq$ \text{Id}_u, where ids(C) $\subseteq$ \text{Id} is the set of identifiers literally occurring in C. As our notion of safety will be defined in terms of system calls' capabilities, we furthermore require that the set of capabilities $\xi(s)$ of a system call *s* includes all identifiers that *s* refers to, directly in its body, or indirectly through procedure or system calls. To define this latter requirement formally, let $\text{refs}_\sigma(C) \subseteq \text{Id} \cup \text{Sys}$ denote the set of identifiers and system calls that the command C refers to, directly or indirectly. Specifically, we call syscalls(C) the set of system calls in C, and we define $\text{refs}_\sigma(C)$ as the smallest set such that: (a) ids(C) $\cup$ syscalls(C) $\subseteq$ $\text{refs}_\sigma(C)$, where (b) if $f \in \text{refs}_\sigma(C)$ then ids($\tau(f)$) $\subseteq$ $\text{refs}_\sigma(C)$, and likewise, (c) if $s \in \text{refs}_\sigma(C)$ then ids($\gamma(s)$) $\subseteq$ $\text{refs}_\sigma(C)$. The requirement can now be stated as $\text{refs}_\sigma(\gamma(s)) \setminus \text{Sys} \subseteq \xi(s)$.

## 3.2 Semantics

We now endow our language with an operational semantics. To define our notion of safety, we directly define an *instrumented semantics*, which signals capability violations. Semantics cannot be defined directly on stores, which directly relate identifiers to their values. Instead, to model address-based memory accesses, we introduce *memories*.

*Memories.* A *memory* is a function $m: \text{Addr} \rightarrow \text{Val} \cup \text{Cmd} \cup \{*\}$ associating addresses with their content, or to the special symbol $*$ $\notin$ *Val* if the location is not occupied. We denote by *Mem* the set of all memories. Arrays will be represented by sequences of values in contiguous memory locations. We use $m[p \leftarrow v]$ to denote the memory that is pointwise identical to $m \in \text{Mem}$, except for the address $p \in \text{Addr}$ that is mapped to $v \in \text{Val}$. Note that updates are restricted to values, in particular updating a memory location with a command is forbidden. Thereby we model a W^X memory protection policy, separating writable from executable memory regions.

*Layouts.* A (*memory*) *layout* is a function $w: \text{Id} \rightarrow \text{Addr}$ that describes where objects are placed in memory. As we mentioned, an array *a* is stored as a continuous block at addresses $w(a) \triangleq \{w(a), \dots, w(a) + \text{size}(a) - 1\}$ within memory. For procedure identifiers $f$, we set $w(f) \triangleq \{w(f)\}$. We overload this notation to sets of identifiers in the obvious way. In particular, $w(\text{Arrld})$ and $w(\text{Procld})$ refer, respectively, to the address-spaces of arrays and procedures under the layout $w$. We regard only layouts that associate identifiers with non-overlapping blocks ($w(id_1) \cap w(id_2) = \emptyset$ for all $id_1 \ne id_2$) and that respect address space separation ($w(id) \subseteq \text{Addr}_b$ for $id \in \text{Id}_b, b \in \{u, k\}$).
$$ \frac{[\mathbb{E}]_{\rho,w}^{\text{Addr}} = p \quad p \in \underline{w}(\text{Arrld}_b) \quad [b = k_s \Rightarrow p \in \underline{w}(\xi(s))]}{w \vdash_{\sigma} ((x := *E; C, \rho, b) : F, m) \rightarrow ((C, \rho[x \leftarrow m(p)], b) : F, m)}_{\text{LOAD}} $$

$$ \frac{[\mathbb{E}]_{\rho,w}^{\text{Addr}} = p \quad p \notin \underline{w}(\text{Arrld}_b)}{w \vdash_{\sigma} ((x := *E; C, \rho, b) : F, m) \rightarrow \text{err}}_{\text{LOAD-ERROR}} $$

$$ \frac{[\mathbb{E}]_{\rho,w}^{\text{Addr}} = p \quad p \in \underline{w}(\text{Arrld}_k) \quad [p \notin \underline{w}(\xi(s))]}{w \vdash_{\sigma} ((x := *E; C, \rho, k_s) : F, m) \rightarrow \text{unsafe}}_{\text{LOAD-UNSAFE}} $$

$$ \frac{[\mathbb{E}]_{\rho,w}^{\text{Addr}} = p \quad p \in \underline{w}(\text{Arrld}_b) \quad [b = k_s \Rightarrow p \in \underline{w}(\xi(s))]}{w \vdash_{\sigma} ((*E := F; C, \rho, b) : F, m) \rightarrow ((C, \rho, b) : F, m[p \leftarrow [\mathbb{F}]_{\rho,w}])}_{\text{STORE}} $$

$$ \frac{[\mathbb{E}]_{\rho,w}^{\text{Addr}} = p \quad p \notin \underline{w}(\text{Arrld}_b)}{w \vdash_{\sigma} ((*E := F; C, \rho, b) : F, m) \rightarrow \text{err}}_{\text{STORE-ERROR}} $$

$$ \frac{[\mathbb{E}]_{\rho,w}^{\text{Addr}} = p \quad p \in \underline{w}(\text{Arrld}_k) \quad [p \notin \underline{w}(\xi(s))]}{w \vdash_{\sigma} ((*E := F; C, \rho, k_s) : F, m) \rightarrow \text{unsafe}}_{\text{STORE-UNSAFE}} $$

$$ \frac{[\mathbb{E}]_{\rho,w}^{\text{Addr}} = p \quad p \in \underline{w}(\text{Procld}_b) \quad [b = k_s \Rightarrow p \in \underline{w}(\xi(s))]}{w \vdash_{\sigma} ((\text{call } E(\vec{F}); C, \rho, b) : F, m) \rightarrow ((m(p), \rho_0[\vec{x} \leftarrow [\mathbb{F}]_{\rho,w}], b) : (C, \rho, b) : F, m)}_{\text{CALL}} $$

$$ \frac{[\mathbb{E}]_{\rho,w}^{\text{Addr}} = p \quad p \notin \underline{w}(\text{Procld}_b)}{w \vdash_{\sigma} ((\text{call } E(\vec{F}); C, \rho, b) : F, m) \rightarrow \text{err}}_{\text{CALL-ERROR}} $$

$$ \frac{[\mathbb{E}]_{\rho,w}^{\text{Addr}} = p \quad p \in \underline{w}(\text{Procld}_k) \quad [p \notin \underline{w}(\xi(s))]}{w \vdash_{\sigma} ((\text{call } E(\vec{F}); C, \rho, k_s) : F, m) \rightarrow \text{unsafe}}_{\text{CALL-UNSAFE}} $$

$$ \frac{b = u \Rightarrow b' = k_s \quad b = k_t \Rightarrow b' = k_t}{w \vdash_{\sigma} ((\text{syscall } s(F_1, \dots, F_n); C, \rho, b) : F, m) \rightarrow ((\gamma(s), \rho_0[\vec{x} \leftarrow [\mathbb{F}]_{\rho,w}], b') : (C, \rho, b) : F, m)}_{\text{SC}} $$

$$ \frac{w \vdash_{\sigma} ((\epsilon, \rho, b) : (C, \rho', b') : F, m) \rightarrow ((C, \rho'[\text{ret} \leftarrow \rho(\text{ret})], b') : F, m)}{[\text{Pop}]} $$

<caption>Fig. 3. Semantics w.r.t. system $\sigma = (\tau, \gamma, \xi)$, excerpt.</caption>

*Small step operational semantics.* Transitions in our semantics take the form

$$ w \vdash_{\sigma} \phi \rightarrow \chi, $$

indicating that, w.r.t. system $\sigma$, configuration $\phi$ reduces to $\chi$ in one step, under layout $w$. The most important reduction rules are defined in Figure 3. Rule [LOAD] implements a successful memory load $x := *E$. The expression $E$ is evaluated to an address $p = [\mathbb{E}]_{\rho,w}^{\text{Addr}}$, and the content of the register $x$ is updated with the value $m(p)$. The side-condition $p \in \underline{w}(\text{Arrld}_b)$ enforces that $p$ refers
to a value accessible in the current execution mode *b* (by slight abuse of notation, we disregard the system call label in kernel-mode), otherwise the instruction leads to err (see Rule [LOAD-ERROR]). As such, we are modeling unprivileged execution and SMAP protection, preventing the access of kernel-space addresses when in user-mode, and vice versa. The final, boxed, side-condition refers to the safety instrumentation. In kernel-mode, triggered by system call *s* (*b* = *k*<sub>s</sub>), the rule ensures that *p* refers to an object within the capabilities of *s* (*p* ∈ *w*(*ξ*(*s*))). When this condition is violated, unsafe execution is signaled (see Rule [LOAD-UNSAFE]). The rules for memory writes and procedure calls are defined in a similar fashion.

Rule [CALL] deals with procedure calls. It opens a new frame and, places the *n* evaluated arguments $F_1, \dots, F_n = \bar{F}$ at registers $x_1, \dots, x_n = \bar{x}$ in an initial register environment $\rho_0$, summarized by the notation $\rho_0[\bar{x} \leftarrow [[\bar{F}]_{\rho,w}]]$. Notice that our choice does not exclude stack-based inter-procedural communication from our model: procedures can use a dedicated array as stack, and pass stack and return pointers as arguments. System calls, modeled by Rule [SC], follow the same calling convention. Note that, in the newly created frame, the execution flag is set to kernel-mode. Once a procedure or system call finishes, Rule [Pop] removes the introduced frame from the stack. Observe how the rule permits return values through a designated register *ret*. The remaining rules are standard.

Let us denote by $w \vdash_{\sigma} \phi \to^* \chi$ that configuration $\phi$ reduces in zero or more steps to configuration $\chi$, and by $w \vdash_{\sigma} \phi \uparrow$ that $\phi$ diverges. In our semantics, under layout $w$, any non-diverging computation either halts in a terminal configuration of the form $\langle\langle\epsilon, \rho, b\rangle, w \diamond \tau'\rangle$, or abnormally terminates through an error err, or safety violation unsafe. This motivates the following definition of an evaluation function:

$$ \text{Eval}_{\sigma,w}(C, \rho, b, \tau) \triangleq \begin{cases} (v, \tau') & \text{if } w \vdash_{\sigma} (\langle C, \rho, b \rangle, w \diamond \tau) \to^* (\langle \epsilon, \rho' \mid [\text{ret} \mapsto v], b \rangle, w \diamond \tau'), \\ \text{err} & \text{if } w \vdash_{\sigma} (\langle C, \rho, b \rangle, w \diamond \tau) \to^* \text{err}, \\ \text{unsafe} & \text{if } w \vdash_{\sigma} (\langle C, \rho, b \rangle, w \diamond \tau) \to^* \text{unsafe}, \\ \Omega & \text{if } w \vdash_{\sigma} (\langle C, \rho, b \rangle, w \diamond \tau) \uparrow. \end{cases} $$

Note how, in the case of normal termination, a computation produces a pair of a return value and a store.

# 4 Threat Model

In our threat model, attackers are unprivileged user-space programs that execute on a machine supporting two privilege rings: user-mode and kernel-mode. The victim is the host operating system which runs in kernel mode and has exclusive access to its private memory. In particular, the operating system exposes a set of procedures, the system calls, that can be invoked by the attacker and that have access to kernel's memory. The attacker's goal is to trigger a system call to perform an unsafe memory access or control flow transfer.

In Section 5, attackers are ordinary programs that do not control speculative execution and do not have access to side-channel info-leaks. However, the target machine has standard kernel protection measures enabled. In particular, these measures include *Data Execution Protection* mechanisms (DEP), *Supervisor Mode Access Prevention* (SMAP) [20] preventing kernel-mode access to user-space data, and *Supervisor Mode Execution Prevention* (SMEP) [35] preventing the execution of user-space functions when running in kernel-mode. More precisely, the above-mentioned protection mechanisms are modeled in our semantics by the preconditions of Rules [CALL], [LOAD], [STORE] that prevent the system from: (i) loading and overwriting procedures, (ii) execute values, (iii) accessing user-space data and procedures when the system is in kernel-mode. Although we assume
that the victim's code remains immutable, our results naturally extend to scenarios where a victim may load new code. Indeed, for any victim that introduces new vulnerable code at runtime, we can consider the victim that has already loaded that code and is at least as vulnerable as the first one. We also assume that the victim hardware supports Intel® Indirect Branch Tracking (IBT) [49], to restrict control flow transfer only to specific program points, typically the beginning of a procedure. This is modeled by restricting the target of indirect call instructions to the beginning of procedures only. Finally, the system adopts kernel address space layout randomization, that is modeled by executing programs with a randomly chosen memory layout.

In Section 6, we consider a stronger threat model where attackers have access to side-channel observations and control *Pattern History Table* (PHT), *Branch Target Buffer* (BTB) and *Store To Load* (STL) dependency prediction, related to Spectre v1, v2 and v4 vulnerabilities, respectively [51]. In addition, we assume that the system supports *Page Table Isolation* (PTI) [50] to prevent speculative accesses to kernel-space memory by user-space program; this is modeled by using the same preconditions of Rules [CALL], [LOAD], [STORE] for their speculative counterparts in Section 6.1.1. We also assume that the victim's machine supports a specific class of indirect branch instructions where the user cannot influence the jump target prediction—this result can be achieved by using retpoline when it is fully effective [24] or by using Intel® enhanced Indirect Branch Restricted Speculation (eIBRS) [21] and BHI_DIS_S [24]. This is modeled by adding an instruction for speculatively safe jumps to the victim's language in Section 8.

Finally, we assume that the victim machine does not support return address speculation (exploited by attacks such as Retbleed [85]), and we model it by not allowing any form of return target speculation. Phantom speculation [79, 86] is out of scope for this work, and the correspondent speculation mechanism is not modeled.

# 5 Kernel Safety in the Classic Threat Model

In this section we show how the result of Abadi et. al. [2–4] scales to the model introduced in Section 3. The safety property that we aim at is defined in terms of our instrumented semantics, as follows:

**Definition 1 (Kernel safety).** We say that a system $\sigma = (\tau, \gamma, \xi)$ is *kernel safe*, if for every layout $w$, *unprivileged attacker* $C \in \text{Cmd}$, and registers $\rho$, we have:

$$ \neg (w \vdash_{\sigma} (\langle C, \rho, u \rangle, w \diamond \tau) \rightarrow^* \text{unsafe}). $$

Thus, safety is broken if an attacker $C$, executing in unprivileged user mode, is able to trigger a system call in such a way that it accesses, or invokes, a kernel-space object outside its capabilities. The source of such a safety violation can be twofold:

1. **Scope extrusion.** An obvious reason why kernel-safety may fail is due to apparent communication channels, specifically through the memory and procedure returns. As an example, consider a system $\sigma = (\tau, \gamma, \xi)$, where:

$$ \gamma(s_1) \triangleq *a := f \qquad \gamma(s_2) \triangleq x := *a; \text{call } x() \qquad \xi(s_1) = \xi(s_2) = \{a\} $$

A malicious program can use $s_1$ to store the address of $f$ at $a[0]$, which is a shared capability. A consecutive call to $s_2$ then breaks safety if $f$ is not within the capabilities of $s_2$.

2. **Probing.** Another source of safety violations is given by a system call accessing memory based on its input, such as the system call that only contains the instruction `call x1()`, which directly invokes the procedure stored at the kernel-address corresponding to the value of its first argument $x_1$. This system call can potentially be used as a gadget to invoke an arbitrary kernel-space procedure from user-space. Since an attacker lacks knowledge of the kernel-space layout, such an invocation needs to happen effectively through probing. As any probe of an
unused memory address leads to an unrecoverable error,<fnref n="1" /> the likelihood of an unsafe memory access is, albeit not zero, diminishingly small when the address-space is reasonably large.

To overcome Issue 1, we impose a form of (layout) non-interference on system calls.

**Definition 2 (Layout non-interference).** Given $\sigma = (\tau, \gamma, \xi)$, a system call s is layout non-interfering, if,

$$Eval_{\sigma, w_1}(\gamma(s), \rho, k_S, \tau') \cong Eval_{\sigma, w_2}(\gamma(s), \rho, k_S, \tau')$$

for all layouts $w_1, w_2$, registers $\rho$ and stores $\tau' =_{\text{Procld}} \tau$. Here, the equivalence $\cong$ extends equality with $\text{err} \cong$ unsafe and unsafe $\cong$ err. The system $\sigma$ is non-interfering if all its system calls are.

In effect, layout non-interfering systems do not expose layout information, neither through the memory nor through return values. In particular, observe how non-interference rules out Issue 1, as witnessed by two layouts placing f at different addresses in kernel-memory.

Concerning Issue 2, it is well known that layout randomization provides in general safety not in an absolute sense, but probabilistically [4, 12, 78]. Indeed, the chance for a probe to be successful depends on the randomization scheme. Following Abadi and Plotkin [4], let $\mu$ be a probability distribution of layouts, i.e., a function $\mu: \text{Layout} \to [0, 1]$ assigning to each layout $w \in \text{Layout}$ a probability $\mu(w)$ (where $\sum_{w \in \text{Layout}} \mu(w) = 1$). Without loss of generality, we assume that the layout of user-space addresses is fixed. For a distribution of layouts $\mu$ and a system $\sigma = (\tau, \gamma, \xi)$, we denote with $\delta_{\mu,\sigma}$ the smallest probability that when probing for an address $p \in \text{Addr}_k$ the system reaches an err state. In practice, $\delta_{\mu,\sigma}$ bounds the probability that, during the execution of a system call s, a probe fails.

Lemmas 1 and 2 prove the adequacy of $\delta_{\mu,\sigma}$ in the presence of layout non-interference. More precisely, Lemma 1 proves this property for partial system call evaluations, and Lemma 2 lifts the result to complete evaluations.

**LEMMA 1.** Let s be a system call of a layout non-interfering system $\sigma = (\tau, \gamma, \xi)$, and let $\text{refs}_\sigma(\gamma(s)) \setminus \text{Sys} = \{\text{id}_1, \dots, \text{id}_h\}$ be identifiers within the references of s. Given a sequence of addresses $p_1, \dots, p_h$, an initial frame $\langle\gamma(s), \rho, k_S\rangle$, and a store $\tau'$ such that $\tau' =_{\text{Procld}} \tau$, for every reduction length $n \in \mathbb{N}$ and distribution of layouts $\mu$, one of the following statements holds:

(1) For every layout $w$ such that $\forall 1 \le i \le h$, $w(\text{id}_i) = p_i$, we have $w \vdash_\sigma (\langle\gamma(s), \rho, k_S\rangle, w \diamond \tau') \to^n (\bar{F}, w \diamond \bar{\tau})$ for some non-empty stack $\bar{F}$ and store $\bar{\tau} =_{\text{Procld}} \tau'$.

(2) For every layout $w$ such that $\forall 1 \le i \le h$, $w(\text{id}_i) = p_i$, we have $w \vdash_\sigma (\langle\gamma(s), \rho, k_S\rangle, w \diamond \tau') \to^{n'} (\langle\epsilon, \bar{\rho}, k_S\rangle, w \diamond \bar{\tau})$ for some $n' \le n, \bar{\rho}$ and store $\bar{\tau} =_{\text{Procld}} \tau'$.

(3) $\text{Pr}_{w \leftarrow \mu} [\exists n' \le n.w \vdash_\sigma (\langle\gamma(s), \rho, k_S\rangle, w \diamond \tau') \to^{n'} \text{err} | \forall 1 \le i \le h.w(\text{id}_i) = p_i] \ge \delta_{\mu,\sigma}$.

**PROOF SKETCH OF LEMMA 1.** The proof proceeds by induction on $n$ and case analysis on the transition rules. In particular, when a configuration tries to access a memory address $p \notin \text{refs}_\sigma(\gamma(s))$, we must observe that:

$$\text{Pr}_{w \leftarrow \mu} [\exists n' \le n.w \vdash_\sigma (\langle\gamma(s), \rho, k_S\rangle, w \diamond \tau') \to^{n'} \text{err} | \forall 1 \le i \le h.w(\text{id}_i) = p_i] \ge \delta_{\mu,\sigma},$$

which follows by definition of $\delta_{\mu,\sigma}$.

<figure><img src="image_3.png" /></figure>

**LEMMA 2.** Let s be a system call of a layout non-interfering system $\sigma = (\tau, \gamma, \xi)$. Given an initial frame $\langle\gamma(s), \rho, k_S\rangle$, and a store $\tau'$ such that $\tau' =_{\text{Procld}} \tau$, for every distribution of layouts $\mu$, one of the following statements holds:

<footnote n="1">¹This is not always the case for user-space software protected with layout randomization, as some programs (e.g. web servers) may automatically restart after a crash to ensure availability. This behavior can be exploited by attackers to probe the entire memory space of the victim program, thus compromising the protection offered by layout randomization [75].</footnote>
(1) For every layout w, we have $Eval_{\sigma,w}(\gamma(s), \rho, \tau', k_s) = (\bar{\tau}, \bar{v})$, for some $\bar{v}$ and $\bar{\tau} =_{\text{Procl'd}} \tau$.

(2) For every layout w, we have $Eval_{\sigma,w}(\gamma(s), \rho, k_s, \tau') = \Omega$.

(3) $\Pr_{w \leftarrow \mu} [Eval_{\sigma,w}(\gamma(s), \rho, k_s, \tau') = \text{err}] \ge \delta_{\mu,\sigma}$.

PROOF SKETCH OF LEMMA 2. The proof is by case analysis: if for some w, $Eval_{\sigma,w}(\gamma(s), \rho, k_s, \tau') \notin \{\text{err, unsafe}\}$, claims (1) or (2) must hold because of layout non-interference. On the other hand, if all layouts lead to err or to unsafe, due to the finiteness of Layout, there exists an upper bound t on the number of steps needed to reach a terminal configuration. We call refs($\gamma(s)$) $\setminus$ Sys = $\{\text{id}_1, \dots, \text{id}_h\}$ and apply Lemma 1 with $n = t$. Observe that for every choice of $p_1, \dots, p_h \in \text{Addr}_k$, we can refuse conclusions (1) and (2) of that lemma because they are contradictory with $\forall w. Eval_{\sigma,w}(\gamma(s), \rho, k_s, \tau') \in \{\text{err, unsafe}\}$, so (3) of Lemma 1 must hold. Observe that:

$$ \Pr_{w \leftarrow \mu} [Eval_{\sigma,w}(\gamma(s), \rho, k_s, \tau') = \text{err}] = \Pr_{w \leftarrow \mu} [\exists n' \le n.w \vdash_{\sigma} (\langle\gamma(s), \rho, k_s\rangle, w \diamond \tau') \to^{n'} \text{err}]. $$

The right-hand-side, in turn, is equal to:

$$ \sum_{p_1, \dots, p_k} \Pr_{w \leftarrow \mu} \left[ \exists n' \le n.w \vdash_{\sigma} (\langle\gamma(s), \rho, k_s\rangle, w \diamond \tau') \to^{n'} \text{err} \mid \forall 1 \le i \le h.w(\text{id}_i) = p_i \right]. $$

$$ \Pr_{w \leftarrow \mu} \left[ \forall 1 \le i \le h.w(\text{id}_i) = p_i \right]. $$

According to conclusion (3) of Lemma 1, all the factors on the left are bounded by $\delta_{\mu,\sigma}$, therefore their convex combination is also bounded, proving (3). $\square$

We arrive now at the main result of this section, where we show the effectiveness of layout randomization:

THEOREM 1. Let $\sigma = (\tau, \gamma, \xi)$ be layout non-interfering. Then, for any unprivileged attacker $C \in \text{Cmd}$ and register map $\rho, \mathbb{P}_{w \leftarrow \mu} [Eval_{\sigma,w}(C, \rho, u, \tau) = \text{unsafe}] \le 1 - \delta_{\mu,\sigma}$.

PROOF. The unsafe state can only be reached during the execution of a system call. Lemma 2 provides a lower bound on the probability of reaching err, and thereby an upper bound on the probability of reaching unsafe. $\square$

Theorem 1 extends the results of Abadi et al. [2–4] by showing that layout randomization guarantees kernel safety probabilistically to operating systems; in contrast with Abadi et al.’s work, this holds even when victim’s code contains unsafe programming constructs, such as arbitrary pointer arithmetic and indirect jumps. This is achieved by replacing Abadi et al.’s restrictions on the syntax of victim programs with a weaker dynamic property: layout non-interference.

Notice that the strength of the security guarantee provided by Theorem 1 depends on the distribution of the layouts $\mu$. Therefore, in practice, it is important to employ randomization schemes that provide strong guarantees. For instance, a suitable randomization scheme picks the base addresses of kernel arrays and procedures uniformly and independently from the multiples of a fixed step size, which is bigger than the size of the largest array to prevent overlaps between allocated regions [31, Section 5].

Relation of kernel safety with security. Kernel safety encompasses some form of spatial memory safety and of control flow integrity, which are among the most critical security properties of operating systems’ kernels. This importance is reflected in the numerous measures developed to enforce such properties [38, 55, 65, 70, 72, 81]. Often, definitions of spatial memory safety associate a software component (a program, an instruction, or even a variable) with a fixed memory area, that this component can access rightfully [7, 10, 64, 66]. In this realm, any load or store operation that does
not fall within this area is considered a violation of *spatial memory safety*. Our notion of *kernel safety* encompasses a form of *spatial memory safety*: if a system enjoys *kernel safety*, then no system call can access a memory region that does not appear within its capabilities. In addition, *kernel safety* also implies a form of *control flow integrity*: a property which requires that the control flow of a program can reach only specific statically determined targets [1]. More precisely, in our semantics it is unsafe to execute a procedure if its address does not belong to the set of capabilities of the current system call. This means that, if a system $(\tau, \gamma, \xi)$ is *kernel safe*, when executing a system call *s*, the control flow will remain across the procedures in $\xi(s)$.

*Final remarks.* Kernel-space layout randomization provides *kernel safety* in a probabilistic sense. In particular, the probability of violating safety depends on the randomization scheme. For certain randomization schemes, this probability approaches zero when the size of the address space goes to infinity. Finally, *kernel safety* provides essential security guarantees by enforcing both *spatial memory safety*—restricting memory accesses to authorized regions—and *control flow integrity*—ensuring that control flow transfers occur only to permitted procedures.

# 6 Kernel Safety in the Speculative Threat Model

In this section we study *kernel safety* in the presence of speculative attackers. To this end, in Section 6.1, we extend the model of Section 3 for this new scenario. More precisely, we endow the semantics of Section 3 with speculative execution and side-channel observations that reveal the accessed addresses and the value of conditional branches [10, 16, 44, 45]. In Section 6.2, we refine the notion of *kernel safety* for this model, by defining *speculative kernel safety*.

## 6.1 The Speculative Execution Model

A popular way to model speculative attacks is by annotating transitions with *directives* that describe the choices made by microarchitectural prediction units [10, 16, 44, 45]. For instance, PHT speculation can be modeled by the directives *br true* and *br false* that, in the presence of a branching command, instruct the processor to speculatively execute the first and the second branch, respectively. In this realm, reductions are driven by sequences of directives governing each transition. Therefore, stating the absence of a speculative attack boils down to stating the absence of a sequence of directives that steer the execution to a bad event. This also means that attacks are never explicitly represented as computational objects, but only as sequences of possibly unrelated directives.

Also our model uses directives to guide predictors; however our approach allows attackers to be explicitly represented as fully-fledged programs equipped with primitives for steering speculative execution and perform side-channel observations. This permits us to naturally extend the notion of *kernel safety* to the new scenario. Besides, we believe that modeling an attack explicitly can be interesting on its own. The feasibility of an attack is witnessed explicitly through a program. In this setting, for instance, assumptions on the attacker's computational capabilities can be imposed seamlessly.

We extend the victim's language and semantics by introducing directives and observations in Section 6.1.1, and then we define the attacker's language in Section 6.1.2.

### 6.1.1 Victim Language and Semantics.
The victims' language remains identical to the classic model, except that we assume that load, branch and call instructions are tagged by unique labels $l \in Lbl$ in order to model the ability of attackers to influence their speculative execution. For example, a tagged load operation looks like $x := l *E$, and can be targeted only with directives with label $l$. We show labels alongside with commands only when they are relevant—e.g. the command is being executed speculatively—and they cannot be inferred from the context.
The speculative semantics is instrumented through *directives*, modeling the choice made by prediction units of the processor. Directives take the form:

$$d \ni \text{Dir} ::= \text{br}_l b \mid \text{run}_l p \mid \text{ld}_l i \mid \text{bt} \mid \text{st},$$

where $i \in \mathbb{N}$, $p \in \text{Addr}$, and $b \in \text{Bool}$. The `br` $b$ directive causes a branch instruction to be evaluated as if the guard resolved to $b$, modeling PHT speculation. The `run` $p$ directive causes a call instruction to execute the procedure stored at address $p$ (if any), modeling BTB speculation. The directive `ld` $i$ causes the load instruction to load the $i$-th most recent value that is associated with the load address from the (buffered) memory, modeling STL speculation. The `bt` directive directs speculations, either backtracking the most recent mis-speculation or committing the microarchitectural state. Finally, the `st` directive evaluates instructions without engaging into speculation, in correspondence to the semantics given in Section 3.

Transitions are also labeled with observations to model timing side-channel leakage. Observations are drawn from the following grammar:

$$o, q \ni \text{Obs} ::= \bullet \mid \text{br} b \mid \text{mem} p \mid \text{jmp} p \mid \text{bt} b,$$

where $b \in \text{Bool}$ and $p \in \text{Addr}$. We use $\bullet$ to label transitions that do not leak specific data. The `br` $b$ observation is caused by branching instructions, with $b$ reflecting the taken branch. The `mem` $p$ observation is caused by memory access, through loads or stores, and contains the address of the accessed location, thus modeling data-cache leaks. Likewise, the `jmp` $p$ observation is caused by calls to procedures residing at address $p$ in memory, modeling instruction-cache leaks. Finally, the `bt` $b$ observation signals a backtracking step during speculative execution. Notice that we leak full addresses on memory accesses, and the value of the branching instructions, i.e. we adopt the *baseline leakage model* that is widely employed in the literature to model side-channel info-leaks [6, 9, 10, 16].

A reduction step now takes the form:

$$w \vdash_{\sigma} S \xrightarrow{o} S',$$

indicating that for a given system $\sigma$, under layout $w \in \text{Layout}$, the system evolves from state $S$ with directive $d \in \text{Dir}$ to $S'$ in one step, producing the side-channel observation $o$. States are described by the following BNF:

$$\begin{align*}
S &::= \epsilon \mid \phi : S \\
\phi, \chi &::= (F, \psi, b_{ms}) \mid (\text{err}, b_{ms}) \mid \text{unsafe} \\
\psi &::= (\mu, m) \\
\mu &::= \epsilon \mid [p \mapsto v] : \mu
\end{align*}$$

Here, $S$ is a stack of backtrackable configurations. During the execution, the state of the system is described by the configuration on top of the stack. To support backtracking, every time a speculation occurs, the system pushes a new configuration to the stack and keeps track of the current state in the configuration just below.

In a configuration $(F, \psi, b_{ms})$, $F$ is a call-stack as in Section 3, $\psi$ is a memory $m$ equipped with a *write buffer* $\mu$, and the Boolean value $b_{ms}$ is the *mis-speculation* flag. The mis-speculation flag governs backtracking of speculative execution: when its value is $\top$, some previous speculation may be incorrect, so a backtracking step will discard the configuration from the stack. As errors are recoverable under mis-speculation, error configurations carry a mis-speculation flag too. As in Section 3, unsafe indicates a safety violation.

Buffered memories are used to model STL speculation, and are based on those from [10]. Writing a value $v$ at address $p$ results in a delayed write $[p \mapsto v]$ that is appended to the buffer $\mu$, in notation:
$$ \frac{\begin{array}{c} \llbracket E \rrbracket_{\rho,w}^{\text{Addr}} = p \\ \phi = (\langle x :=_l *E; C, \rho, b \rangle : F, \psi, b_{ms}) \end{array}}{\begin{array}{c} \psi^i(p) = (v, f) \\ p \in \mathbf{w}(\text{Arrld}_b) \end{array}} \boxed{b = k_S \Rightarrow p \in \mathbf{w}(\xi(s))} \qquad \text{[SLOAD-LOAD]} $$

$$ w \vdash_{\sigma} \phi : S \xrightarrow{\text{mem } p \atop \text{ld}_l i} (\langle C, \rho [x \leftarrow v], b \rangle : F, \psi, b_{ms} \lor f) : \phi : S $$

$$ \frac{\begin{array}{c} \llbracket E \rrbracket_{\rho,w}^{\text{Addr}} = p \quad p \notin \mathbf{w}(\text{Arrld}_b) \quad d = \text{st} \lor d = \text{ld}_l i \\ w \vdash_{\sigma} (\langle x :=_l *E; C, \rho, b \rangle : F, \psi, b_{ms}) : S \xrightarrow{\bullet} (\text{err}, b_{ms}) : S \end{array}}{p \notin \mathbf{w}(\xi(s))} \qquad \text{[SLOAD-ERROR]} $$

$$ \frac{\begin{array}{c} \llbracket E \rrbracket_{\rho,w}^{\text{Addr}} = p \quad p \in \mathbf{w}(\text{Arrld}_k) \quad d = \text{st} \lor d = \text{ld}_l i \end{array}}{p \notin \mathbf{w}(\xi(s))} \qquad \text{[SLOAD-UNSAFE]} $$

$$ w \vdash_{\sigma} (\langle x :=_l *E; C, \rho, k_S \rangle : F, \psi, b_{ms}) : S \xrightarrow{\text{mem } p \atop d} \text{unsafe} $$

$$ \frac{\begin{array}{c} \llbracket E \rrbracket_{\rho,w}^{\text{Addr}} = p \quad \psi^0(p) = v, \perp \quad p \in \mathbf{w}(\text{Arrld}_b) \end{array}}{b = k_S \Rightarrow p \in \mathbf{w}(\xi(s))} \qquad \text{[SLOAD-STEP]} $$

$$ w \vdash_{\sigma} (\langle x := *E; C, \rho, b \rangle : F, \psi, b_{ms}) : S \xrightarrow{\text{mem } p \atop \text{st}} (\langle C, \rho [x \leftarrow v], b \rangle : F, \psi, b_{ms}) : S $$

$$ \frac{\phi = (\langle \text{if}_l E \text{ then } D \text{true else } D \text{false fi}; D, \rho, b \rangle : F, \psi, b_{ms})}{\text{SIF-BRANCH}} \qquad \text{[SIF-BRANCH]} $$

$$ w \vdash_{\sigma} \phi : S \xrightarrow{\text{br } d \atop \text{br}_l d} (\langle D_d; D, \rho, b \rangle : F, \psi, b_{ms} \lor d \neq \llbracket E \rrbracket_{\rho,w}^{\text{Bool}}) : \phi : S $$

$$ \frac{\phi = (\langle \text{call}_l E(\vec{F}); C, \rho, b \rangle : F, (\mu, m), b_{ms}) \quad p \in \mathbf{w}(\text{Procld}_b) \quad b = k_S \Rightarrow p \in \mathbf{w}(\xi(s))}{\text{SCALL}} \qquad \text{[SCALL]} $$

$$ w \vdash_{\sigma} \phi : S \xrightarrow{\text{jmp } p \atop \text{run}_l p} (\langle m(p), \rho_0[\vec{x} \leftarrow \llbracket \vec{F} \rrbracket_{\rho,w}, b \rangle : \langle C, \rho, b \rangle : F, (\mu, m), b_{ms} \lor (p \neq \llbracket E \rrbracket_{\rho,w}^{\text{Addr}}) \rangle) : \phi : S $$

$$ \frac{p \in \mathbf{w}(\text{Procld}_k) \quad p \notin \mathbf{w}(\xi(s))}{\text{SCALL-UNSAFE}} \qquad \text{[SCALL-UNSAFE]} $$

$$ w \vdash_{\sigma} (\langle \text{call}_l E(\vec{F}); C, \rho, k_S \rangle : F, \psi, b_{ms}) : S \xrightarrow{\text{jmp } p \atop \text{run}_l p} \text{unsafe} $$

$$ \frac{\phi = (\langle \text{call}_l E(\vec{F}); C, \rho, b \rangle : F, (\mu, m), b_{ms}) \quad p \notin \mathbf{w}(\text{Procld}_b)}{\text{SCALL-ERROR}} \qquad \text{[SCALL-ERROR]} $$

$$ w \vdash_{\sigma} \phi : S \xrightarrow{\bullet} (\text{err}, b_{ms} \lor (p \neq \llbracket E \rrbracket_{\rho,w}^{\text{Addr}})) : \phi : S $$

$$ \frac{\phi = (F, \psi, \top) \lor \phi = (\text{err}, \top)}{\text{BT}_{\top}} \quad \phi = (F, \psi, \bot) \lor \phi = (\text{err}, \bot) \quad S \neq \epsilon \qquad \text{[BT}_{\bot}$$

$$ w \vdash_{\sigma} \phi : S \xrightarrow{\text{bt } \top \atop \text{bt}} S \qquad w \vdash_{\sigma} \phi : S \xrightarrow{\text{bt } \bot \atop \text{bt}} \phi : \epsilon $$

<caption>Fig. 4. Speculative semantics, excerpt.</caption>

$$ \begin{array}{l} (\epsilon, m)^n(p) \triangleq m(p), \perp \\ \qquad ([p' \mapsto v] : \mu, m)^n(p) \triangleq \begin{cases} (\mu, m)^n(p) & \text{if } p \neq p' \\ v', \top & \text{if } p = p', n > 0, \text{ and } (\mu, m)^{n-1}(p) = v', f \\ v, \perp & \text{if } p = p', \text{ and } n = 0. \end{cases} \end{array} $$

<caption>Fig. 5. Buffered memory lookup function.</caption>

([p' ↦ v] : μ, m). Reading the n-th most recent entry associated with p in a buffered memory is written (μ, m)^n(p) and yields a value v together with a boolean flag f that is ⊥ only if v is the most recent value associated with address p, as described in Figure 5. For a given buffer μ, its domain dom(μ) is the set of memory addresses of its delayed writes.
Some illustrative rules of the semantics are given in Figure 4, the complete set of rules is relegated to the extended version of this work [31]. The rules for load instructions are very similar to the ones we give in Section 3, but attackers can take advantage of the store-to-load dependency speculation by issuing a ld<sub>r</sub> i directive, as in Rule [SLOAD-LOAD]. When this happens, the i-th most recent value associated with the address p = [[E]]<sup>Addr</sup><sub>p,w</sub> is retrieved from the buffered memory. When such value may not correspond to the one of the most recent store operation to the address p, the flag f is ⊤. Depending on the value of f, Rule [SLOAD-LOAD] may be engaging mis-speculation and, for this reason, it keeps track of the starting configuration in the stack and updates the mis-speculation flag with f. A successful load produces the observation mem p that leaks the address to the attacker. The rules for erroneous and unsafe loads are [SLOAD-ERROR] and [SLOAD-UNSAFE]. These rules are analogous to their non-speculative counterparts. In our semantics, every command also supports the st directive, which does not cause speculation. For instance, Rule [SLOAD-STEP] evaluates the x := *E command by fetching the most recent value from the write buffer, instead of an arbitrary one.

Branch instructions can be executed speculatively by issuing the directive br *d* by means of Rule [SIF-BRANCH]. This directive causes the evaluation to continue as if the guard resolved to *d*. This operation leaks which branch is being executed by means of the observation br *d*.

Rule [SCALL] models indirect jump speculation by accepting the directive run *p*. When the call instruction is evaluated with such directive, the system invokes the procedure that is stored at address *p* (if any). This operation leaks the observation *jmp* *p*, which reveals that some procedure is stored at address *p*. To keep track of wrong speculation, the system checks whether the address supplied by the attacker corresponds to the intended jump location and updates the mis-speculation flag accordingly. The rules for erroneous and unsafe speculative call instructions [SCALL-ERROR] and [SCALL-UNSAFE] are similar to their non-speculative counterparts, with the exception that the address supplied by the attacker is used to determine whether the access is erroneous or unsafe.

If the topmost configuration of a stack carries the mis-speculation flag ⊤, some prior speculation may have been incorrect, so the configuration can be discarded with Rule [BT⊤]. If the mis-speculation flag is ⊥, the current state is not mis-speculating, so the whole stack of book-kept configurations can be discarded with Rule [BT⊥].

We write $\rightarrow^*$ for the multi-step reduction relation induced by $\rightarrow$, i.e, $S \xrightarrow{\epsilon} \rightarrow S$ and $S \xrightarrow{\frac{o:O}{d:D}} \rightarrow^* S'$ if

$S \xrightarrow{\frac{o}{d}} \circ \xrightarrow{\frac{O}{D}} \rightarrow^* S'$.

6.1.2 Attacker's Language and Semantics. To give a definition of kernel safety w.r.t. speculative semantics, we endow attackers with the ability to engage speculative execution, to issue directives, and to read side-channel leaks. To this end, we extend the instructions from Section 3 as follows:

$$ \text{SpInstr} \ni \text{SI} ::= \text{I} \mid \text{spec on C end} \mid \text{poison}(d) \mid x ::= \text{observe}(\text{S}) $$

$$ \text{SpAdv} \ni A ::= \varepsilon \mid \text{SI};A $$

The instruction `spec on C end` is used to execute a command C with the speculative semantics defined just above. The instruction `poison(d)` models the attacker's ability to control microarchitectural predictors and to control speculative execution by issuing the directive *d*, which is used to control the evaluation of instructions executed under speculative semantics. Dual, the instruction *x* := `observe()` is used to extract side-channel info-leaks, collected during speculative execution of commands. To model this operation, in the following, we assume `Obs` ⊆ `Val`. As an example, the
<figure><img src="image_4.png" /><figcaption>Fig. 6. Semantics for speculative attackers, excerpt.</figcaption></figure>

snippet

poison(br<sub>l</sub> T);
spec on if<sub>l</sub> E then syscall s(p) fi end; (†)
x := observe()

forces the mis-speculative execution of syscall s(p), independently of the value of E. The register
x will hold the final observation leaked through executing the system call.

The attacker's semantics is defined in terms of a relation

$w \vdash \phi \rightarrow \phi'$.$

Configurations for the attacker's semantics are drawn from the following BNF:

$$
\begin{align*}
\phi, \chi &::= (F, m, D, O) \mid S \mid (F, D, O) \mid \text{err} \mid \text{unsafe} \\
O &::= \epsilon \mid o : O \\
D &::= \epsilon \mid d : D.
\end{align*}
$$

Within attacker's configurations *F* is the evaluation stack (as in Section 3), and *m* is the memory.
The stacks *D* and *O* collect directives and observations respectively. We use hybrid configurations
*S* | (*F*, *D*, *O*) to model the execution of the command *spec on C end*. In hybrid configurations, the
state is given by the stack of speculative configurations *S*, and the frame stack *F* keeps tracks of
the procedure's activation records before the invocation of *spec on C end*. The stack *D* contains
the directives used by the speculative semantics of Section 6.1.1 to evaluate *S*. The stack *O* collects
the side-channel observations produced during speculative execution of *S*.

Figure 6 shows the evaluation rules for the new constructs. Rules [POISON] and [OBSERVE]
define the semantics for poisoning and side-channel observations, modeled by respectively pushing
and popping elements of the corresponding stacks. Rule [SPEC-INIT] deals with the initialization
of speculative execution for the command spec on C end by placing the program C in an initial
speculative stack within an hybrid configuration. A frame for the continuation of the attacker A is
left on the call stack F. This frame is used to resume execution of the attacker, once the victim has
been fully evaluated. The command C of the newly created hybrid configuration is evaluated via the speculative semantics through Rules [SPEC-D], [SPEC-S] and [SPEC-BT]. Note how execution of the victim is directed through the directive stack D (Rule [SPEC-D]). Should the current directive be inapplicable, a non-speculative rewrite step (Rule [SPEC-S]) or backtracking (Rule [SPEC-BT]) is performed. Here, the premise $w \vdash_{\sigma} S \downarrow_{d}$ signifies that S is irreducible w.r.t. the directive d. Likewise, $w \vdash_{\sigma} S \downarrow_{D}$ means that S is irreducible w.r.t. the topmost directive of D, or that D is empty. Also notice how side-channel leakage, modeled through observations, is collected in the configuration via these rules. Upon normal termination, resuming of evaluation of the attacker is governed by Rule [SPEC-TERM]. As a side-effect, this rule commits all buffered writes to memory, as described by the following function:

$$ (\overline{\epsilon, m}) \triangleq m \qquad (\overline{[p \mapsto v] : \mu, m}) \triangleq (\overline{\mu, m}) [p \leftarrow v]. $$

Finally, Rules [SPEC-ERROR] and [SPEC-UNSAFE] deal with abnormal termination.

Apart for the new constructs, the attacker executes under a semantics analogous to the one given in Section 3.

## 6.2 Speculative Kernel Safety

We are now ready to extend the definition of kernel safety (Definition 1) to the speculative semantics.

**Definition 3 (Speculative kernel safety).** We say that a system $\sigma = (\tau, \gamma, \xi)$ is *speculative kernel safe* if for every unprivileged attacker $A \in \text{SpAdv}$, every layout $w$, and register map $\rho$, we have:

$$ \neg (w \vdash_{\sigma} (\langle A, \rho, u \rangle, w \diamond \tau, \epsilon, \epsilon) \to^{*} \text{unsafe}). $$

It is important to note that this safety notion captures violations that occur during transient execution. This is in line with what happens, for instance, for Spectre and Meltdown [51, 57], both exploiting unsafe memory access under transient execution in order to reveal confidential information.

## 6.3 The Demise of Layout Randomization in the Spectre Era

A direct consequence of Definition 3 is that every system that is *speculative kernel safe* is also *kernel safe*. The inverse, of course, does not hold in general. Specifically, the probabilistic form of safety provided by layout randomization in Section 5 does not scale to this extended threat model. This happens for the following reasons:

1. **Side-channel leaks.** *Layout non-interference* (Definition 2) does not account for side-channel leakage. In practice, kernel-space gadgets that leak information on the kernel layout can be exploited by attacker to compromise layout randomization. For instance, with the following gadget

$$ \text{if } f = p \text{ then } C \text{ else } D \text{ fi,} \qquad (\ddagger) $$

an attacker who controls the value of $p$ may gather information on the address of the kernel procedure $f$ by measuring the execution time of this gadget for different values of $p$, assuming that the execution times of C and D are indeed different. In our model, this form of leak is captured by including the value of the guard in the observation produced when executing direct branches.

2. **Speculative execution.** With speculative execution, unsuccessful memory probes within transient executions do not lead to abnormal termination. This fact undermines another fundamental assumption of Theorem 1 and other studies demonstrating the efficacy of layout randomization [2–4], where memory access violations are not fully recoverable. As an example, consider the snippet (†) at page 18. This program will never reach an unrecoverable error state
even when the system call `s` loads an arbitrary address `p` from the memory. If `p` is not allocated, the system performs a memory violation under transient execution that does not terminate the execution, and does not modify the cache state. If `p` is allocated, its content may be loaded into the cache before the execution backtracks. By reading side-channel observations, an attacker can thus distinguish allocated kernel-addresses from those that are not allocated. This last example, in particular, is not at all fictitious: the BlindSide attack [41] uses the same idea to break Linux's KASLR and locate the position of kernel's executable code and data. In our model, we account for a similar attacks by using different observations for successful and unsuccessful memory operations (e.g., see Rules [SCALL] and [SCALL-ERROR]) and by allowing the backtrack of error states reached during transient execution.

## 6.4 Side-channel Layout Non-Interference

As this revised model significantly enhances the attackers' strength, we need to implement more stringent countermeasures in order to restore kernel safety. To counter side-channel info-leaks, we can impose a form of side-channel non-interference that is in line with the notion of speculative constant-time from [16], and that is meant to prevent side-channel info-leaks from leaking information on the kernel's memory layout.

**Definition 4 (Side-channel layout non-interference).** A system call `s` of a system $\sigma = (\tau, \gamma, \xi)$ is side-channel layout non-interferent if for every $\tau' =_{\text{Procld}} \tau$, directives `D`, observations `O`, register map $\rho$ and buffer $\mu$, we have:

$$ \exists S_1.w_1 \vdash_{\sigma} (\langle \gamma(s), \rho, k_s \rangle, (\mu, (w_1 \diamond \tau')), b_{ms}) \xrightarrow{O/D \to *} S_1 $$

implies

$$ \exists S_2.w_2 \vdash_{\sigma} (\langle \gamma(s), \rho, k_s \rangle, (\mu, (w_2 \diamond \tau')), b_{ms}) \xrightarrow{O/D \to *} S_2, $$

for all layouts $w_1, w_2$.

Side-channel layout non-interference ensures the non-leakage of layout information throughout the side-channels by requiring the identity of the sequences of observations produced by the two reductions. However, it indirectly implies severe restrictions on memory interactions—effectively prohibiting non-static memory accesses, that are the main ingredient of layout randomization! Unsurprisingly, this form of non-interference directly establishes kernel safety of system calls:

**LEMMA 3.** *Suppose $\kappa_k \ge \sum_{id \in \mathcal{I}_d} \text{size}(id) + 2 \cdot \max_{id \in \mathcal{I}_d} \text{size}(id)$. Given $\sigma = (\tau, \gamma, \xi)$, if `s` is side-channel layout non-interfering then*

$$ \neg \left( w \vdash_{\sigma} (\langle \gamma(s), \rho, k_s \rangle, (\mu, (w \diamond \tau')), b_{ms}) \xrightarrow{O/D \to *} \text{unsafe} \right) $$

for all layouts `w` and initial configurations over stores $\tau'$ coinciding with $\tau$ on Procld.

**PROOF SKETCH.** The condition on the size of the memory ensures that it is large enough to allow any array or procedure to be moved to a different location. With this precondition, we just need to observe that if an invocation of a system call `s` performs an unsafe memory access when executing under a layout `w`, the address `p` of the accessed resource is leaked; but the same address cannot leak if the resource is moved to another location, leaving `p` free. Therefore, if a system call is not speculatively safe, it cannot be side-channel layout non-interfering because different memory layouts produce different observations. □
<figure><img src="image_5.png" /><figcaption>Fig. 7. Attacks witnessing that $\sigma$ does not enjoy speculative kernel safety.</figcaption></figure>

While we do not formalize it here, our leakage model can be relaxed without invalidating Lemma 3. For instance, our result remains valid in a leakage model where the mem $p$ observation does not leak full addresses.

The following result, stating that *side-channel layout non-interference* entails *speculative kernel safety*, is a direct consequence of Lemma 3.

**THEOREM 2.** *Under the assumption $\kappa_k \ge \sum_{id \in \mathcal{I}_k} \text{size}(id) + 2 \cdot \max_{id \in \mathcal{I}_k} \text{size}(id)$, if a system $\sigma$ is side-channel layout non-interfering, then it is speculative kernel safe.*

**PROOF SKETCH.** As for Theorem 1, observe that the only way to reach the unsafe state is during the execution of a system call. Lemma 3 proves no system call can reach that the unsafe state under this theorem's assumptions. $\square$

*Final remarks.* In contrast with what happens in Theorem 1 of Section 5, the safety guarantee provided by Theorem 2 is not probabilistic and does not rely on *layout randomization*. Therefore, although layout randomization is unlikely to be restored at the software level without imposing *side-channel layout non-interference*, in the presence of this assumption, layout randomization is a redundant protection measure.

In general, non-interference properties do not necessarily entail memory safety. In our case, *side-channel layout non-interference* entails *speculative kernel safety* because the layouts are not only used as data, but they also determine *where* objects are placed in memory.

Notice that *side-channel layout non-interference* is not a necessary condition for *speculative kernel safety*. As an example, take the system that only defines the array *a* with size 1 and the system call *s* with body `*a := v`, and capabilities `{a}`. This system is not *side-channel layout non-interfering* because executing *s* leaks the address of *a*, which depends on the layout. However, the system is speculatively safe because the only operation it can do is writing to *a* through *s*, and *a* is in the capabilities of *s*.

# 7 Assessing the Effectiveness of Existing Mitigations for Speculative Kernel Safety

In this section we review state-of-art countermeasures against speculative attacks to assess to what extent they can help to enforce *speculative kernel safety*.

To this end, we introduce a system $\sigma = (\tau, \gamma, \xi)$ that is intentionally vulnerable to *speculative kernel safety* violations. The system includes a kernel function *f* that simply returns the constant 0, and which is not included in the capabilities of any system call. Additionally, the system defines the system calls *s*, *t*, and *u*, that can trigger transient execution via PHT, STL, and BTB speculation,
<table><caption>Table 1. Effectiveness of the protection mechanisms examined in sections 7 and 8 against the attacks in Figure 7.</caption><thead><tr><th>Protection mechanism</th><th>Attack A</th><th>Attack B</th><th>Attack C</th></tr></thead><tbody><tr><td>SLH and Eclipse</td><td>✓</td><td>✗</td><td>✗</td></tr><tr><td>SCT</td><td>✗</td><td>✗</td><td>✗</td></tr><tr><td>STT</td><td>✗</td><td>✗</td><td>✗</td></tr><tr><td>SPT</td><td>✓</td><td>✗</td><td>✓</td></tr><tr><td>NDA</td><td>✗</td><td>✗</td><td>✗</td></tr><tr><td>PROSPECT</td><td>✗</td><td>✗</td><td>✗</td></tr><tr><td>SESES</td><td>✗</td><td>✓</td><td>✗</td></tr><tr><td>SESES + lvi-cfi</td><td>✓</td><td>✓</td><td>✗</td></tr><tr><td>SESES + lvi-cfi + retpoline</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Our transformations (Section 8)</td><td>✓</td><td>✓</td><td>✓</td></tr></tbody></table>

respectively. These system calls can be exploited to probe kernel memory during transient execution and run *f*. They are defined as follows:

$$ 
\begin{align*}
\gamma(s) &= \text{if}_\ell x_1 \text{ then } \text{call } x_2() \text{ fi} \\
\gamma(t) &= z := *(a + x_1); *a := 1; y := \ell *a; \text{call } x_1() \\
\gamma(u) &= \text{call}_\ell x_1(),
\end{align*}
$$

with $\xi(s) = \xi(u) = \emptyset$ and $\xi(t) = \{a\}^2$.

In Figure 7, we describe the attacks A, B and C that take advantage of *s*, *t* and *u* respectively to break speculative kernel safety. The attack A is reminiscent of BlindSide [41]. In the main loop, the variable *y* ranges over all the kernel addresses. At each iteration, the attacks triggers the speculative execution of the conditional instruction within the victim system call to probe the address *y*, and it stops when it reads a side-channel leak *jmp* *p*, revealing the address of *f*. When the attack reads *jmp* *p* within the inner loop, it exits both the loops and the address of *f* will be equal to *y* − 1. In the inner loop, reading the value null (which indicates an empty observation stack) implies that *y* does not match the address of *f*, so the attack continues with the next iteration. The attack B is very similar to A, but it relies on STL forwarding instead of direct branch speculation to engage speculative execution and transiently execute *call* *x*₁(). Finally, the attack C takes control of branch target speculation to probe the kernel’s memory address space for *f*.

SLH [15] and Eclipse [19]. Speculative Load Hardening (SLH) is a software-level countermeasure that prevents speculative leaks of sensitive information. It keeps track of a predicate indicating whether the execution follows a wrong speculation or not. The value of this predicate is used to obfuscate values loaded during transient execution. SLH can also be used to obfuscate load addresses and the targets of indirect calls or jumps. Later works like Strong SLH [67] and UltimateSLH [88] can obfuscate even more operands, including store addresses and inputs of time-variable arithmetical operations, respectively. Eclipse [19] is a software-level protection measure that adopts the same approach to obfuscate the operands of those instructions that attacks like BlindSide [41] or PACMAN [71] exploit to perform speculative probes. Eclipse achieves lower overhead compared to SLH by protecting only a specific set of instructions—either indirect jumps or instructions for pointer validation, depending on the type of speculative probing the user aims to prevent. However, Eclipse and SLH are specific to PHT speculation—related to Spectre v1—and they fail to detect BTB

<footnote n="2">²In the system calls *s*, *t*, and *u*, the attacker has direct control over the jump target, violating the design principle of not accepting kernel addresses as input for system calls [13, p. 414]. Although our system calls violate such principle, we use them to model the scenario where an attacker controls a jump target addresses, which is a common kernel vulnerability (see, e.g., CVE-2017-1000112, CVE-2017-7294, and CVE-2018-5332).</footnote>
and STL speculation—related to Spectre v2 and v4, respectively. Therefore, although they would be effective against attacks relying on PHT speculation only, such as A, they would not stop B and C because they would not detect STL-dependency speculation or branch target speculation.

SCT. The *Constant-Time* (CT) discipline imposes that programs do not leak secret information via side-channels. *Speculative Constant Time* (SCT) extends (CT) by also taking into account speculative execution [10, 16]. Therefore, SCT programs are not subject to speculative attacks like Spectre [51]. However, SCT is not helpful for enforcing *speculative kernel safety*, as leaking secrets speculatively does not necessarily involve breaking *speculative kernel safety*. So, by imposing SCT, *speculative kernel safety* is not necessarily achieved. For instance, notice that none of the attacks in Figure 7 leaks secrets *stored in memory*, although they break *speculatively kernel safety*.

In Section 6.4 we proposed a policy based on SCT, to prevent (secret) information on the layout to leak during speculative execution: *side-channel layout non-interference*. It was also possible to show that *speculative kernel safety* can be obtained by imposing *side-channel layout non-interference*. However, such property would be too restrictive in practice, as any system call interacting with the memory would violate it.

STT [87]. *Speculative Taint Tracking* (STT) is a hardware protection mechanism to protect from speculative leakage by preventing the propagation of transiently loaded data. However, STT only retains data that is loaded during speculative execution. Therefore, it would neither block A, B or C from speculatively probing the victim's memory. Specifically, STT would not prevent the execution of the vulnerable call instruction, because the jump target is never loaded during transient execution.

SPT [18]. *Speculative Privacy Tracking* (SPT) is a hardware protection mechanism based on STT. Instead of preventing the propagation of *speculatively loaded data*, SPT prevents the propagation of *speculative secrets*, i.e., of data that without this measure would leak during speculative execution, but not during normal execution. To identify *speculative secrets*, the hardware keeps track of the data that is leaked in normal execution. When the hardware detects that some data leaks in normal execution, that data is also allowed to leak in speculative execution.

SPT would be effective against the attacks A and C because the addresses that are probed by the syscalls *s* and *t* do not leak in normal execution. However, it would not be effective against attacks the attack B because the probed address is leaked in normal execution inside *t* by the first load instruction before engaging speculative execution.

NDA [83]. *Non-speculative Data Access* (NDA) is a hardware protection measure similar to STT that restricts the propagation of data during speculative execution. NDA supports different policies to determine whether an instruction can broadcast its output, however NDA is not effective against attacks leaking addresses via a single transient operation [83]. Therefore, it cannot prevent the speculative leaks caused by a single instruction that tries to access a memory address, such as the call instructions in the attacks we are considering.

PROSPECT [28]. PROSPECT is a RISC-V processor prototype that adopts taint-tracking to prevent speculative leaks of secret data stored in a specific address range. In particular, an instruction cannot interact with the memory (performing side-channel leaks) if the register holding the target address depends on secret data. The authors of PROSPECT show that any CT program running on PROSPECT is SCT. Therefore PROSPECT does not enforce *speculative kernel safety* because, as we already mentioned, SCT programs are not necessarily *speculative kernel safe*.

SESES [69]. *LLVM's Speculative Execution Side Effect Suppression* (SESES) aims at preventing the speculative leakage of confidential data by placing *lfence* instructions before load or store
instructions and before branch instructions. This approach partially mitigates speculative memory
safety violations and speculative violations of constant-time execution. However, the SESES miti-
gation itself does not prevent violations of speculative kernel safety by speculative probing with
indirect branch instructions, as those of our examples, BHI [8] and BlindSide [41]. When used in
combination with LLVM's lvi-cfi pass, indirect jumps are replaced by a call to a thunk which
places an additional lfence before the jump. This combination would be effective in blocking
attacks A and B. However, even in combination with LLVM's lvi-cfi enforcement pass, SESES
would not prevent branch target speculation on the branch instruction itself, as in C, where the
attacker may still be able to influence the jump target speculation in the jump inside the thunk.
Therefore, to achieve speculative kernel safety, SESES needs to be combined with lvi-cfi, and
with some mechanism blocking BTB speculation, such as retpoline.

*Final Remarks.* Table 1 reports the effectiveness of the countermeasures discussed above against violations of *speculative kernel safety*. Most of them are designed to prevent the side-channel leakage of sensitive data during transient execution at the hardware level. However, a violation of *speculative kernel safety* does not necessarily leak sensitive data to the attacker. For instance, our attacks break *speculative kernel safety* but do not leak sensitive data, as f returns the constant 0, which is not a secret.

We believe that *speculative kernel safety* could be enforced at hardware level by delaying all
the operations that interact with kernel's memory until all the ongoing speculations are resolved
as correct. Notice that this is not what taint-tracking mechanisms such as STT, SPT, NDA, and
PROSPECT do. For instance, by tainting the content of kernel memory, PROSPECT would only block
accesses to locations whose address depends on kernel data, rather than blocking all speculative
accesses to kernel's memory. This consideration motivates us to develop an alternative software-
based technique specifically aimed at enforcing *speculative kernel safety*.

8 Enforcement of Speculative Kernel Safety

Our last research goal is to define software-level protection mechanism by which we can enforce
speculative kernel safety. Instead of defining a mechanism that enforces speculative kernel safety on
a system from scratch, our goal is rather to nullify the gap between kernel safety and speculative
kernel safety, by making the latter property a consequence of the former. This approach is similar
to the one adopted by the countermeasures of Section 7, that are ultimately aimed to prevent
undesirable events to take place under transient execution. With this guarantee, any software that
is secure in the classic execution model becomes safe in the speculative one as well.

In terms of our model, our goal boils down to finding a transformation $\zeta$ that turns any kernel safe system $\sigma$ into another system $\zeta(\sigma)$ which is secure during speculative execution and indistinguishable from the first one by users that do not control speculative execution and side-channel leaks. The latter requirement is expressed by the notion of semantic equivalence in Definition 6 below.

**Definition 5.** Two systems $\sigma = (\tau, \gamma, \xi)$ and $\sigma' = (\tau', \gamma', \xi')$ are *semantically equivalent* if $\mathrm{Eval}_{\sigma,w}(C, \rho, u, \tau) \approx \mathrm{Eval}_{\sigma',w}(C, \rho, u, \tau)$ for every unprivileged $C \in \mathrm{Cmd}$. Here, the equivalence is given by $(v, \tau_1) \approx (v, \tau_2)$ if $\tau_1 = \mathrm{Id}_u \cup \mathrm{Arrld}_k$ and coincides with equality otherwise.

In the previous definition we require $\tau = \mathrm{Id}_u \cup \mathrm{Arrld}_k$ instead of the identity between the stores in
order to allow reasoning about systems with different kernel-space procedures. In turn, to guarantee
*semantic equivalence*, it is sufficient to impose that the transformation does not change the behavior
of the single system calls, as expressed by the notion of *system call semantics preservation* below.
**Definition 6.** Let $\sigma = (\tau, \gamma, \xi)$ and $\zeta(\sigma) = (\tau', \gamma', \xi')$ be two systems. The transformation $\zeta$ is system call semantics preserving if we have $\tau = \text{Id}_u \cup \text{Arrld}_k$ $\tau'$ and for every layout $w$, registers $\rho$, $s$, and stores $v$, $v'$:

$$v = \text{Procld}_k \quad \tau \wedge v' = \text{Procld}_k \quad \tau' \wedge v = \text{Arrld}_k \quad v'$$

implies

$$\text{Eval}_{\sigma,w}(\gamma(s), \rho, k_s, v) \approx \text{Eval}_{\zeta(\sigma),w}(\gamma'(s), \rho, k_s, v').$$

Reducing speculative kernel safety to kernel safety means reducing safety violations in speculative execution to safety violations in normal execution. Therefore, the second requirement on $\zeta$ can be expressed by asking that the system $\zeta(\sigma)$ violates speculative kernel safety only if it violates kernel safety, as captured by Definition 7.

**Definition 7.** We say that $\zeta$ imposes speculative kernel safety if, for every system $\sigma$ such that $\zeta(\sigma) = (\tau, \gamma, \xi)$, every buffer $\mu$ with $\text{dom}(\mu) \subseteq \underline{w}(\text{Arrld})$ and store $\tau' = \text{Procld} \tau$ we have:

$$\left( w \vdash_{\zeta(\sigma)} ((\gamma(s), \rho, k_s), (\mu, (w \diamond \tau')), b_{ms}) \xrightarrow[D \to]{}^* \text{unsafe} \right)$$

implies

$$\left( w \vdash_{\zeta(\sigma)} ((\gamma(s), \rho, k_s), (\overline{\mu}, (w \diamond \tau')) \to^* \text{unsafe} \right).$$

We now state the main result of this section, that establishes the effectiveness of our mitigation strategy.

**THEOREM 3.** If a system $\sigma$ is kernel-safe, and the transformation $\zeta$ (i) imposes speculative kernel safety and (ii) is system call semantics preserving, then (a) $\zeta(\sigma)$ is speculative kernel safe, and (b) $\zeta(\sigma)$ is semantically equivalent to $\sigma$.

**PROOF SKETCH.** Claim (a) follows by contraposition: assume that the system $\zeta(\sigma)$ is unsafe, so there are a system call, and a sequence of transition that lead to unsafe with the speculative semantics. By combining Definition 7 and (ii), we deduce that the system $\sigma$ is unsafe under the non-speculative semantics, contradicting $\sigma$'s safety. Claim (b) follows by induction on the length of the reduction, and by applying (ii) when a system call is encountered. $\square$

Notice that kernel safety cannot be provided solely by the adoption of layout randomization: by Theorem 1, we know that layout randomization only provides kernel safety modulo a small probability of failure.

With Theorem 3 in mind, our next goal is to show some candidate transformations that fulfill its requirements and which enforce speculative kernel safety on classically safe kernels. To model these transformations, we extend our language with program instructions acting as speculation barriers—modeling the fence instruction found in modern x86 CPUs [49]—and with call instructions that do not support BTB speculation—similar to retpoline chunks [80].

The resulting language looks as follows:

$$\text{Instr} \ni I ::= \dots | \text{fence} | \text{scall} E(E_1, \dots, E_n).$$

The semantics of these additional instructions is in Figure 8. Architecturally, the fence instruction is a no-op, on the micro-architecture level it commits all buffered writes to memory. In particular, for consistency, a potentially mis-speculative state must be resolved. This is why this rule requires the mis-speculation flag to be $\perp$. This means that, if this configuration is reached when the flag is $\perp$, the semantics must backtrack with Rule [BT$_\perp$].
$$ \phi = (\langle \text{scall } E(\vec{F}); C, \rho, b \rangle : F, (\mu, m), b_{ms}) \quad [\llbracket E \rrbracket]^{\text{Addr}}_{\rho, w} = p \quad p \in \underline{w}(\text{Procld}_b) \quad [b = k_s \Rightarrow p \in \underline{w}(\xi(s))] \quad [\text{SSCALL}] $$

$$ w \vdash_{\sigma} (\phi : F, (\mu, m), b_{ms}) : S \xrightarrow{\text{jmp } p} (\langle m(p), \rho_0[\vec{x} \leftarrow [\llbracket \vec{F} \rrbracket_{\rho,w}], b \rangle : \langle C, \rho, b \rangle : F, (\mu, m), b_{ms} \rangle : S) $$

$$ [\llbracket E \rrbracket]^{\text{Addr}}_{\rho,w} = p \quad p \in \underline{w}(\text{Procld}_k) \quad [p \notin \underline{w}(\xi(s))] \quad [\text{SSCALL-UNSAFE}] $$

$$ w \vdash_{\sigma} (\langle \text{scall } E(\vec{F}); C, \rho, k_s \rangle : F, \psi, b_{ms}) : S \xrightarrow{\text{jmp } p} \text{unsafe} $$

$$ [\llbracket E \rrbracket]^{\text{Addr}}_{\rho,w} \notin \underline{w}(\text{Procld}_b) \quad [\text{SSCALL-ERROR}] $$

$$ w \vdash_{\sigma} (\langle \text{scall } E(\vec{F}); C, \rho, b \rangle : F, \psi, b_{ms}) : S \xrightarrow{\bullet} (\text{err}, b_{ms}) : S $$

$$ w \vdash_{\sigma} (\langle \text{fence}; C, \rho, b \rangle : F, \psi, \perp) : S \xrightarrow{\bullet} (\langle C, \rho, b \rangle : F, \bar{\psi}, \perp) : S \quad [\text{FENCE}] $$

<caption>Fig. 8. Speculative semantics, additional constructs.</caption>

$$
\begin{array}{l@{\qquad}l}
\eta(x := E) & \eta(\text{skip}) \\
\eta(*E := F) & \eta(x := *E) \\
\eta(\text{call } E(\vec{F})) & \eta(x := *E) \\
\eta(\text{fence}; *E := F) & \eta(\text{fence}; x := *E) \\
\eta(\text{scall } E(\vec{F})) & \eta(\text{while } E \text{ do } C \text{ od}) \\
\eta(\text{syscall } s(\vec{E})) & \eta(\text{if } E \text{ then } C \text{ else } D \text{ fi}) \\
\eta(I; C) & \eta(\text{if } E \text{ then } C \text{ else } D \text{ fi}) \\
\eta(I; C) & \eta(\text{if } E \text{ then } C \text{ else } D \text{ fi}) \\
\eta(\tau) & \eta(\epsilon) \\
\eta(\gamma) & \eta(\tau) \\
\eta(\gamma) \mapsto \eta(\gamma(s)) & \eta(\tau) \mapsto \text{id} \\
\eta(\tau) \mapsto \text{id} & \begin{cases} \tau(\text{id}) & \text{if } \text{id} \in \text{Arr} \cup \text{Procld}_u \\ \eta(\tau(\text{id})) & \text{otherwise} \end{cases} \\
\eta(\gamma) & \eta(\tau) \\
\eta(\gamma) \mapsto \eta(\gamma(s)) & \eta(\tau) \mapsto \text{id} \\
\eta(\tau) \mapsto \text{id} & \begin{cases} \tau(\text{id}) & \text{if } \text{id} \in \text{Arr} \cup \text{Procld}_u \\ \eta(\tau(\text{id})) & \text{otherwise} \end{cases} \\
\eta(\gamma) & \eta(\tau) \\
\eta(\gamma) \mapsto \eta(\gamma(s)) & \eta(\tau) \mapsto \text{id} \\
\eta(\tau) \mapsto \text{id} & \begin{cases} \tau(\text{id}) & \text{if } \text{id} \in \text{Arr} \cup \text{Procld}_u \\ \eta(\tau(\text{id})) & \text{otherwise} \end{cases}
\end{array}
$$

<caption>Fig. 9. Simple fencing transformation</caption>

The semantics of the scall E(\vec{F}) instruction is similar to the one of ordinary call instructions, with the difference that run<sub>l</sub> p directives are not accepted. Instead, the address of the target procedure is always obtained by evaluating E. In normal execution, the non-speculative call instruction is interpreted in the same way as the ordinary call instruction.

To facilitate proving the system call semantics preservation condition, we make the following remark:

**REMARK 1.** If a transformation $\zeta$ only inserts fence instructions (at any positions) in the kernel code and replaces call instruction with safe calls, then $\zeta$ is system call semantic preserving.

*Simple Fencing Transformation.* As a warm-up example we now consider the simple transformation $\eta$ shown in Figure 9, and prove that it satisfies the requirements of Theorem 3. Similarly to SESES [69], this transformation places a fence instruction before all the potentially unsafe operations, including call instructions, as they can perform transitions to unsafe. In addition to what SESES does, it prevents BTB speculation by rewriting ordinary call instructions with non-speculating call instructions. With $\eta$, any ongoing speculation is stopped before executing potentially unsafe operations (including non-speculative call instructions), and their transient execution is prevented, yet leaving the program's semantics unaltered at the architectural level.

Finally, note that the transformation $\eta$ does not stop speculation completely, instead it only prevents the transient execution of those instructions that can perform unsafe operations. For instance, conditional instructions can still execute speculatively if their branches contain no
$$
\begin{align*}
\pi_e^m(x := E) &\triangleq (x := E, m, e) \\
\pi_e^m(\text{skip}) &\triangleq (\text{skip}, m, e) \\
\pi_e^m(*E := F) &\triangleq \begin{cases} (*E := F, \perp, \perp) & \text{if } m = \perp \\ (\text{fence}; *E := F, \perp, \perp) & \text{otherwise} \end{cases} \\
\pi_e^m(x := *E) &\triangleq \begin{cases} (x := *E, \neg e, e) & \text{if } m = \perp \\ (\text{fence}; x := *E, \perp, \top) & \text{otherwise} \end{cases} \\
\pi_e^m(\text{while } E \text{ do } C \text{ od}) &\triangleq (\text{while } E \text{ do } \pi_\perp^\top(C) \text{ od}, \top, \perp) \\
\pi_e^m(\text{if } E \text{ then } C \text{ else } D \text{ fi}) &\triangleq (\text{if } E \text{ then } \pi_\perp^\top(C) \text{ else } \pi_\top^\top(D) \text{ fi}, \top, \perp) \\
\pi_e^m(\text{call } E(\vec{F})) &\triangleq (\text{fence}; \text{scall } E(\vec{F}), \top, \perp) \\
\pi_e^m(\text{syscall } s(\vec{E})) &\triangleq (\text{syscall } s(\vec{E}), \top, \perp) \\
\pi_e^m(\varepsilon) &\triangleq (\varepsilon, m, e) \\
\pi_e^m(I; C) &\triangleq (I'; C', m'', e'') \text{ where } (I', m', e') = \pi_e^m(I), \\
&\text{and } (C', m'', e'') = \pi_{e'}^{m'}(C).
\end{align*}
$$

$$
\pi(\gamma) \triangleq s \mapsto \pi_{\perp}^{\top}(\gamma(s)) \quad \pi(\tau) \triangleq \text{id} \mapsto \begin{cases} \tau(\text{id}) & \text{if } \text{id} \in \text{Arr} \cup \text{Procl}_{\text{d}} \\ \pi_{\perp}^{\top}(\tau(\text{id})) & \text{otherwise} \end{cases} \quad \pi((\tau, \gamma, \xi)) \triangleq (\pi(\tau), \pi(\gamma), \xi).
$$

<caption>Fig. 10. Optimized fencing transformation. When there is no risk of ambiguity, we use the notation $\pi(\tau(\text{id}))$ to represent the resulting command alone, rather than the full triple.</caption>

potentially unsafe operations. Nevertheless, $\eta$ imposes speculative kernel safety because, even in transient execution, a conditional instruction cannot perform any safety violation by itself. However, as their branches can contain unsafe operations, the transformation visits them to protect any unsafe operation therein. By observing that $\eta$ enjoys both the properties in Definitions 6 and 7, we can draw the following conclusion:

**LEMMA 4.** If a system $\sigma$ is kernel-safe, then $\eta(\sigma)$ is speculative kernel safe and semantically equivalent to $\sigma$.

**PROOF SKETCH.** Fix $\eta(\sigma) = (\tau, \gamma, \xi)$. By induction on $n$, we show that when a system call reaches unsafe with the speculative semantics, i.e., when $w \vdash_{\eta(\sigma)} ((\gamma(s), \rho, k_s), (\mu, (w \diamond \tau'))$, $b_{ms}) \xrightarrow{O/D}^n (F, (\mu', m), b'_{ms}) : S \xrightarrow{o/d} \text{unsafe, } b'_{ms}$ is $\perp$. Moreover, we can assume without loss of generality that $D$ does not contain bt directives. By induction on the sequence of steps, and by inspecting the transition rules not involving bt, we observe that at each step the mis-speculation flag is $\perp$. Therefore, we deduce that the reduction can be mimicked by the non-speculative semantics, i.e., $w \vdash_{\eta(\sigma)} ((\gamma(s), \rho, k_s), (\overline{\mu}, (w \diamond \tau'))) \rightarrow^n (F, (\overline{\mu'}, m')) \rightarrow \text{unsafe. This proves that } \eta \text{ imposes speculative kernel safety. System call semantics preservation follows from Remark 1.} \quad \square$

*Optimized fencing transformation.* The transformation $\eta$ of Figure 9 can be enhanced by means of a simple static analysis to determine whether the current instruction can be reached in transient execution or not. The resulting transformation $\pi$ is described in Figure 10. Specifically, while analyzing the AST of a program, $\pi$ keeps track of two additional flags: $m$ and $e$. The flag $m$ is $\top$ if the instruction may be reached after a mis-speculation, and the flag $e$ is $\perp$ if the instruction can only be reached when the write-buffer is empty. Therefore, when the transformation encounters
an instruction that may lead to the unsafe state, but the flag *m* is ⊥, the *fence* instruction can be avoided.

For instance, consider the following snippet of code:

C ≜ x := *E; y := *F; *z := G. with π⊥(C) = (fence; x := *E; y := *F; *z := G, ⊥, ⊥).

When $\pi$ starts its execution, the initial value of $m$ is $\top$ and that of $e$ is $\bot$, meaning that the system may be mis-speculating and the write buffer is not necessarily empty. Therefore, $\pi$ protects the first load instruction in C with a fence instruction and sets $m$ to $\bot$ and $e$ to $\top$. When it instruments the instruction $y := *F$, no fence instruction is placed because $m = \bot$. The value of $m$ is then set to $\neg e = \bot$ since, due to the empty buffer, no mis-speculation can occur (see Figure 10, case of load operations with $m = \bot$ and $e = \top$). Notice that, after analyzing the last store instruction, the transformation sets the flag $e$ to $\bot$, signaling that the write buffer may be not empty anymore, and that subsequent unprotected load instruction may be mis-speculating (see Figure 10, case of load operations with $m = \bot$). Besides the load and store instruction we just analyzed, the transformation sets the flag $m$ to $\top$ when it explores the branches of if or while constructs to capture PHT speculation. Finally, the flag $m$ is set to $\top$ and $e$ to $\bot$ when returning from an indirect call, due to the lack of information on the called function.

Our optimizations do not impact the security of the transformation $\pi$, as expressed by the following lemma:

**LEMMA 5.** If a system $\sigma$ is kernel-safe, then $\pi(\sigma)$ is speculative kernel safe and $\pi(\sigma)$ semantically equivalent to $\sigma$.

**PROOF SKETCH.** The proof follows a similar structure to that of Lemma 4. However, to establish that whenever an unsafe state is reached, the mis-speculation flag in the predecessor state is $\bot$, we rely on a form of subject reduction and of soundness of our static analysis. Specifically, whenever the execution reaches a command C, either C is instrumented, namely: $C = \pi_e^m(C'); \pi_\bot^\top(D_1); \dots; \pi_\bot^\top(D_k)$, for some $C', D_1, \dots, D_k, m$, and $e$, or C reaches an instrumented command in one step. In both cases, if $m$ is $\bot$, the mis-speculation flag is also $\bot$ and if $e$ is $\top$, the write buffer is empty.

This property can be established by induction on $n$, with the help of other technical invariant properties. $\square$

*Speculation-blocking transformation.* Notice that the transformations proposed in Figures 9 and 10 prevent the speculative execution of unsafe commands *lazily*, as they do not completely stop speculative execution, but they just prevent the transient execution of some instructions that may be unsafe. For instance, if in the conditional instruction if E then C else D fi neither C nor D contain potentially unsafe operations—e.g., if they only contain register assignments—$\eta$ and $\pi$ leave those commands unchanged and the CPU can still speculate over the value of E.

Following Intel®'s guidelines for speculative attacks' mitigation [22], another approach is to systematically prevent any form of speculation by placing speculation barriers after speculation sources and using safe jump instructions. In our model, this solution approach down to:

* placing a fence instruction after every direct branch to stop PHT speculation,

* replacing every ordinary call instruction with a non-speculative one to stop BTB speculation, and

* placing a fence instruction after every store operation to stop STL speculation.

The transformation we outlined above is formally defined in Figure 11. It is quite easy to observe that $\theta$ preserves the semantics of the system it is applied to and that no potentially unsafe instruction can be reached during transient execution. As a consequence, we conclude that $\theta$ enforces *speculative kernel safety* on *kernel safe* systems:
<figure><img src="image_6.png" /><figcaption>Fig. 11. Speculation-blocking transformation.</figcaption></figure>

**LEMMA 6.** If a system $\sigma$ is kernel-safe, then $\theta(\sigma)$ is speculative kernel safe and $\theta(\sigma)$ semantically equivalent to $\sigma$.

**PROOF SKETCH.** The proof of this result is analogous to that of Lemma 4. □

<figure><img src="image_7.png" /></figure>

*Covering additional speculation mechanisms.* In this work, we focused on speculation related to Spectre v1, v2, and v4 in order to keep our model abstract enough to allow for formal reasoning, while covering the most significant speculation mechanisms. However, our model and results can be extended to cover additional forms of speculation, such as Load Value Injection (LVI) and return value speculation. For instance, LVI can be modeled by allowing attackers to control the loaded value with specific directives. Return value speculation can be addressed by introducing explicit returns and directives controlling predicted return addresses. The notions of semantic preservation and speculative safety imposition naturally extend to additional speculation mechanisms, ensuring the validity of Theorem 3 in the enriched model. However, the notion of safety imposition would become more stringent. Therefore, our transformations would need to be modified to take into account the additional sources of speculation. For instance, the $\pi$ transformation could be modified to address LVI and return speculation by replacing return instructions with specific non-speculative return instructions, similar to our *scall* instruction, and by treating loaded values as potential sources of speculation, i.e., by setting $m = \top$ after each load.

# 9 Experimental Evaluation

In this section, we evaluate the performance overhead of the program transformations presented in the previous section. Specifically, our goal is to measure the impact of our transformations to *kernel-space* execution, *user-space* execution, and *user-space I/O-bound* workloads.

## 9.1 Overview of the Implementation

We implemented the transformations of Figures 9 to 11 as parts of the LLVM/Clang compiler infrastructure [54] version 18. More precisely, we introduced a *MachineFunctionPass* called *X86SpeculativeSafetyPass*, implementing our transformations, which can be activated by specific command-line flags. When a transformation is activated, our pass iterates over every block and every instruction within the block, protecting each instruction as required by the corresponding
definition in Figures 9 to 11. We were able to generalize the transformations from our language to the more expressive x86 ISA by relying on the LLVM API, which allows us to determine if a certain instruction may load, store, or jump. Instructions showing these behaviors are protected in the same way the selected transformation protects instructions $x := *E, *E := F$, and call $E(\vec{F})$ respectively. As we mentioned in Section 8, the semantics of fence reproduces that of the x86 instruction lfence, therefore our pass uses lfence to implement the fence instruction. Finally, our LLVM pass supports two ways of implementing the non-speculative call instruction scall $E(\vec{F})$:

* One way is to exchange indirect jump and call instructions with retpoline thunks, aimed at preventing branch target speculation. Specifically, we replace indirect jumps and calls with Linux's retpoline thunks at boot time by passing the specific boot command-line parameter spectre_v2=retpoline.

* A faster alternative is to rely on Intel® eIBRS [21], leaving branch instructions unchanged. This measure prevents the target of any indirect branch that is executed in kernel-space to be predicted depending on user-space execution.

We chose to benchmark both the mechanisms as in our attack model, where RSB speculation is not taken into account, retpoline offers stronger security guarantees than eIBRS: contrarily to eIBRS retpoline is not subject to confused-deputy-attacks [8, 21], although it has larger performance overheads in practice [11].

Like similar passes such as SLH and SESES, the X86SpeculativeSafetyPass runs just before register allocation to ensure that subsequent passes do not alter the program's control flow, which could compromise its protections. The implementation of our LLVM pass, along with additional details on its behavior, is available in [29].

## 9.2 Experimental Evaluation

*Performance evaluation goals.* Our experimental evaluation aims to determine the performance overhead induced by the transformations of Figures 9 to 11 on kernel-space execution, user-space programs that combine kernel- and user-space execution, and on user-space programs that perform intensive I/O workloads.

*Benchmark choice.* We chose to evaluate the overhead on heavy kernel-space tasks with the UnixBench Benchmark, which is meant to evaluate the performance of tasks with high pressure on system calls like exec, getpid, fork, or by executing patterns like file copy and inter-process communication. To benchmark real-world computationally heavy user-space applications, we used the SPEC® benchmark suite, which includes tasks like compilation, interpretation, compression, simulation, and other tasks that engage kernel-space execution only sporadically. To measure the overhead on I/O-bound workloads, we used the following benchmarks:

* The ab [36] benchmark, for measuring the latency of widely used web servers. Specifically, we measured the latency of 1000 HTTP GET requests for a 1GB file.

* The crossdb [26] benchmark, to measure the response speed of the sqlite and crossdb DBMSs to 200.000 and 2.000.000 queries, respectively.

* The cryptsetup [27] benchmark, for measuring the throughput of kernel side cryptographic applications. Specifically, we measured the encryption and decryption throughput of AES-EBC.

* The uprop [48] benchmark, for assessing the speed of GNU's grep tool on different patterns across multiple files and directories.

* The vbench [60] benchmark to measure the transcoding speed of ffmpeg on large videos.
*Performance evaluation methodology.* All the benchmarks were executed on a machine running the Debian 12 distribution using the following Linux 6.10 kernels:

1. **Off-the-shelf kernel.** This kernel was compiled from the Linux source using Clang with Debian 12's default settings.

2. **Baseline transformed kernel.** This kernel is protected with the η transformation (Figure 9), placing 1fence instructions before instructions that interact with the memory and blocking BTB speculation via retpoline or eBRS.

3. **Optimized transformed kernel.** This kernel is protected with the implementation of the π transformation (Figure 10), selectively placing 1fence instructions before instructions that interact with the memory, and blocking BTB speculation via retpoline or eBRS.

4. **Intel® Guidelines' kernel.** This kernel is protected with the implementation of the θ transformation (Figure 11), which applies Intel® guidelines to block *kernel-space* PHT, BTB and STL speculation.

All kernels were compiled with the default settings against speculative attacks. In particular, these settings include support for eBRS [21], retpoline [80], and BHI_DIS_S [24], which is an Intel® mitigation for Branch History Injection [8]. The settings also include measures against *Return Stack Buffer* (RSB) speculation [85]—out of scope for this work—including support for call depth tracking [39] and untrained return thunks—implementing AMD's JMP2RET [5]. All the experiments were run on a machine equipped with an Intel® Core i5-1345U processor with 12 logical cores and 16GB of DDR4 memory. Notably, on such processor, retpoline prevents indirect jump target speculation [23, 25].

*Data collection and results.* The results of our experimental evaluation are summarized in Figure 12. Most of our benchmarks reported execution time measurements. For these benchmarks, the height of the bar represents the average execution times recorded for each of the kernels, divided by the average time required by the off-the-shelf kernel (1). The black line displays the standard deviation of our sample. As UnixBench and cryptsetup measure how many times a specific task can be completed in a fixed amount of time, they provide a throughput measurement and no indicator of the standard deviation. By inverting the throughput measurement, we obtained an indicator of the average execution time of each task. We estimated the overhead by dividing the average indicator by the estimation of the same indicator for the off-the-shelf kernel (1).

*Final remarks.* Our π transformation outperforms others transformations and incurs in negligible overhead in the SPEC® benchmark and some I/O-bound workloads, where its overhead is usually below 1% and never exceeds 5%. In UnixBench, and the I/O-bound workloads which put more pressure on store and load operations, it incurs a 3x-10x overhead compared to the non-transformed kernel. While this overhead is significant, future hardware advancements could help mitigate this cost, making such protections more practical for a wider range of systems.

## 10 Related Work

*On Layout Randomization.* The first work that provided a formal account of layout randomization was by Abadi and Plotkin [4], later extended in [2, 3]. In these works, the authors show that layout randomization prevents, with high probability, malicious programs from accessing the memory of a victim in an execution context with shared address space. We have already discussed this in the body of the paper how these results do not model speculative execution or side-channel observations.

*Spatial Memory Safety and Non-Interference.* Spatial memory safety is typically defined by associating a software component with a memory area and requiring that, at runtime, the component only
<figure><img src="image_8.png" /><figcaption>(a) Overhead on the SPEC® CPU 2017 Benchmark with eBRS.</figcaption></figure>

<figure><img src="image_9.png" /><figcaption>(c) Overhead on the UnixBench Benchmark with eBRS.</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>(e) Overhead on the I/O benchmarks with eBRS.</figcaption></figure>

<figure><img src="image_11.png" /><figcaption>(b) Overhead on the SPEC® CPU 2017 Benchmark with retpoline.</figcaption></figure>

<figure><img src="image_12.png" /><figcaption>(d) Overhead on the UnixBench Benchmark with retpoline.</figcaption></figure>

<figure><img src="image_13.png" /><figcaption>(f) Overhead on the I/O benchmarks with retpoline.</figcaption></figure>

Fig. 12. Overheads of the different transformations of the kernel. In the figures, the scale of the y-axis is linear. To better highlight variations in overhead, the y-axis origin is set to 0.975 in Figures 12a and 12b.

accesses that area [10, 64, 66]. Azevedo de Amorim et al. [7] demonstrated that memory safety can be expressed in terms of non-interference; this property, in turn, stipulates that the final output of
a computation is not influenced by secret data that a program must keep confidential [40]. Both of
these properties have been extended to the speculative model. The definition of *speculative memory
safety* from [10] closely aligns with our notion of *speculative kernel safety*, with the difference that
the latter also imposes some restriction on the victim's control flow. *Speculative non-interference*
was initially introduced in the context of the *SPECTOR* symbolic analyzer [44]. *SPECTOR's*
property disallows information flows to side-channels that occur with transient execution but not
in sequential execution. In contrast to *SPECTOR's* approach, our notion of *speculative kernel
safety* aligns with *speculative constant-time* [16], as it prevents information leaks that occur during
normal and transient execution.

*Formal Analysis of Security Properties of Privileged Execution Environments.* Barthe et al. [9] deploy a model with side-channel leaks and privileged execution mode, without speculative execution. In particular, they are interested in studying the preservation of constant-time in virtualization platforms. They also model privilege-raising procedures *hypercalls*, similar to our system calls. They show that if one of the hosts is constant-time then the system enjoys a form of non-interference with respect to that host's secret memory. For this reason, although the two models are similar, the purposes of Barthe et al. [9] and our work are different: in [9] the victim and the attacker have the same levels of privilege and the role of the hypervisor is to ensure their separation whilst, in our work, the privileged code base is itself the victim. In addition, Barthe et al. [9] study constant-time, while we focus on memory safety and control flow integrity.

*Attacks to Kernel Layout Randomization.* Attacks that aim at leaking information about the kernel's layout are very popular and can rely on implementation bugs that reveal information the kernel's layout [17, 52, 59] or on side-channel info-leaks [14, 43, 53, 58]. In particular attacks such as EchoLoad, TagBleed and EntryBleed [14, 53, 58] are successful even in presence of state-of-art mitigations such as Intel®'s Page Table Isolation (PTI) [50]. However, due to address-space separation between kernel and user space programs, an attacker cannot access the victim's memory by simply dereferencing a kernel address. So, in general, if the attacker does not control the value of a pointer that is used by the kernel, this kind of leak is not harmful.

The Meltdown attack [57] uses speculative execution to overcome address-space separation on operating systems running on Intel® processors that do not adopt KAISER [42] or PTI [50]. In particular, the hardware can speculatively access an address before checking its permissions. The attack uses this small time window to access kernel memory and leak its content by using a side-channel info-leak gadget. Due to the adoption of PTI [50], this kind of attack is mitigated by removing most of the kernel-space addresses from the page tables of user-space programs. The BlindSide attack [41] overcomes this issue by probing directly from kernel-space. Similar attacks can be mounted by triggering different forms of mispredictions [61].

Branch target buffer (BTB) speculation—related to Spectre v2—can be used by attackers to defeat kernel's layout randomization. Evtyushkin et al. [34] were able to show that BTB mis-speculations reveal information on victim's layout. Barberis et al. [8] showed how, in the presence of BTB speculation, an attacker can steer the control flow of kernel's indirect branches close to the context switch, even in the presence of KASLR and eIBRS. As shown by Wiebing et al. [84], currently the Linux kernel contains hundreds of such exploitable indirect jumps. The form of speculation exploited by this attacks is taken into account in our model by allowing arbitrary speculation on unsafe jumps. Akin to BTB speculation, Return Stack Buffer (RSB) speculation can be used to transiently divert the victim's control flow to arbitrary locations when it executes a return instruction. Wikner and Razavi [85] used this vulnerability to break Layout Randomization and to leak kernel's memory. We did not consider RSB speculation in our model. Therefore, systems that are protected with our mitigations may still be vulnerable to attacks relying on RSB speculation.
However, attacks such as Retbleed [85] and BHI [8] do not compromise our reliance on eIBRS and retpoline since such measures are claimed to be effective on modern Intel® processors, including the one used for our benchmarks [23, 25].

*Comparison with Eclipse* [19]. Eclipse [19] is a software-level protection measure designed to prevent speculative memory abuse (SMA) attacks, such as BlindSide [41] and PACMAN [71]. Eclipse blocks speculative memory abuses by inserting artificial data dependencies between the operands of instructions that can perform memory abuses and the guards of direct branches, in a similar manner as SLH. The performance evaluation of Eclipse shows outstanding results on kernel-space execution with maximum overheads smaller than 8%, i.e., more than 100 times smaller than our best performing transformation $\pi$. These results are not surprising, and are due to the specificity of Eclipse to attacks based on PHT speculation [15]. In contrast, our work also protects against BTB and STL speculation, and thereby our transformations block speculative execution with costly 1fence instructions instead of data dependencies. Finally, Eclipse offers weaker guarantees than our transformations by protecting only a narrow class of instructions, i.e., indirect branch instructions subject to PHT speculation. In contrast, our transformations protect a wider class of instructions, including all indirect branches, loads and stores subject to PHT, BTB, and STL speculation. Therefore, our transformations insert more protections, increasing the performance overhead.

*Comparison with Oreo* [76]. Recently, Song et al. [76], developed a hardware/software co-design, named Oreo, aimed at preventing microarchitectural side-channel leaks of the randomized bits of virtual addresses caused by memory accesses. To this aim, Oreo introduces a new address space—the masked address space—that is used for the translation of virtual addresses to physical addresses. Specifically, a virtual address is mapped to a corresponding masked address by masking some of its bits; the masked address is then translated to a physical address via a standard page-table lookup. This approach prevents the side-channel leakage of virtual addresses associated with memory accesses, because all the microarchitectural structures that used to take virtual addresses as input switch to using masked addresses. Although this design effectively prohibits side-channel leaks due to memory operations, it does not other leaks of randomized addresses, such as address-dependent branching conditions. In addition, Oreo does not block violations of speculative kernel safety in general. For instance, an attacker can now perform speculative probing of a kernel-space spectre-like gadget—like in those in Section 7—without the need to know the randomized bits. More precisely, it would be sufficient to probe any addresses only differing in the masked bits to obtain the same microarchitectural side effects of accessing the virtual address where the gadget is located at.

## 11 Conclusion and Future Work

We have formally demonstrated that the kernel's layout randomization probabilistically ensures kernel safety for a classic model, where an attacker cannot compromise the system via speculative execution or side-channels. In this model, users of an operating system execute without privileges, but victims can feature pointer arithmetic, introspection, and indirect jumps. We have also shown that the protection offered by layout randomization does not naturally scale against attackers that can control side-channels and speculative execution related to Spectre v1, v2 and v4. We stipulate a sufficient condition to enforce kernel safety in the Spectre era and we proposed mechanisms based on program transformations that provably enforce speculative kernel safety on a system, provided that this system already enjoys kernel safety in the classic model. We proved the soundness of three such transformation, we implemented them as part of the LLVM/Clang compiler suite, and we established their performance overhead. To the best of our knowledge, our work is the first to
formally investigate and provide methods to achieve kernel safety in the presence of speculative and side-channel vulnerabilities, while also evaluating the performance of the proposed mitigations.

*Future work.* This work prepares the ground for future developments such as the evaluation of other probabilistic techniques for the enforcement of safety properties such as Arm's PA [56], and hardware backed capability machines like CHERI [82]. We also consider the possibility to enhance our model with other speculative vulnerabilities including LVI, RSB or Phantom speculation, to develop software-level protection measures enforcing speculative kernel safety in this stronger attacker model.

## Acknowledgments

We are grateful to Gilles Barthe, Márton Bognár, Ugo Dal Lago, Lesly-Ann Daniel, Benjamin Grégoire, Jean-Pierre Lozi, Frank Piessens, Aurore Poirier, and Manuel Serrano for their comments on an early draft of the paper. This work was partially supported by the projects PPS ANR-19-C48-0014 and UCA DS4H ANR-17-EURE-0004, and by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.

## References

[1] Martín Abadi, Mihai Budiu, Úlfar Erlingsson, and Jay Ligatti. 2005. Control-Flow Integrity. In *Proceedings of the 12th ACM Conference on Computer and Communications Security*. ACM, New York, NY, USA, 340–353.

[2] Martín Abadi and Jérémy Planul. 2013. On Layout Randomization for Arrays and Functions. In *Principles of Security and Trust*. Springer, Berlin, Heidelberg, 167–185.

[3] Martín Abadi, Jérémy Planul, and Gordon D. Plotkin. 2014. *Layout Randomization and Nondeterminism*. Springer International Publishing, Berlin, Heidelberg, 1–39.

[4] Martín Abadi and Gordon D. Plotkin. 2012. On Protection by Layout Randomization. *ACM Trans. Inf. Syst. Secur.* 15, 2 (jul 2012), 29 pages.

[5] AMD. 2022. *Technical Guidance for Mitigating Branch Type Confusion*. Technical Report. AMD. https://www.amd.com/content/dam/amd/en/documents/resources/technical-guidance-for-mitigating-branch-type-confusion.pdf White Paper.

[6] Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya. 2022. Enforcing Fine-grained Constant-time Policies. In *Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security*. ACM, New York, NY, USA, 83–96.

[7] Arthur Azevedo de Amorim, Cătălin Hrițcu, and Benjamin C Pierce. 2018. The meaning of memory safety. In *Proceedings of Principles of Security and Trust: 7th International Conference*. Springer Berlin, Heidelberg, Springer, 79–105.

[8] Enrico Barberis, Pietro Frigo, Marius Muench, Herbert Bos, and Cristiano Giuffrida. 2022. Branch History Injection: On the Effectiveness of Hardware Mitigations Against Cross-Privilege Spectre-v2 Attacks. In *31st USENIX Security Symposium (USENIX Security'22)*. USENIX Association, Boston, MA, 971–988.

[9] Gilles Barthe, Gustavo Betarte, Juan Campo, Carlos Luna, and David Pichardie. 2014. System-Level Non-Interference for Constant-Time Cryptography. In *Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security*. ACM, New York, NY, USA, 1267–1279.

[10] Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, and Peter Schwabe. 2021. High-Assurance Cryptography in the Spectre Era. In *2021 IEEE Symposium on Security and Privacy (SP)*. IEEE, New York, NY, USA, 1884–1901.

[11] Jonathan Behrens, Adam Belay, and M. Frans Kaashoek. 2022. Performance evolution of mitigating transient execution attacks. In *Proceedings of the Seventeenth European Conference on Computer Systems*. ACM, New York, NY, USA, 251–265.

[12] Emery D. Berger and Benjamin G. Zorn. 2006. DieHard: Probabilistic Memory Safety for Unsafe Languages. In *Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation*. ACM, New York, NY, USA, 158–168.

[13] Daniel P Bovet and Marco Cesati. 2005. *Understanding the Linux Kernel: from I/O ports to process management*. "O'Reilly Media, Inc.", "Sebastopol, CA, USA".

[14] Claudio Canella, Michael Schwarz, Martin Haubenwallner, Martin Schwarzl, and Daniel Gruss. 2020. KASLR: Break It, Fix It, Repeat. In *Proceedings of the 15th ACM Asia Conference on Computer and Communications Security*. ACM, New York, NY, USA, 481–493.
[15] Chandler Carruth. 2018. Speculative Load Hardening. https://llvm.org/docs/SpeculativeLoadHardening.html

[16] Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthal, Dean Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe. 2020. Constant-time foundations for the new spectre era. In *Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation*. ACM, New York, NY, USA, 913–926.

[17] Yueqi Chen, Zhenpeng Lin, and Xinyu Xing. 2020. A Systematic Study of Elastic Objects in Kernel Exploitation. In *Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security*. ACM, New York, NY, USA, 1165–1184.

[18] Rutvik Choudhary, Jiyong Yu, Christopher Fletcher, and Adam Morrison. 2021. Speculative Privacy Tracking (SPT): Leaking Information From Speculative Execution Without Compromising Privacy. In *MICRO-54: 54th Annual IEEE/ACM International Symposium on Microarchitecture*. ACM, New York, NY, USA, 607–622.

[19] Neophytos Christou, Alexander J. Gaidis, Vaggelis Atlidakis, and Vasileios P. Kemerlis. 2024. Eclipse: Preventing Speculative Memory-error Abuse with Artificial Data Dependencies. In *Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security (CCS '24)*. ACM, New York, NY, USA, 15 pages.

[20] Jonathan Corbet. 2012. Supervisor mode access prevention. https://lwn.net/Articles/517475/

[21] Intel Corporation. 2018. Indirect Branch Restricted Speculation. https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/technical-documentation/indirect-branch-restricted-speculation.html

[22] Intel Corporation. 2018. *Intel Analysis of Speculative Execution Side Channels*. Technical Report. Intel Corporation. https://www.intel.com/content/www/us/en/content-details/671163/intel-analysis-of-speculative-execution-side-channels.html White Paper.

[23] Intel Corporation. 2018. Retpoline: A Branch Target Injection Mitigation. https://www.intel.com/content/dam/develop/external/us/en/documents/retpoline-a-branch-target-injection-mitigation.pdf

[24] Intel Corporation. 2022. *Branch History Injection and Intra-mode Branch Target Injection / CVE-2022-0001, CVE-2022-0002 / INTEL-SA-00598*. Technical Report. Intel Corporation. https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/technical-documentation/branch-history-injection.html Technical Documentation.

[25] Intel Corporation. 2025. Affected Processors: Guidance for Security Issues on Intel® Processors. https://www.intel.com/content/www/us/en/developer/topic-technology/software-security-guidance/processors-affected-consolidated-product-cpu-model.html

[26] CrossDB. 2024. Bench Test. https://crossdb.org/get-started/bench/

[27] cryptsetup Group. 2025. cryptsetup. https://gitlab.com/cryptsetup/cryptsetup

[28] Lesly-Ann Daniel, Marton Bognar, Job Noorman, Sébastien Bardin, Tamara Rezk, and Frank Piessens. 2023. ProSpeCT: Provably Secure Speculation for the Constant-Time Policy. In *32nd USENIX Security Symposium (USENIX Security 23)*. USENIX Association, Anaheim, CA, 7161–7178.

[29] Davide Davoli. 2024. Comprehensive Kernel Safety in the Spectre Era. https://gitlab.inria.fr/ddavoli/comprehensive-kernel-safety-in-the-spectre-era

[30] Davide Davoli, Martin Avanzini, and Tamara Rezk. 2024. On Kernel's Safety in the Spectre Era (And KASLR is Formally Dead). In *Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security, CCS 2024, USA, October 14-18, 2023*. ACM, New York, NY, USA, 15 pages.

[31] Davide Davoli, Martin Avanzini, and Tamara Rezk. 2025. Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation (Extended Version). arXiv:2411.18094

[32] Theo de Raadt. 2017. OpenBSD 6.3. https://www.openbsd.org/33.html

[33] Jake Edge. 2013. Kernel address space layout randomization. https://lwn.net/Articles/569635/

[34] Dmitry Evtyushkin, Dmitry Ponomarev, and Nael Abu-Ghazaleh. 2016. Jump over ASLR: attacking branch predictors to bypass ASLR. In *The 49th Annual IEEE/ACM International Symposium on Microarchitecture*. IEEE, New York, NY, USA, 13 pages.

[35] Stephen Fischer. 2011. Supervisor Mode Execution Protection. https://www.ncsi.com/nsatc11/presentations/wednesday/emerging_technologies/fischer.pdf

[36] The Apache Software Foundation. 2025. ab – Apache HTTP server benchmarking tool. https://httpd.apache.org/docs/2.4/programs/ab.html

[37] Thomas Garnier. 2016. Randomizing the Linux kernel heap freelists. https://mxatone medium.com/randomizing-the-linux-kernel-heap-freelists-b899bb99c767

[38] Xinyang Ge, Nirupama Talele, Mathias Payer, and Trent Jaeger. 2016. Fine-Grained Control-Flow Integrity for Kernel Software. In *2016 IEEE European Symposium on Security and Privacy (EuroS&P)*. IEEE, New York, NY, USA, 179–194. https://doi.org/10.1109/EuroSP.2016.24

[39] Thomas Gleixner. 2022. Fix RSB fill on context switch for SERIALIZE. https://lore.kernel.org/all/20220716230344.239749011@linutronix.de/. Linux Kernel Mailing List.
[40] J. A. Goguen and J. Meseguer. 1982. Security Policies and Security Models. In *1982 IEEE Symposium on Security and Privacy*. IEEE, New York, NY, USA, 11 pages.

[41] Enes Göktas, Kaveh Razavi, Georgios Portokalidis, Herbert Bos, and Cristiano Giuffrida. 2020. Speculative Probing: Hacking Blind in the Spectre Era. In *Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security*. ACM, New York, NY, USA, 1871–1885.

[42] Daniel Gruss, Moritz Lipp, Michael Schwarz, Richard Fellner, Clémentine Maurice, and Stefan Mangard. 2017. KASLR is Dead: Long Live KASLR. In *Engineering Secure Software and Systems*. Springer International Publishing, Berlin, Heidelberg, 161–176.

[43] Daniel Gruss, Clémentine Maurice, Anders Fogh, Moritz Lipp, and Stefan Mangard. 2016. Prefetch Side-Channel Attacks: Bypassing SMAP and Kernel ASLR. In *Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security*. ACM, New York, NY, USA, 368–379.

[44] Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke, and Andrés Sánchez. 2020. Spectector: Principled Detection of Speculative Information Flows. In *2020 IEEE Symposium on Security and Privacy (SP)*. IEEE, New York, NY, USA, 1–19.

[45] Marco Guarnieri, Boris Köpf, Jan Reineke, and Pepe Vila. 2021. Hardware-Software Contracts for Secure Speculation. In *2021 IEEE Symposium on Security and Privacy (SP)*. IEEE, New York, NY, USA, 1868–1883.

[46] Ralf Hund, Carsten Willems, and Thorsten Holz. 2013. Practical Timing Side Channel Attacks against Kernel Space ASLR. In *2013 IEEE Symposium on Security and Privacy*. IEEE, New York, NY, USA, 191–205.

[47] Apple Inc. 2011. Mac OS X has you Covered. http://www.apple.com/macosx/security/

[48] Genivia Inc. 2025. ugrep. https://github.com/Genivia/ugrep-benchmarks

[49] Intel Corporation 2023. *Intel®64 and IA-32 Architectures Software Developer's Manual*. Intel Corporation.

[50] The kernel development community. 2023. Page Table Isolation (PTI). https://www.kernel.org/doc/html/next/x86/pti.html

[51] Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2019. Spectre Attacks: Exploiting Speculative Execution. In *2019 IEEE Symposium on Security and Privacy (SP)*. IEEE, New York, NY, USA, 1–19.

[52] Jakob Koschel, Pietro Borrello, Daniele Cono D'Elia, Herbert Bos, and Cristiano Giuffrida. 2023. Uncontained: Uncovering Container Confusion in the Linux Kernel. In *32nd USENIX Security Symposium (USENIX Security 23)*. USENIX Association, Anaheim, CA, 5055–5072.

[53] Jakob Koschel, Cristiano Giuffrida, Herbert Bos, and Kaveh Razavi. 2020. TagBleed: Breaking KASLR on the Isolated Kernel Address Space using Tagged TLBs. In *2020 IEEE European Symposium on Security and Privacy (EuroS&P)*. IEEE, New York, NY, USA, 309–321.

[54] C. Lattner and V. Adve. 2004. LLVM: a compilation framework for lifelong program analysis & transformation. In *International Symposium on Code Generation and Optimization, 2004. CGO 2004*. IEEE, New York, NY, USA, 75–86.

[55] Jinku Li, Zhi Wang, Tyler Bletsch, Deepa Srinivasan, Michael Grace, and Xuxian Jiang. 2011. Comprehensive and Efficient Protection of Kernel Control Data. *IEEE Transactions on Information Forensics and Security* 6, 4 (2011), 1404–1417.

[56] Arm Limited. 2022. Learn the architecture – Providing protection for complex software. https://developer.arm.com/documentation/102433/0100

[57] Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018. Meltdown: Reading Kernel Memory from User Space. In *27th USENIX Security Symposium (USENIX Security 18)*. USENIX Association, Baltimore, MD, 973–990.

[58] William Liu, Joseph Ravichandran, and Mengjia Yan. 2023. EntryBleed: A Universal KASLR Bypass against KPTI on Linux. In *Proceedings of the 12th International Workshop on Hardware and Architectural Support for Security and Privacy (Toronto, Canada) (HASP '23)*. ACM, New York, NY, USA, 10–18.

[59] Ziqin Liu, Zhenpeng Lin, Yueqi Chen, Yuhang Wu, Yalong Zou, Dongliang Mu, and Xinyu Xing. 2023. Towards Unveiling Exploitation Potential With Multiple Error Behaviors for Kernel Bugs. *IEEE Transactions on Dependable and Secure Computing* 21, 1 (2023), 1–18.

[60] Andrea Lottarini, Alex Ramirez, Joel Coburn, Martha A. Kim, Parhasarathy Ranganathan, Daniel Stodolsky, and Mark Wachsler. 2018. vbench: Benchmarking Video Transcoding in the Cloud. In *Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems (Williamsburg, VA, USA) (ASPLOS '18)*. Association for Computing Machinery, New York, NY, USA, 797–809.

[61] A. Mambretti, A. Sandulescu, A. Sorniotti, W. Robertson, E. Kirda, and A. Kurmus. 2021. Bypassing memory safety mechanisms through speculative control flow hijacks. In *2021 IEEE European Symposium on Security and Privacy (EuroS&P)*. IEEE Computer Society, Los Alamitos, CA, USA, 633–649.

[62] Tarjei Mandt. 2013. Attacking the iOS Kernel: A Look at 'evasi0n'. https://papers.putas/papers/ios/2013/NISlecture201303.pdf
[63] Ed Maste. 2023. Address Space Layout Randomization (ASLR). https://wiki.freebsd.org/AddressSpaceLayoutRandomization

[64] Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan. 2023. MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code. In *Proceedings of the 50th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '23, Vol. 7)*. ACM, New York, NY, USA, 30 pages.

[65] João Moreira, Sandro Rigo, Michalis Polychronakis, and Vasileios P. Kemerlis. 2017. DROP THE ROP: Fine-Grained Control-Flow Integrity for the Linux Kernel. In *Black Hat Asia 2017*. Black Hat, Singapore, 25.

[66] Santosh Nagarakatte, Jianzhou Zhao, Milo M.K. Martin, and Steve Zdancewic. 2009. SoftBound: Highly Compatible and Complete Spatial Memory Safety for c. SIGPLAN Not. 44, 6 (2009), 245–258.

[67] Marco Patrignani and Marco Guarnieri. 2021. Exorcising Spectres with Secure Compilers. In *Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security*. ACM, New York, NY, USA, 445–461.

[68] Android Open Source Project. 2022. Kernel Hardening. https://source.android.com/docs/core/architecture/kernel/hardening

[69] The LLVM Project. 2025. X86SpeculativeExecutionSideEffectSuppression.cpp File Reference. https://www.llvm.org/doxygen/X86SpeculativeExecutionSideEffectSuppression_8cpp.html

[70] Liam Proven. 2022. Linux 6.1: Rust to hit mainline kernel. https://www.theregister.com/2022/10/05/rust_kernel_pull_request_pulled/

[71] Joseph Ravichandran, Weon Taek Na, Jay Lang, and Mengjia Yan. 2022. PACMAN: Attacking ARM Pointer Authentication with Speculative Execution. In *Proceedings of the 49th Annual International Symposium on Computer Architecture*. ACM, New York, NY, USA, 685–698.

[72] Elena Reshetova, Hans Liljestrand, Andrew Paverd, and N Asokan. 2018. Toward Linux kernel memory safety. *Software: Practice and Experience* 48, 12 (2018), 2237–2256.

[73] Michael S and Vitaly Nikolenko. 2022. Linux kernel heap feng shui in 2022. https://duasynt.com/blog/linux-kernel-heap-feng-shui-2022

[74] SecurityScorecard. 2022. Threat overview for Linux Kernel. https://www.cvedetails.com/product/47/Linux-Linux-Kernel.html

[75] Hovav Shacham, Matthew Page, Ben Pfaff, Eu-Jin Goh, Nagendra Modadugu, and Dan Boneh. 2004. On the Effectiveness of Address-Space Randomization. In *Proceedings of the 11th ACM Conference on Computer and Communications Security*. ACM, New York, NY, USA, 298–307.

[76] Shixin Song, Joseph Zhang, and Mengjia Yan. 2025. Oreo: Protecting ASLR Against Microarchitectural Attacks. In *32nd Annual Network and Distributed System Security Symposium, NDSS 2025, San Diego, California, USA, February 24-28, 2025*. The Internet Society, Reston, VI, USA, 20 pages.

[77] Andrew S. Tanenbaum and Herbert Bos. 2014. *Modern Operating Systems* (4th ed.). Prentice Hall Press, USA.

[78] PaX Team. 2003. Documentation for the PaX project. https://pax.grsecurity.net/docs/

[79] Daniël Trujillo, Johannes Wikner, and Kaveh Razavi. 2023. Inception: Exposing New Attack Surfaces with Training in Transient Execution. In *32nd USENIX Security Symposium (USENIX Security 23)*. USENIX Association, Anaheim, CA, 7303–7320.

[80] Paul Turner. 2018. Retpoline: a software construct for preventing branch-target-injection. https://support.google.com/faqs/answer/7625886

[81] Zhi Wang and Xuxian Jiang. 2010. HyperSafe: A Lightweight Approach to Provide Lifetime Hypervisor Control-Flow Integrity. In *2010 IEEE Symposium on Security and Privacy*. IEEE, New York, NY, USA, 380–395.

[82] Robert N.M. Watson, Jonathan Woodruff, Peter G. Neumann, Simon W. Moore, Jonathan Anderson, David Chisnall, Nirav Dave, Brooks Davis, Khilan Gudka, Ben Laurie, Steven J. Murdoch, Robert Norton, Michael Roe, Stacey Son, and Munraj Vadera. 2015. CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization. In *2015 IEEE Symposium on Security and Privacy*. IEEE, New York, NY, USA, 20–37.

[83] Ofir Weisse, Ian Neal, Kevin Loughlin, Thomas F. Wenisch, and Baris Kasikci. 2019. NDA: Preventing Speculative Execution Attacks at Their Source. In *Proceedings of the 52nd Annual IEEE/ACM International Symposium on Microarchitecture*. ACM, New York, NY, USA, 572–586.

[84] Sander Wiebing, Alvise de Faveri Tron, Herbert Bos, and Cristiano Giuffrida. 2024. InSpectre Gadget: Inspecting the Residual Attack Surface of Cross-privilege Spectre v2. In *33rd USENIX Security Symposium (USENIX Security 24)*. USENIX Association, Philadelphia, PA, 577–594.

[85] Johannes Wikner and Kaveh Razavi. 2022. RETBLEED: Arbitrary Speculative Code Execution with Return Instructions. In *31st USENIX Security Symposium (USENIX Security 22)*. USENIX Association, Boston, MA, 3825–3842.

[86] Johannes Wikner, Daniël Trujillo, and Kaveh Razavi. 2023. Phantom: Exploiting Decoder-detectable Mispredictions. In *Proceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture* (Toronto, ON, Canada) (MICRO '23). Association for Computing Machinery, New York, NY, USA, 49–61.
[87] Jiyong Yu, Mengjia Yan, Artem Khyzha, Adam Morrison, Josep Torrellas, and Christopher W. Fletcher. 2019. Speculative Taint Tracking (STT): A Comprehensive Protection for Speculatively Accessed Data. In *Proceedings of the 52nd Annual IEEE/ACM International Symposium on Microarchitecture*. ACM, New York, NY, USA, 954–968.

[88] Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, and Yuval Yarom. 2023. Ultimate SLH: taking speculative load hardening to the next level. In *Proceedings of the 32nd USENIX Conference on Security Symposium*. USENIX Association, USA, 18 pages.