Detecting speculative leaks with compositional semantics

\caption{The Reflexive-transitive-closure of $\xrightarrow{}$ and behaviour of $\mu$ \textsc{Asm} programs.}
\label{fig:uasm-non-spec:beheavior}

Figure 4 presents the rules for deriving the trace of observations associated with an execution according to the non-speculative semantics $\xrightarrow{}$. We denote by $\left(\langle p,\sigma \rangle\right)\mathsf{ghost}_{\mathit{NS}}\overline{\tau}$ the trace $\overline{\tau}$ associated with executing the program $p$ starting from an initial configuration $\sigma$ until reaching a final configuration $\sigma'$ (the section) using the reflexive-transitive-closure $\Downarrow$ of the non-speculative semantics $\xrightarrow{}$ (the section and). To simplify our notation, we introduce the shorthand $\mathit{Beh}_{NS}(p, \sigma)$ to denote the specific trace $\tau$ generated by this execution. Finally, the *non-speculative behaviour* $\mathit{Beh}_{NS}(p)$ of a program $p$ is the set of all traces generated by all possible initial states for program $p$ (the section).

## 4. Modelling Speculative Execution

In this section, we propose a general approach for modeling, at program-level, the effects of speculative execution induced by different kinds of speculation mechanisms. For this, we extend a non-speculative (i.e., architectural) semantics to a *speculative semantics* that is equipped with a *prediction oracle* (which captures how predictions are made) used to explore mispredicted paths. For this, we first informally explain the core concepts behind our model (Section 4.1). Then, we formalize prediction oracles and prediction histories (Section 4.2). We conclude by presenting the states and the evaluation relation associated with the (speculative) oracle semantics (Section 4.3).

We remark that here we present only a general template for defining the oracle semantics. Such template needs to be instantiated to capture specific speculation mechanisms, and we do so in Section 6 for a large class of mechanisms. In the following, we indicate a speculative semantics as $\mathsf{ghost}_{x}$, where the metavariable $x$ is used as a placeholder indicating the type of speculation mechanism.

### 4.1 High-level Description

The core idea behind our approach is to extend a non-speculative semantics—like the one from Section 3—to a *speculative semantics* that captures the effect of speculatively executed instructions. For this, our speculative semantics is parametric in two components: (1) a set $\mathit{instr}_{\mathsf{ghost}}$ of $\mu$ $\textsc{Asm}$ instructions that might trigger speculation, and (2) a *prediction oracle* ${\mathcal{O}}$ capturing the prediction strategy associated with the modeled speculation mechanism.

In a nutshell, our speculative semantics works as follows. All instructions not in $\mathit{instr}_{\mathsf{ghost}}$ are executed as in the standard non-speculative semantics. In contrast, whenever an instruction in $\mathit{instr}_{\mathsf{ghost}}$ is reached, the oracle ${\mathcal{O}}$ is queried to obtain the next predicted state, which records the effects of the prediction. For instance, for branch prediction, the program counter in the predicted state is updated to decide which of the two branches to execute speculatively.

To enable a subsequent rollback in case of a misprediction, a snapshot of the current program state is taken, before starting a *speculative transaction*. In this speculative transaction, the program is executed speculatively starting from the predicted state for a bounded number $w$ of computation steps, called the speculative window. To abstract from the complexity of estimating the actual speculative window (which depends on the details of a CPU's microarchitecture), in our model the speculation window $w$ is also provided by the prediction oracle.

At the end of a speculative transaction, the correctness of the prediction is evaluated:

(1) If the prediction was *correct*, the transaction is committed and the computation continues using the current configuration. (2) In contrast, if the prediction was *incorrect*, the transaction is aborted, the original configuration is restored, and the computation continues on the correct branch.

In the following sections, we formalize the behavior intuitively described above in the general structure of the *speculative oracle semantics*, whereas in Section 6 we will present instantiations of the oracle semantics (and $\mathit{instr}_{\mathsf{ghost}}$) for different speculation mechanisms.

### 4.2 Prediction Oracles

In our semantics, the prediction oracle serves two distinct purposes: (1) predicting the next program state (i.e., modeling how the speculation mechanism works), and (2) determining the length of the speculative transactions (i.e., determining for how long the speculative execution lasts). Our notion of prediction oracle is general enough to account for both control-flow speculation, such as branch prediction, and data-flow speculation, such as value prediction.

A *prediction oracle* ${\mathcal{O}}$ is a partial function that takes as input a program $p$, a prediction history $h$, and the current program state $\sigma$ such that $p(\sigma(\mathbf{pc}))$ is an instruction triggering speculation, i.e., $p(\sigma(\mathbf{pc})) \in \mathit{instr}_{\mathsf{ghost}}$. The prediction oracle returns as output a triple $\langle \delta, w, \tau \rangle$, where $\delta \in \mathit{Conf}$ is a partial configuration indicating the predicted values, $w \in \mathbb{N}$ represents the speculative transaction's length, and $\tau$ is a (potentially empty) observation. One can then join the returned partial configuration $\delta$ with the current configuration $\sigma$, indicated as $\sigma \uplus \delta$, to obtain the next speculative configuration. Informally, $\sigma \uplus \delta$ simply updates $\sigma$ with the values in $\delta$ at the same places (registers, memory locations, etc). We say that a prediction oracle ${\mathcal{O}}$ has *speculative window at most* $w$ if the length of the transactions generated by its predictions is at most $w$, i.e., for all programs $p$, histories $h$, and configurations $\sigma$, ${\mathcal{O}}(p, h, \sigma) = \langle \delta,w', \tau \rangle$, for some $\delta, \tau$ such that $w' \leq w$.

Taking into account the prediction history enables us to capture history-based predictors, a general class of predictors that base their decisions on past behaviors. Formally, a *prediction history* is a sequence of triples $\langle \ell, \mathit{id}, \delta \rangle$, where $\ell \in \mathit{Vals}$ is the label of an instruction related to speculation, $\mathit{id}\in \mathbb{N}$ is the unique identifier of the transaction that triggered speculation, and $\delta$ are the predicted values.

Next, we describe in detail the rules formalizing the oracle semantics, which capture the intuition from Section 4.1 and are depicted in Figure 5. Whenever none of the speculative instances in the current state has a speculative window of $0$ or is stuck (denoted by $\mathit{canStep}(\overline{\Psi}_{x})$), the computation proceeds by doing one step for the instance at the top of the stack (the section) and by updating the speculative window of the other instances. In particular, if the instruction to be executed in the topmost instance is a speculative barrier, then all speculative windows are set to 0 ($\overline{\Psi}_{x}'' = \mathit{zeroes}(\overline{\Psi}_{x})$), otherwise all windows are decremented by $1$ ($\overline{\Psi}_{x}'' = \mathit{decr}(\overline{\Psi}_{x})$).

In the topmost speculative instance, instructions that do not trigger speculation (i.e., they are not in $\mathit{instr}_{\mathsf{ghost}}$) are executed following the non-speculative semantics while also decrementing the current speculative window by 1 (the section). Speculation barriers are handled similarly except for setting the speculative window in the topmost instance to $0$ (the section). Finally, the section handles instructions that trigger speculation (i.e., those that belong to $\mathit{instr}_{\mathsf{ghost}}$). In this case, the oracle is queried to obtain the prediction $\delta$ and the next speculative window $w$, and a new speculative instance (starting from the predicted state $\sigma \uplus \delta$ and with an updated prediction history $h'$) is pushed on top of the stack to start the new speculative transaction. This fresh speculative instance is decorated with the original program state $\sigma$ and with the predicted values $\delta$, which will later on be used to determine whether the transaction should be committed or rolled back. The rule also appends the observation $\textcolor{RoyalBlue}{\mathtt{start}}_{x}\ n$ to the trace to record the beginning of a speculative transaction.

A speculative transaction must be finalized (committed or rolled back) whenever its speculation window reaches $0$ or the execution cannot proceed further. We refer to the latter case as the instance being 'stuck', formally indicated by the judgment $p, \sigma' \vdash \text{fin}$. This judgment holds whenever the current instruction is undefined, i.e., $p(sigma(\mathbf{pc})) = \bot$ (see). To determine whether to commit or rollback, the semantics inspects the snapshot state $\sigma$ and prediction $\delta$ that decorate the instance $\Psi_{x}^{\langle \sigma,\delta \rangle}$ whose window has reached $0$.

- If the prediction was *correct* (i.e., doing one step from $\sigma$ results indeed in the predicted state $\sigma \uplus \delta$), the transaction is committed and the computation continues using the current configuration (the section).
- If the prediction was *incorrect* (i.e., doing one step from $\sigma$ produces a state different from the predicted state $\sigma \uplus \delta$), the transaction is aborted and the computation continues on the correct branch (the section).

Thus, committing and rolling back speculative transactions happen along the stack of states. Rolling back deletes all the instances above the rolled back instance, whereas committing updates the configuration, the counter, the prediction history $h$ and additional data tracked by the semantics of the instance below and the committed instance is deleted. the section and also record the end of speculative transactions on the trace with the $\textcolor{RoyalBlue}{\mathtt{commit}}_{x}\ n$ and $\textcolor{RoyalBlue}{\mathtt{rlb}}_{x}\ n$ observations respectively.

Analogously to the non-speculative case, the behaviour $\mathit{Beh}^{{\mathcal{O}}}_{x}(p)$ of a program $p$ under the oracle semantics is the set of all traces generated from an initial state until termination.

**Non-Speculative Consistency** Fundamentally, a valid speculative semantics must preserve the program's architectural behaviour. Speculation should only introduce observational side-effects during transient execution, without altering the program's non-speculative behaviour. We formalize this correctness requirement in Property 4, stating that the standard non-speculative behaviour can be exactly recovered from the oracle behaviour by applying the non-speculative projection $\mathord{\upharpoonright_{ns}}$, which (1) removes from the trace $\tau$ any sub-trace enclosed between $\textcolor{RoyalBlue}{\mathtt{start}}_{x}\ n$ and $\textcolor{RoyalBlue}{\mathtt{rlb}}_{x}\ n$ for some $n$, and then (2) drops all remaining $\textcolor{RoyalBlue}{\mathtt{start}}_{x}\ n$ and $\textcolor{RoyalBlue}{\mathtt{commit}}_{x}\ n$ observations. In Section 6, we prove that all our specualtive semantics instances satisfy Property 4.

• It mispredicts every time, hence its name. For every instruction that might trigger speculation (i.e., the instruction belongs to ${instr}_{\mathsf{ghost}}$), the always-mispredict semantics first speculatively explores all possible wrong paths for a bounded number of steps and then continues with the correct one. Thus, the semantics is not parametric in the prediction oracle.
• It initializes the length of every non-nested transaction to $w$, and the length of every nested transaction to the remaining length of its enclosing transaction, decremented by $1$.
• Upon executing instructions, only the remaining length of the innermost transaction is decremented.

\caption{Always-mispredict speculative semantics}\label{fig:am-rules}

**Formalization** The state $\Sigma_{x}$ of the AM semantics is a stack of speculative instances $\Phi_{x}$. As shown in all rules in Figure 6, reductions in the always-mispredict semantics happen only on top of the stack. Each instance $\Phi_{x}$ contains the program $p$, a counter $\mathit{ctr}$ that identifies the speculative transaction , a configuration $\sigma$, and the remaining speculation window $n$ describing the number of instructions that can still be executed speculatively (or $\bot$ when no speculation is happening). Depending on the specific speculation that is modelled, additional data is tracked (indicated with $\cdots$ in the rules). Throughout the paper, we fix the maximal speculation window, i.e., the maximum number of speculative instructions, to a global constant $\omega$.

• Oracle Overapproximation: $p{⊢}_x\text{SNI}\text{iff}\forall \mathcal{O}.p{⊢}_x^{\mathcal{O}}\text{SNI}$
• NS Consistency: ${Beh}_x^{\omega }(p){\upharpoonright }_{ns}={Beh}_{NS}(p)={Beh}_x^{\mathcal{O}}(p){\upharpoonright }_{ns}$
• Symbolic Consistency: ${Beh}_x^{\omega }(p)=\mu ({Beh}_x^{\mathcal{S}}(p))$

• ($\mathsf{ghost}$ is $WFSS$) $\mathsf{ghost}$
• ($\mathsf{ghost}$ is $WFSS$) $\mathsf{ghost}$
• ($\mathsf{ghost}$ is $WFSS$) $\mathsf{ghost}$
• ($\mathsf{ghost}$ is $WFSS$) $\mathsf{ghost}$
• ($\mathsf{ghost}$ is $WFSS$) $\mathsf{ghost}$

• (Confluence) Whenever ${\Sigma }_{xy}{\stackrel{\tau }{\to }}_{xy}{\Sigma }_{xy}^{\prime }$ and ${\Sigma }_{xy}{\stackrel{\tau }{\to }}_{xy}{\Sigma }_{xy}^{\prime \prime }$, then ${\Sigma }_{xy}^{\prime }={\Sigma }_{xy}^{\prime \prime }$.
• (Projection preservation) For all $p$, ${Beh}_x^{\omega }(p)={Beh}_{xy}^{\omega }((p)){\upharpoonright }_{xy}^x$ and ${Beh}_y^{\omega }(p)={Beh}_{xy}^{\omega }((p)){\upharpoonright }_{xy}^y$.
• (Relation preservation) If ${\Sigma }_{xy}{\approx }_{xy}{X}_{xy}$ and ${\Sigma }_{xy}{\stackrel{\overline{\tau }}{\to }}_{xy}^{\ast }{\Sigma }_{xy}^{\prime }$ then $X_{xy}{⇝}_{xy}^{{\mathcal{O}}_{xy}}{X}_{xy}^{\prime }$ and ${\Sigma }_{xy}^{\prime }{\approx }_{xy}{X}_{xy}^{\prime }$.
• (Symbolic preservation) If ${\Sigma }_{xy}^{\mathcal{S}}{\stackrel{{\tau }_{\mathcal{S}}}{\to }}_{xy}^{\mathcal{S}}{\Sigma }_{xy}^{{\mathcal{S}}^{\prime }}$ and $\mu {\Sigma }_{xy}^{\mathcal{S}}={\Sigma }_{xy}$, then there is ${\Sigma }_{xy}^{\prime }$ s.t. ${\Sigma }_{xy}{\stackrel{\mu ({\tau }_{\mathcal{S}})}{\to }}_{xy}{\Sigma }_{xy}^{\prime }$ and $\mu {\Sigma }_{xy}^{{\mathcal{S}}^{\prime }}={\Sigma }_{xy}^{\prime }$.

• Confluence (point 1) ensures that the non-determinism of the combined semantics (that non-deterministically delegates back to its sources) is not harmful. Consider the assignment in the theorem in. $\mathsf{ghost}$ can delegate to either $\mathsf{ghost}$ or $\mathsf{ghost}$ to reduce the assignment. If the combined semantics is confluent, then it does not matter which source rule executes the assignment in the theorem in, the semantics reaches the same state either way.
• Projection preservation (point 2) ensures that the combined semantics is not hiding or forgetting traces of its sources. Any observable emitted by a source semantics must be propagated to the combined one, this is also the reason why ${Obs}_{xy}$ is defined as the union of the source $Obs$.
• To explain relation preservation (point 3), we need to mention a technical detail: the state relation (denoted ${\approx }_{xy}$ and defined in our technical report) between the AM states (${\Sigma }_{xy}$) and the Oracle ones ($X_{xy}$). Intuitively, two states are related if they are the same or if one is waiting on a speculation of the other to end. Then, point (3) ensures that whenever we start from related states (${\Sigma }_{xy}{\approx }_{xy}{X}_{xy}$) and we do one or more steps of the AM composed semantics (${\stackrel{\overline{\tau }}{\to }}_{xy}^{\ast }$), then we can always find a related state (${\Sigma }_{xy}^{\prime }{\approx }_{xy}{X}_{xy}^{\prime }$) that is reachable by performing one or more steps of the composed oracle semantics (${⇝}_{xy}^{{\mathcal{O}}_{xy}}$). This fact is used when proving that SNI of a program under the composed AM semantics implies SNI under the composed oracle semantics (point 1 of Definition 10). Thus, it is not important for the AM and the Oracle semantics to produce the same traces, just that the two AM traces and the two Oracle traces are pairwise equivalent – which follows from the state relation.
• Finally, symbolic preservation (point 4) ensures that any step of the always-mispredict composed semantics corresponds to the concretization of a step of the symbolic composed semantics (and vice versa⁵). Note that proving symbolic preservation is almost trivial whenever both source semantics enjoy the same property (like our semantics $\mathsf{ghost}$, $\mathsf{ghost}$, $\mathsf{ghost}$, $\mathsf{ghost}$ and $\mathsf{ghost}$).

• If $p/{⊢}_x\text{SNI}$ or $p/{⊢}_y\text{SNI}$, then $p/{⊢}_{xy}\text{SNI}$.
• If $p{⊢}_{xy}\text{SNI}$, then $p{⊢}_x\text{SNI}$ and $p{⊢}_y\text{SNI}$.