We address the problem of preserving non-interference across compiler transformations under speculative semantics.

We develop a proof method that ensures the preservation uniformly across all source programs.

The basis of our proof method is a new form of simulation relation.

It operates over directives that model the attacker's control over the micro-architectural state,
and it accounts for the fact that the compiler transformation may change the influence of the micro-architectural state on the execution (and hence the directives).

Using our proof method, we show the correctness of dead code elimination.

When we tried to prove register allocation correct,
we identified a previously unknown weakness that introduces violations to non-interference.

We have confirmed the weakness for a mainstream compiler on code from the  cryptographic library.

To reclaim security once more, we develop a novel static analysis that operates on a product of source program and register-allocated program.

Using the analysis, we present an automated fix to existing register allocation implementations.

We prove the correctness of the fixed register allocations with our proof method.

The recent discovery of Spectre Attacks
lead to the development of software-based, speculation-aware countermeasures
in order to protect programs and reclaim their security.

The security guarantees of countermeasures are amenable to verification:

Information-flow analyses on the protected program ensure their formal security by proving them non-interferent under speculative semantics.

Non-interference, however, is only guaranteed for the program analyzed.

Compiler transformations revoke any guarantees established.

§ INTRODUCTION

Cryptographic implementations must satisfy two conflicting requirements:
They must compute highly performant to be of practical use and be absolutely secure for use in critical systems.

Implementations optimize performance with knowledge about underlying micro-architectural hardware features such as memory access patterns that improve cache usage.

Security, however, is threatened by side-channel attacks that exploit precisely these hardware features to leak sensible information brumleyRemoteTimingAttacks2005.

To mitigate side-channel attacks, leakage of sensible data needs to be eliminated.

This confronts the programmer with two challenges:
First, semantics of source-level languages do not model leaks produced by side-channels vuReconcilingOptimizationSecure2021.

And second, even if the source-level code is secure, incautious implementation of compiler optimizations can insert new leakage, rendering efforts to secure the source program useless bartheFormalVerificationConstanttime2019,simonWhatYouGet2018.

Developers address these problems with coding guidelines such as constant time programming and disabling compiler optimizations.

But following the guidelines is non-trivial and overlooked mistakes corrupt the guarantee for security alfardanLuckyThirteenBreaking2013.

At the same time, disabling compiler optimizations is dissatisfactory.

Formal methods have shown to help with the challenges:

The first challenge is overcome with novel leakage semantics that model side-channel leakage within the programming language's semantics molnarProgramCounterSecurity2006,bartheSystemlevelNoninterferenceConstanttime2014.

For the second, novel proof methods for compilers under leakage semantics provide a guarantee that side-channel security of the source program carries over to the executable bartheSecureCompilationConstantResource2021,bartheSecureCompilationSideChannel2018,bartheFormalVerificationConstanttime2019,bartheStructuredLeakageApplications2021.

Sadly, the recent discovery of Spectre Attacks kocherSpectreAttacksExploiting2019,canellaSystematicEvaluationTransient2019 again presents a hardware feature that leakage semantics fall short of:

Speculative execution produces side-channel leakages not captured by leakage semantics.

This means both challenges were open again, and the verification community was quick to address the first:

The development of speculative execution semantics has already taken place guarnieriHardwareSoftwareContractsSecure2021,cauligiConstanttimeFoundationsNew2020,
and formal tools find speculative side-channel leakages
or even prove their absence.

Provably correct compilation under speculative execution semantics, however, remains an unsolved challenge.

It is the challenge that we address in this paper.

Before we detail our contributions,
we want to recall the mechanics of Spectre Attacks
and sketch the concepts of speculative execution semantics,
non-interference as the property that guarantees a program's side-channel security,
and the methods used for provably correct compilation to preserve side-channel security to the executable.

Registers are orange and memory variables teal.
The stack contents are shifted by the stack pointer to appear constant.
Memory addresses are chosen arbitrarily towards presentation.
Framed instructions were inserted by Register Allocation.

0x48     stk

0x40     buf

[after skip=0pt]Heap
rl!  l
0xE0             [borders=left]4-1sensible

0xC8     sec

chacha20(..., uint8* sec, uint8 bytes)
uint8 buf[8];
|startspillendspillmauvestartspill|stk[0] = bytes;|endspill|
||for (i = 0; i < 8; i++)
|| buf[i] = sec[i];
|startfillendfillmauvestartfill|bytes = stk[0];|endfill|
|| if (bytes < 64) ...

§.§.§ Spectre Attacks
Spectre Attacks observe side-channel leakages that are produced during speculative execution.

Speculative execution allows the processor to speculatively execute instructions from the pipeline that still have unevaluated instruction parameters.

When the processor detects a miss-speculation, i.e. it assumed incorrect values for the unevaluated parameters, it rolls back execution to erase its effect.

Rollbacks are invisible to typical source-level semantics, but micro-architectural side-channel leakage during speculative execution remains observable to an attacker.

Spectre Attacks target this discrepancy in the following way:

* Train some micro-architectural component to speculatively execute a code fragment that

* under miss-speculation brings sensible data into a processor's register,
* is leaked through side-channels.

The prominent example is Spectre- kocherSpectreAttacksExploiting2019,
whose source of speculation is the processor's branch prediction unit (Prediction History Table),
and the side-channel leakage happens via cache-eviction or program counter.

<Ref> demonstrates the attack
[The attack on this code is unlikely to execute on actual hardware because the specific speculation patterns would be hard to train. We chose it because it also demonstrates a new vulnerability in Register Allocation that we present in this paper.]:

The code is intended to load an 8-byte chunk from ,
which points into a stream of sensible data,
and to store it into a stack-local buffer  in order to later perform computation on it.

The -conditional in <Ref> might speculatively execute <Ref> an additional time even though .

<Ref> then stores sensible data, say $\val$, to .

If speculation continues with <Ref>, $\val$ is loaded into
and is used as an address in <Ref>,
where the branching condition is leaked, effectively leaking to the attacker, whether $\val < 64$.

§.§.§ Speculative execution semantics and Non-interference

Speculative execution semantics are an extension of leakage semantics for speculation.

The achievement of leakage semantics is to incorporate a model of attacker observed leakage into the semantics.

The constant-time model for side-channel leakage (without speculation) exposes memory accesses and program counter as observations to the attacker bartheSystemlevelNoninterferenceConstanttime2014.

Transitions in leakage semantics are of the form $\statec \xrarrow{\leak}{} \stated$.

They prompt a transition from $\statec$ to $\stated$ while capturing effects on the micro-architectural state in the leakage observation $\leak$.

Side-channel security can now be stated as a property of the program's leakage semantics.

For that, a relation on initial states is necessary that identifies states as different only wrt. sensible data.

The property is non-interference, which states that the sequence of leakages observed when executing from $\statec_1$ is equal to the sequence of leakages observed when executing from $\statec_2$.

Non-interference makes it impossible for leakages to depend on sensible data in any way.

The extension to speculative execution semantics came with a new challenge: Non-determinism.

Whether the processor miss-predicts and when it detects miss-prediction is highly hardware dependent and potentially even under the attacker's influence.

As a result, there is not a single execution but instead a set of possible executions, each with a different sequence of leakages.

In order to phrase non-interference on speculative execution semantics,
one wants to compare executions where the attacker trained the hardware in the same way.

Because then, the attacker can be sure that observed differences are accounted to sensible data.

A transition in speculative execution semantics is of the form $\statec \ntrans{\leak}{\direct} \stated$.

Again, $\leak$ is the attacker observed leakage.

What is new is the directive $\direct$ that allows the attacker to steer the behaviour of speculation cauligiConstanttimeFoundationsNew2020,bartheHighAssuranceCryptographySpectre2021.

As an example, the sequence of directives that leads to the leakage of sensible data in <Ref> is

\[
\underset{\text{\Cref{line:spill}}}{\vphantom{)}\Dstep}
\quad\lseq\quad\underset{\text{\Cref{line:for,line:for_body}}}{{(\Dif\;\lseq\;\Dstep)}^8}
\quad\lseq\quad \underset{\text{\Cref{line:for}}}{\vphantom{)}\Dspec}
\quad\lseq\quad \underset{\text{\Cref{line:for_body}}}{\vphantom{)}\Dstore{\texttt{\colvar{stk}}}{0}}
\quad\lseq\quad \underset{\text{\Cref{line:for,line:fill,line:leak}}}{\vphantom{)}\Dif\;\lseq\;\Dstep\;\lseq\;\Dstep} .
\]

It starts with an instruction that can only step forward ($\Dstep$),
then executes the correct branch 8 times ($\Dif$),
begins speculation with a miss-prediction ($\Dspec$),
followed by an unsafe memory access ($\Dstore{\texttt{\colvar{stk}}}{0}$),
and finally the sequence that leads to the leaking instruction.

We define our own language model (<Ref>) in this spirit.

§.§.§ Secure compilation

The goal of secure compilation is to prove that a compiler pass preserves non-interference from source to target program.

The methods draw from classical methods for compiler correctness.

Traditional proofs for correct compilation utilize simulation in order to argue that the target program's executions
can be found in the source program's semantics mccarthyCorrectnessCompilerArithmetic1967,leroyFormallyVerifiedCompiler2009,.

Traditional simulations are a relation $\simrel$ between the target program's states and the source program's states.

Whenever a target state $\stated$ is simulated by a source state $\statec$,
and transitions to $\stated \xrarrow{o}{} \statef$,
where $o$ is an observable environment interaction,
then $\statec$'s next transition needs to be $\statec \xrarrow{o}{} \statee$,
so that $\statef \simrel \statee$.

Simulation ensures that the target program's execution produces the same observations as the source-program.

For non-interference on leakage semantics, a notion of simulation needs more:

Compilers aim to preserve observations such as system-calls,
but they regularly modify side-channel leakage between source and target program.

Leakage transformation costanzoEndtoendVerificationInformationflow2016,bartheStructuredLeakageApplications2021,bartheSecureCompilationSideChannel2018 solves this issue:
Given the source program's execution,
the simulation also provides a function to transform the observed leakage in the source program
into the observed leakage of the target program.

In order to preserve non-interference, simulation with leakage transformation needs to satisfy the constant-time cube diagram.

The cube diagram can be seen in <Ref> on the right.

It looks at a pair of simulated states $\stated_1 \simrel \statec_1$ and $\stated_2 \simrel \statec_2$.

Then, if $\statec_1$'s next transitions leak a sequence $\tracek$ and so do $\statec_2$'s next transitions (black)
then the next transitions' leakage from $\stated_1$ and $\stated_2$ must coincide as well (purple).

Note that the target leakage does not need to be $\tracek$.

<Ref> (left) lists compilers employing simulations with leakage transformation and constant-time cube diagram.

In the speculative execution setting,
compilers so far try to avoid spectre attacks with mitigation passes such as fence insertion and speculative load hardening zhangUltimateSLHTaking2023.

The mitigations are one of the last passes in the compiler chain in order to withstand any further compilation.

They aim to eliminate speculative leakage by inserting speculation barriers conservatively, which entails significant performance overhead.

Even worse: Efforts to improve performance were flawed, again leading to insecure executables patrignaniExorcisingSpectresSecure2021.

Mitigations are nonetheless desirable because they free the developer from speculation:

Previous to the mitigation pass,
semantics can be considered speculation-free.

However, recent research suggests that in order to obtain minimal performance overhead,
the cryptographic developer needs an interface to control inserted mitigations shivakumarTypingHighSpeedCryptography2023.

This means a new proof method for compilation is needed that works when both, source and target program, operate under speculative execution semantics.

To the best of our knowledge, <cit.> is the only work so far to (dis-)prove compiler correctness under consideration of speculative execution semantics.

The authors target specifically compiler mitigations and discovered the aforementioned flaws in fence insertion and speculative load hardening.

Being tailored towards mitigations, they employ assumptions on the setting that do not hold in general and that we overcome in our development.

We detail the differences to our work in <Ref> (right):

The first difference lies in the property ensuring side-channel security.

Their work aims to preserve Speculative Non-interference ($\propsnip$ for Speculative Non-interference Preservation),
but the proof method is designed to preserve speculative taint safety $\propstsp$ (Speculative Taint safety Preservation).

Taint safety is a safety property that soundly approximates non-interference.

Our method is designed to prove $\propsnip$ instead.

Speculation and Non-Det:
A bigger difference is speculative execution semantics they assume:

A speculation window () limits speculative execution to a constant number of steps
and miss-predict semantics () force execution to always miss-predict.

Together, they form a deterministic restriction of speculative execution semantics.

Miss-predict semantics on their own are no real restriction,
as they maximize the side-channel leakages produced during speculative execution.

However, speculation windows restrict the speculative semantics.

While the restriction is reasonably chosen with respect to current hardware,
we decided against under-approximate semantics for our proof method.

Further, the focus on compiler mitigations lead them to the assumption that the source language is speculation-free,
meaning the speculative semantics are target program only ().

In this paper, we deal with unbounded speculation () and the induced non-determinism in both, source and target semantics ().

Our method is presented for structured memory () with the assumption that source programs are memory safe when executed under speculation-free semantics.

This is a common assumption for compilers.

Nonetheless, this assumption is not necessary.

We have a version of our method that was defined with programs operating on unstructured memory ().

We chose structured memory for presentation because we need it for a static analysis later in our work.

To keep it simple, we decided against introducing a separate program semantics for that.

Mitigations insert speculation barriers and do not change the code otherwise.

As the source program in patrignaniExorcisingSpectresSecure2021 does not speculate,
the leakages of the source program will still be fully present and unchanged in the target program.

Because the target program is executed with speculative execution semantics,
there can, however, be additional leakages interleaved in the target program.

This leads their work to consider leave-out simulations (),
where source leakages are equal to target leakages with additional speculatively leakages.

For general compiler transformations and unbounded speculation, we introduce the more general directive transforming simulations ().

Proving that compilers preserve side-channel security under leakage semantics (left) and under speculative execution semantics (right).
Green parameters are more expressive.

[right color=lightgreen,left color=base] ([shift=(0.5,0)]7-|4) rectangle (8-|5) ;

Compcert *leroyFormallyVerifiedCompiler2009
Jasmin *bartheStructuredLeakageApplications2021
Ex. Spec. *patrignaniExorcisingSpectresSecure2021
This Paper

Property                $\propnip$        $\propnip$        $\propstsp$            lightgreen $\propsnip$

Simulation              LT-Sim            LT-Sim            LO-Sim                 lightgreen DT-Sim

Speculation             —               —               SW, M, TO              lightgreen UB, ST

Non-Det                 No                No                No                     lightgreen Yes

Spec Source             —               —               PHT                    PHT

Memory Safety           S                 S                 U                      S

Passes                  Full              Full              SLH & Fence Ins       DC & RA

§.§.§ Contributions

In this paper, we present snippy simulations,
a novel proof method for preservation of non-interference under speculative execution semantics.

The main challenge to overcome with speculation is its inherent non-determinism.

For once, the definition of simulations becomes more involved:

Deterministic semantics have the advantage that simulations are always bi-simulations milnerAlgebraicDefinitionSimulation1971.

A simulation in that setting presents synchronization points between the (singular) execution of the source program and the target program.

For the non-deterministic speculative execution semantics,
the synchronization must happen for each of the target program's executions.

Second, similar to how compilers do not preserve leakage,
they also modify where the attacker can influence the computation.

A sequence of directives on the source program might no longer be executable on the target program.

Technically, we address this by introducing the new concept of directive transformations.

Directive transformations match every executable sequence of directives in the target program
with a sequence of directives in the source program.

We then embed directive transformations in a new constant-time cube for speculative execution semantics (<Ref>, right).

It is our contribution to make the constant-time cube applicable for speculative semantics.

We demonstrate our proof method on a challenging compiler transformation: Register Allocation.

This is the first time, that register allocation has been formally analyzed under speculative execution semantics —
and to our surprise, we found a serious vulnerability:

In <Ref>, the framed instructions are inserted by Register Allocation.

The source program (without <Ref>) has no side-channel leakage of sensible data under speculative execution semantics.

The target program however (with <Ref>), can be attacked as we discussed above.

In order to fix register allocation,
we present a static analysis on the product of source program and target program
that finds speculative leakage introduced only by register allocation.

In short, we address the problem of non-interference preservation for compiler passes under speculative execution semantics.

We make the following contributions:

* We develop a proof method for non-interference preservation under speculative execution semantics based on simulation relations.
Technically, we address non-determinism from speculation with directive transformations.

* We demonstrate our proof method on dead code elimination.

* We show that register allocation does not preserve non-interference under speculative execution semantics.
We confirm this on the  compiler.

* We propose a static analysis that finds and automatically fixes vulnerabilities introduced by register allocation.
We apply our proof method to show that the fixed version is secure.

§ LANGUAGE MODEL

We introduce our programming language and its speculative execution semantics.

A program is a mapping $\prog : \pcsof{\prog} \to \instrs$ from program counters to instructions.

The initial program counter is $\entry \in \pcsof{\prog}$.

Instructions $\inst \in \instrs$ are of the following form.

We denote registers by $\rega, \regb, \regc \in \regs$
and memory variables by $\vara, \varb \in \vars$.

The subscripts $\pcsuc \in \pcsof{\prog}$ are the successors of $\inst$.

We may also call $\pcsuc$ a successor of $\pc$ instead, if it is a successor of $\progof{\pc}$.

\begin{align*}
\inst \in \instrs \;& \Coloneqq \;
\Iexit
\bnfalt \Inop{\pcsuc}
\bnfalt \Iasgn{\rega}{\regb \op \regc}{\pcsuc}
\bnfalt \Iload{\rega}{\vara}{\regb}{\pcsuc}
\bnfalt \Istore{\vara}{\regb}{\regc}{\pcsuc}
\bnfalt \Iif{\regb}{\pcsuc_{\btrue}}{\pcsuc_{\bfalse}}
\bnfalt \Isfence{\pcsuc}
\bnfalt \Islh{\rega}{\pcsuc}
\end{align*}

The instructions are return (or exit), no-op, assignment, load, store, conditional branching, and two instructions that control speculation:
a speculation fence and speculative load hardening.

§.§.§ Semantics

We introduce two semantics:
Speculation-free $\statec \trans{\leak}{\direct} \stated$ (<Ref>)
and speculative $\nstatec \ntrans{\leak}{\direct} \nstated$ (<Ref>).

The transitions are labelled by leakage $\leak \in \leaks$
and directives $\direct \in \directs$.

Leakages are the addresses of memory accesses as well as branching conditions.

Directives resolve non-determinism for the speculative semantics,
i.e. where accesses to memory can become unsafe (out-of-bounds).

Directives are considered under the attacker's control.

A speculation-free state is a tuple $(\pc, \rasgn, \masgn) \in \states$
that tracks the program counter $\pc \in \pcs$,
register contents $\rasgn : \regs \to \vals$,
and memory $\masgn : \mems \to \vals$.

The semantics is fairly standard with selected rules in <Ref>.

Memory is structured and without dynamic allocation.

Each variable $\vara$ has static size and for an offset address $\adr \in \adrs \subseteq \vals$,
we write $\adr \in \sizeof{\vara}$ to indicate that $\adr$ lies within $\vara$'s size.

The memory is $\mems = \setcond{(\vara, \adr)}{\adr \in \sizeof{\vara}}$.
Loads (rule:load,rule:load-unsafe) and stores (rule:store,rule:store-unsafe) leak the address used via $\Eload{\adr}$ and $\Estore{\adr}$,
and branching (rule:branch) leaks its condition with $\Eif{\bvalue}$.

The directives $\Dload{\varb}{\adrp}$ (rule:load-unsafe) and $\Dstore{\varb}{\adrp}$ (rule:store-unsafe) resolve memory access for unsafe (out-of-bounds) addresses.

The directive $\Dif$ is used by the speculative semantics to control whether to miss-predict or branch correctly.

[label=rules:spec-free]Speculation-free Semantics
(, , )  (, , )

(, , )  (, , )

= __

= (0 )

(, , )  (_, , )

=  ∈

(, , )  (, , )

=  ∈

(, , )  (, , (,))

=  ∉

(, , )
(, , )

=  ∉

(, , )
(, , (, ))

[label=rules:spec]Speculating Semantics

$\instof{\statec}$ speculation insensitive

= __

= (0 )

(, , ) ¬
(, , )(_¬, , )

(, , )  (, , )

=  > 00

(, , )  (, , )

[label=rules:spectranscl]Transitive closures

The source of speculation are $\IWif{\regb}$ instructions triggering branch-prediction ().

Speculation starts with a branch miss-prediction,
and later ends with a rollback to the state before speculation
[This means our semantics allows for another speculation immediately after rollback.
This could be avoided with an additional flag to store whether a state has already been miss-predicted.]

A speculating state tracks all currently active miss-predictions in a stack of states $\nstatec \in \nstates = \states^*$.

The semantics $\nstatec \ntrans{\leak}{\direct} \nstated$ is provided in <Ref>.

With $\instof{\statec}$, we access $\statec$'s instruction $\progof{\pc}$, when $\statec = (\pc, \rasgn, \masgn)$.

The speculation sensitive instructions are $\IWsfence$ and $\IWslh{\rega}$,
as their semantics depend on whether the current state is speculating.

A speculation fence $\IWsfence$ disallows speculation, so rule:nsfence only executes in states currently not speculating.

rule:nslh performs speculative load hardening $\IWslh{\rega}$, which wipes a register only if the state is currently speculating.

The remaining instructions are speculation insensitive.

rule:nstep executes them on the currently speculating state, i.e. the top-most state in the sequence of states.

The directives that determine whether a miss-prediction happens or not are $\Dspec$ and $\Dif$.

$\Dspec$ demands the miss-prediction performed by rule:nspec.

A copy of the current state is pushed on top of the current state and the program counter is set to the incorrect branch.

Otherwise, rule:branch executes on directive $\Dif$ for a correct branching.

rule:nrb rolls back execution to before the last miss-prediction.

It can be triggered with a $\Drb$ directive in any state that is currently speculating.

There is no bound on the length of a speculation.

We write $ \nstatec \ntranss{\tracel}{\dtraced} \nstated$ for finite executions
and $\nstatec \ntransi{\itrace}{\idtrace}$ for diverging executions.

We use $\tracel$ and $\dtraced$ for both, finite and infinite sequences,
i.e. $\tracel \in \leaks^* \cup \leaks^{\infty}$ and $\dtraced \in \directs^* \cup \directs^{\infty}$.

We call any $(\entry, \rasgn, \masgn)$ initial and $(\pc, \rasgn, \masgn)$ with $\progof{\pc} = \Iexit$ final.

We say that $\stated$ is reachable from $\statec$ if $\statec \transs{\tracel}{\dtraced} \stated$.

We say that $\stated$ is reachable if it is reachable from some initial state.

The behaviour of a program consists of the directives and events along any execution from an initial state.

The speculation-free semantics is deterministic, so its behaviour is a single execution;
the speculative behaviour is non-deterministic and its behaviour forms a set of executions.

\begin{align*}
\behdefof{\prog}{\statec}
\; & \defeq \;
\begin{cases}
\tbeh{\dtpair{\tracel}{\dtraced}} & \statec \transs{\tracel}{\dtraced} \stated, \textnormal{$\stated$ final} \\
\dbeh{\dtpair{\itrace}{\idtrace}} & \statec \transi{\itrace}{\idtrace}
\end{cases} &
\nbehdefof{\prog}{\nstatec}
\; & \defeq{} \;
\begin{aligned}
{\nstatec \ntranss{\tracel}{\dtraced} \nstated, \textnormal{$\nstated$ final}} \\
{} \cup {} &
\setcond{\dbeh{\dtpair{\itrace}{\idtrace}}}{\nstatec \ntransi{\itrace}{\idtrace}}
\end{aligned}
\end{align*}

We call $\prog$ safe if no memory access is unsafe,
i.e. for every initial state $\statec$
no directives $\Dload{\vara}{\adr}, \Dstore{\vara}{\adr}$
occur in the speculation-free behaviour $\behof{\prog}{\statec}$.

For the remaining paper we assume safe programs.

Note that this does not mean that speculating memory accesses need to be safe.

As seen in <Ref>, Spectre Attacks target the fact that safe programs are not safe under speculative semantics.

[label=code:simplerv1]Simplified <Ref>
a = (b < buf_size)
br (a)|$\NextInst{\mkern1mu\makepc{d},\;\makepc{e}}$|
buf[b] = secret
bytes = stk[0]
br (bytes)|$\NextInst{\mkern1mu\makepc{g},\;\makepc{g}}$|

<Ref> contains a simplified version of <Ref>.

The secret is already in a register $\rasgnof{\makereg{secret}} = \texttt{0x5ec}$ and to be stored to buf at offset b.

Assume the offset is out of bounds, $\rasgnof{\makereg{b}} = 8 \notin \sizeof{\makevar{buf}}$.

From a state $\statec = (\makepc{2}, \rasgn, \masgn)$, where the first instruction was already executed, i.e. $\rasgnof{\makereg{a}} = \bfalse \neq 0$,
the following transitions are available:

First, a speculation is started with rule:nspec and $\statec$ is copied with program counter set to the incorrect branch 3.

Next, rule:store-unsafe is executed with target $(\makevar{stk}, 0)$, so $\masgnp = {\subst{\masgn}{(\makevar{stk}, 0)}{\texttt{0x5ec}}}$.

The rule:load then brings the secret to a register, $\rasgnp = \subst{\rasgn}{\makereg{bytes}}{\texttt{0x5ec}}$.

Finally, rule:branch leaks the secret,

\begin{align*}
\statec &\ntrans{\Eif{\bfalse}}{\Dspec} \statec\lseq(\makepc{3},\rasgn, \masgn)
\ntrans{\Estore{8}}{\Dstore{\makevar{stk}}{0}} \statec\lseq(\makepc{4}, \rasgn, \masgnp)
\ntrans{\Eload{0}}{\Dstep} \statec\lseq(\makepc{5}, \rasgnp, \masgnp)
\ntrans{\Eif{\texttt{0x5ec}}}{\Dif} \statec\lseq(\makepc{6}, \rasgnp,\masgnp)\,.
\end{align*}

Speculative semantics exhibit two important properties:

First, similar to just leakage semantics under the $\propcct$-model,
speculative semantics reveal the program counter to the attacker.

This is the case, because the leaked branching conditions let the attacker know of every path a branching instruction has been taken.

Second, directives resolve non-determinism introduced by speculation.

To express the first property,
we write $\nstatec \defsamepoint \nstated$ to mean that $\nstatec$ and $\nstated$ are at the same program point.

For speculation-free states $\statec \atpc \pc$ means that
$\statec$ is at program counter $\pc$, $\statec = (\pc, \rasgn, \masgn)$.

Then, $\statec \samepoint \stated$ means that $\statec$ and $\stated$ share the program counter, $\statec \atpc \pc \atpc \stated$.

For speculating states, we write $\nstatec \samepoint \nstated$ if each pair of configurations in their speculation stack is at same program point.

Formally, $\varepsilon \samepoint \varepsilon$,
and $\nstatec\lseq\statec \samepoint \nstated\lseq\stated$ if $\nstatec \samepoint \nstated$ and $\statec \samepoint \stated$.

The following two lemmas express the properties.

If two same-point states $\nstatec_1 \samepoint \nstatec_2$ execute with the same directives and leakages, $\nstatec_1 \ntranss{\tracel}{\dtraced} \nstated_1$, $\nstatec_2 \ntranss{\tracel}{\dtraced} \nstated_2$,
then the resulting states are also same-point, $\nstated_1 \samepoint \nstated_2$.

For all $\nstatec$ and $\direct$
exist at most one $\nstated$ and $\leak$
with $\nstatec \ntrans{\leak}{\direct} \nstated$.

§.§.§ Notation

Similar to how we access the current instruction with $\instof{\statec}$,
we write $\ofnota{f}{\statec}$ instead of $\ofnota{f}{\pc}$ when $\statec = (\pc, \rasgn, \masgn)$ for any $f : \pcs \to A$.

Further, we extend not only the $\samepoint$-relation to speculating states,
but any relation $R \subseteq \states \times \states$ is extended to a relation on $\nstates$ in the obvious way:

$\varepsilon \mathrel{R} \varepsilon$ and $\nstatec\lseq\statec \mathrel{R} \nstated\lseq\stated$, if $\nstatec \mathrel{R} \nstated$ and $\statec \mathrel{R} \stated$.

§ NON-INTEREFERENCE PROPERTIES

We define non-interference and non-interference preservation for our speculative semantics.

We require the initial state's memory to be partitioned into public and sensible data
through a security level assignment $\lows : \vars \to \secset$
to a lattice $\secset = (\set{\low, \high}, \low \leq \high)$.

Sensible data ($\high$) is considered unknown to the attacker,
and we say that initial states are indistinguishable $(\entry,\rasgn,\masgn)\seceq (\entry,\rasgn,\masgnp)$ to the attacker
when the memory coincides on all variables considered public.
That is, for all $\vara$ with $\lowsof{\vara} = \low$, $\masgnofflat{\vara} = \masgnpofflat{\vara}$.

Our formulation of speculative non-interference ($\propsni$, <Ref>) requires indistinguishable initial states $\statec_1\seceq\statec_2$ to produce equal behaviour.

That means that for both initial states

* the sequences of executable directives are the same, and

* for each sequence of executable directives, the observed leakage is the same.

Let us explain the necessity for the first condition.

As long as the second condition is satisfied, any two executions $\statec_1 \ntrans{\tracel}{\dtraced} \nstated_1$ and $\statec_2 \ntrans{\tracel}{\dtraced} \nstated_2$
will stay in same program point $\nstated_1 \samepoint \nstated_2$ (<Ref>) and synchronously execute the same instructions.

If at $\nstated_1$ the set of executable directives is different to those in $\nstated_2$,
then the instruction has to be a memory access.

All other instructions have the same set of executable directives, independent of register and memory contents.

This means that one state executes an unsafe memory accesses (rule:load-unsafe or rule:store-unsafe)
while the other executes a safe memory accesses (rule:load or rule:store).

However, unsafe and safe memory accesses both leak the address used.

A difference in executable directive thus amounts to different leakage.

A program is speculatively non-interferent, $\prog \semmodels \propsni$,
if all indistinguishable initial states $\nstatec_1 \seceq \nstatec_2$
have the same behaviour $\nbehof{\prog}{\nstatec_1} = \nbehof{\prog}{\nstatec_2}$.

Our goal is to prove preservation of non-interference for compiler transformations.

We model compiler transformations $\translp$ that map a source program $\prog$ to the transformed target program $\tgtp$.

Transformations may modify the structure of initial states from source program $\prog$ to target program $\tgtp$.

For example, a pass that realizes the architecture's calling convention relocates parameters to specific registers.

We require each pass to come with a relation $\simrel$ on initial states that identifies the initial states of $\tgtp$ with the initial states of $\prog$.

In order to define preservation of non-interference, the relation has to respect $\lows$ in the following sense:
[One could also have a second security assignment on the target program, but for simplicity we assume they are the same.]

A relation ${\simrel} \subseteq \nstatesof{\tgtp} \times \nstatesof{\prog}$ respects $\lows$
if every initial $\stated \in \nstatesof{\tgtp}$
is mapped to an initial $\statec \in \nstatesof{\prog}$, $\stated \simrel \statec$,
and for all pairs of initial states $\stated_1 \simrel \statec_1$ and $\stated_2 \simrel \statec_2$ holds:
$\stated_1 \seceq \stated_2$ if and only if $\statec_1 \seceq \statec_2$.

Speculative non-interference preservation for a transformation $\translp$ states that for all source programs $\prog$,
whenever $\prog \semmodels \propsni$ then also $\tgtp \semmodels \propsni$.

However, defining preservation in this way leads to potentially surprising outcomes.

If the source program $\prog$ fails $\propsni$ for just some initial states,
a compiler can introduce leakage into $\tgtp$
that reveals secrets on other initial states,
that behaved non-intereferent on the source program.

To counteract that, our definition of speculative non-interference preservation is more precise patrignaniExorcisingSpectresSecure2021.

It requires preservation of equal leakage for every pair of source program's and target program's initial states individually.

In particular, this definition entails that if $\prog \semmodels \propsni$ then also $\tgtp \semmodels \propsni$.

A program translation $\translp$ with $\lows$-respecting mapping $\simrel$
is $\propsni$-preserving, $\translp \semmodels \propsnip$,
if all initial states $\stated_1 \seceq \stated_2$ of $\tgtp$
with initial source states $\stated_1 \simrel \statec_1$ and $\stated_2 \simrel \statec_2$
of equal behaviour $\nbehof{\prog}{\statec_1} = \nbehof{\prog}{\statec_2}$
also have equal target behaviour,
$\nbehof{\translpof{\prog}}{\stated_{1}} = \nbehof{\translpof{\prog}}{\stated_2}$.

§ PROVING SPECULATIVE NON-INTERFERENCE PRESERVATION

We present our proof method for speculative non-interference preservation.

We introduce snippy simulations which ensure that a code transformation preserves speculative non-interference:

If for all $\prog$ there is a snippy simulation $(\simrel, \dtffamily)$
between $\tra$ and $\prog$, then $\translp \vDash \propsnip$.

In order to reach that goal,
we first define simulations that transform directives to cope with the fact that compilers do not preserve executable sequences of directives.

We then introduce snippy simulations as a constraint on simulations with directive transformation and prove <Ref>.

This reduces proving a transformation $\propsnip$ to proving that it has a snippy simulation for each program $\prog$.

In the next section, we show how to craft a snippy simulation
that is parametric in $\prog$, reducing proof effort to a once-and-for-all proof.

§.§ Simulation with Directive Transformation

The new feature in our work is directive transformation.

Conceptually, a simulation between the target program $\tgtp$ and the source program $\prog$ shall replay any execution of $\tgtp$ in $\prog$.

A directive sequence $\dtraced$ selects a single execution in $\tgtp$ (<Ref>).

Our simulation wants to select a corresponding execution in $\prog$.

However, the directives $\dtraced$ may not be executable in $\prog$,
or it might select an inappropriate execution.

Instead, a different sequence of directives may be necessary on the source program,
since transformations $\translp$ are not designed to preserve them.

[float,label=code:dce]Example code transformation from Dead Code Elimination.
[height=0pt,after skip=0pt]Source $\prog$aa

if (i < buf_size)
a = buf[i];
a = 0;

[height=0pt,after skip=0pt]Target $\tgtp$

if (i < buf_size)
a = 0;

We accompany our formal development with the example transformation in <Ref>,
where an unnecessary $\IWload{\makereg{a}}{\makevar{buf}}{\makereg{i}}$ instruction is replaced by a $\IWnop$.

Consider an initial target state $\stated = (\makepc{a},\rasgn,\masgn)$
where $\rasgnof{\makereg{i}} \notin \sizeof{\makevar{buf}}$,
and the source state $\statec = (\makepc{1}, \rasgn, \masgn)$.

The directives $\Dspec\lseq\Dstep\lseq\Dstep$ are executable from $\stated$.

But the same sequence cannot be executed from $\statec$:
An unsafe load necessitates a directive $\Dload{\vara}{\adrp}$ for any $\colvar{\vara}$ and $\adrp$.

Thus, a transformed sequence of directives $\Dspec\lseq\Dload{\colvar{\vara}}{\adrp}\lseq\Dstep$ is executed.

A simulation with directive transformation ($\dtsim$) is a relation on states $\nstated \simrel \nstatec$
where a target state $\nstated \in \nstatesof{\tgtp}$ is related to a $\nstatec \in \nstatesof{\prog}$ is a source state.

The directive transformation is a family of relations
${\dtfat{\nstatec}{\nstated}} \subseteq \directs^* \times \directs^*$.

We characterize $\dtsim$ in <Ref>.

Consider any states $\nstated \in \nstatesof{\tgtp}$ and $\nstatec \in \nstatesof{\prog}$ and $\nstated \simrel \nstatec$.

To express that $\nstated$ is simulated by $\nstatec$ means the following:

Either both states are final (rule:final),
or we have to explore all sequences of executable directives $\nstated \ntranss{\tracel}{\dtraced} \nstatef$ in $\tgtp$ up to some bound (rule:tgt).

For each explored sequence of directives we apply the directive transformation $\dtfat{\nstatec}{\nstated}$.

Then, we need to replay the execution with a sequence of executable directives $\nstatec \ntranss{\tracek}{\dtracee} \nstatee$ in $\prog$ (rule:src),
so that $\nstatef \simrel \nstatee$.

Formally, we write $\proofnode{\sderivetgtsim{\simrel}{\dtf}{\nstated}{\nstatec}{\dtraced}}$
to mean that we are exploring executions in $\tgtp$,
have already seen a sequence of directives $\dtraced$ and arrived at target state $\nstated$.

We can now either bound the exploration with rule:direct-tf,
or continue exploration via rule:tgt.

With rule:direct-tf we look up a directive transformation for the explored $\dtraced$
and swap to $\proofnode{\sderivesrcsim{\simrel}{\dtf}{\nstatef}{\nstatec}{\dtracee}}$.

This states that we are seeking to replay the explored sequence with its transformation $\dtracee$ from $\nstatec$.

If $\dtracee$ is executable $\nstatec \ntranss{\tracek}{\dtracee} \nstatee$ in $\prog$,
rule:coind checks that the states reached from exploration in $\tgtp$ and replay in $\prog$ are again related, $\nstatef \simrel \nstatee$.

The notions of $\guarded{\simrel}$ and $\unguarded{\simrel}$ make sure that both,
exploration in $\tgtp$ and replaying in $\prog$, take at least one execution step.

The guarded version $\guarded{\simrel}$ requires at least one application of rule:tgt or rule:src to become the unguarded version $\unguarded{\simrel}$.

Only then, rule:direct-tf,rule:coind become applicable.

We write $\eitherguarded{\simrel}$ for any of $\guarded{\simrel}$ or $\unguarded{\simrel}$.

A simulation with directive transformation $(\simrel, \dtffamily)$ consists
of a relation ${\simrel} \subseteq \nstatesof{\tgtp} \times \nstatesof{\prog}$
and a family $\dtffamily = (\dtfat{\nstatec}{\nstated})_{(\nstated, \nstatec) \in \simrel}$
so that for all initial $\stated \in \nstatesof{\tgtp}$,
there is an initial $\statec \in \nstatesof{\prog}$ with $\stated \simrel \statec$,
and for all $\nstated \simrel \nstatec$,
$\proofnode{\sderivetgtsim{\guarded{\simrel}}{\dtfat{\nstatec}{\nstated}}{\nstated}{\nstatec}{\varepsilon}}$ can be proven in <Ref>.
[Our way to define simulations is inspired by recent work to unify stuttering <cit.>.]

[label=rules:simulation]Characterizing Simulations
∀ .

$\nstated$ not final

∃ .

$\nstated, \nstatec$ final

[label=rules:synctrans]Simulation Intervals

(, )  (, )

Consider once again the transformation in <Ref> and the initial states $\stated$ and $\statec$ from <Ref>.

Further, let $\statee = (\makepc{4},\rasgnp,\masgn)$ and $\statef = (\makepc{d},\rasgnp,\masgn)$ with $\rasgnp = \subst{\rasgn}{\makereg{a}}{0}$.

We want to prove that $\stated \simrel \statec$ is justified,
i.e. we need to construct ${\dtfat{\statec}{\stated}}$ so that $\proofnode{\sderivetgtsim{\guarded{\simrel}}{\dtfat{\statec}{\stated}}{\stated}{\statec}{\varepsilon}}$ is derivable.

We drop the subscript and just write $\dtf$.

Exploration via rule:tgt yields (among others) two sequences of directives executable from $\stated$ in $\tgtp$:

$\Dspec\lseq\Dstep\lseq\Dstep$ as in <Ref> and $\Dif$.

The corresponding execution takes us to $\stated \ntranss{\Eif{\bfalse}\lseq\Enone\lseq\Enone}{\Dspec\lseq\Dstep\lseq\Dstep} \stated\lseq\statef$
and $\stated \ntrans{\Eif{\bfalse}}{\Dif} \statef$, respectively.

After exploration with rule:tgt, we are thus left to prove $\proofnode{\sderivetgtsim{\unguarded{\simrel}}{\dtf}{\stated\lseq\statef}{\statec}{\Dspec\lseq\Dstep\lseq\Dstep}}$
and $\proofnode{\sderivetgtsim{\unguarded{\simrel}}{\dtf}{\statef}{\statec}{\Dif}}$.

For the first sequence, we transform the directives as in <Ref>:
$\Dspec\lseq\Dload{\makevar{secret}}{0}\lseq\Dstep \dtf \Dspec\lseq\Dstep\lseq\Dstep$.

For the other case, we do not need a transformation, so $\Dif \dtf \Dif$.

With rule:direct-tf, we are left with deriving $\proofnode{\sderivesrcsim{\guarded{\simrel}}{\dtf}{\stated\lseq\statef}{\statec}{\Dspec\lseq\Dload{\makevar{secret}}{0}\lseq\Dstep}}$
and $\proofnode{\sderivesrcsim{\guarded{\simrel}}{\dtf}{\statef}{\statec}{\Dif}}$.

Indeed, $\prog$ can replay the directives with rule:src $\statec \ntranss{\Eif{\bfalse}\lseq\Eload{\adr}\lseq\Enone}{\Dspec\lseq\Dload{\makevar{secret}}{0}\lseq\Dstep} \statec\lseq\statee$,
where $\adr = \rasgnof{\makereg{i}}$
and $\statec \ntrans{\Eif{\bfalse}}{\Dif} \statee$, respectively.

To now utilize rule:coind we need $\statef \simrel \statee$ and $\stated\lseq\statef \simrel \statec\lseq\statee$.

Each would again have to be justified independently.

Justifying the first is easy with rule:final,
while the other needs another application of rule:tgt, rule:direct-tf, and rule:src
and can then utilize $\statec \simrel \statec$.

§.§.§ Simulation Intervals

Our goal is to formulate snippy simulations as a constraint on simulations with directive transformation.

We define it with simulation intervals.

A simulation interval for states $\nstated \simrel \nstatec$ is a pair of an explored sequence of directives from $\nstated$ in $\tgtp$
and the corresponding replay from $\nstatec$ in $\prog$.

Formally, we define simulation intervals through a synchronized product,
whose transitions are the simulation intervals.

The states of the synchronized product are of shape $(\nstatec,\nstated)$ so that $\nstated \simrel \nstatec$.

Its transitions are of the form $(\nstatec, \nstated) \synctrans{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee, \nstatef)$,
where $\dtracee$ is the directive transformation of an explored $\dtraced$ in $\tgtp$.

In order to formally define the transition relation, consider a proof tree that justifies $\nstated \simrel \nstatec$,
i.e. that derives $\proofnode{\sderivetgtsim{\guarded{\simrel}}{\dtfat{\nstatec}{\nstated}}{\nstated}{\nstatec}{\varepsilon}}$.

We use the notation

\[
\proofnode{{\nstated}\tgtsim{\nstatec}}
\rproofedges{\dtraced}
\proofnode{{\nstatef}\tgtsim{\nstatec}}
\rproofedges{\dtracee \dtfspaced \dtraced}
\proofnode{{\nstatef}\srcsim{\nstatec}}
\rproofedges{\dtracee}
\proofnode{{\nstatef}\srcsim{\nstatee}}
\]

to state that the proof tree contains a path with nodes
and $\proofnode{{\sderivesrcsim{\unguarded{\simrel}}{\dtfat{\nstated}{\nstatec}}{\nstatef}{\nstatee}{\varepsilon}}}$.

In particular, this means that $\nstated \ntranss{\tracel}{\dtraced} \nstatef$ and $\nstatec \ntranss{\tracek}{\dtracee} \nstatee$ for appropriate $\tracel$, $\tracek$,
and $\dtracee \dtfat{\nstatec}{\nstated} \dtraced$.

We define a synchronized transition relation that executes both in a single step.

Given a simulation $(\simrel, \dtffamily)$,
its simulation interval transition is defined by <Ref>.

\begin{align*}
{\synctrans{\,}{}{}{\,}} &\quad\subseteq\quad {\simrel} \times \directs^* \times \leaks^* \times \directs^* \times \leaks^* \times {\simrel}
\end{align*}

Transitive Closures

(, ) εεεε (, )

(, )  (, )

(, )  (, )

(, )  (, )

(, )  (, )

(, )

(, )

Fix inftrace — keep closures at all?

rule:sync further defines the transition relations $\simtranss{}{}$ and $\simtranst{}{}$ as the projection of simulation intervals to source and target program.

Transitive closures of the transition relations are defined as usual.

We say that a simulation is lock-step if simulation intervals are single step: ${\simtranst{}{}}, {\simtranss{}{}} \subseteq {\ntrans{}{}}$.

The simulation intervals resulting from <Ref> for $\stated \simrel \statec$ are:

\begin{align*}
(\statec, \stated) & \synctransdisp{\Eif{\bfalse}\lseq\Eload{\adr}\lseq\Enone}{\Dspec\lseq\Dload{\makevar{secret}}{0}\lseq\Dstep}{\Eif{\bfalse}\lseq\Enone\lseq\Enone}{\Dspec\lseq\Dstep\lseq\Dstep} (\statec\lseq\statee, \stated\lseq\statef)
(\statec, \stated) & \synctransdisp{\Eif{\bfalse}}{\Dif}{\Eif{\bfalse}}{\Dif} (\statee, \statef)
\end{align*}

The following lemma states that our formulation of simulations is sound.

That is, we find all of $\tgtp$'s behaviour in the projection of the simulation interval transition relation $\simtranst{}{}$.

This lets us perform (co-)induction on $\nbehof{\tgtp} \nstatec$ with $\simtranst{}{}$ rather than $\ntrans{}{}$, which we will utilize in our proof of <Ref>.

The same is not true for the source program's behaviour and $\simtranss{}{}$.

If $\nstated$ occurs in $\simrel$,
$\nbehof{\translpof{\prog}}{\nstated} = \setcond{\tbeh{\dtpair{\tracel}{\dtraced}}}{\nstated \simtransts{\tracel}{\dtraced} \nstateh, \textrm{$\nstateh$ final}} \cup
\setcond{\dbeh{\dtpair{\itrace}{\idtrace}}}{\nstated \simtransti{\itrace}{\idtrace}}$.

§.§ Snippy simulations

So far, simulations are very liberal:
Simulation merely require that a sequence of directives in $\tgtp$ can be transformed via $\dtffamily$ into a sequence of directives in $\prog$.

The length and contained directives can change when applying $\dtffamily$ and there are no restrictions on how the leakage changes when applying $\dtffamily$.

In this section, we establish snippy simulations,
a constant-time cube constraint bartheSecureCompilationSideChannel2018 on simulations for speculative semantics
that entails $\propsnip$ when satisfied.

The intuition for snippy simulation can be explained as follows.

In order to prove that a transformation $\translp$ satisfies $\propsnip$,
we are given a source program $\prog$ and the target program $\tgtp$,
as well as four initial states:

Two target initial states $\stated_1 \samepoint \stated_2$
and two simulating source states $\stated_1 \simrel \statec_1$ and $\stated_2 \simrel \statec_2$,
so that $\nbehof{\prog}{\statec_1} = \nbehof{\prog}{\statec_2}$.

The goal is to prove that the equality of behaviour carries over to the target program.

Given a simulation $(\simrel, \dtffamily)$ we so far know how to replay any sequence of directives $\dtraced$ from $\stated_1$ transformed on $\statec_1$ (<Ref>).

Consider a simulation interval $(\statec_1, \stated_1) \synctrans{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee_1, \nstatef_1)$.

Due to same behaviour of $\statec_1$ and $\statec_2$,
the source directives can also be executed from $\statec_2$,
$\statec_2 \ntrans{\tracek}{\dtracee} \nstatee_2$.

Snippy simulations now state, that in such a situation,
the simulation interval for $\statec_2$ and $\stated_2$
also contains $(\statec_2, \stated_2) \synctrans{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee_2, \nstatef_2)$.

That means, $\stated_2$ can also execute $\dtraced$ and produce same leakage.

And further, $(\simrel, \dtffamily)$ does also explore $\dtraced$ from $\stated_2$, not a longer or shorter sequence.

<Ref> demonstrates the constraint in the general case, where states need not be initial.

The simulation interval of $\nstatec_1$ and $\nstated_1$ and the ability for another source state $\nstatec_2$ to mimic the behaviour are in black.

The constraint is in purple: $(\simrel, \dtffamily)$ has to also provide the same simulation interval for any other state $\nstated_2 \simrel \nstatec_2$ at the same program point as $\nstated_1$.

With snippy simulations defined, we conclude the section with the proof of <Ref>.

A snippy simulation $(\simrel, \dtffamily)$ is $\lows$-respecting and satisfies the diagram in <Ref>.
That is, for all $\nstatec_1 \samepoint \nstatec_2$ and $\nstated_1 \samepoint \nstated_2$
with $\nstated_1 \simrel \nstatec_1$, and $\nstated_2 \simrel \nstatec_2$
and $(\nstatec_1, \nstated_1) \synctrans{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee_1, \nstatef_1)$,

\begin{align*}
\nstatec_2 &\ntranss{\tracek}{\dtracee} \nstatee_2
&&\text{implies the existence of $\nstatef_2$ with}
(\nstatec_2, \nstated_2) &\synctrans{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee_2, \nstatef_2)
\end{align*}

Consider a program $\prog$ and a snippy simulation $(\simrel, \dtffamily)$.

We need to prove the following:
For all initial $\stated_1 \seceq \stated_2$ with $\stated_1 \simrel \statec_1$ and $\stated_2 \simrel \statec_2$:
When $\nbehof{\tgtp}{\nstatec_1} = \nbehof{\tgtp}{\statec_2}$,
then also $\nbehof{\tgtp}{\stated_1} = \nbehof{\tgtp}{\stated_2}$.

We claim a stronger statement:

Whenever $\nstated_1 \simrel \nstatec_1$, $\nstated_2 \simrel \nstatec_2$,
$\nstatec_1 \samepoint \nstatec_2$, and $\nstated_1 \samepoint \nstated_2$,
and $\nbehof{\prog}{\nstatec_1} = \nbehof{\prog}{\nstatec_2}$:

Then $\nbehof{\tgtp}{\nstated_1} \subseteq \nbehof{\tgtp}{\nstated_2}$ holds.

This is sufficient:

Consider initial target states $\stated_1 \seceq \stated_2$ as well as source states $\stated_1 \simrel \statec_1$ and $\stated_2 \simrel \statec_2$
with $\nbehof{\prog}{\statec_1} = \nbehof{\prog}{\statec_2}$.

Initial states are all at the same program point, so the requirements of the claim are satisfied
and $\nbehof{\tgtp}{\stated_1} \subseteq \nbehof{\tgtp}{\stated_2}$ holds.

By symmetry, $\nbehof{\tgtp}{\stated_1} = \nbehof{\tgtp}{\stated_2}$.

We prove our claim coinductively on $\nbehof{\tgtp}{\nstated_1}$ split into simulation intervals (<Ref>).

The case of a final $\nstated_1$, i.e. $\nbehof{\tgtp}{\nstated_1} = \set{\tbeh{\dtpair{\varepsilon}{\varepsilon}}}$,
$\nstated_2 \samepoint \nstated_1$ is final, too,
and thus $\tbeh{\dtpair{\varepsilon}{\varepsilon}} \in \nbehof{\tgtp}{\nstated_2}$.

In the (co-)inductive case, let
$\tbeh{\dtpair{\tracek\lseq\tracel}{\dtracee\lseq\dtraced}} \in \nbehof{\tgtp}{\nstated_1}$
with $\nstated_1 \simtranst{\tracek}{\dtracee} \nstatef_1$
from a simulation interval $(\nstatec_1, \nstated_1) \synctrans{\tracem}{\dtracef}{\tracek}{\dtracee} (\nstatee_1, \nstatef_1)$.

From $\nbehof{\prog}{\nstatec_1} = \nbehof{\prog}{\nstatec_2}$ follows $\nstatec_2 \ntranss{\tracem}{\dtracef} \nstatee_2$.

<Ref> gives $\nstatee_1 \samepoint \nstatee_2$
and same behaviour of $\nstatec_1$ and $\nstatec_2$ entails $\nbehof{\prog}{\nstatee_1} = \nbehof{\prog}{\nstatee_2}$.

Any difference in behaviour for $\nstatee_1$ and $\nstatee_2$ would immediately violate same behaviour of $\nstatec_1$ and $\nstatec_2$:

$\dbeh{\dtpair{\itracep}{\idtracep}} \in \nbehof{\prog}{\nstatee_1} \setminus \nbehof{\prog}{\nstatee_2}$
$\dbeh{\dtpair{\tracem\lseq\itracep}{\dtracef\lseq\idtracep}} \in \nbehof{\prog}{\nstatec_1} \setminus \nbehof{\prog}{\nstatec_2}$.

Snippyness then yields the simulation interval $(\nstatec_2, \nstated_2) \synctrans{\tracem}{\dtracef}{\tracek}{\dtracee} (\nstatee_2, \nstatef_2)$,
i.e. $\nstated_2 \ntranss{\tracek}{\dtracee} \nstatef_2$.

<Ref> gives $\nstatef_1 \samepoint \nstatef_2$.

We can now apply (co-)induction hypothesis for $\nbehof{\tgtp}{\nstatef_1} \subseteq \nbehof{\tgtp}{\nstatef_2}$,
which implies $\tbeh{\dtpair{\tracek\lseq\tracel}{\dtracee\lseq\dtraced}} \in \nbehof{\tgtp}{\nstatef_2}$.

Together with $\nstated_2 \ntranss{\tracek}{\dtracee} \nstatef_2$, we arrive at $\tbeh{\dtpair{\tracek\lseq\tracel}{\dtracee\lseq\dtraced}} \in \nbehof{\tgtp}{\nstated_2}$.

§ CASE STUDY: DEAD CODE ELIMINATION

In this section, we prove that Dead Code Elimination $\tdconly$ satisfies $\propsnip$ as a warm-up for the next section,
where we do so for our fixed, more involved Register Allocation.

We first give a short recall on the transformation before crafting a snippy simulation for $\tdconly$ that is parametric in the source program $\prog$.

Dead Code Elimination is responsible for removing instructions from $\prog$ whose computed values are not utilized anywhere.

It is the result of a data flow analysis that finds removable instructions.

Typically, the analysis follows constant propagation in order to identify as many aliasing memory accesses as possible.

To support that, we assume that load and store instructions $\IWloadconst{\rega}{\vara}{\adr}$ and $\IWstoreconst{\vara}{\adr}{\regc}$ can hold a constant address $\adr \in \adrs$
instead of a register,
where we require $\adr \in \sizeof{\vara}$.

For this section, fix an arbitrary program $\prog$ with entry point $\entry$.

§.§.§ Flow analysis

The static analysis for Dead Code Elimination is a Liveness analysis.

Since we will later define our own flow analysis when fixing the weaknesses in register allocation, we recall flow analysis in a more general setting.

A flow analysis searches for a fixed-point solution to a system of flow inequalities in order to obtain approximate knowledge about all executions of a program.

Formally, a forward/backward flow analysis finds a solution $\flow$ to the inequalities eqn:flow-fwd/eqn:flow-bwd,
where $\pc$ and $\pcsuc$ range over program counters so that $\pc$ is a predecessor to $\pcsuc$.

\[
\begin{minipage}{.5\displaywidth}
\abovedisplayskip=0pt
\belowdisplayskip=0pt
\begin{equation}
\begin{split}
\flowof{\pcsuc} &\geq \transferof{\pc}{(\flowof{\pc})} \\
\flowof{\entry} &\geq \flowinit
\end{split}\label{eqn:flow-fwd}\tag{fwd}
\end{equation}
\end{minipage}
\begin{minipage}{.5\displaywidth}
\abovedisplayskip=0pt
\belowdisplayskip=0pt
\begin{equation}
\begin{split}
\flowof{\pc} &\geq \transferof{\pcsuc}{(\flowof{\pcsuc})} \\
\flowof{\pc} &\geq \flowinit \qquad\qquad \progof{\pc} = \Iexit
\end{split}\label{eqn:flow-bwd}\tag{bwd}
\end{equation}
\end{minipage}
\]

Flow values stem from a semi-lattice $(\lattice, \leq)$ and a solution $\flow : \pcs \to \lattice$ finds a flow value for each program point.

In case of a forward analysis, $\flowof{\pc}$ denotes the flow value at $\pc$ before the execution of $\progof{\pc}$.

For a backward analysis $\flowof{\pc}$ denotes the flow value at $\pc$ after the execution of $\progof{\pc}$.

The flow value $\flowinit$ is the initial flow value of entry / exit points of the program.

The functions $\transferat{\pc} : \lattice \to \lattice$ are monotonic and constitute the transfer of the flow values along instructions.

A flow analysis can have additional constraints.

Additional constraints are of shape $\flowof{\pc} \leq \latelem$.

They additionally require flow values of certain $\pc$ not to exceed a bound $\latelem \in \lattice$.

If the least solution to the flow analysis does not satisfy the additional constraints, then no solution does.

§.§.§ Dead Code Elimination

Liveness analysis is a backward flow analysis.

The flow values for are sets of registers and memory locations that are live at any given program point in that their current value will be used later.

The flow lattice is $\lattice = \powerset{\regs \cup \mems}$,
and the initial flow value at any exit point is $\flowinit = \regs\cup\mems$,
but can be different dependent on calling conventions.

The transfer functions are folklore, so we instead formulate the guarantee that comes with a solution.

Note that the guarantee holds for speculative semantics, too, because the analysis is branch-independent.

Whenever $\statec \ntranss{\tracel}{\dtraced} \nstatee\lseq\statee$ in $\prog$,
if $\progof{\statee}$ uses a register $\regb$, then $\regb \in \transferof{\pc}{(\flowof{\pc})}$,
and if $\progof{\statee}$ loads a memory location $\vara$ with offset $\adr$, then $(\vara, \adr) \in \transferof{\pc}{(\flowof{\pc})}$.

The transformation $\tdconly$ uses a Liveness analysis solution $\flow$ of the backward flow inequalities eqn:flow-bwd to remove unnecessary instructions.

A function $\tfdc : \lattice \to \instrs \to \instrs$ inspects the flow value at a given program point and removes an instruction if it writes a register or memory location that is not live.

The transformation of $\prog$ is then defined per program point with $\tdcof{\pc} = \tfdcof{(\flowof{\pc})}{(\progof{\pc})}$.

\begin{align*}
\tfdcof{\latelem}{(\Iasgn{\rega}{\regb \op \regc}{\pcsuc})} &=
\begin{cases}{}
\Inop{\pcsuc} & \rega \notin \latelem \\
\Iasgn{\rega}{\regb \op \regc}{\pcsuc} & \rega \in \latelem
\end{cases}
\tfdcof{\latelem}{(\Iload{\rega}{\vara}{\regb}{\pcsuc})} &=
\begin{cases}{}
\Inop{\pcsuc} & \rega \notin \latelem \\
\Iload{\rega}{\vara}{\regb}{\pcsuc} & \rega \in \latelem
\end{cases}
\\
\tfdcof{\latelem}{(\Istore{\vara}{x}{\regc}{\pcsuc})} &=
\begin{cases}{}
\Inop{\pcsuc} &x = \adr, (\vara, \adr) \notin \latelem \\
\Istore{\vara}{x}{\regb}{\pcsuc} & \text{otherwise}
\end{cases}
\tfdcof{\latelem}{\inst} &= \inst \quad \text{for other $\inst$}
\end{align*}

§.§.§ Dead Code Simulation

We now craft a snippy simulation $(\simrel, \dtffamily)$ between $\tdc$ and $\prog$.

The simulation is parametric in $\prog$ as it depends on the Liveness analysis $\flow$.

That way, we craft a single simulation relation and provide one for every source program $\prog$ and its transformation $\tdc$.

First, we define the simulation $\stated \simrel \statec$ and directive transformation $\dtfat{\statec}{\stated}$ for speculation-free states,
and afterwards lift them to speculating states.

The simulation identifies states whenever they differ only on dead registers and memory locations:

\begin{align*}
(\pc, \rasgn, \masgn) &\simrel (\pc, \rasgnp, \masgnp) &
&\iffsymb &
\begin{aligned}
\forall \rega\in\transferof{\pc}{(\flowof{\pc})}.\,
& \rasgnof\rega = \rasgnpof{\rega}\\
\forall (\vara, \adr)\in\transferof{\pc}{(\flowof{\pc})}.\,
& \masgnof{\vara}{\adr} = \masgnpof{\vara}{\adr}
\end{aligned}
\end{align*}

In order to define the directive transformation $\dtfat{\statec}{\stated}$,
we need to think about the shape of simulation intervals.

Because $\tdconly$ leaves the control flow fully intact,
we can choose to create a lockstep simulation.

With that, we can choose $\dtfat{\statec}{\stated}$ to be the identity relation on $\directs$
and add transformations where $\tdconly$ replaced an instruction with $\IWnop$.

Let $\inst = \instof{\statec}$ and $\instp = \tdcof{\stated}$.

We set:

\begin{align*}
{\dtfat{\statec}{\stated}} & = \identity{\directs} \cup
\begin{cases}
\setcond{(\Dload{\varb}{\adrp}, \Dstep)}{\varb \in \vars, \adrp \in \adrs} & \inst = \Iload{\rega}{\vara}{\regb}{\pcsuc}, \;\;\instp = \Inop{\pcsuc} \\
\setcond{(\Dstore{\varb}{\adrp}, \Dstep)}{\varb \in \vars, \adrp \in \adrs} & \inst = \Istore{\vara}{\regb}{\regc}{\pcsuc}, \;\;\instp = \Inop{\pcsuc} \\
\varnothing & \text{otherwise}
\end{cases}
\end{align*}

For speculating states, we simply lift $\simrel$ by setting $\nstated\lseq\stated \simrel \nstatec\lseq\statec$ if $\nstated \simrel \nstatec$ and $\stated \simrel \statec$ (and $\varepsilon \simrel \varepsilon$ for the base case).

For the directive transformation, we delegate to the executing states ${\dtfat{\nstatec\lseq\statec}{\nstated\lseq\stated}} = {\dtfat{\statec}{\stated}}$.

$(\simrel, \dtffamily)$ is a snippy lockstep simulation.

We need to prove that $(\simrel, \dtffamily)$

*  is a simulation (<Ref>),

*  is snippy (<Ref>),
*  respects $\lows$ (<Ref>).

The first part item:dcissim is considerably easier than in the general case, because the simulation is lockstep,
i.e. both $\prog$ and $\tdc$ only perform a single step before finding new states in $\simrel$.

Consider $\nstated_1\lseq\stated_1 \simrel \nstatec_1\lseq\statec_1$,
$\nstated_2\lseq\stated_2 \simrel \nstatec_2\lseq\statec_2$,
$\nstated_1 \lseq\stated_1 \samepoint \nstated_2 \lseq\stated_2$
$\nstatec_1 \lseq\statec_1 \samepoint \nstatec_2 \lseq\statec_2$
$\nstated_1 \lseq\stated_1 \ntrans{\leak}{\direct} \nstatef_1$.

We need to show that there is
$\directp \dtfat{\statec_1}{\stated_1} \direct$
so that $\nstatec_1\lseq\statec_1 \ntrans{\leakp}{\directp} \nstatee_1$
and $\nstatef_1 \simrel \nstatee_1$.

Second we prove snippyness item:dcissnippy:
We additionally consider the existence of $\nstatec_2\lseq\statec_2 \ntrans{\leakp}{\directp} \nstatee_2$.

We then need to show that $\nstated_2\lseq\stated_2 \ntrans{\leak}{\direct} \nstatef_2$
and $\directp \dtfat{\statec_2}{\stated_2} \direct$ (which implies $(\statec_2, \stated_2) \synctrans{\leak}{\direct}{\leakp}{\directp} (\statee_2, \statef_2)$).

We first split off the case $\direct = \directp = \Drb$, where $\sizeof{\nstated_1} > 0$.

For item:dcissim, we need to prove $\nstatec_1\lseq\statec_1 \ntrans{\Erb}{\Drb} \nstatec_1$ because $\Drb \dtfat{\statec_1}{\stated_1} \Drb$.

But $\nstated_1 \simrel \nstatec_1$ implies $\sizeof{\nstated_1} = \sizeof{\nstatec_1} > 0$ which meets the premise for the transition.

For item:dcissnippy, additionally consider $\nstatec_2 \lseq \statec_2 \ntrans{\Erb}{\Drb} \nstatec_2$.

We need to show $\nstated_2\lseq\stated_2 \ntrans{\Erb}{\Drb} \nstated_2$.

With the same argument as before, $\sizeof{\nstated_1} = \sizeof{\nstatec_1} = \sizeof{\nstatec_2} = \sizeof{\nstated_2} > 0$ satisfies the premise for the transition.

Proving item:dcissim,item:dcissnippy in the case of $\direct \neq \Drb \neq \directp$ is a large case distinction on $\langle\progof{\pc}, \tdcof{\pc}\rangle$.

There are two subcases: $\rasgniof{\statec_1}{\regb} = \adr$ is within $\sizeof{\vara}$ or not.

We present the subcase $\adr \notin \sizeof{\vara}$.

For item:dcissim, consider $\stated_1 \trans{\Enone}{\Dstep} \statef_1$.

We need to show that $\Dload{\varb}{\adrp}$ is executable in $\statec_1$,
because $\Dload{\varb}{\adrp} \dtfat{\statec_1}{\stated_1} \Dstep$.

Indeed, we have $\statec_1 \trans{\Eload{\adr}}{\Dload{\varb}{\adrp}} \statee_1$ because $\rasgniof{\statec_1}{\regb} = \adr \notin \sizeof{\vara}$.

We also need to show that $\statef_1 \simrel \statee_1$.

From the definition of $\tfdc$, we know $\rega \notin \flowof{\pc}$ because the instruction was replaced by $\IWnop$.

The transfer $\transferof{\pc}{(\flowof{\pc})}$ is again $\flowof{\pc}$
because a load to a dead register makes no registers or memory locations live.

Together with eqn:flow-bwd, we get $\transferof{\pc}{(\flowof{\pc})} = \flowof{\pc} \supseteq \transferof{\pcsuc}{(\flowof{\pcsuc})}$.

Registers and memory of $\stated_1$ and $\statef_1$ are equal ($\IWnop$)
and $\statec_1$ and $\statee_1$ only differ on $\rega$.

This means $\stated_1 \simrel \statec_1$ implies $\statef_1 \simrel \statee_1$ because $\rega \notin \flowof{\pc} \supseteq \transferof{\pcsuc}{(\flowof{\pcsuc})}$.

For item:dcissnippy, further consider $\statec_2 \trans{\Eload{\adr}}{\Dload{\varb}{\adrp}} \statee_2$.

We need to show that $\stated_2 \trans{\Enone}{\Dstep} \statef_2$ and $\statef_2 \simrel \statee_2$.

The former is immediate from semantics.

For the latter, we apply the same arguments as in item:dcissim.

All other cases are very similar.

For item:dcissecrespecting, we need to restrict us to Liveness analysis where all registers and memory locations are initially live.
[A weaker formalization of $\sec$-respecting relations would lift this restriction, but incur more presentational overhead.]

Every solution $\flow$ is easily modified to satisfy this restriction.

The proof that $\simrel$ respects $\sec$ is then straightforward:

For initial states $\stated$ and $\statec$, $\stated \simrel \statec$ if and only if $\stated = \statec$.

§ FIXING WEAKNESSES IN REGISTER ALLOCATION

Register allocation happens in the compilation phase that moves from an IR to the hardware instructions of the target architecture.

It reduces the unbounded amount of virtual registers in the IR to the finite set of hardware registers.

In order to do so, register allocation performs a relocation of register contents.

For each program point, a subset of the virtual registers is selected to be kept as hardware registers and the remaining virtual registers are spilled to memory locations on the stack.

There are various approaches to register allocation in the literature

Traditional approaches find relocations with graph-coloring chaitinRegisterAllocationColoring1981.

Modern approaches tend towards faster, simpler algorithms and rely on sophisticated heuristics to reduce the overhead of inserted instructions from spilled variables
tichadouRegisterAllocation2022,polettoLinearScanRegister1999,traubQualitySpeedLinearscan1998.würdest du das alles citen?

In this paper, we express register allocation as a set of constraints the relocation has to satisfy.

That makes our results indifferent to the implemented version.

We first present the constraints a register allocation needs to satisfy.

We then demonstrate how register allocation violates speculative non-interference preservation.

We continue to develop a static analysis that finds potential weaknesses.

Finally, we fix the violations and craft a snippy simulation for the fixed register allocation to prove that the transformation satisfies $\propsnip$.

§.§ Characterizing Register Allocation

Register allocation transforms a source program $\prog$ by inserting shuffle instructions.

The instructions are inserted in between the existing instructions and maintain the register relocation.

\begin{align*}
\text{\itshape Shuffle Inst} &&
\shuffleinstcmd & \,\,\Coloneq\,\, \Imove{\rega}{\regb}{\pcsuc}
\bnfalt \Ifill{\rega}{\stackl}{\pcsuc}
\bnfalt \Ispill{\stackl}{\rega}{\pcsuc}
\bnfalt \Islh{\rega}{\pcsuc}
\bnfalt \Isfence{\pcsuc}
\end{align*}

§.§.§ Shuffle Instructions

We extend $\instrs$ with new shuffle instructions: Move, fill, and spill.

We also include $\IWslh{\rega}$ and $\IWsfence$ because we need them later to fix weaknesses in register allocation.

The semantics are as expected:

A move $\Cmove{\rega}{\regb}$ relocates contents from $\regb$ to $\rega$,
$\Cfill{\rega}{\stackl}$ reloads a spilled register from a constant address $\stackl \in \adrs$ in the stack,
and $\Cspill{\stackl}{\regb}$ spills a register to the stack.

We model the stack frame's section used for spilled registers in our syntax and semantics with a fresh memory variable $\varstack$ not occurring in $\prog$.

We assume that $\varstack$ has appropriate size to fit all spilled registers and is typed $\lowsof{\varstack} = \low$.

Shuffle code inserted between two instructions of $\prog$ is fully straight line.

We introduce the notion $\progof{\pc} = \shufseq{\pcsuc}$ to express that $\prog$ executes the shuffle sequence $\shufseqcmd$ and then ends in $\pcsuc$.

It states that either $\shufseqcmd = \varepsilon$ and $\pcsuc = \pc$
or $\shufseqcmd = \shuffleinst\lseq\shufseqp{\pcsuc}$
and $\progof{\pc} = \shuffleinst$,
the successor of $\shuffleinst$ is $\pcss$,
and $\progof{\pcss} = \shufseqp{\pcsuc}$.

§.§.§ Characterizing Register Allocation

Register allocation inserts shuffle code between existing instructions to realize the register relocation.

Formally, a target program $\tra : \pcsof{\tra} \to \instrs$ is a register allocation if there is a pair of functions $(\instinj, \regmap)$.

The first function is an injection $\instinj : \pcsof{\prog} \to \pcsof{\tra}$ of the original instructions of $\prog$ to their counterpart in $\tra$.

The second function is a relocation mapping $\regmap : \pcsof{\tra} \to \regs \partialto (\regs \cup \stack)$,
where $\stack = \setcond{(\varstack, \stackl)}{\stackl \in \sizeof{\varstack}} \subseteq \mems$ is the stack frame for spilled variables.

At each program counter $\pcp \in \pcsof{\tra}$, $\regmapofof{\pcp}{\rega}$ is the relocation of the virtual register $\rega$ from $\prog$ to the hardware register or stack location in $\tra$.
[In general, the content of a register $\rega$ could be relocated to multiple locations. For simplicity of presentation, we forbid that.]

The functions are subject to the following conditions.

Instruction matching: The $\instinj$-injected instructions must operate on the same registers up to relocation by $\regmap$.

Shuffle conformity: The relocation $\regmap$ must conform to the (shuffle) instructions in $\tra$.

Obeying Liveness: Every live register in $\prog$ is mapped under $\regmap$ and no location is doubly allocated.

To state the conditions formally, we introduce notation for the defined and used registers of an instruction.

A register $\regb$ is used by $\inst\in\instrs$ if the register is read out by the corresponding rule in <Ref>.

Similarly, $\rega$ is defined by $\inst$, if it is written in that rule.

For example, $\IWload{\rega}{\vara}{\regb}$ uses $\set{\regb}$ and defines $\set{\rega}$.

\begin{align*}
\usesof{\inst} & = \setcond{\regb}{\text{$\regb \in \regs$ is used by $\inst$}}
\defof{\inst} & = \setcond{\rega}{\text{$\regb \in \regs$ is defined by $\inst$}}
\end{align*}

[float,label=code:ra]An Example Register Allocation. Lines b and e are the inserted shuffle code.
[height=0pt,after skip=0pt]Source $\prog$aa

a = (b < buf_size)

br (a)|$\NextInst{\mkern1mu\makepc{3},\;\makepc{4}}$|
buf[b] = secret

br (bytes)|$\NextInst{\mkern1mu\makepc{5},\;\makepc{5}}$|

[height=0pt,after skip=0pt]Target $\tra$

a = (b < buf_size)
stk[0] = bytes
br (a)|$\NextInst{\mkern1mu\makepc{d},\;\makepc{e}}$|
buf[b] = secret
a = stk[0]
br (a)|$\NextInst{\mkern1mu\makepc{g},\;\makepc{g}}$|

Instruction Matching requires that source instructions from $\prog$ reappear in $\tra$:

For every $\pc \in \pcsof{\prog}$ and $\pcp = \instinjof{\pc}$, $\inst = \progof{\pc}$ has to match with $\instp = \traof{\pcp}$.

To match, the instruction $\instp$ must be the same,
but registers $\regb \in \usesof{\inst}$ are replaced with $\regmapofof{\pcp}{\regb} \in \regs$.

Similarly, registers $\rega \in \defof{\inst}$ are replaced with $\regmapofof{\pcsucp}{\rega} \in \regs$,
where $\pcsucp$ is the successor of $\pcp$.

Defined registers are found in the successor's relocation, because they are live only after executing $\instp$.

All other instructions at program points $\pcp \notin \imgof{\instinj}$ must be shuffle instructions.

Given $\statec \in \statesof{\prog}$ and $\stated \in \statesof{\tra}$,
we write $\statec \defrinstinj \stated$ when $\statec \atpc \pc$ and $\instinjof{\pc} \atpc \stated$.

We extend the notation to $\nstatec \rinstinj \nstated$ in the expected way.

Shuffle Conformity requires that the relocation $\regmap$ is upheld by the instructions in $\tra$.

Consider an instruction $\instp = \traof{\pcp}$ at $\pcp \in \pcsof{\tra}$ and let $\pcsucp$ be a successor.

First, registers and stack locations untouched by $\instp$ must stay at the same location in $\regmap$:

For any register $\regd$ with $\regmapofof{\pcp}{\regd} \notin \usesof{\instp}$
and $\regmapofof{\pcsucp}{\regd} \notin \defof{\instp}$,
$\regmapofof{\pcp}{\regd} = \regmapofof{\pcsucp}{\regd}$.

Second, if $\instp$ is a shuffle instruction there are additional requirements:

Shuffle instructions move one source register's content from one location in $\tra$ to another.

As a consequence, if $\instp$ is a shuffle instruction, there must be a source register $\rega$ being moved.

Further, each shuffle instruction moves only to free locations.

We write $\freeof{\pcssp}{\regdp}$ and $\freeof{\pcssp}{(\varstack, \stackl)}$ for $\regdp, (\varstack, \stackl) \notin \imgof{\regmapof{\pcssp}}$.

Dependent on $\instp$, we have the following constraints, where $\rega$ is the moved source register:

\begin{align*}
\instp & = \Imove{\regap}{\regbp}{\pcsucp} \\
\instp & = \Ifill{\regap}{\stackl}{\pcsucp} \\
\instp & = \Ispill{\stackl}{\regbp}{\pcsucp} \\
\instp & = \Islh{\regap}{\pcsucp} \\
\end{aligned}
\begin{alignedat}{3}
&\regmapofof{\pcp}{\rega} = \regbp &&\land \regmapofof{\pcssp}{\rega} = \regap &&\land \freeof{\pcp}{\regap} \\
&\regmapofof{\pcp}{\rega} = (\varstack, \stackl) &&\land \regmapofof{\pcssp}{\rega} = \regap &&\land \freeof{\pcp}{\regap} \\
&\regmapofof{\pcp}{\rega} = \regbp &&\land \regmapofof{\pcssp}{\rega} = (\varstack, \stackl) &&\land \freeof{\pcp}{(\varstack, \stackl)} \\
&\regmapofof{\pcp}{\rega} = \regap &&\land \regmapofof{\pcssp}{\rega} = \regap
\end{alignedat}
\end{align*}

Obeying Liveness means that all live variables in $\prog$ must be allocated.

There must be a Liveness solution $\flow$ (<Ref>) for $\prog$
so that for all locations $\pc \in \pcsof{\prog}$,
all registers $\rega \in \flowof{\pc}$ live at $\pc$
are allocated, i.e. $\regmapofof{(\instinjof{\pc})}{\rega} \neq \bot$.

Further, a location cannot be allocated twice,
i.e. for all $\pc \in \pcsof{\tra}$, $\regmapof{\pc}$ forms an injection on the live registers at $\pc$.

A transformation from $\prog$ to $\tra$ is a register allocation
if there are instruction matching, shuffle conform, and Liveness obeying $(\instinj, \regmap)$.

<Ref> contains an example register allocation.
It is a simplified version of <Ref>, which still exhibits the weakness of register allocation.
The left program holds starts with a secret value in register secret and public values in b and bytes.
It stores the secret into buf when the address b is in bounds of $\sizeof{\makevar{buf}}$.
Then, it leaks bytes at 4.
The right program is after Register Allocation.
Register allocation has inserted the spill and fill instructions b and e.
The instruction injection $\instinj$ can be seen from side by side alignment.
It is the mapping $\set{\makepc{1} \mapsto \makepc{b},\makepc{2} \mapsto \makepc{c},\makepc{3} \mapsto \makepc{d},\makepc{4} \mapsto \makepc{f},\makepc{5} \mapsto \makepc{g}}$.
The register mapping $\regmap$ at a and b makes no relocations: $\regmapof{\makepc{a}} = \regmapof{\makepc{b}} = \identity{\regs}$.
The spill instruction at b relocates bytes to the stack.
It remains spilled from c to e: $\regmapofof{\makepc{c}}{\makereg{bytes}} = \ldots = \regmapofof{\makepc{e}}{\makereg{bytes}} = (\makevar{stk},0)$.
Further, because a is not live after 2
it is not allocated from c to g: $\regmapofof{\makepc{c}}{\makereg{a}} = \ldots = \regmapofof{\makepc{g}}{\makereg{a}} = \bot$.
Instead, the register allocation reuses a in f:
The fill instruction at e relocates bytes to a: $\regmapofof{\makepc{f}}{\makereg{bytes}} = \makereg{a}$.

§.§ Register Allocation is not SNIP

Register allocation is known to be non-interference preserving, provided that the semantics are speculation-free bartheStructuredLeakageApplications2021,bartheFormalVerificationConstanttime2019.

We first assumed that the same is true for speculative semantics as well,
because register allocations only inserts shuffle instructions.

While shuffle instructions produce leakages,
they are constant address loads and stores
which means they only leak constant values.

To our surprise, when we tried to form a snippy simulation relation for register allocation,
we realized that it was not $\propsnip$.

<Ref> demonstrates a minimalistic example for how register allocation introduces weaknesses into $\tra$.

The left program is $\propsni$,
because the leakage at Line 4 depends on the register bytes that holds a public value untouched from the start of the execution.

The right program, however, is susceptible to the same attack as described in <Ref> for <Ref>:

Speculatively executing c when b holds a value out of $\sizeof{\makevar{buf}}$ can store the secret value in secret to .

That value is then loaded at e into a and leaked at f.

The fault for this attack is not with the constant leakage of shuffle instructions.

The weakness occurs from relocation of registers to memory:

Conceptually, speculative execution can access memory everywhere because it performs unsafe memory accesses.

But it cannot read or write register contents.

Register allocation moves registers into memory, effectively granting unsafe memory operations access to spilled registers.

We were able to reproduce the weakness with a real compiler.

<Ref> is inspired by <Ref>
which is an excerpt of the  function  with slight modifications.

Compiling it without optimizations on [Targeting  with only  and default  register allocator.]
inserts the instructions in <Ref>.

§.§ Poison-Tracking Product

We present a product construction for a static analysis that reveals weaknesses like <Ref> in register allocated programs.

To motivate the following product construction,
we inspect the existing simulations
that work for register allocation under speculation-free semantics,
and explain why they fail under speculative semantics.

Intuitively, a simulation for register allocation matches a state $\statec$ of the source program $\prog$
to a state $\stated$ of the target program $\tra$
whenever the instruction is matched, $\statec \rinstinj \stated$,
and the values of all registers and memory locations in $\statec$ and $\stated$ are equal up to relocation by $\regmap$.

Relying on the memory safety of $\prog$ under speculation-free semantics,
one can then prove that any instruction executed from $\stated$ can be replayed from $\statec$.

The simulation preserves non-interference:

Apart from the inserted shuffle instructions' leakage (which are constant adresses),
the leakage that arises from execution in $\stated$ is equal to the leakage from $\statec$.

The previous section showed that it is not enough to just extend this approach to speculating states:

Speculation introduces unsafe memory accesses to $\regmap$-mapped stack locations in $\tra$.

Such an access cannot be simulated by $\prog$, as it has the accessed value in a register.

As a result, if we executed $\prog$ and $\tra$ in parallel we will eventually see speculating states $\nstatec$ and $\nstated$ with different values in registers of $\nstatec$ and their $\regmap$-mapped location in $\nstated$.

Further execution then propagates those differences to other locations.

The goal in fixing register allocation is to make sure that differences in value do not lead to leakage of sensible data.

An immediate mitigation would be to insert an $\IWsfence$ instruction before every load and store operation.

This would eliminate speculating unsafe memory accesses altogether.

However, this introduces a many $\IWsfence$ instructions and reduces performance more than necessary.

Instead, we construct a product of $\prog$ and $\tra$ that tracks differences in values between $\nstatec$ and $\nstated$.

We call registers and memory locations that hold different values poisoned,
because leaking them in $\tra$ might be unsafe:

If $\nstatec$ and $\nstated$ execute an instruction that leaks the value of a poisoned register,
we cannot rely on $\prog$ being $\propsni$ to justify that the leakage from $\nstated$ is safe.

Leakage of healthy (not poisoned) registers, however, is safe for that reason.

As a result, we only need to protect instructions that leak a poisoned register's value.

§.§.§ Poison types

Poison types represent the registers and memory locations where $\prog$ and $\tra$ can have different values.

Consider states $\statec \in \statesof{\prog}$ and $\stated \in \statesof{\tra}$.

A poison type $\poison \in \ptypes$ is a function $(\regs \cup \mems \setminus \stack) \to \pvals$.

It assigns a poison value to each register and memory location of $\statec$.

The poison values $\pvals = \set{\poisoned, \weakpoisoned, \healthy}$ have the following meaning:

Healthy registers and memory locations ($\healthy$) are equal between $\statec$ and $\stated$ up to relocation by $\regmap$.

Poisoned registers and memory locations ($\poisoned$) can differ between $\statec$ and $\stated$ up to relocation by $\regmap$.

Finally, registers and memory locations can be weakly poisoned ($\weakpoisoned$).

This poison value is introduced because of $\IWslh{\rega}$.

If $\IWslh{\rega}$ occurs as a shuffle instruction, executing it speculatively sets $\rega$ to 0.

But because it is a shuffle instruction it does not occur in $\prog$.

That makes $\rega$'s value different between $\prog$ and $\tra$.

However, every execution in $\tra$ that executes this shuffle instruction speculatively also sets $\rega$ to 0.

This makes it safe to leak in $\tra$, even though the value differs between $\prog$ and $\tra$.

We thus type registers and memory locations that hold a 0 due to an $\IWslh{\rega}$ instruction weakly poisoned ($\weakpoisoned$).

Formally, we express that states $\statec \in \statesof{\prog}$ and $\stated \in \statesof{\tra}$ are equal up to a poison-type $\poison$ and relocation $\regmap$
with the notation $\statec \nrrmp{\poison} \stated$.

We then extend the notation to speculating states $\nstatec \in \nstatesof{\prog}$ and $\nstated \in \nstatesof{\tra}$ of equal speculation depth $\sizeof{\nstatec} = \sizeof{\nstated}$.

For that, we have sequences of poison types $\pseq \in \ptypes^*$,
one poison type for each level of speculation $\sizeof{\nstatec} = \sizeof{\nstated} = \sizeof{\pseq}$.

To formalize the notation $\nstatec \nrrmp{\pseq} \nstated$,
write $\pvof{\pval}{\poison}$ for the set of all registers and memory locations typed $\pval$ by $\poison$,
$\pvof{\pval}{\poison} = \setcond{ \rega, (\vara, \adr) }{\poisonof{\rega} = \pval, \pmemof{\vara}{\adr} = \pval}$.

Further, we write $\evalin{\stated}{\rega} = \rasgniof{\stated}{\rega}$ and $\evalin{\stated}{(\vara, \adr)} = \masgniof{\stated}{\vara}{\adr}$.

Let $\statec = (\pc, \rasgn, \masgn) \in \statesof{\prog}$ and $\stated = (\pcp, \rasgnp, \masgnp) \in \statesof{\tra}$ range over states of $\prog$ and $\tra$.

We define:

\begin{align*}
\begin{aligned}
& \statec \defnrrmp{\poison} \stated \\
& \ifftxt
\end{aligned}
\begin{alignedat}{3}
&& \forall \rega \in \pvof{\healthy}{\poison}.\, &\rrmat{\stated}{\rega} = \rasgnof{\rega} \\
&{}\land{}&\forall \rega \in \pvof{\weakpoisoned}{\poison}.\,& \rrmat{\stated}{\rega} = 0 \\
&{}\land{}&\forall (\vara, \adr) \in \pvof{\healthy}{\poison}.\,& \masgnpof{\vara}{\adr} = \masgnof{\vara}{\adr} \\
&{}\land{}&\forall (\vara, \adr) \in \pvof{\weakpoisoned}{\poison}.\,& \masgnpof{\vara}{\adr} = 0
\end{alignedat} \label{def:nrrmp}
\begin{aligned}
&\nstatec\lseq\statec \nrrmp{\pseq\lseq\poison} \nstated\lseq\stated \\
\end{aligned}
\begin{alignedat}{3}
&&&\nstatec \nrrmp{\pseq} \nstated \\
&{}\land{}&& \statec \nrrmp{\poison} \stated
\end{alignedat}
\end{align*}

The definition of $\statec \nrrmp{\poison} \stated$ meets the intuition:
Healthy registers and memory locations need to coincide between $\statec$ and $\stated$ and weakly poisoned locations must be 0 in $\stated$.

For poisoned locations, there are no requirements.

For speculating states, the definition is applied at each speculation level.

We write $\healthy$, $\weakpoisoned$, and $\poisoned$ for the poison types that assign the respective poison value everywhere.

We want to observe the differences in value in the attack from <Ref> in <Ref> when running $\prog$ and $\tra$ side by side.

The register allocation $(\instinj, \regmap)$ is already described in <Ref>.

The initial states are $\statec = (\makepc{1}, \rasgn, \masgn)$ and $\stated = (\makepc{a}, \rasgn, \masgn)$,
so that $\rasgnof{\makereg{b}} \notin \sizeof{\makevar{buf}}$ and $\rasgnof{\makereg{secret}} = \val \neq \rasgnof{\makereg{bytes}}$.

For ease of presentation, we also assume that already $\rasgnof{\makereg{a}} = \bfalse$ (so that the updates in 1 and a have no effect).

After executing the store instruction at 3 with the directive $\Dstore{\makevar{buf}}{0}$,
$\prog$'s state is $\statee = (\makepc{4}, \rasgn, \subst{\masgn}{(\makevar{buf},\adr)}{\val})$.

Similarly, after executing the store instruction at $\makepc{d}$ with the directive $\Dstore{\makevar{stk}}{0}$,
$\tra$'s state is $\statef = (\makepc{e},\rasgn,\subst{\masgn}{(\makevar{stk}, 0)}{\val})$.

We see a difference in the register bytes:

At $\makepc{e}$, it is still located in $\regmapofof{\makepc{e}}{\makereg{bytes}} = (\makevar{stk}, 0)$ due to the spill at b.

But the values differ with $\rasgnof{\makereg{bytes}} \neq \val = \masgnof{\makevar{stk}}{0}$,
because of the unsafe store to stk.

With a poison type that is fully healthy, except on $(\makevar{stk}, 0)$, i.e. $\poison = \subst{\healthy}{(\makevar{stk}, 0)}{\poisoned}$,
we have $\statee \nrrmp{\poison} \statef$.

(, , )

(, , )

= (, )

= ,(,)

(, , )

(, , )

(, , )
(, , , (, _1))

[label=rules:ploads]Loads$\instof{\statec} = \Iload{\rega}{\vara}{\regb}{\pcsuc}$

(, , )
(, , )

(, , )
(, , )

(, , )

(, , )

(, , )

(, , )

[label=rules:pstores]Stores$\instof{\statec} = \Istore{\vara}{\regb}{\regc}{\pcsuc}$

(, ), (, 0)

(, , )
(, , )

(, , )
(, , (,),(,0))

(, )

(, , )

(, , )

(, , )

(, , (, ))

(, , )
(, , )

(, , )
(, , )

(, , )
(, , )

(, , )
(, , )

=  0

(, , )
(, , )

[label=rules:pspec]Speculation Sensitive

(, , )

(, , )

(, , )

(, , )

=  =  ≥1

(, , )

(, , )

= __

(, , )

(, , )

(, , )

(, , )

=  0

(, , )

(, , )

§.§.§ Poison product

The poison product $\prodra$ tracks how poison types are updated
when executing $\prog$ and $\tra$ side by side.

We design the side by side execution so that transitions in $\tra$ are replayed by $\prog$.

We later want to craft a simulation from the product,
so every transition of $\tra$ must be included in $\prodra$.

However, when a transition of $\tra$ can be replayed by multiple transitions in $\prog$,
which happens when $\prog$ performs an unsafe memory access,
we choose a memory location for the access so that the transition poisons as little registers and memory locations as possible.

The states of $\prodra$ take the shape $(\nstatec,\nstated,\pseq)$
with $\nstatec \in \nstatesof{\prog}$, $\nstated \in \nstatesof{\tra}$, $\pseq \in \ptypes^*$,
and $\nstatec \nrrmp{\pseq} \nstated$
(which already implies $\sizeof{\nstatec} = \sizeof{\nstated} = \sizeof{\pseq}$).

There are two types of states:
Instruction-matched states and shuffling states.

Instruction-matched states satisfy $\nstatec \rinstinj \nstated$.

Shuffling states have $\nstated$ at a shuffle sequence after which the states would be instruction-matched again.

That is, $\nstatec = \nstatecp\lseq\statec$ and $\nstated = \nstatedp\lseq\stated$,
so that $\traof{\stated} = \shufseq{\pcsuc}$ with $\instinjof{\statec} = \pcsuc$.

Each type of state has transitions in $\prodra$:

\begin{align*}
(\nstatec, \nstated, \pseq) &\sprodtrans{\leakp}{\directp}{\leak}{\direct} (\nstatee, \nstatef, \pseqp) &
(\nstatec, \nstated, \pseq) &\sprodtrans{\varepsilon}{\varepsilon}{\leak}{\direct} (\nstatec, \nstatef, \pseqp)
\end{align*}

The first type of transition is enabled only for instruction-matched $\nstatec \rinstinj \nstated$.

It executes a transition simultaneously in both programs via $\nstatec \ntrans{\leakp}{\directp} \nstatee$ and $\nstated \ntrans{\leak}{\direct} \nstatef$.

The second type is enabled only for shuffling states.

In that case, $\nstatec$ stutters while $\nstated$ progresses through the shuffle sequence.

In both cases, the transition needs to update the poison values depending on the transition rules taken in $\prog$ and $\tra$.

We present how $\prodra$ updates poison values in <Ref>.

We mirror the approach in the semantics and provide the updates in two steps.

In a first step, we define the updates for instruction-matched, speculation-free states in <Ref>.

They represent the transitions for the speculation-free semantics (<Ref>).

In the second step we lift the speculation-free updates with <Ref>
to define the transitions of the product on the speculative semantics (<Ref>).

<Ref> defines the transitions for shuffling states.

The instruction-matched transitions for $\IWnop$, $\IWasgn{\rega}{\regb}{\regc}$ and $\IWif{\regb}$ can be found in the appendix.

We explain the transitions in detail.

The transitions rule:pintro-load,rule:pintro-store are the source of poison values.

They represent the situation from above, where we argued that values between $\prog$ and $\tra$ can differ:

In rule:pintro-load a target program's speculating unsafe load (recognizable from the directive $\Dload{\varstack}{\adrp}$) loads from a spilled register's stack location.

The source program cannot perform that load and thus has to perform any other unsafe load.

This leads to different loaded values and poisons the register loaded to.

While we could choose the location of the unsafe access in $\prog$,
the register is poisoned in either case, so we allow arbitrary unsafe loads in $\prog$.

Similarly, in rule:pintro-store a speculating unsafe store poisons the overwritten memory location from the source program.

Again, the source program can not replay that store and needs to store somewhere else.

In this case, we always let the source program store to $\vara$ instead,
because it reduces the number of poisoned memory locations for static analysis.

The overwritten register and the memory location are both poisoned.

Notice how both rules require the source program to access memory unsafely, as well.

This is because the register holding the offset address must be healthy, $\pregof{\regb} = \healthy$,
and thus has the same value in $\statec$ and $\stated$.

The address must be healthy, because a poisonous address could be unsafe to leak.

A weakly poisoned address, on the other hand, would be 0 in $\tra$ which is always a safe access.

This is because we chose $\IWslh{\rega}$ to wipe a register to 0.

Any other constant would work the same way, but the number of rules in the product would increase.

<Ref> for instruction-matched transitions just propagate already poisoned registers and memory locations.

For example, rule:pload-hsafe considers the case where the addressing register is healthy.

That means, that both, source and target program load from the same memory location.

We can recognize from the premise that the memory access is safe:
Source and target program execute the load with the directive $\Dstep$, so they execute with rule:load.

The rule then propagates the poison value from the memory location loaded from to the register loaded to.

As before, the product transition can only be taken when the leaked content is not poisoned as that could represent an unsafe leakage.

The case of a weakly poisoned address is separately handled by rule:pload-ss,rule:pload-us.

<Ref> propagate poison values for stores.

<Ref> provides the poison updates for instruction-matched states that execute speculation sensitive instructions.

<Ref> lifts the speculation-free transitions to the speculative setting.

rule:hspec forbids weakly poisoned branching conditions even though they are safe to leak.

This is to avoid that $\prog$ and $\tra$ arrive at different program points (up to $\instinj$).[Branching on weakly poisoned registers could be supported but further complicates the product definition.]

Branching with weakly poisoned registers could be supported by letting one state speculate while the other does regular branching to keep them at the same program point.
However, this would violate the condition $\sizeof{\nstatec} = \sizeof{\nstated}$ and leads to a less intuitive product definition.

rule:pslh creates healthy values when the product is speculating, because source and target program both wipe the register to 0.

If not speculating, the poison values are untouched.

<Ref> provides the second type of transitions, for shuffling states, in $\prodra$.

The speculation insensitive shuffle instructions are again brought to speculating states with rule:pstep.

The insensitive shuffle instructions only move values and don't modify them.

There is no need to update the poison type because the relocation is already included in $\regmap$ with shuffle conformity.

Thus, the poison type is untouched.

Only rule:pshuf-slh can be a new source of poisoned values.

As discussed earlier, when speculatively executed, it wipes the register's value to 0, which makes it weakly poisoned.

On speculation-free states, $\IWsfence$ and $\IWslh{\regap}$ do not update the poison type.

The transitions of $\prodra$ are well-defined in the sense that executing a transition leads to a state that again satisfies the constraints of being a state (<Ref>).

Also, the speculation-free states never become poisoned,
because rule:pintro-load,rule:pintro-store can not happen:

$\prog$ is memory safe under speculation-free semantics.

Further, the only other rule to introduce poison values is rule:pshuf-slh,
but it introduces no poison value in speculation-free states.

Given $(\nstatec, \nstated, \pseq)$ and a transition $(\nstatec, \nstated, \pseq) \sprodtrans{\leakp}{\directp}{\leak}{\direct} (\nstatee, \nstatef, \pseqp)$,
then $\nstatee \nrrmp{\pseqp} \nstatef$.

Speculation-free states are never poisoned.
I.e. $(\statec, \stated, \healthy) \sprodtranss{\tracek}{\dtracee}{\tracel}{\dtraced} (\statee, \statef, \poison)$
implies $\poison = \healthy$.

Consider the execution of $\prodra$ in <Ref>.

It depicts the side by side execution from <Ref> in $\prodra$.

Each state of $\prodra$ is depicted as a small table listing the program counters of $\prog$ and $\tra$,
the values of the registers (we use $\bfalse$ for a value other than 0)
and the relevant memory locations.

The right column contains the poison type associated with the pair of states.

The first transition simultaneously executes the instruction-matched assignment at 1 and a.

Second follows the shuffle instruction that spills bytes to $\makevar{stk}[0]$ at b, while $\prog$ waits.

The third transition speculates.

Notice that rule:hspec only admits this transition because a is $\healthy$.

The next transition is the unsafe store to stk in $\tra$,
overwriting the spilled bytes.

Notice that rule:pintro-store has changed the poison value for bytes to $\poisoned$,
because the memory location written to was $\regmapofof{\makepc{e}}{\makereg{bytes}} = (\makevar{stk},0)$.

The rule also poisons the memory location where $\prog$ writes to.

The last transition is the shuffle instruction that relocates the poisoned bytes to a.

The product is now stuck: rule:hspec is disabled because the poison value for bytes is $\poisoned$ and thus not safe to leak in $\tra$.

Indeed, $\regmapofof{\makepc{f}}{\makereg{bytes}} = \makereg{a}$ holds the secret value 42.

[every node/.style=inner sep=0pt,outer sep=0pt]
= 1; = 0.5;

[scale=0.7] (legend)

[scale=0.7,above=0 of legend] (legend2)

[scale=0.7,anchor=south,right=0.2 of legend] (a)
1     a

32     32     $\healthy$

$\bfalse$     $\bfalse$     $\healthy$

8     8     $\healthy$

42     42     $\healthy$

0     0     $\healthy$

[scale=0.7,anchor=south,right=of a] (b)
2     b

32     32     $\healthy$

peach!60$\bfalse$     peach!60$\bfalse$     $\healthy$

8     8     $\healthy$

42     42     $\healthy$

0     0     $\healthy$

[scale=0.7,anchor=south,right=of b] (c)
2    c

32     32     $\healthy$

$\bfalse$     $\bfalse$     $\healthy$

8     8     $\healthy$

42     42     $\healthy$

0     0     $\healthy$

[scale=0.7,right=of c] (d1)
2    c

32     32     $\healthy$

$\bfalse$     $\bfalse$     $\healthy$

8     8     $\healthy$

42     42     $\healthy$

0     0     $\healthy$

[scale=0.7,anchor=north,above=0 of d1,fill=peach!60] (d2)
3     d

32     32     $\healthy$

$\bfalse$     $\bfalse$     $\healthy$

8     8     $\healthy$

42     42     $\healthy$

0     0     $\healthy$

[scale=0.7,right=of d1] (e1)
2    c

32     32     $\healthy$

$\bfalse$     $\bfalse$     $\healthy$

8     8     $\healthy$

42     42     $\healthy$

0     0     $\healthy$

[scale=0.7,anchor=north,above=0 of e1] (e2)
4     e

32     32     peach!60$\poisoned$

$\bfalse$     $\bfalse$     $\healthy$

8     8     $\healthy$

42     42     $\healthy$

peach!60 42     0     peach!60 $\poisoned$

peach!60 42

[scale=0.7,right=of e1] (f1)
2    c

32     32     $\healthy$

$\bfalse$     $\bfalse$     $\healthy$

8     8     $\healthy$

42     42     $\healthy$

0     0     $\healthy$

[scale=0.7,anchor=north,above=0 of f1] (f2)
4     f

32     32     $\poisoned$

$\bfalse$     peach!60 42     $\healthy$

8     8     $\healthy$

42     42     $\healthy$

42     0     $\poisoned$

= 0.03;
[ntrans] ([shift=(0,-)]a.north east) – ([shift=(0.1,-)]a.north east)
– node[right=0.2,scale=.7,anchor=south east,pos=0.9] 270rule:pasgn ([shift=(0.1,)]a.south east) – ([shift=(0,)]b.south west);
[ntrans] ([shift=(0,-)]b.north east) – ([shift=(0.1,-)]b.north east)
– node[right=0.2,scale=.7,anchor=south east,pos=0.9] 270rule:pspill ([shift=(0.1,)]b.south east) – ([shift=(0,)]c.south west);
[ntrans] ([shift=(0,-)]c.north east) – ([shift=(0.1,-)]c.north east)
– node[right=0.2,scale=.7,anchor=south east,pos=0.9] 270rule:hspec ([shift=(0.1,)]c.south east) – ([shift=(0,)]d1.south west);
[ntrans] ([shift=(0,-)]d2.north east) – ([shift=(-0.1,-)]e2.north west)
– node[left=0.2,scale=.7,anchor=north west,pos=0.1] 270rule:pintro-store ([shift=(-0.1,)]e2.south west) – ([shift=(0,)]e2.south west);
[ntrans] ([shift=(0,-)]e2.north east) – ([shift=(-0.1,-)]f2.north west)
– node[left=0.2,scale=.7,anchor=north west,pos=0.1] 270rule:pfill ([shift=(-0.1,)]f2.south west) – ([shift=(0,)]f2.south west);

An execution of $\prodra$ on <Ref>. Updated values are highlighted. Dead registers are gray.

§.§ Static poison analysis of the product

The poison product finds weaknesses:

Whenever a poisoned register's value would be leaked in $\tra$,
the product cannot execute the transition.

To find the program points where a poisoned register can be leaked,
we design a static analysis that over-approximates the poison values any execution could produce.

The analysis constructs, for each program point pair $(\pc, \pcp)$, an approximate poison type $\poison$.

This poison type is approximate in that a statically $\healthy$-typed register is always healthy in any execution that reaches $(\pc, \pcp)$ in a speculating state.

Similarly, if it is statically typed $\weakpoisoned$ it is always weakly poisoned in a speculating state.

However, if it is statically typed $\poisoned$ it might also be healthy or weakly poisoned.

Formally, the analysis constructs a function $\passigns : \prodpcs \to \ptypes$, where $\prodpcs$ are the program points of $\prodra$,

\begin{align*}
\prodpcs & \defeq \setcond{(\pc, \pcp)}{\exists (\nstatec\lseq\statec, \nstated\lseq\stated, \pseq\lseq\poison).\, \pc \atpc \statec \land \pcp \atpc \stated} \\
& = \setcond{(\pc, \pcp), (\pc, \pcssp)}{\instinjof{\pc} = \pcp \land \traof{\pcssp} = \shufseq{\pcp}}\,.
\end{align*}

The pairs $(\pc, \pcp)$ are instruction-matched program counters and $(\pc, \pcssp)$ are from shuffling states.

We design our analysis as a forward flow analysis (<Ref>).

For that, we need to define a flow lattice $\lattice$, transfer functions, and the initial flow value $\flowinit$.

The flow analysis then yields $\passigns$ as a solution.

The lattice is constructed on $\ptypes$.

We create an ordering $\healthy < \poisoned$ and $\weakpoisoned < \poisoned$ on $\pvals$.

In order to arrive at a lattice,
we further extend it by an artificial least element $\bot \in \pvals$.[This is a standard construction. In the remainder, we assume that transfer functions preserve $\bot$.]

We then lift the ordering point-wise to poison types for the flow lattice $\lattice = (\ptypes, \leq)$.

The ordering is chosen with the intention that when $\poison \leq \poisonp$,
then $\statec \nrrmp{\poison} \stated$ implies $\statec \nrrmp{\poisonp} \stated$ (which would not be the case if we had set $\healthy < \weakpoisoned$).

The initial value is set to healthy, $\flowinit = \healthy$, because the initial states of $\prog$ and $\tra$ are fully equal up to $\regmap$.

The transfer functions $\ptransferat{(\pc, \pcp)} : \ptypes \to \ptypes$ need to approximate the poison types in $\prodra$.

Conceptually, they update the current poison type by simultaneously executing all updates that $\prodra$ could do.

For instruction-matched $\instinjof{\pc} = \pcp$ that means to look at the instruction $\inst = \progof{\pc}$ which is the same as $\traof{\pcp}$ up to $\regmap$.

Then, we poison all registers and memory locations that a rule for $\inst$ from <Ref> could poison.

This means, the transfer function is solely dependent on the instruction $\inst = \progof{\pc}$, and we define it via $\ptransferat{(\pc, \pcp)} = \ptransferat{\inst}$ below.

For a shuffling product state, $\prodra$ offers for each instruction $\instp = \traof{\pcssp}$ only one update which we find in <Ref>.

We again define transfer solely dependent on $\instp$ via $\ptransferat{(\pc, \pcssp)} = \ptransferpat{\instp}$.

For a shuffling $\instp = \IWslh{\regap}$ we assume that the source register for $\regap$ is $\rega$, i.e. $\regmapofof{\pcssp}{\rega} = \regap$.

We only present the interesting cases of $\ptransferat{\inst}$ and $\ptransferpat{\instp}$.

The initial poison type for $(\entry, \entryp)$ is healthy.

\begin{align*}
\begin{aligned}
\ptransferof{\Iload{\rega}{\vara}{\regb}{\pcsuc}}{\poisons} & = \subst{\poisons}{\rega}{\poisoned} \\
\ptransferof{\Islh{\rega}{\pcsuc}}{\poisons} & = \subst{\poisons}{\rega}{\healthy} \\
\ptransferpof{\Islh{\regap}{\pcsuc}}{\poisons} & = \subst{\poisons}{\rega}{\weakpoisoned} \\
\ptransferpof{\Isfence{\pcsuc}}{\poisons} &= \healthy
\end{aligned}
\begin{aligned}
\ptransferof{\Iasgn{\rega}{\regb \op \regc}{\pcsuc}}{\poisons} & =
\begin{cases}
\subst{\poisons}{\rega}{\healthy} & \poisonsof{\regb} = \poisonsof{\regc} = \healthy \\
\subst{\poisons}{\rega}{\poisoned} & \text{otherwise}
\end{cases} \\
\ptransferof{\Istore{\vara}{\regb}{\regc}{\pcsuc}}{\poisons} & =
\subst{\subst{\poisons}{\mems}{\poisonsof{\regc}}}{\regs, \vara}{\poisoned} \\
\end{aligned}
\end{align*}

All transfer functions are monotonic.

All but one transfer function are easily defined in order to approximate the rules of $\prodra$.

The exception is for $\IWstore{\vara}{\regb}{\regc}$ instructions which we explain.

The first substitution sets all memory locations to $\poisonof{\regc}$.

This approximates rule:pload-hsafe,,rule:pload-hunsafe, because both $\prog$ and $\tra$ store to the same location.

The second substitution sets all of $\vara$ and all registers $\regs$ to $\poisoned$.

This approximates rule:pintro-store,,rule:pload-ss,,rule:pload-us:

It is only possible because in these rules $\prodra$ replays a transition in $\prog$ that only writes to $\vara$.

In order to formally express how a solution $\passigns$ approximates the poison values of all reachable states in $\prodra$,
we introduce shorthand notations for sequences of poison types fully consisting of poison types from $\passigns$.

Fix a solution $\passigns$ to the flow equations.

We define:
[=0.6em=0.5em plus 0.2em]
=  =  (, )

⇔  ⇔ (, , ) = (, , )

The notation $\pseqofof{\nstatec}{\nstated}$, where $\nstatec$, $\nstated$ are speculating states,
stands for a sequence of poison types of length $\sizeof{\pseqofof{\nstatec}{\nstated}} = \sizeof{\nstatec} = \sizeof{\nstated}$.

Intuitively, $\pseqofof{\nstatec}{\nstated}$ consists of the poison types of $\passigns$, applied to the program counters of $\nstatec$ and $\nstated$ at every level.

The only exception is the lowest level in the speculating states.

They are always set to $\healthy$, because we know from <Ref>
that those states are reachable speculation-free
and can never have poisoned registers or memory locations.

The notation $\nstatec \relrm \nstated$, $\nstatec \rrmp{\poison} \nstated$, and $(\nstatec\lseq\statec, \nstated\lseq\stated, \poison)$
are shorthand notations to avoid a lot of repeating $\pseqofof{\nstatec}{\nstated}$.

Similarly,  stands for the same except for the top most speculating states, where the poison type is $\poison$.

Whenever $(\nstatec, \nstated, \pseqofof{\nstatec}{\nstated}) \sprodtranss{\leakp}{\directp}{\leak}{\direct} (\nstatee, \nstatef, \pseqp)$
then $\pseqp \leq \pseqofof{\nstatee}{\nstatef}$.

§.§ Fixing Register Allocation

We can use our static analysis solution $\passigns$ to identify situations when register allocation has not introduced any weaknesses in $\tra$.

If $\passigns$ guarantees that leakages are never poisonous, then $\tra$ has no register allocation induced weaknesses.

A register allocation $(\instinj, \regmap)$ between $\prog$ and $\tra$ is poison-typable,
if there is a solution $\passigns$ to eqn:flow-fwd
that for every $(\pc, \pcp)$ with $\instinjof{\pc} = \pcp$
satisfies the additional constraints

\begin{align*}
\poisonsof{\regb} &= \weakpoisoned \lor \poisonof{\regb} = \healthy &&\text{if} &
\progof{\pc} &= \Iload{\rega}{\vara}{\regb}{\pcsuc}
\lor \progof{\pc} = \Istore{\vara}{\regb}{\regc}{\pcsuc}\;,
\\
\poisonsof{\regb} & = \healthy
&&\text{if} &
\progof{\pc} &= \Iif{\regb}{\pcsuc_{\btrue}}{\pcsuc_{\bfalse}}\;.
\end{align*}

Our fix is applicable to any register allocation $(\instinj, \regmap)$ between $\prog$ and $\tra$:

We check if $(\instinj, \regmap)$ is poison-typable.

For that, we solve the flow analysis (e.g. kildallUnifiedApproachGlobal1973) to obtain a static poison assignment $\passigns$ and then check the additional constraints.

If it is not poison-typable, then an additional constraint is violated for some program point $(\pc, \pcp)$ and register $\regbp$ of $\prodra$.

We insert an $\IWsfence$ or $\IWslh{\regbp}$ instruction into $\tra$ at the end of the shuffle sequence right before $\pcp$ and obtain a new register allocation where that additional constraint is now satisfied.

We then repeat the process until we obtain a poison-typable register allocation.

§.§ Poison-typable Register Allocation is SNiP

We now prove that making register allocation poison-typable already makes it $\propsnip$.

With our proof method from <Ref>,
this reduces to crafting a snippy simulation.

Again, the crafted simulation is parametric, so that it works for all poison-typable register allocations.

If $(\regmap, \instinj)$ is a poison-typeable register allocation between $\prog$ and $\tra$,
then there exists a snippy simulation $(\simrel, \dtffamily)$ between $\tra$ and $\prog$.

For the remainder of the section, fix a poison-typable register allocation $(\regmap, \instinj)$ between $\prog$ and $\tra$,
and the static poison assignment $\passigns$.

Let further $\entry$ be the entry point for $\prog$ and $\entryp$ for $\tra$.

§.§.§ Defining (≺,◃)

intervalpath1/.style = teal,rounded corners, shorten <=4pt, shorten >=5pt,
intervalpath2/.style = red,rounded corners, shorten <=4pt, shorten >=5pt
= 2; = 0.7;

(c) $\nstatec$;
[right=of c] (e) $\nstatee$;
[below=0.8 of c,anchor=south west,draw] (proglabel) $\prog$;
[below=of e] (cp) $\nstatee\rlap{$'$}$;

[right=of e] (d) $\nstated$;
[right=of d] (h) $\nstateh$;
[right=of h] (dots) $\ldots\vphantom{X}$;
[right=of dots] (f) $\nstatef$;
[below=of h] (hp) $\nstateh\rlap{$'$}$;
[below=0.8 of f,anchor=south east,draw] (proglabeltra) $\tra$;

[ntrans] (c) – node[above] $\smash{\dtpair{\leakp}{\directp}}$ (e);
[ntrans] (d) – node[above] $\smash{\dtpair{\leak}{\direct}}$ (h);
[ntrans] (h) – node[above] $\smash{\dtpair{\leak_1}{\Dstep}}$ (dots);
[ntrans] (dots) – node[above] $\smash{\dtpair{\leak_m}{\Dstep}}$ (f);

[ntrans] (e) – node[right] $\smash{\dtpair{\Erb}{\Drb}}$ (cp);
[ntrans] (h) – node[right] $\smash{\dtpair{\Erb}{\Drb}}$ (hp);
([shift=(0,0.1)]h.north) – ([shift=(0,0.2)]h.north) – node[below=-1pt] shuffle only ([shift=(0,0.2)]f.north) – ([shift=(0,0.1)]f.north);

[intervalpath1] (c.center) – (c.south east) – (e.south west) – (cp.north west) – (cp.center);
[intervalpath2] (c.center) – ([shift=(0,0.05)]c.south east) – ([shift=(0,0.05)]e.south west) – (e.center);
[intervalpath1] (d.center) – (d.south east) – (h.south west) – (hp.north west) – (hp.center);
[intervalpath1] (d.center) – (d.south east) [rounded corners=10pt] – ([shift=(-.37,0)]dots.south west) [rounded corners] – (hp.north east) – (hp.center);
[intervalpath1] (d.center) – (d.south east) [rounded corners=10pt] – ([shift=(-0.01,0)]dots.south) [rounded corners] – ([shift=(0.1,-0.05)]hp.east) – ([shift=(0,-0.05)]hp.center);
[intervalpath2] (d.center) – ([shift=(0,0.05)]d.south east) – ([shift=(0,0.05)]f.south west) – (f.center);
[ntrans] (dots) – node[fill=white,below right] $\dtpair{\Erb}{\Drb}$ (hp);

The shape of $\instinj$-intervals. Teal and red paths form separate intervals.

We define ${\simrel} \subseteq \nstatesof{\tra} \times \nstatesof{\prog}$ similar to the simulation for register allocation without speculative semantics:

Source state $\nstatec$ and target state $\nstated$ are instruction-matched and coincide in values up to relocation by $\regmap$.

The difference is, that the states do not need to coincide on registers and memory locations poisoned by $\passigns$:

\begin{align*}
\nstated \simrel \nstatec & \ifftxt \nstatec \rinstinj \nstated \land \nstatec \relrm \nstated \,.
\end{align*}

For the directive transformation $\dtfat{\nstatec}{\nstated}$,
we rely on $\prodra$'s transitions.

We say that a transition sequence $(\nstatec, \nstated, \poison) \sprodtranss{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee, \nstatef, \poisonp)$ is a $\instinj$-interval
if $\nstatec \rinstinj \nstated$, $\nstatee \rinstinj \nstatef$, and no intermediary state pairs are instruction matched.

The intent is that $\instinj$-intervals are precisely the simulation intervals once we have proven that our defined relation is a simulation.

<Ref> depicts the shape of $\instinj$-intervals:
The product first executes the instruction-matched instruction on both, $\nstatec$ and $\nstated$.

Then, the target program can perform any number of shuffle steps,
until either the shuffle sequence is fully executed (the pair of red paths),
or a rollback happened before that (any pair of teal paths).

In that case, $\prodra$ rolls back on $\nstatee$ as well.

We use the $\instinj$-intervals as directive transformations,

\[
\dtfat{\nstatec}{\nstated} \quad\defeq\quad
\setcond{(\dtracee, \dtraced)}
{\text{$(\nstatec, \nstated, \poison) \sprodtranss{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee, \nstatef, \poisonp)$ is a $\instinj$-interval}} \, .
\]

$(\simrel, \dtffamily)$ is a snippy simulation between $\tra$ and $\prog$.

Like for Dead Code Elimination in <Ref>,
we need to prove that $(\simrel, \dtffamily)$

* is a simulation (<Ref>),

* respects $\lows$ (<Ref>),
* is snippy (<Ref>).

The intermediary lemmas are proved subsequently in their own sections.

We required $\lowsof{\varstack} = \low$ so when $\stated_1 \seceq \stated_2$,
and $\statec_1 \nrrmp{\healthy} \stated_1$ as well as $\statec_2 \nrrmp{\healthy} \stated_2$,
then $\statec_1$ and $\stated_1$ equal on all values in memory other than $\varstack$ (remember that $\poison$ is not defined on $\varstack$).

Similarly, $\statec_2$ and $\stated_2$ equal on memory.

So, $\statec_1 \seceq \statec_2$ if and only if $\stated_1 \seceq \stated_2$.

In order to prove that $\simrel$ is a simulation (<Ref>),
we first need to show that for all initial $\stated$ of $\tra$
there is an initial $\statec$ for $\prog$ with $\stated \simrel \statec$.

Secondly, for all pairs of states $\nstated \simrel \nstatec$, we need to derive $\proofnode{\sderivetgtsim{\guarded{\simrel}}{\dtfat{\nstatec}{\nstated}}{\nstated}{\nstatec}{\varepsilon}}$ in <Ref>.

For the initial states, let $\stated = (\entryp, \rasgnp, \masgnp)$.

We construct $\statec = (\entry, \rasgn, \masgn)$.

First, we know from instruction matching, that $\instinjof{\entry} = \entryp$, thus $\statec \rinstinj \stated$.

We can then choose $\masgn = \masgnp$ and $\rasgnof{\rega} = \evalin{\stated}{\regmapofof{\entryp}{\rega}}$.

For the second part, consider $\nstated \simrel \nstatec$.

We need to provide a proof for $\proofnode{\sderivetgtsim{\guarded{\simrel}}{\dtfat{\nstatec}{\nstated}}{\nstated}{\nstatec}{\varepsilon}}$.

The case where $\nstated$ is final is trivial, so consider non-final $\nstated$ and $\nstatec$.

We need two small helping-lemmas that state that $\instinj$-injected instructions and shuffle instructions of $\tra$ are preserved to the product.

The proof of these we skip, but they rely on the fact that $(\instinj, \regmap)$ is poison-typable with $\passigns$.

Let $\nstated \simrel \nstatec$,
$\nstated \ntrans{\leak}{\direct} \nstateh$,
and $\pseq\lseq\poison = \pseqofof{\nstatec}{\nstated}$.

Then, $(\nstatec, \nstated, \poison) \sprodtrans{\leakp}{\directp}{\leak}{\direct} (\nstatee, \nstateh, \poisonp)$
with $\nstatee \rrmp{\poisonp} \nstateh$.

Let $\nstatee \rrmp{\poison} \nstateh$
and $\nstateh \ntranss{\tracel}{\dtraced} \nstatef$ be shuffle only in $\tra$.
Then, $\prodra$ has a unique execution $(\nstatee, \nstateh, \poison)
\sprodtranss{\varepsilon}{\varepsilon}{\tracel}{\dtraced}
(\nstatee, \nstatef, \poisonp)$ with $\nstatee \rrmp{\poisonp} \nstatef$.

Let $\nstated = \nstatedp\lseq\stated$ and $\nstatec = \nstatecp\lseq\statec$, and $\passignsof{(\statec, \stated)} = \poison$.

We sketch how to derive $\proofnode{\sderivetgtsim{\guarded{\simrel}}{\dtfat{\nstatec}{\nstated}}{\nstated}{\nstatec}{\varepsilon}}$.

We will first explore executions from $\nstated$ in $\tra$ with rule:tgt,
perform a directive transformation with rule:direct-tf,
replay the execution from $\nstatec$ in $\prog$,
and finally prove that the reached states belong to $\simrel$ to end the proof with rule:coind.

First, we explore executions from $\nstated$ in $\tra$ with rule:tgt.

Every execution in $\tra$ from $\nstated$ eventually enters a $\instinj$-injected state.

So we explore executions $\nstated \ntrans{\leak}{\direct} \nstateh \ntranss{\tracel}{\dtraced} \nstatef$,
where $\nstatef$ is again $\instinj$-injected but no intermediary state is.

The explored executions have the shape of the teal and red paths of $\tra$ in <Ref>.

We thus need to prove $\proofnode{\sderivetgtsim{\unguarded{\simrel}}{\dtfat{\nstatec}{\nstated}}{\nstatef}{\nstatec}{\direct\lseq\dtraced}}$.

The next step is to perform directive transformation with $\dtfat{\nstatec}{\nstated}$.

But we defined the transformation on $\instinj$-intervals.

So we find the appropriate transitions for $\nstated \ntrans{\leak}{\direct} \nstateh \ntranss{\tracel}{\dtraced} \nstatef$ in $\prodra$.

For the first transition,
<Ref> yields $(\nstatec, \nstated, \poison) \sprodtrans{\leakp}{\directp}{\leak}{\direct} (\nstatee, \nstateh, \poisonp)$
so that $\nstatee \rrmp{\poisonp} \nstateh$.

For the remaining transitions, there are two cases:

No $\Drb$ occurs in $\dtraced$.
Then, $\nstateh \ntranss{\tracel}{\dtraced} \nstatef$ is shuffle-only,
and we can apply <Ref> for transitions
$(\nstatee, \nstateh, \poisonp)
\sprodtranss{\varepsilon}{\varepsilon}{\tracel}{\dtraced}
(\nstatee, \nstatef, \poisonpp)$ with $\nstatee \rrmp{\poisonpp} \nstatef$.

Together with the first transition, $\prodra$ can execute the transitions $(\nstatec, \nstated, \poison)
\sprodtrans{\leakp}{\directp}{\leak}{\direct}
(\nstatee, \nstateh, \poisonp)
\sprodtranss{\varepsilon}{\varepsilon}{\tracel}{\dtraced}
(\nstatee, \nstatef, \poisonpp)$.

This is precisely the red $\instinj$-interval, so $\directp \dtfat{\nstatec}{\nstated} \direct\lseq\dtraced$.

We can thus use rule:direct-tf and are left proving $\proofnode{\sderivesrcsim{\guarded{\simrel}}{\dtfat{\nstatec}{\nstated}}{\nstatef}{\nstatec}{\directp}}$.

However, $(\nstatec, \nstated, \poison) \sprodtrans{\leakp}{\directp}{\leak}{\direct} (\nstatee, \nstateh, \poisonp)$ already provides us the replay $\nstatec \ntrans{\leakp}{\directp} \nstatee$ in $\prog$.

We can use it with rule:src,
and it remains to show $\proofnode{\sderivesrcsim{\unguarded{\simrel}}{\dtfat{\nstatec}{\nstated}}{\nstatef}{\nstatee}{\varepsilon}}$.

In order to use rule:coind, we need to establish $\nstatef \simrel \nstatee$,
i.e. $\nstatee \rinstinj \nstatef$ and $\nstatee \relrm \nstatef$.

The condition $\nstatee \rinstinj \nstatef$ holds because it has been the condition for terminating exploration in $\tra$.

For the latter condition, we have already established $\nstatee \rrmp{\poisonpp} \nstatef$.

Thanks to <Ref>,
we also have $\pseqofof{\nstateep}{\nstatefp}\lseq\poisonpp \leq \pseqofof{\nstatee}{\nstatef}$,
where $\nstatee = \nstateep\lseq\statee$ and $\nstatef = \nstatefp\lseq\statef$.

We designed the lattice so that $\nrrmp{\poison}$ is monotonic in $\poison$, so they yield $\nstatee \relrm \nstatef$.

Thus, we get $\nstatef \simrel \nstatee$ and can use rule:coind.

Otherwise, let $\Drb$ occur in $\dtraced$.
Then, the explored execution from $\nstateh$ is $\nstateh \ntranss{\tracelp}{\dtracedp} \nstatey \ntrans{\Erbless}{\Drb} \nstatef$ with $\dtraced = \dtracedp\lseq\Drb$.

Indeed, $\dtraced$ must end with $\Drb$, because $\nstatef$ is already $\instinj$-injected:

When $\nstateh = \nstatehp\lseq\stateh$ and $\nstatee = \nstateep\lseq\statee$,
then $\nstatef = \nstatehp$.

Further, $\nstatehp$ and $\nstateep$ are already contained in $\nstated$ and $\nstatec$, respectively.

Because $\nstatec \rinstinj \nstated$ we also have $\nstateep \rinstinj \nstatehp = \nstatef$.

So $\nstatef$ is $\instinj$-injected and exploration stopped upon discovering it.

Again, by <Ref>
there is
$(\nstatee, \nstateh, \poisonp)
\sprodtranss{\varepsilon}{\varepsilon}{\tracel}{\dtraced}
(\nstatee, \nstatey, \poisonpp)$ with $\nstatee \rrmp{\poisonpp} \nstatey$.

By definition of $\prodra$, $(\nstatee, \nstatey, \poisonp) \prodtrans{\Erb}{\Drb}{\Erb}{\Drb} (\nstateep, \nstatehp, \pseqofof{\nstateep}{\nstatehp})$.

This is one of the teal $\instinj$-intervals, so $\directp\lseq\Drb \dtfat{\nstatec}{\nstated} \direct\lseq\dtracedp\lseq\Drb$.

The remaining arguments for rule:src,rule:coind are similar to the previous case.

For $\nstated \simrel \nstatec$, $(\nstatec, \nstated, \pseqofof{\nstatec}{\nstated}) \sprodtranss{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee, \nstatef, \pseqp)$ is a $\instinj$-interval
iff $(\nstatec, \nstated) \synctrans{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee, \nstatef)$.

In order to prove the simulation snippy, we are given the black parts of <Ref>.

So, consider $\nstated_1 \simrel \nstatec_1$, $\nstated_2 \simrel \nstatec_2$, $\nstated_1 \samepoint \nstated_2$, and $\nstatec_1 \samepoint \nstatec_2$.

Further, consider a simulation interval $(\nstatec_1, \nstated_1) \synctrans{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee_1, \nstatef_1)$ and $\nstatec_2 \ntrans{\tracek}{\dtracee} \nstatee_2$.

We need to prove $(\nstatec_2, \nstated_2) \synctrans{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee_2, \nstatef_2)$.

As simulation intervals are the same as $\instinj$-intervals,
we have the $\instinj$-interval $(\nstatec_1, \nstated_1, \pseqofof{\nstatec_1}{\nstated_1}) \sprodtranss{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee_1, \nstatef_1, \poisonp)$,
and want to prove that $(\nstatec_2, \nstated_2, \pseqofof{\nstatec_2}{\nstated_2}) \sprodtrans{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee_2, \nstatef_2, \poisonp)$.

We again split the interval into the instruction-matched transition
$(\nstatec_1, \nstated_1, \pseqofof{\nstatec_1}{\nstatec_1}) \sprodtrans{\leakp}{\directp}{\leak}{\direct} (\nstateg_1, \nstateh_1, \poisonpp)$
and a shuffle sequence $(\nstateg_1, \nstateh_1, \poisonpp) \sprodtranss{\tracekp}{\dtraceep}{\tracelp}{\dtracedp} (\nstatee_1, \nstatef_1, \poisonp)$.

The difficult part is to reproduce the instruction-matched transition from $(\nstatec_2, \nstated_2, \pseqofof{\nstatec_2}{\nstated_2})$.

Because $\pseqofof{\nstatec_1}{\nstated_1}$ is only dependent on program counters, $\pseqofof{\nstatec_1}{\nstated_1} = \pseqofof{\nstatec_2}{\nstated_2}$.

There is a transition $(\nstatec_2, \nstated_2, \pseqofof{\nstatec_2}{\nstated_2}) \sprodtrans{\leakp}{\directp}{\leak}{\direct} (\nstatee_2, \nstatef_2, \poisonp)$ in $\prodra$.

We reproduce the second part of the $\instinj$-interval,
$(\nstateg_1, \nstateh_1, \poisonpp_1) \sprodtranss{\tracekp}{\dtraceep}{\tracelp}{\dtracedp} (\nstatee_1, \nstatef_1, \poisonp_1)$.

Once more, we perform case distinction on whether $\dtracedp$ and $\dtraceep$ follow the red or teal paths in <Ref>.

No $\Drb$ occurs in $\dtracedp$.
In this case, $\dtracedp$ is shuffle-only and $\dtraceep = \varepsilon$.

Because shuffle semantics are deterministic and all have the same directive $\Dstep$,
the following lemma is straightforward to show.

Together with <Ref>, the shuffle sequence is reproduced from $(\nstateg_2, \nstateh_2, \poisonp)$.

If $\nstatef_1 \samepoint \nstatef_2$ and $\instof{\nstatef_1} = \shufseq{\pcsucp}$ with shuffle-only $\nstatef_1 \ntranss{\tracel}{\dtraced} \nstateh_1$,
then $\nstatef_2 \ntranss{\tracel}{\dtraced} \nstateh_2$.

Indeed, we complete reproduction in this case:
With $(\nstatec_2, \nstated_2, \poison) \sprodtrans{\leakp}{\directp}{\leak}{\direct} (\nstateg_2, \nstateh_2, \poisonpp)$ from <Ref>
and $(\nstateg_2, \nstateh_2, \poisonpp_2) \sprodtranss{\varepsilon}{\varepsilon}{\tracelp}{\dtracedp} (\nstatee_2, \nstatef_2, \poisonp)$ from <Ref>,
we have constructed $(\nstatec_2, \nstated_2, \pseqofof{\nstatec_2}{\nstated_2}) \sprodtrans{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee_2, \nstatef_2, \poisonp)$.

Otherwise, let $\Drb$ occur in $\dtraced$.
Then, $(\nstateg_1, \nstateh_1, \poisonpp) \sprodtranss{\tracekp}{\dtraceep}{\tracelp}{\dtracedp} (\nstatee_1, \nstatef_1, \poisonp)$
is actually the teal path $(\nstateg_1, \nstateh_1, \poisonpp) \sprodtranss{\varepsilon}{\varepsilon}{\tracelp'}{\dtracedp'} (\nstategp_1, \nstatehp_1, \poisonpp') \sprodtrans{\Erb}{\Drb}{\Erb}{\Drb} (\nstatee_1, \nstatef_1, \poisonp)$,
where $\dtracedp'$ is a shuffle sequence.

Same as in the previous case, we can reproduce $(\nstateg_2, \nstateh_2, \poisonpp) \sprodtranss{\varepsilon}{\varepsilon}{\tracelp'}{\dtracedp'} (\nstategp_2, \nstatehp_2, \poisonpp')$.

The product can clearly execute $(\nstategp_2, \nstatehp_2, \poisonpp') \sprodtrans{\Erb}{\Drb}{\Erb}{\Drb} (\nstatee_2, \nstatef_2, \poisonp)$
because $\sizeof{\nstategp_2} = \sizeof{\nstatehp_2} = \sizeof{\nstategp_1} = \sizeof{\nstatehp_1} > 1$.

Reproduction of $(\nstatec_2, \nstated_2, \pseqofof{\nstatec_2}{\nstated_2}) \sprodtrans{\tracek}{\dtracee}{\tracel}{\dtraced} (\nstatee_2, \nstatef_2, \poisonp)$ is done.

§ RELATED WORK

We already discussed the closely related work in the context of compiler correctness.

Here, we give a broader picture and elaborate on methods for proving non-interference for single programs.

Note the difference: when reasoning about compiler passes, we reason over all programs.

For a broader overview, we defer the reader to a recent survey cauligiSoKPracticalFoundations2022.

§.§.§ Speculation Sources

Since its discovery in 2018,
the Spectre Attack has been rediscovered in multiple variants.

The main difference between the variants lies in the hardware feature that is trained in order to trigger a miss-speculation.

We call the respective feature the source of speculation.

The first version of the attack trains the Prediction History Table () of the processor, in order to inflict a miss-predicted branching speculation kocherSpectreAttacksExploiting2019.

In this paper, we consider only  as the source of speculation.

Other variants train the Branch Target Buffer () kocherSpectreAttacksExploiting2019,
the Return Stack Buffer () koruyehSpectreReturnsSpeculation2018,
the Speculative Store Bypass feature () hornSpeculativeExecutionVariant2018,
and the Predictive Store Forwarding mechanism () guancialeInSpectreBreakingFixing2020.

Other variants train the Branch Target Buffer () to misspredict indirect branching instructions kocherSpectreAttacksExploiting2019,
the Return Stack Buffer () to misspredict return points koruyehSpectreReturnsSpeculation2018,
the Speculative Store Bypass () mechanism, also called Store To Load Forwarding (), to read from memory when pending stores are still missing their address hornSpeculativeExecutionVariant2018,
and the Predictive Store Forwarding () mechanism to forward pending stores to loads, whose address is still missing guancialeInSpectreBreakingFixing2020.

The Meltdown attack introduces speculation through an out-of-order read from elevated-permission memory regions, racing against the MMU to detect the violation lippMeltdownReadingKernel2018.

While the speculation sources are varying, leaking secrets is uniform across all attack variants.

§.§.§ Properties

The constant time programming guideline requires no influence of sensible data towards the leakage observed by the attacker.

Formally, non-interference goguenSecurityPoliciesSecurity1982 expresses this property.

Its definition requires a relation $\seceq$ for indistinguishable initial states.

Non-interference states that any two $\seceq$-indistinguishable initial states do not produce different leakage traces.

Non-interference is a hyper-property clarksonHyperproperties2010:
It requires to reason about two executions of the program.

Hyper-properties tend to be harder to verify than single trace properties due to synchronization issues with the traces compared.

Non-interference for side-channel leakage evades these issues:

Side-channel leakage exposes the program counter to the attacker.