# Protecting cryptographic code against Spectre-RSB
(and, in fact, all known Spectre variants)

Santiago Arranz Olmos¹ ⬒, Gilles Barthe² ⚙️IDEA software

Chitchanok Chuengsatiansup³ ⚙️, Benjamin Grégoire⁴ *Inria*, Vincent Laporte⁵ *Loria*

Tiago Oliveira⁶ ⚙️, Peter Schwabe⁷ ⚙️, Yuval Yarom⁸ ⚙️, Zhiyuan Zhang⁹ ⚙️

MPI-SP, Bochum, Germany

*Inria* - Inria, Sophia Antipolis, France

SandboxAQ, USA

Radboud University, Nijmegen, The Netherlands

Ruhr University Bochum, Bochum, Germany

IMDEA Software Institute, Madrid, Spain

University of Melbourne, Melbourne, Australia

*Loria* Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

¹santiago.arranz-olmos@mpi-sp.org
²gilles.barthe@mpi-sp.org

³c.chuengsatiansup@unimelb.edu.au
⁴benjamin.gregoire@inria.fr

⁵vincent.laporte@inria.fr
⁶tiago.oliveira@sandboxquantum.com

⁷peter@cryptojedi.org
⁸yuval.yarom@rub.de
⁹zhiyuanz5@student.unimelb.edu.au

**Abstract**—It is fundamental that executing cryptographic software must not leak secrets through side-channels. For software-visible side-channels, it was long believed that “constant-time” programming would be sufficient as a systematic countermeasure. However, this belief was shattered in 2018 by attacks exploiting speculative execution—so called Spectre attacks.

Recent work shows that language support suffices to protect cryptographic code with minimal overhead against one class of such attacks, Spectre v1, but leaves an open question of whether this result can be extended to also cover other classes of Spectre attacks.

In this paper, we answer this question in the affirmative: We design, validate, implement, and verify an approach to protect cryptographic implementations against all known classes of Spectre attacks—the main challenge in this endeavor is attacks exploiting the return stack buffer, which are known as Spectre-RSB. Our approach combines a new value-dependent information-flow type system that enforces speculative constant-time in an idealized model of transient execution and a compiler transformation that realizes this idealized model on the generated low-level code. Using the Coq proof assistant, we prove that the type system is sound with respect to the idealized semantics and that the compiler transformation preserves speculative constant-time.

We implement our approach in the Jasmin framework for high-assurance cryptography and demonstrate that the overhead incurred by full Spectre protections is below 2% for most

cryptographic primitives and reaches only about 5–7% for the more complex post-quantum key-encapsulation mechanism Kyber.

## 1. Introduction

In this paper we present techniques to systematically protect high-performance cryptographic software against all known classes of Spectre attacks. Our work uses the computer-aided cryptography paradigm [12], i.e., we employ methodologies and tools from formal methods to build very efficient and formally verified cryptographic software. More specifically, we build our solution as part of Jasmin [4], [7], a programming language and framework that has been used to produce highly optimized and machine checked implementations of symmetric cryptography [7], elliptic-curve cryptography [4], hash functions [6] and very recently also post-quantum cryptography [5]. The Jasmin compiler is formally proven in Coq to preserve semantics, and offers tools to ensure properties relating to implementation security like memory safety, thread safety, and absence of secret-dependent branches and secretly indexed memory access; and furthermore offers an interface to the EasyCrypt [26] interactive theorem prover for proofs of functional correctness of implementations, that can be further connected to computer-verified reductionist cryptographic proofs of security, as, for instance, in [13], [14], [8].
An S&P 2023 paper [9] made an important first step toward integrating systematic protections against Spectre attacks into Jasmin. In short, that paper proposes a type system to ensure that typable programs are secure against a specific class of Spectre attacks, namely attacks exploiting misspecified conditional branches (aka Spectre-v1 or Spectre-PHT attacks). Furthermore, it presents extensions to the Jasmin language to protect programs (and thus make them typable). These protections mostly consist of selectively employing speculative load hardening (SLH) [21] as proposed in [39], incurring a remarkably small overhead of (typically) below 1%.

However, as that paper addresses only one class of Spectre attacks, the conclusion expresses hope that the work may serve as “a starting point to upgrade the gold standard of constant-time cryptography and will help deliver new post-quantum implementations that are not only protected against attacks by future large quantum computers, but also against the most common classes of speculative attacks.”

**Contributions.** In this paper, we first show that Jasmin programs are very easily, even naturally, protected against other classes of Spectre attacks. We then identify one major remaining challenge in protecting against all known classes of Spectre attacks. This remaining class is Spectre-RSB, i.e., attacks exploiting the return stack buffer.

We then present the main contribution of our paper, namely efficient and systematic protections against Spectre-RSB and their integration into the Jasmin framework. Our solution is a hybrid approach that combines selective speculative load hardening (selSLH) with program transformation. First, we replace calls and returns by conditional direct jumps, a transformation we call return table insertion. This transformation, which is inspired from prior work on return-oriented programming (ROP) [36], removes all Spectre-RSB gadgets. Second, we instrument programs with (an enhanced set of) language constructs to enforce selSLH on the source program (with calls). The combination of program transformation and selective speculative load hardening guarantees that transformed programs are speculative constant-time [23], i.e., do not leak secrets through timing even during speculative execution.

The next step is to check that programs are correctly instrumented. For this purpose, we define an information-flow type system for source programs in the spirit of the approach taken for Spectre v1 in [9]. Being cognizant that source programs will be transformed, the type system can check that program instrumentation will be sufficient to track misspeculation and to eliminate sources of speculative leakage through masking. We use the Coq proof assistant to formalize our approach for a core language: We define the source language and its speculative operational semantics, the return table insertion, and the type system. Our main result is a proof that the compilation of a well-typed program is speculative constant-time.

Next, we integrate our approach into the Jasmin framework. We extend the Jasmin language with an annotation for function calls and we modify the existing speculative

constant-time type system from [9] so that inserting return tables in well-typed programs yields speculative constant-time programs. Our implementation addresses practical issues ignored by our core language in the setting of a full-blown programming language. Last, we extend the Jasmin compiler with a new return table insertion pass; we consider different variants, allowing for instance return addresses to be stored in MMX registers or on the stack.

Finally, we perform an in-depth evaluation of the impact of our approach on cryptographic software. The evaluation is carried on a set of Jasmin implementations of cryptographic algorithms. These routines are derived from existing implementations from [9] that are already protected against Spectre-PHT. We use these routines to measure the overhead of our approach, both in terms of programmer effort and performance overhead. We show that the overhead for full Spectre protections is below 2% for most primitives and reaches only about 5–7% for the more complex post-quantum scheme Kyber [18].

**Artifacts.** We produce three artifacts: the Coq formalization, a new version of the Jasmin framework, and the libjade implementations. All artifacts are submitted as supplementary material and will be made publicly available. Items marked with ✖ can be found in the Coq formalization. The artifacts are in https://artifacts.formosa-crypto.org/data/rsbsecure.tar.bz2.

## 2. Background

As a starting point of this work we consider cryptographic software following the “constant-time” (CT) paradigm, i.e., software that, in sequential execution, systematically avoids data flow from secrets into memory addresses or branch conditions. The CT paradigm is widely regarded as a standard baseline defense mechanism against timing attacks [28]. The motivation for this paradigm is a leakage model that captures most traditional timing attacks by leaking the trace of all accessed memory locations and the complete control flow of the program. The goal of this paper is to systematically avoid leakage of secret data in this leakage model also during speculative execution. We specifically aim to protect cryptographic software in the Jasmin framework for high-assurance cryptography [4].

In Jasmin, the constant-time paradigm is enforced through an information-flow type system on source level. In short, all variables are typed as either secret or public and the type system enforces that operations taking secret inputs also produce secret outputs. Memory addresses and branch conditions have to be public. Preservation of the constant-time property through compilation has been formally proven in [15].

Spectre attacks, i.e., attacks that exploit leakage of secrets during speculative execution, are commonly classified based on the type of speculation. Let us briefly recall the nomenclature of Spectre attacks, based on [29] and [20], and review how Jasmin implementations protect against them.
**Spectre v1 (PHT).** Spectre v1 attacks [29, Sec. IV]—also called “Spectre-PHT” because they employ the *Pattern History Table*—exploit speculative execution following a mispredicted conditional branch. The simplest Spectre v1 gadget is a speculative bounds-check bypass, which results in speculatively reading outside a buffer. An efficient approach to protect CT cryptographic code in Jasmin against Spectre v1 was recently proposed in [9]. The high-level idea is to extend Jasmin’s CT type system to systematically avoid secretly indexed memory access and secret branch conditions even under speculative execution following a mispredicted conditional branch. The type system is extended by an additional security level, transient, for variables that are always public in sequential (non-mispredicted) execution but may contain secret data in speculative execution after a mispredicted branch. Variables typed as transient are not allowed to influence memory addresses or branch conditions, but they can be lowered to public through one of two mechanisms: inserting an *lfence* instruction introduces a speculation barrier and thus turns all transient variables to public; alternatively, a programmer can choose to lower a single transient variable to public by masking the variable with a misspeculation flag that is updated through arithmetic instructions at each branch. This second technique is selective speculative load hardening [39]. It is supported in Jasmin through three instructions:

* `init_msf()` inserts a speculation fence and sets a special register `msf` to the neutral value of masking NOMASK. We will use this register to track speculation and call it the *missspeculation flag* (MSF).<fnref n="1" />

* `update_msf(e)` conditionally updates the misspeculation flag `msf` to `MASK`, depending on the boolean expression `e`; it is essentially `msf = e ? msf`: `MASK`, implemented as an atomic conditional move instruction CMOV (which is not subject to the PHT speculation mechanism). We use this instruction after branches to check if execution has proceeded sequentially (and therefore the MSF should not be modified) or if the branch predictor has misspecified (and therefore the MSF should become `MASK`).

* `x = protect(y)` protects, i.e., masks, register `x` conditioned on the value of the misspeculation flag `msf`; that is, if the value of `msf` is `NOMASK`, register `x` receives the value of `y`, but if it is `MASK`, it gets the default value of the masking. This instruction is used to lower the type of `x` from transient to public.

**Spectre v2 (BTB).** Spectre v2 attacks [29, Sec. V]—also called “Spectre-BTB” because they employ the *Branch Target Buffer*—exploit speculative execution following a mispredicted indirect branch. A variant is BHI (for Branch History Injection), also called Spectre-BHB [11].

The Jasmin language does not support indirect branches, which means that Jasmin programs are inherently protected against Spectre v2.

**Spectre v4 (STL & PSF).** We define the class of Spectre v4 attacks as attacks where load instructions retrieve speculative data. This can be the case either because not all earlier store addresses have been resolved (speculative store bypass, STL) [29, Sec. VI], or because the CPU wrongly predicted a store-to-load forward (predictive store forwarding, PSF) [3]. These attacks are prevented by disabling the respective speculation, which, on Intel and AMD CPUs, is accomplished by setting the SSBD (speculative store bypass disable) flag in the CPU. As we will see in Section 8, the performance impact of setting this flag on cryptographic code is very small.

The one remaining class of Spectre attacks exploits the return stack buffer (RSB), so for the remainder of this paper we will assume that Spectre v2 and v4 attacks are addressed and focus on countermeasures against Spectre-RSB and their integration with countermeasures against Spectre v1.

## 3. Overview

Spectre-RSB was discovered independently by [30] and [32]. It exploits speculative execution when returning from a function; this speculation uses entries in the return stack buffer (RSB), hence the name. As the RSB is shared between processes, it can be trained by an attacker to direct speculative execution after a RET to *anywhere in the program*. Consider, e.g., the program in Figure 1a, which is vulnerable because when we call `id` (with `sec` as an argument), speculative execution may return to the `leak(x)` instruction and leak the secret.

Our countermeasure against Spectre-RSB uses two ingredients. The first is to use a program transformation that replaces all calls with direct jumps and all returns with return tables, i.e., nested conditional direct jumps. Figure 1b shows the transformation of the source program in Figure 1a. The transformed program is trivially protected against Spectre-RSB attacks, as there are no RET instructions.

However, after the transformation, the program is vulnerable to Spectre-PHT because the branch in `id` might be mispredicted, and speculative execution after the second invocation of `id` might proceed from the first call site and thus leak `sec`. At first glance, it might look like we have gained nothing. However, the transformation ensures that speculative execution can no longer be directed to an *arbitrary* location; instead, it can only be directed to a well-defined, known set of possible locations: the set of all call sites of the function we are “returning” from. This idea of rewriting RET instructions to a sequence of direct conditional jumps is not new; it was mentioned (but not implemented) as a potential Spectre-RSB countermeasure in [16, Sec. 7]. The second ingredient we use to protect the program is selective speculative load hardening. For a high-level description of `selSLH` and its implementation in Jasmin, see Section 2; for an example of its application to our simple example program, see Figure 1c.

We combine these two ingredients in a way that integrates well with the Jasmin workflow and is in spirit very

<footnote n="1">1. We will, for simplicity of presentation, assume that `msf` is a distinguished variable that does not occur in the program. This restriction is unnecessary and not present in our Coq development or the Jasmin language.</footnote>
1 id {
2   return
3 }
4
5 main {
6     x = pub
7     call id
8     leak(x)
9     x = sec
10    call id
11    ... // do not leak x
12 }

1 id:
2   if ra = 0 jump $\ell_0$
3   jump $\ell_1$
4
5 main:
6     x = pub
7     ra = 0
8     jump id
9     $\ell_0$: leak(x)
10    x = sec
11    ra = 1
12    jump id
13    $\ell_1$: ... // do not leak x

1 id:
2   if ra = 0 jump $\ell_0$
3   jump $\ell_1$
4
5 main:
6   init_msf()
7   x = pub
8   ra = 0
9   jump id
10  $\ell_0$: update_msf ra = 0
11  x = protect(x)
12  leak(x)
13  x = sec
14  ra = 1
15  jump id
16  $\ell_1$: ... // do not leak x

(a) This program leaks `sec` speculatively: an attacker can force the second call to `id` to return to the `leak(x)` instruction, thus leaking `x` which holds the value `sec`.

(b) Compiled program using return tables. This program does not use `RET` instructions. The second time the `id` block executes, when `x` gets a secret value, an attacker can mistrain the conditional jump predictor to predict that the jump to `$\ell_0$` will be taken, and speculatively leak `x`.

(c) Compiled program with `selSLH` protections. This program is protected because the value of `x` is masked before leaking it. If the attacker mounts the attack discussed in the previous snippet, only a default masked value gets leaked.

<caption>Figure 1: (a) Source program, (b) program with return tables, (c) protected program with return tables.</caption>

similar to the type system presented in [9]: We perform security typing on source level with function returns, and apply the transform from `RET` instructions to nested conditional jumps *afterward*, during compilation. This, however, means that the speculative semantics and the type system from [9] are insufficient to capture all effects of speculative execution. Specifically, they only capture misspeculation of source level conditionals (i.e., `if`/`else` constructions) and while loops. For these, the control-flow graph of the program is the same for sequential and for speculative execution. This is different for function returns that have been transformed into sequences of branch instructions: in sequential execution, the control-flow graph has only one edge, to the *actual* call site, while under speculative execution it has edges to *every* call site of the function in the whole program. This is a situation that the type system from [9] does not handle.

We therefore first define a language featuring calls and returns in addition to conditional statements and loops, together with a speculative semantics that captures at source level the protections offered by return tables (Section 4). We then present a type system that enforces speculative constant-time under these semantics (Section 5) and a compilation scheme that realizes the semantics and preserves leakage (Section 6). After this, Section 7 discusses how we implement this type system and compilation scheme in Jasmin, and Section 8 how we use that to protect libjade with little overhead. Lastly, we compare and contrast with related work in Section 9, discuss limitations (Section 10) and conclude (Section 11).

## 4. Language

In this section we introduce a core imperative language with function calls and returns and primitives for selective

speculative load hardening. This language allows us to define our security model and notion of speculative constant-time.

### 4.1. Security model

As stated in Section 2, we are considering Spectre-RSB and Spectre-PHT attacks; however, as compilation transforms function returns to return tables, our security model does not aim to capture the full power of a Spectre-RSB attacker at source level. Opting for a weaker security model at source level is beneficial, because it minimizes the amount of protections that programmers need to write in their code, and leads to more efficient programs. Moreover, the choice of a weaker model has no negative security implication, as our method still ensures that compiled programs are protected against all Spectre attacks.

### 4.2. Syntax

For simplicity, we consider function calls without local variables, arguments, or return values. The syntax of expressions, instructions and code is as follows:

$$ 
\begin{align*}
e &::= n \mid b \mid x \mid \text{op1}(e) \mid \text{op2}(e, e) \\
i &::= x = e \mid x = a[e] \mid a[e] = x \\
   &\quad | \text{if } e \text{ then } c \text{ else } c \mid \text{while } e \text{ do } c \mid \text{call}_b f \\
   &\quad | \text{init\_msf()} \mid \text{update\_msf}(e) \mid x = \text{protect}(x) \\
c &::= [] \mid i; c
\end{align*}
$$

where `n` is an integer, `b` a boolean, `x` a register variable, and `a` an array variable. We assume that each array comes with its size $|a|$. The definitions are standard, except for the call
<figure><img src="image_1.png" /><figcaption>Figure 2: The function *g* has two continuations of *f*, one after each call site.</figcaption></figure>

instruction and the selSLH instructions (which are described
in Section 3). The call_ f instruction calls f and performs
an MSF update on the register msf upon return. On the
other hand, the instruction call_ f is a usual assembly
CALL f instruction, which does not update the misspeculation
flag. We need this MSF update in call instructions because
we will compile returns to tables of conditional branches,
which may trigger misspeculation. Instead of interleaving
several MSF updates in the table, as is usual in SLH, we
can perform just one at the return site.

A program is a set of pairs of function names and code, i.e., *p* := *P*(*f* × *c*), where there is one distinguished pair that is the entry point. The entry point has no callers, and execution halts after reaching its return.

4.3. Semantics

To formalize our security model, we define for every
function *f* its set of continuations *C*(*f*), consisting of triples
(*c*, *g*, *b*), where *g* is a function that contains an instruction
call<sub>*b*</sub> *f* and *c* is the code that remains to be executed after
returning from the call. Intuitively, if the code of *g* is of
the form ...; call<sub>*b*</sub> *f*; *c* then (*c*, *g*, *b*) is a continuation of
*f*; however, some care is needed to deal with function calls
within loops.

Let *c* be the body of function *g* in Figure 2. We note
that there are two continuations of *f* in *c*: the first one is
(*x* = *x* + 1; *c*, *g*, ⊤), i.e., when returning from *f* to the first call
site we need to finish executing the loop body and then
reenter the loop, and the second one is (*x* = 0, *g*, ⊥), i.e.,
when returning from *f* to the second call site we only need
to execute the last assignment to *x*. We present the precise
definition of continuations in Appendix A.

Directives use continuations to model the attacker's
power to influence execution. The directive step is a usual
sequential step, force *b* takes the *b* branch of a conditional,
mem *a* *i* forces an unsafe memory access to read from or
write to the address (*a*, *i*) instead, and return *c* *f* *b* forces the
function to return to a continuation (*c*, *f*, *b*). On the other
hand, observations model execution leakage from control
flow and memory accesses. The observation • corresponds
to no observation, branch *b* indicates that the condition of
a conditional evaluated to *b*, and addr *a* *i* that a memory
access to array *a* in position *i* occurred.

Dir ::= step | force b | mem a i | return c f b

Obs ::= • | branch b | addr a i

We define the single-step semantics of our language with a judgment *m* $\stackrel{o}{\rightarrow}_d$ *m'* that expresses that the directive *d* makes the machine *m* step to *m'* and produce an observation *o*. Machines are 6-tuples <*c*, *f*, *cs*, *ρ*, *μ*, *ms*> that consist of the code being executed, the name of the function being executed, the call stack, the register map, the memory, and the misspeculation status. A call stack is a list of pairs of code and function names, a register map maps register names to values, a memory maps arrays and valid indices to values, and a misspeculation status is a boolean. Since we will only deal with one program at a time, we will always leave the program implicit.

Figure 3 presents the semantics for loads, protects, conditionals, calls and returns. The N-LOAD rule is the usual rule for memory loads, where the expression needs to evaluate to an integer that is in bounds for the array. This rule has addr *a* *i* as an observation because memory accesses leak their addresses, and ignores its directive. On the other hand, the S-LOAD rule only applies if the access is out of bounds, and allows the attacker to read data from *any* array and index. We require the misspeculation status to be ⊤ because we assume the program to be sequentially safe.

The PROTECT rule shows how we can use the MSF to
mask a value. If the variable msf is set to MASK, the result
of a protection is a default value.

The COND rule shows that the attacker controls the
execution of conditionals via the force *b* directive. The con-
dition of the statement only plays a role in the observation,
branch [[e]]<sub>ρ</sub>.

The CALL rule states that a function call puts the body
and name of the callee as the code and function name under
execution, and pushes the current code and function name
to the call stack.

The N-RET rule represents a normal return, during which execution is transferred to the caller, i.e., the top of the call stack. The S-RET rule forces execution to continue to a continuation (*c*, *g*, *b*) of *f* (of the adversary’s choosing, different from the top of the call stack), sets the misspeculation status to ⊤, and, if *b* is ⊤, sets *msf* to MASK. Note that the call stack plays no role during speculative execution and hence is discarded. This rule captures a misspeculation in the return table of a compiled function.

Figure 3 also defines multi-step semantics as the reflex-
ive transitive closure of the single-step one, accumulating
the directives and observations. The rest of the rules are
similar, and shown in Appendix A.

4.4. Speculative constant-time

We now have all the ingredients to define speculative
constant-time. The definition is parameterized by an equiv-
alence relation on machines.

**Definition 1** (Speculative constant-time, *φ*-SCT). Let *φ*
be an equivalence relation on machines. A program *p* is
speculative constant-time with respect to *φ*, denoted *φ*-SCT,
if and only if all executions of machines that are related
by *φ* following a given list of directives produce the same
<figure><img src="image_2.png" /><figcaption>Figure 3: Selected rules of the small step operational semantics.</figcaption></figure>

observations. That is, for every pair of related machines $m_1 \phi m_2$ with executions $m_i \xrightarrow{O_i/D} m'_i$ we get $O_1 = O_2$.

## 5. Type system

In this section we introduce a type system for speculative constant-time. We then prove that all initial machines of a well-typed program that coincide in their public parts produce the same observations under all sequences of adversarial directives ⚙️.

Our type system uses security types to track the confidentiality of data and detect possible violations, both under sequential and speculative execution. Concretely, we attach security levels to data (in our case, a confidentiality lattice {L, H} with L ≤ H, corresponding to public and secret data) and define types as either a level or a type variable α (this is the case when the same register or memory location is used to hold data of different levels at different times). Finally, registers and memory locations get security types, which consist of a type (that represents the confidentiality of the data under sequential execution) and a level (that represents the maximum confidentiality of the data under all possible speculative executions)

level ::= H | L type ::= level | α stype ::= <type, level>

<figure><img src="image_3.png" /><figcaption>Figure 4: MSF type automaton.</figcaption></figure>

and we write $\tau_n$ to refer to the normal (first) component, and $\tau_s$ for the speculative (second) component of the security type $\tau$. Thus, a public variable has type $\langle L, L \rangle$, a secret one $\langle H, H \rangle$, and a transient one $\langle L, H \rangle$. Allowing polymorphism in the speculative component of a security type makes the type system unsound, see Appendix A for a detailed explanation.

### 5.1. Misspeculation type

Our type system also needs to keep track of the misspeculation flag to detect whether protections will be effective.
$$
\begin{align*}
\mathit{FV}(\Sigma) &:= \begin{cases} \mathit{FV}(e) & \text{if } \Sigma \text{ is outdated}(e) \\ \emptyset & \text{otherwise} \end{cases} \\
\mathit{to\_lvl}(t) &:= \begin{cases} \mathsf{L} & \text{if } t \text{ is } \mathsf{L} \\ \mathsf{H} & \text{otherwise} \end{cases} \\
\Sigma|_e &:= \begin{cases} \mathit{outdated}(e) & \text{if } \Sigma \text{ is updated} \\ \mathit{unknown} & \text{otherwise} \end{cases} \\
\Sigma \subseteq \Sigma' &:= \Sigma = \mathit{unknown} \lor \Sigma = \Sigma'
\end{align*}
$$

<caption>Figure 5: Auxiliary definitions for type rules. The free variables of an MSF type are the free variables of its condition if it is outdated, and empty otherwise. Note that $\Sigma|_e$ corresponds to the `if e` and `while e` arrows of the MSF type automaton (Figure 4). The order for MSF types is flat with unknown as the bottom element.</caption>

For this, we define the MSF type

$$
\Sigma ::= \text{unknown} \mid \text{updated} \mid \text{outdated}(e)
$$

Figure 4 gives an intuition of the behavior of these types. The MSF type unknown expresses that we do not know whether the machine is misspeculating. The MSF type updated means that the variable *msf* accurately tracks speculation: *msf* holds the value NOMASK if execution has been sequential, and MASK if there has been misspeculation. Performing an *init_msf()* takes us to updated since this instruction executes a speculation fence. Lastly, the MSF type outdated(*e*) expresses that *msf* holds a value that can be updated to track speculation accurately. After a conditional jump on *e* in state updated, we transition to outdated(*e*), and we need to execute an *update_msf*(*e*) to recover the MSF.<fnref n="2" />

The typing judgment is of the form $\Gamma, \Sigma \vdash c : \Gamma', \Sigma'$, where $\Gamma$ and $\Gamma'$ are mappings from register and array variables to security types (which have a normal and a speculative component), $\Sigma$ and $\Sigma'$ are a MSF types, and $c$ is code. Figure 6 presents the typing rules, with some auxiliary definitions in Figure 5.

Type checking requires a static signature for all functions of the program, which associates each function name *f* with a signature $\Sigma_f, \Gamma_f \rightarrow \Sigma'_f, \Gamma'_f$ of input and output MSF types and contexts. Signatures may contain type variables that get instantiated at each call site. The purpose of the signature is to fix the type of each function, as functions may be typable with different types; they also allow modular verification.

The first three rules are straightforward. Firstly, the ASSIGN rule assigns to *x* the type of the expression *e*. We must ensure that the assigned variable does not occur in Σ to be able to accurately update the MSF later on; however, if we do not want to update the MSF, we can always choose to weaken Σ to unknown with the WEAK rule and make this restriction vacuous. Secondly, the LOAD rule ensures that

the array index is public, even speculatively. Variable *x* gets its normal type from the array, but since the index might be speculatively out of bounds, we need to overapproximate the speculative type as H. Lastly, the STORE rule also ensures that the index is public, and we update the normal type of the array to the normal type of *x*, but similarly to the case for load, the index might be out of bounds, so we need to update the speculative types of all arrays.

Next come the rules for selSLH instructions. The INIT-MSF rule sets the MSF type to updated, and sets the type of each register and array variable to its sequential counterpart, overapproximating polymorphic type variables with H: $\langle L, t \rangle$ goes to $\langle L, L \rangle$, $\langle H, t \rangle$ goes to $\langle H, H \rangle$, and $\langle \alpha, t \rangle$ goes to $\langle \alpha, H \rangle$. We define this to(·) overapproximation in Figure 5. Secondly, the UPDATE-MSF rule expects the MSF type to be outdated, and updates it if the condition is the same. Lastly, the PROTECT rule requires that the MSF is updated, and sets the security type of *y* to the sequential counterpart of the one for *x*, similarly to the INIT-MSF rule but for one variable only.

The COND rule ensures that the condition of an if instruction is public, and that each branch is typable with an outdated MSF type w.r.t. the appropriate condition. We define this, denoted $\Sigma|_e$, in Figure 5. This means that the then-branch will need to perform an MSF update with respect to *e* if it needs to use protect, and similarly for the else-branch with !*e*. The WHILE rule is analogous.

The CALL rule ensures that before every call site of *f*, the current MSF type and context are what *f* expects them to be, according to its signature. The resulting MSF type depends on the boolean parameter of the instruction: if we want the type to be updated, we need the parameter to be ⊤ and the output MSF type of the function to be updated. This rule allows instantiating the type variables in $\Gamma$ with $\theta$.

The WEAK rule allows to compose typing judgments by weakening them, and the NIL and CONS rules chain judgments in the usual way. Finally, a program is well-typed if the body of each function is typable with its signature.

## 5.2. Soundness

Our soundness theorem states that executions of a typable program depend only on public data. Recall that the definition of SCT is parameterized by a relation. The relation we need is indistinguishability of machines, which holds when two machines coincide on their public values.

We interpret types as relations between values

$$
\begin{align*}
x =_{\tau} y &:= \tau = \mathsf{L} \implies x = y \\
\rho =_{f} \rho' &:= \forall x. \rho(x) =_{f(x)} \rho'(x) \\
\mu =_{f} \mu' &:= \forall a i. \mu(a, i) =_{f(a)} \mu'(a, i)
\end{align*}
$$

where $\tau$ can be a type variable: we show that this is not a problem since a program that is typable under $\Gamma$ is also typable under $\theta(\Gamma)$ for every instantiation $\theta$, in particular when $\theta(\tau)$ is $\mathsf{L}$ ⊢ .

We use these notions to define the indistinguishability relation between machines, extending [9].

<footnote n="2">2. For clarity, we depart from the notation in [9]: what that work denotes ms we write as updated, and for ms|e we write outdated(e).</footnote>
<figure><img src="image_4.png" /><figcaption>Figure 6: Type system. Here $\theta: \text{typeVar} \to$ level is an instanciation of type variables and $\text{Sig}$ is the signature for functions of the program. We define $\Gamma \le \Gamma'$ pointwise.</figcaption></figure>

**Definition 2** (Machine indistinguishability). Two machines are indistinguishable under $\Gamma$, denoted $\langle c, f, cs, \rho, \mu, ms \rangle =_{\Gamma} \langle c', f', cs', \rho', \mu', ms' \rangle$, if their code, function name, call stack and misspeculation status are the same

$$c = c' \quad f = f' \quad cs = cs' \quad ms = ms'$$

they coincide on their speculatively public parts

$$\rho =_{\Gamma_s} \rho' \quad \mu =_{\Gamma_s} \mu'$$

and they coincide on their sequentially public parts if they are not misspeculating

$$ms \lor (\rho =_{\Gamma_n} \rho' \land \mu =_{\Gamma_n} \mu')$$

The relation we will use for our main theorem states that the machines are indistinguishable and are executing the entry point of the program

**Definition 3** (Initial machine). An initial machine for a program $p$ is of the form $\langle c, f, \emptyset, \rho, \mu, ms \rangle$, where $c$ is the code for the entry function and $f$ its name.

**Definition 4** (Initial SCT relation). We will say that two machines are in the relation $\phi_{\Gamma}$ if they are initial and indistinguishable under $\Gamma$.

**Theorem 1** (Soundness $\blacksquare$). If a program is safe and typable, and the initial type for its entry point is (unknown, $\Gamma$), then it is $\phi_{\Gamma}$-SCT (that is, every pair of initial machines that coincide on their public parts and their misspeculation statuses produce the same observations, under the assumption that the directives are the same).

Informally, the notion of safety is that any reachable state (starting from an initial state of the program) is either misspeculating, final (i.e., the program has been executed fully), or there is a directive that allows a step of execution.

Remark that the notion imposes the usual conditions only when the reached state is not misspeculating, i.e., under sequential execution.

The proof of the soundness theorem needs two important lemmas, for single and multi-step execution soundness. These say that if a machine is well-typed, which intuitively means that the code being executed and the contents of the call stack are typable, the resulting machine after one (resp. many) execution step (resp. steps) is also well-typed and the observations are the same for all indistinguishable machines. Naturally we also need to show that initial machines are well-typed.

The definition of SCT states that both related machines must step under the same directives. At first sight, if one of the machines steps but the other one gets stuck, it is not guaranteed that leakage is independent from secrets. We prove that this is impossible: if a typable machine can step under directives $D$, then all indistinguishable machines can step under the same directives $\blacksquare$.

## 6. Return table insertion

In this section we present return table insertion and show that this transformation preserves speculative constant-time. We compile our structured source language into an unstructured linear language with the same base instructions (assignments, loads, stores, and seSLH instructions) but without the control flow primitives (i.e., conditional, while, and function calls). The linear language has only two control flow constructs, conditional and unconditional direct jumps,
$$ (\lfloor \text{call}_\top f \rfloor) := \begin{array}{l} ra_f = \ell_{\text{ret}} \\ \text{jump } f \\ \ell_{\text{ret}} : \text{update\_msf}(ra_f = \ell_{\text{ret}}) \end{array} $$

$$ (\lfloor \{\ell_r\} \rfloor)_{\text{rettbl}}^f := \text{jump } \ell_r \\ (\lfloor \{\ell_r\} \cup \ell^* \rfloor)_{\text{rettbl}}^f := \text{if } ra_f = \ell_r \text{ jump } \ell_r; (\lfloor \ell^* \rfloor)_{\text{rettbl}}^f $$

Figure 7: Compilation of function calls and return tables. We write $\lfloor c \rfloor$ for the compilation of $c$, and $\lfloor \ell^* \rfloor_{\text{rettbl}}^f$ for the compilation of the return table of $f$ whose entries are $\ell^*$. We omit the labels of instructions that do not need them. The register $ra_f$ is where the function $f$ expects its return address.

and programs are lists of labeled instructions:

$$ \begin{array}{l} li ::= x = e \mid x = a[e] \mid a[e] = x \\ \quad \mid \text{init\_msf()} \mid \text{update\_msf}(e) \mid x = \text{protect}(x) \\ \quad \mid \text{jump } \ell \mid \text{if } e \text{ jump } \ell \\ lc ::= [] \mid (\ell : li); lc \end{array} $$

Linear machines, while similar to source ones, are 4 tuples $\langle \ell, \rho, \mu, ms \rangle$, where instead of code being executed we have the *program counter*, which is a label pointing to an instruction in the program. If $t$ is a linear machine, $t_{pc}$ denotes its program counter. The operational semantics of this language is standard, with similar directive and observation behavior as the source. We show the precise rules in Appendix B.

Figure 7 presents our compilation scheme for non-recursive function calls. Compiling assignments, memory and selSLH instructions is trivial since the two languages coincide on these constructs. We compile conditionals and loops in the standard way with a conditional jump. For a non-recursive function $f$, we pass its return address in a dedicated return address register $ra_f$; we discuss this restriction in Section 7.

Figure 7 also shows the compilation of return tables as a sequence of conditional direct jumps, given a non-empty set of return labels. If the set has only one return label, we generate a direct jump to it. Otherwise, we generate conditional branches comparing return addresses with each return label. We show rigorous definitions for the compilation scheme, including basic instructions, in Appendix B.

Compiling a program $p$, denoted $\lfloor p \rfloor$, entails compiling for each function $f$ its body at a distinguished label $\ell_f$, followed by its return table at $\ell_{\text{ret}_f}$. We derive the set of return labels of a function from its set of continuations, that is, the program points following a call to it. As mentioned in Section 4, the entry point has no callers, and thus no return table.

**Preservation of SCT.** We use a similar definition of SCT to the one in Section 4.4 for linear programs and define a

similar relation $\phi_\Gamma^l$ which expresses the same indistinguishability relation between states. Note that while the source relation requires that the code of the machines are equal, the linear relation requires that the program counters point to the same instruction. Our compilation scheme preserves SCT for typable source programs.

**Theorem 2 (Preservation of SCT $\mathcal{P}$).** If $p$ is typable then $\lfloor p \rfloor$ is $\phi_\Gamma^l$-SCT.

We prove this theorem by showing that the leakage of an execution depends only on the public part of the initial state and a corresponding source execution. In order to do this, we define a directive transformer $T_{\text{Dir}}(\cdot, \cdot) : \text{label} \times \text{Dir} \to \text{Dir}^*$ that computes source directives given the program counter and a target directive, and a leakage transformer $T_{\text{Obs}}(\cdot, \cdot) : \text{label} \times \text{Obs}^* \to \text{Obs}$ that computes target leakage given the program counter and source leakage. For single step executions, we prove

**Lemma 1 (Single-step leakage transformation $\mathcal{P}$).** For all single-step executions $t \xrightarrow{\alpha_t} t'$, if there exists a typable source machine $s \sim t$, then there exists $s'$ and $O_s$ such that $s \xrightarrow[T_{\text{Dir}}(t_{pc}, d)]{O_s} s'$, $T_{\text{Obs}}(t_{pc}, O_s) = o_t$, and $s' \sim t'$.

Here the relation $s \sim t$ indicates that the linear machine $t$ is the compilation of the source machine $s$. Note that $T_{\text{Dir}}(t_{pc}, d)$ can be empty, which corresponds to a silent step in the source. It is usual that backward simulations for compiler correctness proofs require showing that there are a finite number of silent steps, but for security proofs like ours this is not needed—silent steps do not leak secrets.

Extending this to multi-step executions allows us to prove **Theorem 2**: given two target executions with leakages $O_t$ and $O'_t$, we know that there exist source executions with leakages $O_s$ and $O'_s$ such that $T_{\text{Obs}}^*(t_{pc}, O_s) = O_t$ and $T_{\text{Obs}}^*(t_{pc}, O'_s) = O'_t$. By soundness of the source type system we know $O_s = O'_s$, and therefore $O_t = O'_t$.

Let us now give an intuition for the transformers for directives and observations. Recall the example in Figure 1a and its compilation in Figure 1b. In Figure 8 we present the attack discussed before, showing the current instruction and directive in the second and third columns. Recall that the attack consists of executing sequentially until the second call to id, and when we return for the second time, we mispredict and go to the first call site (we mark sequential execution with **thin blue directives** and misspeculating execution with **thick red directives**). The transformers tell us how, from the current program counter $pc$ and the target directive $d$, we can produce a list of source directives $T_{\text{Dir}}(pc, d)$, such that their leakage $O_s$ predicts the target observation $o$. We have two interesting cases in this execution: first, instructions that store return addresses are not present in the source, so the source directives are $[]$, i.e., the source machine does not step (we mark these with $\rightsquigarrow$). In these cases the target observation is always $\bullet$. Second, return tables consist of conditional branches, so we need to translate force directives into return directives (we mark these with $\to$). The leakage here depends on the value of $ra$, which we can compute since
<figure><img src="image_5.png" /><figcaption>Figure 8: The attack from the example in Figure 1b. Here $κ$ is the continuation after the first call to id, that is $(leak(x); ..., main, ⊥)$.</figcaption></figure>

the CFG is public. We present the precise definition of the directive and observation transformers in Appendix B.

## 7. Implementation in the Jasmin compiler

In this section, we describe how we implemented the type system and compilation scheme, presented in Sections 5 and 6, in Jasmin [4], [7], a low-level programming language for high-assurance high-speed cryptography. The Jasmin language is designed to write efficient and verification-friendly assembly code. It directly exposes assembly instructions to the programmer, except for jumps, since control flow in Jasmin consists of if statements, while loops, for loops (which are always unrolled), and function calls. Jasmin also provides several zero-cost abstractions over assembly, such as register and stack variables, that the compiler allocates to architectural registers and stack offsets.

The Jasmin compiler consists of around thirty passes and is written and verified in Coq; it outputs AMD64 (i.e., x86-64) assembly and has experimental support for ARMv7-M. Some exemplary passes are: Inlining, which removes function calls annotated as `#inline` by the bodies of their functions; Unrolling, which unrolls all for loops; Stack Allocation, which replaces operations on stack variables by memory accesses; Register Allocation, which renames and reuses variables to require only architectural registers; and Linearization, which replaces structured control flow by jumps. For the present work, we introduce a new pass after Linearization that replaces all CALL and RET instructions with direct jumps and return tables.

The Jasmin compiler can also produce a representation of the program to reason in the EasyCrypt [26] proof assistant. Finally, Jasmin comes with three static analyzers: 1) a safety checker that attempts to prove that a program terminates, accesses only valid memory, and produces no arithmetic errors like division by zero; 2) a constant-time checker that ensures that a program does not leak secrets through timing side-channels in sequential execution; and 3) a speculative constant-time checker that ensures that a program is constant-time even under speculative execution.

**Changes to the SCT checker.** Jasmin provides an automatic checker for Spectre-PHT vulnerabilities that takes into account seSLH instructions. We extend this checker to consider also Spectre-RSB, following the type system from Section 5. We must now bridge the gap between the model presented in this work and Jasmin. Firstly, function calls in our model are nothing more than a transfer of control to the body of the function, while in Jasmin, functions have local variables, arguments, and results. Since, at the source level, we do not know which variables of the callers of a function will be allocated to which registers, we need to be coarser than in Section 5 and consider all variables as speculatively secret after a function call. Secondly, we introduce an annotation for function calls corresponding to the boolean parameter of call instructions, where $⊥$ is the default and $⊤$ requires an annotation

$$ 
\begin{align*}
call_{\perp} f &\Rightarrow x = f(y); \\
call_{\top} f &\Rightarrow \#update_{after\_call} x, msf = f(y, msf);
\end{align*}
$$

Note that in Jasmin, the MSF variable is explicit, and, as mentioned in Section 2, in both the Coq development and the Jasmin compiler, we can keep the MSF in any location (registers, MMX registers, or on the stack), which allows us to spill it when register pressure is high.

**Changes to the compiler.** We adapt the Jasmin compiler to use direct jumps instead of CALL and RET instructions. As discussed in Section 6, we compile unannotated function calls as two instructions (to save the return address and perform a direct jump). In contrast, calls annotated with `#update_after_call` issue a third one, an MSF update.

We implement return tables as trees, which means that the number of comparisons is logarithmic in the number of callers of a function. Moreover, at return sites, in most cases, we can reuse the flags that we set in the last comparison before jumping. The most frequent instance of this is the one depicted in Figure 9, where at the return site $ℓ$ we can reuse the EQ condition in the MSF update without performing another comparison.

The compiler is flexible in passing return addresses
<table><caption>Figure 9: A return table implemented as a tree and a return site that reuses the comparison made in the table.</caption><tr><td>1</td><td>callee:</td></tr><tr><td>2</td><td>...</td></tr><tr><td>3</td><td>CMP ra, l</td></tr><tr><td>4</td><td>JMPeq l</td></tr><tr><td>5</td><td>JMPIt LTahan branch</td></tr><tr><td>6</td><td>// GTah branch</td></tr></table>

<table><caption>Figure 10: How a secret may leak as a return tag.</caption><tr><td>1</td><td>f:</td></tr><tr><td>2</td><td>...</td></tr><tr><td>3</td><td>ra<sub>g</sub> = f<sub>0</sub></td></tr><tr><td>4</td><td>jump g</td></tr><tr><td>5</td><td>f<sub>0</sub>: ...</td></tr><tr><td>6</td><td>if ra<sub>f</sub> = l jump l</td></tr><tr><td>7</td><td>jump l'</td></tr></table>

in different ways. For libjade, using MMX registers was the best option. Cryptographic implementations seldom use these registers. By modifying the type checker to ensure that all writes to MMX registers are public, even speculatively, we never need to protect them. This restriction is also beneficial when we only need to protect a few values since we can place them in MMX registers and thus avoid keeping an MSF. Since using these registers can be expensive and register pressure can be high in some of the programs in libjade, the compiler also allows passing return addresses on the stack or in general-purpose registers. This, however, requires some care: when passing them in an arbitrary location, we need to be mindful of speculative writes to this location.

Figure 10 shows how naively passing the return address is insecure. Remark that a return table leaks its return address since it performs conditional branches on it. In this example, the problem is that the return table in f leaks the secret that evil puts into the register ra<sub>f</sub>. The function g cannot modify register ra<sub>f</sub> because one of its callers, f, uses it. However, a different caller, evil, can put a secret there, and when it calls g, the attacker can force g to return to f. The return table in f then leaks ra<sub>f</sub> as remarked.

Protecting the return address using an MSF mitigates the problem: the leaked comparisons will be against a default value instead of a secret. Note that there is no risk of a speculative write to the return address forcing execution to an invalid program point since the table will perform comparisons on it, but the targets of all jumps are hard coded valid labels. We can pass the return address on the stack for recursive, or more generally reentrant, functions, but this is unnecessary for Jasmin as it does not support them. The drawback of protecting return addresses is that we need an MSF at each return site that needs the protection. This entails keeping an MSF updated, which means more instructions and data dependencies, and, therefore, a greater

overhead. Fortunately MMX registers are free from this drawback.

## 8. Evaluation

This section overviews the changes to libjade and evaluates the computational cost of applying Spectre-RSB countermeasures. Libjade is a high-assurance cryptographic library written in Jasmin and extended by [9] to be Spectre-PHT protected. The present work uses the artifac from that work as our starting point, which contains the constant-time implementations (without countermeasures against any Spectre attack) and the corresponding Spectre-PHT protected implementations.

### 8.1. Modifications to libjade

We started by updating these implementations to be compatible with recent versions of the Jasmin compiler and then added RSB protections to the Spectre-PHT protected version. Most of the changes were in the context of Kyber, and no implementations other than Kyber required the \#update_after_call annotation. Kyber512 and Kyber768 share a significant part of the code, which is generic on the algorithm's parameters. We needed to annotate 49 out of 51 call sites in Kyber512 with \#update_after_call, and 56 out of 58 in Kyber768. The rejection sampling algorithm is the main reason for the difference in the number of call sites between Kyber512 and Kyber768 (it accounts for six call sites). Very briefly and informally, Kyber512 samples a 2 × 2 matrix of polynomials, while Kyber768 a 3 × 3 one. AVX2 256-bit registers and instructions work nicely to perform four samplings at a time, which means that Kyber768 follows the same pattern as Kyber512 for the first eight polynomials and then needs to sample an extra one separately.

Sometimes, we can avoid keeping an MSF by applying one of four different strategies while still protecting our code; Kyber, in both versions, has examples of all four. First, we inline function calls when the code size penalty is minor; this is the case for two function calls in Kyber. Second, we spill public values to MMX registers—these are guaranteed to remain public—when the performance penalty is minor; this is the case for all calls to SHAKE in Kyber. Third, we enforce that some function arguments are always public since, in some cases, the type system (soundly) generalizes too much and gives false positives. An example of this is the id function in Figure 1a: the type system will greedily assign a polymorphic type to this function, α → α, and thus will we need to protect its result after calling it. If in our program we notice that we only call it with public arguments, we can annotate this function as id(#public x) -> #public, which is a weaker type, but frees us from having to protect its result after calling it. To justify the fourth and last strategy, let us remark that if a function does not modify a particular register, which is guaranteed to be public at every call site of the function, we can safely assume that it is public at each return site—this is an extension of the third strategy. We can
capitalize on this realization at the Jasmin level by making
such functions take extra arguments, *annotating them as public*, and returning them unmodified. In this way, the type
system will enforce that these variables are always public
at every call site, even speculatively, and register allocation
will force these variables to the same architectural register
since they are an argument to a function.

We note that the keypair and enc functions of Kyber each
use a call to an external randombytes function that serves
as a wrapper around a getrandom system call. These calls
to external functions (with actual RET instructions) violate
the assumptions of our security arguments; they are currently
being replaced by a re-implementation of randombytes for an
upcoming Jasmin release. We expect no significant perfor-
mance difference from this upcoming change to Jasmin.

8.2. Performance of libjade

Table 1 reports benchmarks of highly optimized imple-
mentations of various cryptographic primitives in libjade
with different Spectre protections. The reported benchmarks
are median cycle counts of 10000 executions on a single
core of an Intel Core i7 11700K (Rocket Lake) CPU running
at 3600 MHz with TurboBoost and hyper-threading disabled.
The benchmarking machine is running Debian 6.1.76, and
we compiled our benchmarking code using GCC 12.2.

For each primitive, the leftmost ("plain") cycle count
is the baseline CT implementation without any Spectre
protections. As a first step ("+SSBD"), we set the SSBD
CPU flag to protect against Spectre v4 attacks. In a next step
("+SSBD+v1"), we additionally add the selSLH protections
against Spectre v1 as described in [9]. Finally, we report
cycle counts with the full protections as described in this
paper ("+SSBD+v1+RSB").

We see that for the symmetric primitives, i.e., ChaCha20,
Poly1305, and XSalsa20Poly1305, the overhead for full
Spectre protection is solidly below 1% when processing
sufficiently long messages. The rather large overhead for
short messages is due to the fixed cost of the initial *lfence*;
this is consistent with the observations reported in [9].

For the elliptic-curve Diffie-Hellman key exchange
X25519 [17] we see a slightly larger overhead, which is
almost entirely due to Spectre-v4 protections, i.e., setting the
SSBD flag. This is not surprising, because the active data set
in the speed-critical main loop of X25519 is considerably
larger than in the symmetric primitives. The main loop thus
involves more loads and stores that potentially benefit from
speculative store bypass and may thus be slowed down by
SSBD.

The most interesting measurements are those for Ky-
ber512 and Kyber768. Kyber is the most complex scheme
in our benchmarks in terms of code size, number of function
calls, and size of the active data set throughout the speed-
critical computations. Consequently, it is not surprising to
see a slightly higher overhead from Spectre protections in
Kyber than, e.g., X25519. As explained above, given that
the generation of a 3 × 3 matrix in Kyber768 does not
vectorize quite as straightforwardly as the generation of

a 2 × 2 matrix in Kyber512, it is also expected that the
overhead for Kyber768 is higher than for Kyber512. The
keypair operation is surprising: it has the smallest overhead
in Kyber512 but the largest in Kyber768.

9. Related work

**Return tables in optimizing compilers.** Calder and Grunwald [19] show that return tables can improve performance in object-oriented programs. Yang, Cooprider, and Regehr [43] show that return tables can reduce RAM usage in embedded code. Both transformations keep some indirect jumps, since their goal is efficiency, and thus are inadequate as mitigations against Spectre.

**ROP countermeasures.** Return-oriented programming (ROP) [37] is an exploitation technique that targets return instructions to force program execution to jump to arbitrary program points. In contrast to Spectre-RSB, ROP does not exploit speculative execution. There are many countermeasures against ROP. Our work is closely related to countermeasures that remove calls and returns [35], [31] and replace them with indirect jumps. Arthur *et al.* [10] is the closest since it introduces only *direct* branches. The main difference with our work is that we make this transformation resistant to speculative execution attacks and compatible with selective speculative load hardening. Other countermeasures harden return instructions by using return indirection or randomizing return addresses. Unfortunately, these transformations are ineffective in our scenario.

**Spectre countermeasures.** There is a large body of work that proposes countermeasures and verification approaches against Spectre. We refer the reader to two recent surveys for background [20], [22] and focus on closely related work.

Swivel [34] is a software-only compiler framework (with
a hardware-assisted variant) for WebAssembly that tackles
Spectre-PHT, Spectre-BTB, and Spectre-RSB. Similarly to
Venkman [38], it enforces a coarse-grained CFI under spec-
ulation by starting from a clean BTB and RSB and restrict-
ing jumps to the beginning of basic blocks. It implements
various mitigations on top of this, including disjoint mem-
ory regions for blocks (enforced with masking), a Spectre-
protected shadow stack (using either guard pages or Intel
CET), masking of addresses, and flushes of the BTB (on
every transition into and out of the sandbox). In contrast
to our work, Swivel incurs significant overhead and lacks
formal guarantees.

Serberus [33] is a comprehensive approach to protect
programs against all known Spectre attacks. Serberus uses
control flow integrity (CFI) protections to constrain the at-
tacker's power over speculative control flow, and a sequence
of program transformations to eliminate speculative leakage.
One main difference with our approach is that Serberus
requires hardware and operating system support. Specifi-
cally, Serberus derives its CFI protection from hardware
mechanisms, e.g., Intel CET [1] and DOIT [2], and requires
the operating system to perform RSB filling on context
<table><caption>TABLE 1: libjade benchmarks on Intel Core i7 11700K (most optimized implementation of each primitive). “plain”: cycles without any Spectre protections; “+SSBD”: with SSBD CPU flag set; “+SSBD+v1”: with SSBD CPU flag set and v1 countermeasures from [9]; “+SSBD+v1+RSB”: with full Spectre protection as described in this paper; “increase”: relative increase in CPU cycles between unprotected (“plain”) and fully protected (+SSBD+v1+RSB).</caption><thead><tr><th>Primitive</th><th>Impl.</th><th>Op.</th><th>plain</th><th>+SSBD</th><th>+SSBD+v1</th><th>+SSBD+v1+RSB</th><th>increase</th></tr></thead><tbody><tr><td rowspan="6">ChaCha20</td><td>avx2</td><td>128 B</td><td>344</td><td>344</td><td>398</td><td>398</td><td>15.70%</td></tr><tr><td>avx2</td><td>128 B xor</td><td>350</td><td>350</td><td>402</td><td>400</td><td>14.29%</td></tr><tr><td>avx2</td><td>1 KiB</td><td>1198</td><td>1202</td><td>1244</td><td>1246</td><td>4.01%</td></tr><tr><td>avx2</td><td>1 KiB xor</td><td>1208</td><td>1212</td><td>1248</td><td>1250</td><td>3.48%</td></tr><tr><td>avx2</td><td>16 KiB</td><td>19040</td><td>19052</td><td>19066</td><td>19068</td><td>0.15%</td></tr><tr><td>avx2</td><td>16 KiB xor</td><td>19070</td><td>19086</td><td>19096</td><td>19110</td><td>0.21%</td></tr><tr><td rowspan="6">Poly1305</td><td>avx2</td><td>128 B</td><td>138</td><td>142</td><td>182</td><td>180</td><td>30.43%</td></tr><tr><td>avx2</td><td>128 B verif</td><td>142</td><td>146</td><td>180</td><td>178</td><td>25.35%</td></tr><tr><td>avx2</td><td>1 KiB</td><td>670</td><td>672</td><td>720</td><td>718</td><td>7.16%</td></tr><tr><td>avx2</td><td>1 KiB verif</td><td>674</td><td>676</td><td>726</td><td>724</td><td>7.42%</td></tr><tr><td>avx2</td><td>16 KiB</td><td>8942</td><td>8948</td><td>8990</td><td>8986</td><td>0.49%</td></tr><tr><td>avx2</td><td>16 KiB verif</td><td>8942</td><td>8984</td><td>8984</td><td>8984</td><td>0.47%</td></tr><tr><td rowspan="6">XSalsa20Poly1305</td><td>avx2</td><td>128 B</td><td>1206</td><td>1212</td><td>1250</td><td>1246</td><td>3.32%</td></tr><tr><td>avx2</td><td>128 B open</td><td>1964</td><td>1970</td><td>2044</td><td>2046</td><td>4.18%</td></tr><tr><td>avx2</td><td>1 KiB</td><td>3140</td><td>3142</td><td>3190</td><td>3188</td><td>1.53%</td></tr><tr><td>avx2</td><td>1 KiB open</td><td>3900</td><td>3904</td><td>3988</td><td>3988</td><td>2.26%</td></tr><tr><td>avx2</td><td>16 KiB</td><td>32598</td><td>32574</td><td>32604</td><td>32602</td><td>0.01%</td></tr><tr><td>avx2</td><td>16 KiB open</td><td>33292</td><td>33274</td><td>33358</td><td>33362</td><td>0.21%</td></tr><tr><td>X25519</td><td>mulx</td><td>smult</td><td>102848</td><td>104150</td><td>104424</td><td>104428</td><td>1.54%</td></tr><tr><td rowspan="3">Kyber512</td><td>avx2</td><td>keypair</td><td>27676</td><td>28106</td><td>28040</td><td>28090</td><td>1.50%</td></tr><tr><td>avx2</td><td>enc</td><td>37050</td><td>38332</td><td>38876</td><td>38792</td><td>4.70%</td></tr><tr><td>avx2</td><td>dec</td><td>29302</td><td>30444</td><td>30590</td><td>30714</td><td>4.82%</td></tr><tr><td rowspan="3">Kyber768</td><td>avx2</td><td>keypair</td><td>43432</td><td>45708</td><td>45860</td><td>46548</td><td>7.17%</td></tr><tr><td>avx2</td><td>enc</td><td>57006</td><td>59316</td><td>60028</td><td>60674</td><td>6.43%</td></tr><tr><td>avx2</td><td>dec</td><td>46138</td><td>48418</td><td>48532</td><td>49294</td><td>6.84%</td></tr></tbody></table>

switches. Another main difference is that Serberus needs to use fences and to spill all function arguments as its primary protection mechanisms against speculative leaks, rather than selective speculative load hardening. This is reflected in the experimental evaluation, which reports a 21.3% overhead. In contrast, our approach uses hardware support only for Spectre-STL, and the overhead is minimal.

Retpoline [27] is a software-based countermeasure against Spectre-BTB—and some variants of Spectre-RSB—that replaces indirect jumps by return instructions. This mitigation leverages knowledge of how the RSB is implemented—as a LIFO buffer—to insert fences at the points where execution would continue if the predictor is wrong. Unfortunately, Wikner and Razavi [41] show that the assumptions that retpoline relies on are incorrect. Switchpoline [16] is a software-based countermeasure that replaces indirect jumps with direct ones, and a JIT compiler in some cases. Although Switchpoline targets Spectre-BTB in ARM, the transformation is very similar to ours. A critical difference between Switchpoline and our approach is that they do not consider how to combine their transformation with efficient countermeasures to protect programs. Furthermore, our proof shows that return tables introduce leakage, which needs mitigation.

**Other attacks and countermeasures.** There are many micro-architectural attacks beyond Spectre, see e.g., [40], [42], [24]. There exist initial efforts to develop formal foundations, verification techniques and countermeasures against these attacks, see e.g., [25]. Extending our approach to integrate these attacks and countermeasures is an exciting direction for future work.

## 10. Limitations

One limitation of our approach is that it applies only to full programs, because an (unprotected) external function call can exploit RSB to bypass protections. This limitation is common to other approaches, including Serberus [33], Switchpoline [16], Swivel [34], and Venkman [38].

Another limitation of our approach is that it does not account for declassification. We are confident that our results extend with declassification, at the cost of switching from speculative constant-time to relative speculative constant-time. In the future, we hope to leverage a formalization of the type system in Coq to extend our results to declassification.

## 11. Conclusion

We have proposed an approach to protect Spectre programs against all known forms of Spectre attacks. An important direction for future work is to reduce the Trusted Computing Base of our extension by using the formalization presented in this work to prove in Coq that the Jasmin type
system is sound, the return table insertion pass is correct, and
the Jasmin compiler preserves speculative constant-time.

Our approach is currently limited to Jasmin programs.
A pragmatic solution to carry our techniques to main-
stream languages would be to instrument existing compil-
ers with a pass for return table instructions and to de-
velop assembly-level type systems for checking speculative
constant-timeness.

Acknowledgments

This research was supported an ARC Discovery Early
Career Researcher Award (project number DE200101577);
an ARC Discovery Project (project number DP210102670);
by Deutsche Forschungsgemeinschaft (DFG, German re-
search Foundation) as part of the Excellence Strategy of the
German Federal and State Governments – EXC 2092 CASA
- 390781972; by the European Commission through the ERC
Starting Grant 805031 (EPOQUE); by the German Federal
Ministry of Education and Research (BMBF) in the course
of the 6GEM research hub under grant number 16KISK038;
by the *Agence Nationale de la Recherche* (French National
Research Agency) as part of the France 2030 programme –
ANR-22-PECY-0006. Author Peter Schwabe is a member of
the advisory boards of Bitmark Inc., PQShield, Neutrality,
and SciEngines.

References

[1] https://www.intel.com/content/www/us/en/developer/articles/
    technical/technical-look-control-flow-enforcement-technology.html.

[2] https://www.intel.com/content/www/us/en/developer/articles/
technical/software-security-guidance/best-practices/data-operand-
independent-timing-isa-guidance.html.

[3] "Security analysis of AMD predictive store forwarding," AMD, Tech. Rep., 2021, https://www.amd.com/system/files/documents/security-analysis-predictive-store-forwarding.pdf.

[4] J. B. Almeida, M. Barbosa, G. Barthe, A. Blot, B. Grégoire, V. Laporte, T. Oliveira, H. Pacheco, B. Schmidt, and P. Strub, "Jasmin: High-assurance and high-speed cryptography," in *ACM CCS*, 2017, pp. 1807–1823, https://doi.org/10.1145/3133956.3134078.

[5] J. B. Almeida, M. Barbosa, G. Barthe, B. Grégoire, V. Laporte, J. Léchenet, T. Oliveira, H. Pacheco, M. Quaresma, P. Schwabe, A. Séré, and P. Strub, "Formally verifying Kyber episode IV: implementation correctness," *IACR Trans. Cryptogr. Hardw. Embed. Syst.*, vol. 2023, no. 3, pp. 164–193, 2023, https://doi.org/10.4658/tches.v2023.i3.164-193.

[6] J. B. Almeida, C. Baritel-Ruet, M. Barbosa, G. Barthe, F. Dupressoir, B. Grégoire, V. Laporte, T. Oliveira, A. Stoughton, and P. Strub, "Machine-checked proofs for cryptographic standards: Indifferentiability of sponge and secure high-assurance implementations of SHA-3," in *ACM CCS*, L. Cavallaro, J. Kinder, X. Wang, and J. Katz, Eds., 2019, pp. 1607–1622, https://doi.org/10.1145/3319535.3363211.

[7] J. B. Almeida, M. Barbosa, G. Barthe, B. Grégoire, A. Koutsos, V. Laporte, T. Oliveira, and P.-Y. Strub, "The last mile: High-assurance and high-speed cryptographic implementations," in *IEEE S&P*, 2020, pp. 965–982, https://doi.org/10.1109/SP40000.2020.00028.

[8] J. B. Almeida, S. A. Olmos, M. Barbosa, G. Barthe, F. Dupres-
soir, B. Grégoire, V. Laporte, J.-C. Léchenet, C. Low, T. Oliveira,
H. Pacheco, M. Quaresma, P. Schwabe, and P.-Y. Strub, "Formally
verifying Kyber episode V: Machine-checked IND-CCA security and
correctness of ML-KEM in EasyCrypt," in *IACR CRYPTO*, 2024, p.
to appear, https://eprint.iacr.org/2024/843.

[9] B. Ammanaghatta Shivakumar, G. Barthe, B. Grégoire, V. Laporte, T. Oliveira, S. Priya, P. Schwabe, and L. Tabary-Maujean, "Typing high-speed cryptography against Spectre v1," in *IEEE S&P*, 2023, pp. 1094–1111, https://doi.org/10.1109/SP46215.2023.10179418.

[10] W. Arthur, B. Mehne, R. Das, and T. Austin, "Getting in control of your control flow with control-data isolation," in *IEEE/ACM CGO*, 2015, pp. 79–90, https://ieeexplore.ieee.org/abstract/document/7054189.

[11] E. Barberis, P. Frigo, M. Muench, H. Bos, and C. Giuffrida, "Branch history injection: On the effectiveness of hardware mitigations against cross-privilege Spectre-v2 attacks," in *USENIX Security*, 2022, pp. 971–988, https://www.usenix.org/conference/UsenixSecurity22/presentation/barberis.

[12] M. Barbosa, G. Barthe, K. Bhargavan, B. Blanchet, C. Cremers, K. Liao, and B. Parno, "SoK: Computer-aided cryptography," in *IEEE S&P*, 2021, pp. 777–795, https://doi.org/10.1109/SP40001.2021.00008.

[13] M. Barbosa, G. Barthe, C. Doczkal, J. Don, S. Fehr, B. Grégoire, Y. Huang, A. Hülsing, Y. Lee, and X. Wu, "Fixing and mechanizing the security proof of Fiat-Shamir with aborts and Dilithium," in *IACR CRYPTO*, 2023, pp. 358–389, https://doi.org/10.1007/978-3-031-38554-4_12.

[14] M. Barbosa, F. Dupressoir, B. Grégoire, A. Hülsing, M. Meijers, and P. Strub, "Machine-checked security for XMSS as in RFC 8391 and SPHINCS+," in *IACR CRYPTO*, 2023, pp. 421–454, https://doi.org/10.1007/978-3-031-38554-4_14.

[15] G. Barthe, B. Grégoire, V. Laporte, and S. Priya, "Structured leakage and applications to cryptographic constant-time and cost," in *ACM CCS*, 2021, pp. 462–476, https://doi.org/10.1145/3460120.3484761.

[16] M. Bauer, L. Hetterich, C. Rossow, and M. Schwarz, "Switch-
poline: A software mitigation for Spectre-BTB and Spectre-BHB
on ARMv8," in *ACM AsiaCCS*, 2024, https://misc0110.net/files/
switchpoline_asiaccs24.pdf.

[17] D. J. Bernstein, "Curve25519: new Diffie-Hellman speed records," in *IACR PKC*, 2006, pp. 207–228, https://cr.yp.to/papers.html#curve25519.

[18] J. W. Bos, L. Ducas, E. Kiltz, T. Lepoint, V. Lyubashevsky, J. M. Schanck, P. Schwabe, G. Seiler, and D. Stehlé, "CRYSTALS-Kyber: A CCA-secure module-lattice-based KEM," in *IEEE EuroS&P*, 2018, pp. 353–367, https://doi.org/10.1109/EuroSP.2018.00032.

[19] B. Calder and D. Grunwald, "Reducing indirect function call over-
head in C++ programs," in *ACM POPL*, 1994, pp. 397–408, https://dl.acm.org/doi/10.1145/174675.177973.

[20] C. Canella, J. V. Bulck, M. Schwarz, F. Piessens, D. Evtushkin, and D. Gruss, "A systematic evaluation of transient execution attacks and defenses," in *USENIX Security*, 2019, pp. 249–266, https://www.usenix.org/conference/usenixsecurity19/presentation/canella.

[21] C. Carruth, "Speculative load hardening – a Spectre variant #1 mitigation technique," *LLVM* documentation, https://llvm.org/docs/SpeculativeLoadHardening.html.

[22] S. Cauligi, C. Disselkoen, D. Moghimi, G. Barthe, and D. Stefan, "SoK: Practical foundations for software spectre defenses," in *IEEE S&P*, 2022, pp. 666–680, https://doi.org/10.1109/SP46214.2022.9833707.

[23] S. Cauligi, C. Disselkoen, K. von Gleissenthall, D. M. Tullsen, D. Stefan, T. Rezk, and G. Barthe, "Constant-time foundations for the new Spectre era," in *ACM PLDI*, 2020, pp. 913–926, https://doi.org/10.1145/3385412.3385970.

[24] B. Chen, Y. Wang, P. Shome, C. W. Fletcher, D. Kohlbrenner, R. Paccagnella, and D. Genkin, "GoFetch: Breaking constant-time cryptographic implementations using data memory-dependent prefetchers," in *USENIX Security*, 2024, p. to appear, https://gofetch fail/files/gofetch.pdf.
[25] M. Flanders, R. K. Sharma, A. E. Michael, D. Grossman, and D. Kohlbrenner, "Avoiding instruction-centric microarchitectural timing channels via binary-code transformations," in *ACM ASPLOS*, 2024, pp. 120–136, https://doi.org/10.1145/3620665.3640400.

[26] G. Gilles Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, "Computer-aided security proofs for the working cryptographer," in *IACR CRYPTO*, 2011, pp. 71–90, https://iacr.org/archive/crypto2011/68410071/68410071.pdf.

[27] Intel Labs, "Retpoline: a software construct for preventing branch-target-injection," 2018, https://www.intel.com/content/dam/develop/external/us/en/documents/retpoline-a-branch-target-injection-mitigation.pdf.

[28] J. Jancar, M. Fourné, D. D. A. Braga, M. Sabt, P. Schwabe, G. Barthe, P.-A. Fouque, and Y. Acar, ""They're not that hard to mitigate": What cryptographic library developers think about timing attacks," in *IEEE S&P*, 2022, pp. 632–649, https://eprint.iacr.org/2021/1650.

[29] P. Kocher, J. Horn, A. Fogh, D. Genkin, D. Gruss, W. Haas, M. Hamburg, M. Lipp, S. Mangard, T. Prescher, M. Schwarz, and Y. Yarom, "Spectre attacks: Exploiting speculative execution," in *IEEE S&P*, 2019, pp. 1–19, https://spectreatattack.com/spectre.pdf.

[30] E. M. Koruyeh, K. N. Khasawneh, C. Song, and N. Abu-Ghazaleh, "Spectre returns! speculation attacks using the return stack buffer," in *USENIX WOOT*, 2018, https://www.usenix.org/conference/woot18/presentation/koruyeh.

[31] J. Li, Z. Wang, X. Jiang, M. C. Grace, and S. Bahram, "Defeating return-oriented rootkits with "Return-Less" kernels," in *ACM EuroSys*, 2010, pp. 195–208, https://doi.org/10.1145/1755913.1755934.

[32] G. Maisuradze and C. Rossow, "ret2spec: Speculative execution using return stack buffers," in *ACM CCS*, 2018, pp. 2109–2122, https://dl.acm.org/doi/10.1145/3243734.3243761.

[33] N. Mosier, H. Nemati, J. C. Mitchell, and C. Trippel, "Server-: Protecting cryptographic code from spectres at compile-time," in *IEEE S&P*, 2024, https://doi.ieeecomputersociety.org/10.1109/SP54263.2024.00048.

[34] S. Narayan, C. Disselkoen, D. Moghimi, S. Cauligi, E. Johnson, Z. Gang, A. Vahldiek-Oberwagner, R. Sahita, H. Shacham, D. Tullsen, and D. Stefan, "Swivel: Hardening WebAssembly against Spectre," in *USENIX Security*, 2021, pp. 1433–1450, https://www.usenix.org/conference/usenixsecurity21/presentation/narayan.

[35] K. Onarlioglu, L. Bilge, A. Lanzi, D. Balzarotti, and E. Kirda, "G-free: defeating return-oriented programming through gadget-less binaries," in *ACM ACSAC*, 2010, pp. 49–58, https://doi.org/10.1145/1920261.1920269.

[36] R. Roemer, E. Buchanan, H. Shacham, and S. Savage, "Return-oriented programming: Systems, languages, and applications," *ACM Transactions on Information and System Security*, vol. 15, no. 1, pp. 2:1–2:34, 2012, https://dl.acm.org/doi/10.1145/2133375.2133377.

[37] H. Shacham, "The geometry of innocent flesh on the bone: return-into-libc without function calls (on the x86)," in *ACM CCS*, 2007, pp. 552–561, https://doi.org/10.1145/1315245.1315313.

[38] Z. Shen, J. Zhou, D. Ojha, and J. Criswell, "Restricting control flow during speculative execution with Venkman," https://arxiv.org/abs/1903.10651v1, 2019.

[39] B. A. Shivakumar, J. Barnes, G. Barthe, S. Cauligi, C. Chuengsatian-sup, D. Genkin, S. O'Connell, P. Schwabe, R. Q. Sim, and Y. Yarom, "Spectre declassified: Reading from the right place at the wrong time," in *IEEE S&P*, 2023, pp. 1753–1770, https://doi.org/10.1109/SP46215.2023.10179355.

[40] J. R. S. Vicarte, P. Shome, N. Nayak, C. Trippel, A. Morrison, D. Kohlbrenner, and C. W. Fletcher, "Opening Pandora's box: A systematic study of new ways microarchitecture can leak private data," in *ACM/IEEE ISCA 2021*, 2021, pp. 347–360, https://doi.org/10.1109/ISCA52012.2021.00035.

[41] J. Wikner and K. Razavi, "RETBLEED: Arbitrary speculative code execution with return instructions," in *USENIX Security*, 2022, pp. 3825–3842, https://www.usenix.org/conference/usenixsecurity22/presentation/wikner.

[42] J. Wikner, D. Trujillo, and K. Razavi, "Phantom: Exploiting decoder-detectable mispredictions," in *IEEE/ACM MICRO*, 2023, pp. 49–61, https://doi.org/10.1145/3613424.3614275.

[43] X. Yang, N. Cooprider, and J. Regehr, "Eliminating the call stack to save RAM," in *ACM LCTES*, 2009, pp. 60–69, https://doi.org/10.1145/1542452.1542461.

# Appendix

## 1. Source language and soundness

This appendix gives precise definitions of the source language, semantics, type system, and soundness proof discussed in the main paper.

**Continuations.** Figure 11 defines the continuations $C(f)$ of a function $f$ as the set of code that follows a call to $f$, along with a boolean that indicates whether the MSF gets updated.

**Source semantics.** Figure 12 presents the rest of the semantics. For speculative returns, that is the S-RET rule, we pin down the whole continuation $(cont, f, b)$ in the directive, instead of just the code, because *cont* might come from different program points, with different MSF updates. We require $cs \neq (f, cont) :: cs'$ simply to make the semantics deterministic: our approach does not need determinism, but it makes presenting the rules and proofs easier.

**Polymorphism.** Our type system has polymorphism over security types to allow function calls in contexts where variables have different security types. It is critical in our model where variables and memory are global since it is unrealistic that calling a function requires that all registers and memory locations have some fixed security type. Nevertheless, we need some care when a function call occurs in different contexts since we do not know to which call site it will return. We need to distinguish between sequential and speculative types, as we do not want to allow instantiating as public a register that may, due to misspeculation, contain secret data.

Recall the example in Figure 1a. If we assigned the type $\{x : \langle\alpha, \beta\rangle\} \to \{x : \langle\alpha, \beta\rangle\}$ to *id*, with a polymorphic variable in the speculative component, then we would be able to type this program (by choosing as instantiations $\{\alpha, \beta \to L\}$ for the first call site and $\{\alpha, \beta \to H\}$ for the second). What we need is to ensure that under speculation, the output type of the function is the maximum of all possible instantiations we need for the program: $\langle\alpha, \max_{\theta \in p}\{\theta(\beta)\}\rangle$. Since we only have two levels, this restriction means that if at *any* call site we need to instantiate *x* as speculatively secret, we need to assume that it could be secret in *all* return sites. Conversely, if we guarantee that at *all* call sites *x* is speculatively public, we can assume this at every return site. In this way, the example is no longer typable: the type must be of the form $\{x : \langle\alpha, t\rangle\} \to \{x : \langle\alpha', t'\rangle\}$ where $\alpha \le \alpha'$ and $t \le t'$. We
$$
\begin{align*}
C \oplus c &:= \{ (\text{cont}; c, b) \mid (\text{cont}, b) \in C \} \\
C_i(f, i) &:= \begin{cases}
C_c(f, c_\top) \cup C_c(f, c_\perp) & \text{if } i \text{ is if } e \text{ then } c_\top \text{ else } c_\perp \\
C_c(f, c) \oplus i & \text{if } i \text{ is while } e \text{ do } c \\
\{ \nil, b \} & \text{if } i \text{ is call}_b f \\
\emptyset & \text{otherwise}
\end{cases} \\
C_c(f, c) &:= \begin{cases}
\emptyset & \text{if } c \text{ is } \nil \\
C_i(f, i) \oplus c' \cup C_c(f, c') & \text{if } c \text{ is } i; c'
\end{cases} \\
C(\text{callee}) &:= \bigcup_{(\text{caller}, c) \in p} \{ (\text{cont}, \text{caller}, b) \mid (\text{cont}, b) \in C_c(\text{callee}, c) \}
\end{align*}
$$

Figure 11: Continuations. Here $C_i(f, i)$, where $f$ is a function name and $i$ an instruction, returns a set of pairs: the code that follows (in the execution, not syntactically) each function call to $f$ in $i$ and the boolean argument of the call. The operation $\oplus$ takes a set of code and appends its second argument to each element in the set. The definition of $C_c(f, c)$ is analogous to the one of $C_i(f, i)$, where $c$ is code. Finally, $C(f)$ aggregates all the continuations of the whole program, adding the name of the caller.

$$
\begin{array}{l@{\qquad}l}
\frac{\langle x = e; c, f, cs, \rho, \mu, ms \rangle \xrightarrow{\bullet} \langle c, f, cs, \rho[x \leftarrow \llbracket e \rrbracket_\rho], \mu, ms \rangle}{\text{ASSIGN}} & \\
\frac{\llbracket e \rrbracket_\rho = i \quad 0 \le i < |a|}{\langle a[e] = x; c, f, cs, \rho, \mu, ms \rangle \xrightarrow{\text{addr } a \; i \atop \text{mem } b \; j} \langle c, f, cs, \rho, \mu[(a, i) \leftarrow \rho(x)], ms \rangle} & \text{N-STORE} \\
\frac{\llbracket e \rrbracket_\rho = i \quad \neg (0 \le i < |a|) \quad 0 \le j < |b|}{\langle a[e] = x; c, f, cs, \rho, \mu, \top \rangle \xrightarrow{\text{addr } a \; i \atop \text{mem } b \; j} \langle c, f, cs, \rho, \mu[(b, j) \leftarrow \rho(x)], \top \rangle} & \text{S-STORE} \\
\frac{\llbracket e \rrbracket_\rho = b' \quad c' = \text{if } b \text{ then } c_0; \text{while } e \text{ do } c_0; c \text{ else } c}{\langle \text{while } e \text{ do } c_0; c, f, cs, \rho, \mu, ms \rangle \xrightarrow{\text{branch } b' \atop \text{force } b} \langle c', f, cs, \rho, \mu, ms \lor (b \neq b') \rangle} & \text{WHILE} \\
\frac{\langle \text{init\_msf}(); c, f, cs, \rho, \mu, \perp \rangle \xrightarrow{\bullet} \langle c, f, cs, \rho[msf \leftarrow \text{NOMASK}], \mu, \perp \rangle}{\text{INIT-MSF}} & \\
\frac{v = \text{if } \llbracket e \rrbracket_\rho \text{ then } \rho(msf) \text{ else } \text{MASK}}{\langle \text{update\_msf}(e); c, f, cs, \rho, \mu, ms \rangle \xrightarrow{\bullet} \langle c, f, cs, \rho[msf \leftarrow v], \mu, ms \rangle} & \text{UPDATE-MSF}
\end{array}
$$

<caption>Figure 12: Rest of the semantics.</caption>

need $t'$ to be L for the first call site to be typable since we leak $x$ after it, but we need $t'$ to be H for the second call site to be typable since it is after the assignment of a secret value to $x$. There is no way of typing this example $\mathcal{P}$. We can type this example where we protect $x$ after the first call site because of subtyping: we can choose $\langle \alpha, H \rangle \rightarrow \langle \alpha, H \rangle$ as the type of `id` and instantiate first with L and then with H $\mathcal{P}$. Doing so means that $x$ is speculatively H after the first call site, but the protect ensures we do not leak any secrets.

**Soundness.** To prove that typable programs are speculatively constant-time, we show that pairs of single step executions preserve a property that includes equality of observations. This property entails the code of the machines and their call stack being typable, the MSF being synchronized with its type, and the machines being indistinguishable. Figure 13 presents the formal definitions of these properties. The precise statement of the lemma is as follows

**Lemma 2** (Single-step soundness $\mathcal{P}$). If two machines $m_1$ and $m_2$ step under directive $d$ to $m'_1$ and $m'_2$ respectively, are typable under $(\Sigma, \Gamma)$, are synchronized with $\Sigma$, and are indistinguishable under $\Gamma$, then the observation of both steps are the same, and the resulting machines are typable, synchronized, and indistinguishable. That is, we will prove that there exist $\Sigma'$, and $\Gamma'$ such that

$$
\begin{align*}
m_1 &\xrightarrow{o_1} m'_1 & o_1 = o_2 \\
m_2 &\xrightarrow{o_2} m'_2 & \wedge \Sigma', \Gamma' \vdash m'_1 \\
\Sigma, \Gamma \vdash m_1 &\implies \wedge \operatorname{synced}(\Sigma', \rho'_1, ms'_1) & \\
\operatorname{synced}(\Sigma, \rho_1, ms_1) &\implies \wedge \operatorname{synced}(\Sigma', \rho'_2, ms'_2) & \\
\operatorname{synced}(\Sigma, \rho_2, ms_2) &\implies \wedge m'_1 = \Gamma' m'_2 & \\
m_1 = \Gamma m_2 & &
\end{align*}
$$

We show an analogous property for multi-step execu-
<figure><img src="image_6.png" /><figcaption>Figure 16: Compilation relation.</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>Figure 17: Directive and observation transformers. The transformer are undefined in the cases not shown here.</figcaption></figure>

instruction (at position $\ell$) and the target directive $d$. The first four cases say that the source machine skips a step when the target executes jumps, return address stores, MSF updates after a function call, and entries of the return table that are not taken. The next two cases are when an entry of the return table entry is taken, and it produces a return $c g b$ directive, which is uniquely identified by $(f, c, g, b) \leftrightarrow_{\mathcal{L}} \ell_r$. In all other cases, the source and target machines behave identically.

On the other hand, the transformer for observations $T_{\text{Obs}}(\ell, \rho^*, O)$ determines the observation of the target machine given the current instruction (at position $\ell$), the values of the return addresses, and the source observations. For the first four cases, which are intermediate steps in the

compilation of a source instruction, it predicts that the target observation will be $\bullet$. The next case is an intermediate jump in a return table: it uses the value of the return addresses to determine the observation of this comparison. We are able to provide the values of the return addresses because they are uniquely determined from the public part of the initial state and the directives executed until now. Similarly to the directive transformer, in all other cases, the source and target machines behave identically.

In order to prove Theorem 2, we need to extend the transformers to multi-step executions. This is straightforward if we note that from the current instruction and directive we can predict the next instruction: it is the following label, unless it is a conditional jump, in which case the directive
is force $b$ and the label $l_b$ follows.