11institutetext:  CISPA Helmholtz Center for Information Security, Germany
22institutetext: Technion, Israel

# Automatic and Incremental Repair
for Speculative Information Leaks

Joachim Bard 11 Swen Jacobs 11 Yakir Vizel 22

###### Abstract

We present CureSpec, the first model-checking based framework for _automatic
repair_ of programs with respect to information leaks in the presence of side-
channels and speculative execution. CureSpec is based on formal models of
attacker capabilities, including observable side channels, inspired by the
Spectre attacks. For a given attacker model, CureSpec is able to either prove
that the program is secure, or _detect_ potential side-channel vulnerabilities
and _automatically insert mitigations_ such that the resulting code is
provably secure. Moreover, CureSpec can provide a _certificate_ for the
security of the program that can be independently checked. We have implemented
CureSpec in the SeaHorn framework and show that it can effectively repair
security-critical code, for example the AES encryption from the OpenSSL
library.

##  1 Introduction

Speculative execution is an indispensable performance optimization of modern
processors: by predicting how branching (and other) conditions will evaluate
and speculatively continuing computation, it can avoid pipeline stalls when
data from other computations is still missing. When this data arrives, in case
of a correct guess the results of the computations can be committed. Otherwise
they have to be discarded, and the correct results computed. However, even
when the results are not committed to registers that are available at the
software level, speculative computations may leave traces in the
microarchitecture that can leak through _side channels_ , as demonstrated by
the family of Spectre attacks [21, 5, 10]. For example, the cache is usually
not cleaned up after a misspeculation, enabling _timing attacks_ that can
discover data used during speculation.

Since the discovery of Spectre, several countermeasures have been developed
[19, 20, 21, 29]. As neither speculation nor side channels can be removed from
current hardware without sacrificing significant amounts of computing power,
the problem is usually dealt with at the software level. Mitigations for
Spectre usually prevent information leaks during speculative execution by
prohibiting “problematic” instructions from being executed speculatively.

Most of the existing mitigations prevent some Spectre attacks, but are known
to be incomplete [10], i.e., the modified code may remain vulnerable, in
circumstances that may or may not be known. In addition, there have been
approaches that use formal methods to obtain code that is _guaranteed_ to be
resilient against clearly defined types of Spectre attacks, and a formal
notion of _speculative constant-time security_ has been proposed [11] that can
give guarantees against timing attacks under speculation. However, these
methods all have certain shortcomings: either they require manual modification
of the code if potential leaks are found [16, 12, 11], they do not precisely
state the security guarantees of automatically hardened code [28], or they are
based on a security type system, which are known to be rather difficult to
extend to different assumptions (e.g., attacker models) or guarantees [27].

#### Motivating example

Consider the three programs in Fig. 1. The original program $P$ is shown in
1(a). It accesses a public array a at position i after checking that the
access to a is in bounds. In speculative execution, this bounds-check can be
ignored, which enables to read arbitrary program memory and store it (albeit
temporarily) into k. The information leak appears when k is used in another
memory access to public array b, making k observable to an attacker through a
cache-based timing attack.

Our repair approach is based on a transformation of $P$ with the following
goals:  (i) capture computations that are executed speculatively;  (ii)
identify possible information leaks under speculation; and  (iii) enable the
prevention of speculation using fences111 Other methods, e.g. _speculative
load hardening_ (SLH, as appears in https://tinyurl.com/3nybax4u), can also be
used as a mitigation in our repair algorithm..

⬇

1if (i < size_a) {

2 k = a[i] * 512;

3 tmp = b[k];

4}

(a) Original program

⬇

1bool spec = false;

2if (*) {

3 spec = spec | !(i < size_a);

4 k = a[i] * 512;

5 assert(!spec);

6 tmp = b[k];

7}

(b) Speculative execution semantics

⬇

1bool spec = false;

2bool fence2 = true;

3bool fence3 = false;

4if (*) {

5 spec = spec | !(i < size_a);

6 assume(!(fence2 && spec));

7 k = a[i] * 512;

8 assume(!(fence3 && spec));

9 assert(!spec);

10 tmp = b[k];

11}

(c) Speculative execution and fence semantics

Figure 1: Example program and its version with speculative and fence semantics

Fig. 1(b) presents a modification $P_{s}$ of $P$, demonstrating the first
point. We assume that speculative executions can start at conditional
statements, i.e., the processor may ignore the condition and take the wrong
branch. Therefore, we replace the branching condition by a non-deterministic
operator $*$ that can return either true or false (Line 2). Moreover, an
auxiliary variable spec is added in order to identify whether an execution of
$P_{s}$ corresponds to a speculative or a non-speculative execution of $P$.
Namely, $\texttt{spec}=\textsf{true}$ at some point in an execution of $P_{s}$
iff the corresponding execution of $P$ is possible _only_ under speculation.
In Fig. 1(b), spec is assigned true in Line 3 if the negation of the branching
condition holds.

To detect information leaks under speculative execution, we assume that there
is a set VInst of memory accesses that should not be performed under
speculation, and for such memory accesses we add an assertion
$\texttt{spec}=\textsf{false}$. Assuming that the nested array read in Line 3
of $P$ (Fig. 1(a)) is in VInst, the transformed program $P_{s}$ (Fig. 1(b))
contains such an assertion at Line 5.

To enable prevention of speculation, in Fig. 1(c) we add auxiliary variables
$\texttt{fence}i$ for every line $i$ in $P$ with an instruction, and
initialize them with truth values that determines whether speculation should
be stopped before reaching line $i$ of $P$. We model the fact that fences stop
speculation by adding assumptions that at line $i$ of $P$ we cannot have
$\texttt{fence}i=\textsf{true}$ and $\texttt{spec}=\textsf{true}$
simultaneously (Line 6 and Line 8 of Fig. 1(c)). In this example, speculation
can only start in Line 1 of $P$ and $\texttt{fence}2=\textsf{true}$ stops
speculation before Line 2 of $P$, implying that the vulnerable instruction in
Line 3 of $P$ is not reachable under speculation.

Note that in this example we assume that fence variables have fixed truth
values, reducing the problem to a safety verification problem. In our repair
algorithm, we start with a program where all variables $\texttt{fence}i$ are
initialized to false, and allow the algorithm to manipulate initial values of
the $\texttt{fence}i$ in order to find a version of the program that is secure
against a given type of Spectre attacks (determined by our choice of
vulnerable memory accesses VInst). Upon termination, our algorithm returns a
list of instructions such that adding fence instructions in these positions
(of the LLVM code) will make $P$ secure.

To formalize the ideas presented on this example, in Section 2 we will
introduce a formal model for the standard semantics of a program $P$, then
introduce a semantics that includes speculative executions in Section 3, and
finally present our automatic repair approach in Section 4.

#### Our contribution

In this paper, we present CureSpec. CureSpec is the first model checking based
framework for _automatic repair_ of programs with respect to information leaks
that are due to speculative execution. Applying CureSpec to a given program
results in a program with a _certified_ security guarantee. CureSpec is
_parameterized by a threat model_ , given as a set of instructions that may
leak secret information to the attacker if executed under speculation. This
makes our technique applicable to a wide range of speculative execution
attacks, including different Spectre attacks that have been identified in the
literature [10]. For a given threat model, CureSpec is able to either prove
that the program is secure, or _detect_ potential side-channel
vulnerabilities. In case vulnerabilities are detected, CureSpec _automatically
inserts mitigations_ that remove these vulnerabilities, and proves that the
modified code is _secure_. Since CureSpec is based on model checking, it
provides a _certificate_ for the security guarantee in the form of an
inductive invariant.

CureSpec is a framework with two main parts:  (i) a reduction of the problem
of finding information leaks that are due to speculation to a safety
verification problem; and  (ii) a model checking based algorithm for detection
and repair of possible vulnerabilities.  For (i), we build on previous results
that introduced formal modeling of speculative execution semantics [7], and
extend this formal model to enable not only the detection of possible leaks,
but also their automatic repair. For (ii), we extend the well-known IC3/Pdr
approach [9, 18, 22] to a repair algorithm for our problem. When the
underlying model checking algorithm discovers a possible leak, CureSpec
modifies the program to eliminate this vulnerability. Then it resumes the
verification process, and eliminates further vulnerabilities until the program
is secure. An important feature of our technique is that the modified code is
not verified from scratch, but the model checking algorithm maintains its
state and re-uses the information obtained thus far. Finally, when CureSpec
proves safety of the (possibly repaired) program, the underlying Pdr-algorithm
produces an inductive invariant, which is a formal certificate of the desired
security property.

We implemented CureSpec in SeaHorn [17], a verification framework for C
programs, and evaluated it on the “standard” test cases for Spectre
vulnerabilities, as well as different parts of OpenSSL, demonstrating its
practicality.

To summarize, in this paper we provide the first method that _combines_ the
following aspects:

  1. 1.

formal verification of programs with respect to information leaks under
speculation, parameterized by a threat model;

  2. 2.

automatic repair by insertion of mitigations that stop speculative execution;

  3. 3.

formal guarantees for the repaired code in form of inductive invariants; and

  4. 4.

an implementation that scales to practical encryption algorithms.

##  2 Preliminaries

###  2.1 Model Checking Programs

We consider first-order logic modulo a theory $\mathcal{T}$ and denote it by
$FOL(\mathcal{T})$. We adopt the standard notation and terminology, where
$FOL(\mathcal{T})$ is defined over a signature $\Sigma$ of constant, predicate
and function symbols, some of which may be interpreted by $\mathcal{T}$. In
this paper $\mathcal{T}$ is the theory of Linear Integer Arithmetic and Arrays
(LIA). We use true and false to denote the constant truth values.

#### Transition Systems

We define transition systems as formal models of programs. Let $X$ be a set of
variables, used to represent program variables. A _state_ is a valuation of
$X$. For a state $\sigma$ and $a\in X$, we denote by $\sigma[a]$ the value of
$a$ in $\sigma$. We write $\theta(X)$ to represent a formula over $X$ in
$FOL(\mathcal{T})$. $\theta(X)$ is called a _state formula_ and represents a
set of states.

A _transition system_ is a tuple $M=\langle
X,\mathit{Init}(X),\mathit{Tr}(X,X^{\prime})\rangle$ where $\mathit{Init}(X)$
and $\mathit{Tr}(X,X^{\prime})$ are quantifier-free formulas in
$FOL(\mathcal{T})$. $\mathit{Init}$ represents the initial states of the
system and $\mathit{Tr}$ represents the (total) transition relation. We write
$\mathit{Tr}(X,X^{\prime})$ to denote that $\mathit{Tr}$ is defined over
variables $X\cup X^{\prime}$, where $X$ is used to represent the pre-state of
a transition, and $X^{\prime}=\\{a^{\prime}\mid a\in X\\}$ is used to
represent the post-state. A _path_ in a transition system is a sequence of
states $\pi:=\sigma_{0},\sigma_{1},\ldots$, such that for $i\geq 1$:
$(\sigma_{i-1},\sigma_{i}^{\prime})\models\mathit{Tr}$. We also consider the
case where a path is a finite sequence of states such that every two
subsequent states have a transition. We use $\pi[i]$ to refer to the $i$-th
state of $\pi$, namely $\sigma_{i}$. We use $\pi^{[0..n]}$ to refer to the
prefix $\sigma_{0},\sigma_{1},\ldots,\sigma_{n}$, and $\pi^{n}$ to the suffix
$\sigma_{n},\ldots$ of $\pi$. A path (or a prefix of a path) is called an
_execution_ of $M$ when $\sigma_{0}\models\mathit{Init}$. Given two paths
$\pi_{1}=\sigma_{0},\sigma_{1}\ldots$ and
$\pi_{2}=\sigma^{\prime}_{0},\sigma^{\prime}_{1}\ldots$, then
$\pi=\pi_{1}^{[0..n]}\pi_{2}$ is a path if
$(\sigma_{n},\sigma^{\prime}_{0})\models\mathit{Tr}$.

A formula $\varphi(X,X^{\prime})$ such that for every valuation $\mathit{I}$
of $X$ there is exactly one valuation $\mathit{I}^{\prime}$ of $X^{\prime}$
such that $(\mathit{I},\mathit{I}^{\prime})\models\varphi(X,X^{\prime})$ is
called a _state update function_. For $Y\subseteq X$, we denote by
$\mathsf{id}(Y,Y^{\prime})$ the state update function $\bigwedge_{a\in
Y}a^{\prime}=a$. While $\mathsf{id}(Y,Y^{\prime})$ is a formula over $Y\cup
Y^{\prime}$, for readability we use $\mathsf{id}(Y)$.

#### Safety Verification

A _safety problem_ is a tuple $\langle M,\mathit{Bad}(X)\rangle$, where
$M=\langle X,\mathit{Init},\mathit{Tr}\rangle$ is a transition system and
$\mathit{Bad}$ is a quantifier-free formula in $FOL(\mathcal{T})$ representing
a set of bad states. A safety problem has a _counterexample of length $n$_ if
there exists an execution $\pi:=\sigma_{0},\ldots,\sigma_{n}$ with
$\sigma_{n}\models\mathit{Bad}$. The safety problem is _SAFE_ if it has no
counterexample, of any length. It is _UNSAFE_ otherwise.

A _safe inductive invariant_ is a formula $\mathit{Inv}(X)$ such that  (i)
$\mathit{Init}(X)\rightarrow\mathit{Inv}(X)$,  (ii)
$\mathit{Inv}(X)\wedge\mathit{Tr}(X,X^{\prime})\rightarrow\mathit{Inv}(X^{\prime})$,
and  (iii) $\mathit{Inv}(X)\rightarrow\neg\mathit{Bad}(X)$.  If such a safe
inductive invariant exists, then the safety problem is SAFE.

In this work we use Spacer [22] as a solver for a given safety problem. Spacer
is based on the Property Directed Reachability (Pdr) algorithm [9, 18].
Algorithm 1 presents Spacer as a set of rules, following the presentation
style of [18]. We only give a brief overview of Pdr and Spacer and highlight
the details needed later in the paper for CureSpec. Given a safety problem,
Spacer tries to construct an inductive invariant, or find a counterexample. In
order to construct an inductive invariant, Spacer maintains a sequence of
formulas $F_{0},F_{1},\ldots,F_{N}$, with the following properties:  (i)
$F_{0}\rightarrow\mathit{Init}$;  (ii) $\forall 0\leq j<N\cdot
F_{j}\rightarrow F_{j+1}$;  (iii) $\forall 0\leq j<N\cdot
F_{j}(X)\land\mathit{Tr}(X,X^{\prime})\rightarrow F_{j+1}(X^{\prime})$; and
(iv) $\forall 0\leq j<N\cdot F_{j}\rightarrow\neg\mathit{Bad}$.

$F_{j}$ is an over-approximation of the states reachable in $j$ steps or less.
Additionally, Spacer maintains a set Reach of states that are known to be
reachable. Reach is an under-approximation of the reachable states.

Pdr performs a backward traversal of the states space. The traversal is
performed starting from states that violate $\mathit{Bad}$ and constructing a
suffix of a counterexample backwards, trying to either show that a state that
can reach $\mathit{Bad}$ is reachable (Candidate, Predecessor and Cex rules)
or prove that such states are unreachable (NewLemma and Push rules). During
this process the trace of over-approaximations $F_{0},F_{1},\ldots,F_{N}$ is
constructed and reachable states are discovered. We later show how these are
used in CureSpec. For more details about Pdr and Spacer the interested reader
is referred to [9, 18, 22].

Input: A safety problem $\langle
X,\mathit{Init}(X),\mathit{Tr}(X,X^{\prime}),\mathit{Bad}(X)\rangle$.

Assumptions: $\mathit{Init}$, $\mathit{Tr}$ and $\mathit{Bad}$ are quantifier
free.

Data: A queue $\mathcal{Q}$ of potential counterexamples, where
$c\in\mathcal{Q}$ is a pair $\langle m,j\rangle$, $m$ is a cube over state
variables, $j\in\mathbb{N}$. A level $N$. A sequence $F_{0},F_{1},\ldots$. An
invariant $F_{\infty}$. A set of reachable states Reach.

Output: (_SAFE_ , $F_{\infty}$), where $F_{\infty}$ is a safe inductive
invariant, or _Cex_

Initially: $\mathcal{Q}=\emptyset$, $N=0$, $F_{0}=\mathit{Init}$, $\forall
j\geq 1\cdot F_{j}=\mathit{true}$, $F_{\infty}=\mathit{true}$.

Require: $\mathit{Init}\to\neg\mathit{Bad}$

repeat

Safe

If $F_{\infty}\to\neg\mathit{Bad}$ return (_SAFE_ , $F_{\infty}$).

Cex

If $\langle m,j\rangle\in\mathcal{Q}$ and ,
$m\cap(\textsc{Reach})\neq\emptyset$ return _Cex_.

Unfold

If $F_{N}\rightarrow\neg\mathit{Bad}$, then set $N\leftarrow N+1$.

Candidate

If for some $m$, $m\to F_{N}\land\mathit{Bad}$, then add $\langle m,N\rangle$
to $\mathcal{Q}$.

Predecessor

If $\langle m,j+1\rangle\in\mathcal{Q}$ and there are $m_{0}$ and $m_{1}$ s.t.

$m_{1}\to m$, $m_{0}\land m^{\prime}_{1}$ is satisfiable, and $m_{0}\land
m_{1}^{\prime}\to F_{j}\land\mathit{Tr}\land m^{\prime}$, then

add $\langle m_{0},j\rangle$ to $\mathcal{Q}$.

* NewLemma

For $0\leq j<N$: given $\langle m,j+1\rangle\in\mathcal{Q}$ and a clause
$\varphi$ s.t. $\varphi\to\neg m$,

if $(\textsc{Reach})\to\varphi$, and $\varphi\land
F_{j}\land\mathit{Tr}\to\varphi^{\prime}$, then add $\varphi$ to $F_{k}$, for
$k\leq j+1$.

* ReQueue

If $\langle m,j\rangle\in\mathcal{Q}$, and $F_{j-1}\land\mathit{Tr}\land
m^{\prime}$ is unsatisfiable, then

add $\langle m,j+1\rangle$ to $\mathcal{Q}$.

* Push

For $1\leq j$ and a clause $(\varphi\lor\psi)\in F_{j}\setminus F_{j+1}$,

if $(\textsc{Reach})\to\varphi$ and $\varphi\land
F_{j}\land\mathit{Tr}\to\varphi^{\prime}$, then

add $\varphi$ to $F_{k}$, for each $k\leq j+1$.

* MaxIndSubset

If there is $j>N$ s.t. $F_{j+1}\subseteq F_{j}$, then

$F_{\infty}\leftarrow F_{i}$, and $\forall k\geq j\cdot F_{j}\leftarrow
F_{\infty}$.

* Successor

If $\langle m,j+1\rangle\in\mathcal{Q}$ and exist $m_{0}$, $m_{1}$ s.t.

$m_{0}\land m^{\prime}_{1}$ are satisfiable and $m_{0}\land
m^{\prime}_{1}\to(\textsc{Reach})\land\mathit{Tr}\land m^{\prime}$, then

add $m_{1}$ to Reach.

* ResetQ

$\mathcal{Q}\leftarrow\emptyset$.  ResetReach
$\textsc{Reach}\leftarrow\mathit{Init}$.

until  _$\infty$_ ;

Algorithm 1 The rules of the Spacer procedure.

###  2.2 Standard Program Semantics

We assume a program $P$ is represented in a low-level language (e.g. LLVM bit-
code) with standard semantics, and includes standard low-level instructions
such as unary and binary operations, conditional and unconditional branches,
load and store for accessing memory. In addition, it includes the instructions
$\textsf{assume}(b)$ and $\textsf{assert}(b)$ used for safety verification.

Let $i\in\mathbb{N}$ be a line in the program $P$ to be encoded. For
simplicity we refer to the instruction at line $i$ as $i$, and write $i\in P$.
We assume there is a special program variable $\mathsf{pc}\in X$, called the
_program counter_ , defined over the domain $\mathbb{N}\cup\\{\bot\\}$. Let
$i\in P$ be an instruction to be encoded. If $i$ is a conditional branch
instruction, it is encoded by a _conditional state update function_ of the
form

$\tau_{i}(X,X^{\prime}):=\mathsf{pc}=i\rightarrow(\mathit{cond}_{i}(X)\ ?\
\mathsf{pc}^{\prime}=\vartheta_{i}(X):\mathsf{pc}^{\prime}=\varepsilon_{i}(X))\land\mathsf{id}(X\setminus\\{\mathsf{pc}\\}),$

where $\mathit{cond}_{i}(X)$ is the condition represented by a state formula
and $\mathsf{pc}$ is updated to $\vartheta_{i}(X)$ when the condition holds,
and otherwise it is updated to $\varepsilon_{i}(X)$.

All other instructions are encoded by an _unconditional state update function_
of the form
$\tau_{i}(X,X^{\prime}):=\mathsf{pc}=i\rightarrow\varphi_{i}(X,X^{\prime})$,
where $\varphi_{i}(X,X^{\prime})$ is a state update function 222Note that
$\mathsf{pc}$ is updated also by $\varphi_{i}$. We therefore assume that
unconditional state update functions accompany every instruction that is not a
conditional branch.. Instructions are either conditional or unconditional
depending on their corresponding state update function. We denote by
$C\subseteq P$ the set of conditional instructions, i.e., if $i\in C$, then
$\tau_{i}$ is a conditional state update function.

The semantics for the verification instruction
$\textsf{assume}(\mathit{cond}_{i}(X))$ is captured by a state update
function, which is encoded by

$\displaystyle\tau_{i}(X,X^{\prime}):=\mathsf{pc}=i\rightarrow((\mathit{cond}_{i}(X)\
?\ \mathsf{pc}^{\prime}=\vartheta_{i}(X)\
:\mathsf{pc}^{\prime}=\mathsf{pc})\wedge\mathsf{id}(X\setminus\\{\mathsf{pc}\\})).$

This encoding requires that at line $i$ the condition $\mathit{cond}_{i}(X)$
holds. If it does not hold, then the transition relation is stuck in an
infinite loop and the program does not progress. Similarly,
$\textsf{assert}(\mathit{cond}(X))$ is captured by a state update function,
which is encoded by

$\displaystyle\tau_{i}(X,X^{\prime}):=\mathsf{pc}=i\rightarrow((\mathit{cond}_{i}(X)\
?\ \mathsf{pc}^{\prime}=\vartheta_{i}(X)\
:\mathsf{pc}^{\prime}=\bot)\wedge\mathsf{id}(X\setminus\\{\mathsf{pc}\\}))$

For assert, if the condition $\mathit{cond}_{i}(X)$ holds, the program
continues. Otherwise, $\mathsf{pc}$ is set to $\bot$. This special case allows
us to create a safety verification problem by defining the bad states to be
those where $\mathsf{pc}=\bot$. To ensure the resulting transition relation is
total, we add a state update function that makes sure that if a state where
$\mathsf{pc}=\bot$ is ever reached, this state is stuttering:

$\displaystyle\tau_{\bot}(X,X^{\prime}):=pc=\bot\rightarrow\mathsf{id}(X)$

To conclude, given a program $P$, we obtain a symbolic representation of the
transition relation by conjoining the formulas for all lines of the program
including $\tau_{\bot}$, i.e.,
$\mathit{Tr}(X,X^{\prime}):=(\bigwedge_{i}\tau_{i}(X,X^{\prime}))\land\tau_{\bot}(X,X^{\prime})$.
The corresponding safety problem is then defined by the resulting transition
system $M=\langle X,\mathit{Init},\mathit{Tr}\rangle$ and a set of bad states,
given as $\mathit{Bad}(X):=\mathsf{pc}=\bot$.

###### Remark 1

Let $P$ be a program, $\langle M,\mathit{Bad}\rangle$ the corresponding safety
problem, and $\pi=\sigma_{0},\sigma_{1},\ldots,\sigma_{n}$ an execution of
$M$. Then, for every $1\leq j\leq n$ such that
$(\sigma_{j-1},\sigma_{j}^{\prime})\models\mathit{Tr}$ there exists $i\in P$
such that $(\sigma_{j-1},\sigma_{j}^{\prime})\models\tau_{i}$. We denote this
as $i\in\pi$. Moreover, if $\sigma_{n}\models\mathit{Bad}$ then there exists
an assertion violation in $P$.

##  3 Modeling Speculative Execution Semantics

When analyzing the _functionality_ of a program, speculative execution can be
ignored since the results of a computation that is based on _misspeculation_
do not alter the program’s state: if the condition of a branch turns out to be
wrong after speculative execution, any of its results (visible in the
microarchitecture, but not on the program level) are discarded and computation
backtracks to the correct branch. However, the data used in such a computation
may still leak through side channels. Therefore, when analyzing _information
leaks through side channels_ , the formal model must include speculative
execution semantics and take into account possible observations based on
misspeculation.

In this section, we first discuss the notion of security and threat models we
consider. Later we give a formal definition of the speculative execution model
in Section 3.2.

###  3.1 Threat Models for Speculative Information Leaks

Verifying secure information flow deals with proving that confidential data
does not flow to public outputs during the execution of a system [15]. Another
way of describing secure information flow is by specifying that confidential
data is not _observable_ by an attacker.

A well-known class of attacks that can cause information leaks are _timing-
attacks_. These attacks use observations about the run-time of a system in
order to infer secret data. More precisely, in order for a program to be
secure against timing-attacks any two executions of a system where the public
inputs and outputs are equivalent for both executions, should be
indistinguishable w.r.t. some measure of time (e.g. time to execute a program,
latency in memory access, etc.).

Most variants of the Spectre attack fall within this class of timing-attacks.
These attacks use side-effects of cache collisions caused by code that
executes speculatively in order to leak secret information. It is important to
note that speculative execution does not change the architectural state of the
CPU and only has side-effects (e.g. modifications to the cache). Consequently,
if we consider a program to be secure with respect to standard execution
semantics, given two different executions of that program that start from the
same public inputs, where one execution uses speculative execution and the
other does not, both produce the same public outputs. However, due to the
side-effects caused by speculative execution, these two executions may still
be distinguishable.

We therefore use the following definition of Constant-Time Security (cp. [2]):

###### Definition 1

Let $M$ be a transition system of a program $P$, let $H\subseteq X$ be a set
of high-security variables and $L:=X\setminus H$ a set of low-security
variables. $M$ is _Constant-Time Secure_ if for any two executions $\pi_{1}$
and $\pi_{2}$ of $M$ with $\forall x\in
L,i\in\mathbb{N}\cdot\pi_{1}[i][x]=\pi_{2}[i][x]$ are also indistinguishable.

Since the focus of this paper is timing-attacks that can incur due to Spectre,
we make the standard assumption that the attacker can _distinguish_ executions
if they differ in the values of $\mathsf{pc}$, i.e., their control-flow, or in
the location of certain memory accesses. We collect these _vulnerable memory
instructions_ in a set $\texttt{VInst}\subseteq P$.

In practice, identifying these instructions depends on our assumptions on the
attacker capabilities in the given setting333Compared to the work in [7], our
threat model is parameterized in the set of vulnerable instructions and
strictly generalizes the fixed threat model used there.. We consider two
variants of Spectre- PHT vulnerabilities that are based on the classification
by Canella et al. [10]:

  * •

we consider a _strong_ Spectre model, where the attacker is very powerful and
can observe the value of any array access, i.e., any memory access (e.g. array
access $a[i]$) is in VInst. This is motivated by the use of side-channels
other than cache timing attacks (and by advanced mistraining strategies for
the speculation unit [10]).

  * •

in the _classical_ Spectre model, an attacker uses the cache content for
timing attacks, i.e., if the location $i$ of an array access $a[i]$ is
controlled by the attacker (e.g., the attacker can directly provide it as an
input, or the inputs of the attacker have some influence on $i$), then a
nested array access $b[a[i]]$ can be used to reveal the content of $a[i]$.
Therefore, here we consider VInst to contain all array accesses that amount,
directly or indirectly, to a nested array access at an attacker-controlled
position. Detecting such array accesses can be done statically, using
information flow analysis techniques like taint tracking or self-composition.

###  3.2 Formal Model of Speculative Execution Semantics

Our goal is to check for information leaks _under speculative execution_. To
this end, we _assume_ that the given program $P$ is constant-time secure in
the absence of speculation. We will show that this allows us to reduce the
problem of detecting speculative information leaks to the standard safety
property of checking whether instructions in the given set VInst are reachable
under speculation in $P$. First, let us formalize the speculative semantics of
$P$.

Let $M=\langle X,\mathit{Init},\mathit{Tr}\rangle$ be the standard transition
system (Section 2.1) of the program $P$ and VInst the set of vulnerable
instructions. Define the set of Boolean auxiliary variables used to model
fences as $\mathcal{F}:=\\{\mathsf{fence}_{i}\mid i\in P\\}$, and let
$B\subseteq P$ be the set of fenced instructions, i.e., with
$\mathsf{fence}_{i}=\textsf{true}$. Then, the transition system that includes
speculative execution semantics is defined as
$\hat{M}:=\langle\hat{X},\hat{\mathit{Init}},\hat{\mathit{Tr}}\rangle$ where
$\hat{X}:=X\cup\\{\mathsf{spec}\\}\cup\mathcal{F}$, where $\mathsf{spec}$ is
of sort $\mathbb{N}_{0}$. The initial states of $\hat{M}$ are defined as

$\displaystyle\hat{\mathit{Init}}(\hat{X}):=$
$\displaystyle\mathit{Init}\land(\mathsf{spec}=0)\land\bigwedge_{i\in
B}\mathsf{fence}_{i}\land\bigwedge_{i\in P\setminus B}\neg\mathsf{fence}_{i}$

where spec is initialized to $0$, and auxiliary variables in $\mathcal{F}$ are
initialized to true if the corresponding instruction is fenced, and otherwise
to false.

To define $\hat{\mathit{Tr}}$, recall that speculation starts if the wrong
branch is taken for some $i\in C$. At the first such position, $\mathsf{spec}$
becomes positive and remains positive for the rest of the execution. In order
to formally model this behavior we modify the state update functions in the
following manner.

#### Conditional Instructions

The state update function for each conditional instruction $i\in C$ (as it
appears in Section 2.2) is defined as follows:

$\displaystyle\hat{\tau}_{i}(\hat{X},\hat{X}^{\prime})$
$\displaystyle:=\mathsf{pc}=i\rightarrow\Big{(}\mathsf{fence}_{i}\land\mathsf{spec}>0\
?\
\mathsf{id}(\hat{X}):\mathsf{id}(\hat{X}\setminus\\{\mathsf{spec},\mathsf{pc}\\})\,\land$
$\displaystyle\Big{[}((\mathsf{spec}^{\prime}=((\neg\mathit{cond}(X)\lor\mathsf{spec}>0)\
?\ \mathsf{spec}+1:0))\land\mathsf{pc}^{\prime}=\hat{\vartheta}(X))\,\lor$
$\displaystyle((\mathsf{spec}^{\prime}=((\mathit{cond}(X)\lor\mathsf{spec}>0)\
?\
\mathsf{spec}+1:0))\land\mathsf{pc}^{\prime}=\hat{\varepsilon}(X))\Big{]}\Big{)}$

Note that $\hat{\tau}_{i}$ is stuck in an infinite loop in case
$\mathsf{spec}>0$ and $\mathsf{fence}_{i}$ is set to true. Otherwise, if the
respective branch condition does not hold, the value of $\mathsf{spec}$ has to
become positive. If $spec$ is already positive, it remains positive and is
incremented. Overall, $\mathsf{spec}$ can only be positive in a given
execution iff at least one branch condition of the execution is not met.
Careful inspection of the state update function reveals the updates to
$\mathsf{pc}$ are different (e.g. $\hat{\vartheta}(X)$ instead of
$\vartheta(X)$). We address this later in the section ($\clubsuit$).

#### Unconditional Instructions

For unconditional instructions, we must take into account the new auxiliary
variables, as well as the fence assumptions that prevent speculation. Given an
unconditional instruction
$\tau_{i}(X,X^{\prime}):=pc=i\rightarrow\varphi(X,X^{\prime})$ we define
$\hat{\tau}_{i}$ in the following manner:

$\displaystyle\hat{\tau}_{i}(\hat{X},\hat{X}^{\prime}):=pc=i\rightarrow$
$\displaystyle\left.(\mathsf{fence}_{i}\land\mathsf{spec}>0\ ?\
\mathsf{id}(\hat{X}):\right.$ $\displaystyle\quad\
\hat{\varphi}(X,X^{\prime})\land\mathsf{id}(\mathcal{F})\land\mathsf{spec}^{\prime}=(\mathsf{spec}>0\
?\ \mathsf{spec}+1:0))$

Again, $\hat{\tau}_{i}$ enters an infinite loop in case $\mathsf{spec}>0$ and
$\mathsf{fence}_{i}$ is set to true.

#### Speculation Bound

In order to allow a realistic modeling of speculative execution, we consider a
model that only allows a bounded speculation window. This modeling comes from
the fact that, in any given microarchitecture, the Reorder Buffer (ROB) used
to allow out-of-order execution is limited in the number of instructions it
can occupy.

Therefore, we assume that for a given micro-architecture there exists a
parameter $\Bbbk$ that is a bound on speculative executions. In order to
enforce this bound, we constrain the transition relation $\hat{\mathit{Tr}}$
such that if $\mathsf{spec}$ ever reaches $\Bbbk$, $\hat{M}$ is stuck in an
infinite loop (this can be viewed as a global assumption).

This results in the following two cases for the transition relation:

$\displaystyle\hat{\mathit{Tr}}_{<\Bbbk}(\hat{X},\hat{X}^{\prime}):=$
$\displaystyle(\mathsf{spec}<\Bbbk)\land\bigwedge_{i\in
P}\hat{\tau}_{i}(\hat{X},\hat{X}^{\prime})$
$\displaystyle\hat{\mathit{Tr}}_{\geq\Bbbk}(\hat{X},\hat{X}^{\prime}):=$
$\displaystyle(\mathsf{spec}>=\Bbbk)\land\mathsf{id}(\hat{X})$

#### Speculative Constant-time Security as a Safety Property

We want to ensure that $P$ does not leak information under speculation. We
assume that the attacker has control over speculation, which implies that
$\mathsf{spec}\in L$. Therefore, the condition of Definition 1 needs to hold
for executions that make the same speculative choices (cp. _speculative
constant-time_ [11, 14]). Since we assume that the transition system $M$
(without speculation) is constant-time secure, we therefore only have to
compare speculative executions that agree on their control-flow. Since we also
assume that additional side-channel observations of the attacker are only
possible when a vulnerable instruction in VInst is executed, our problem
reduces to the standard safety property of checking whether instructions in
VInst are _reachable under speculation_. This can be modeled by adding an
assertion instruction $\mathbf{assert}(\mathsf{spec}==0)$ before every such
instruction.

In the transition relation, this is reflected by defining

$\displaystyle\hat{\tau}_{a_{i}}(\hat{X},\hat{X}^{\prime}):=\mathsf{pc}=a_{i}\rightarrow((\mathsf{spec}=0)\
?\ \mathsf{pc}^{\prime}=i\
:\mathsf{pc}^{\prime}=\bot)\wedge\mathsf{id}(\hat{X}\setminus\\{\mathsf{pc}\\}))$

and letting

$\hat{\mathit{Tr}}(\hat{X},\hat{X}^{\prime}):=\left(\hat{\mathit{Tr}}_{<\Bbbk}(\hat{X},\hat{X}^{\prime})\land\bigwedge_{i\in\texttt{VInst}}\hat{\tau}_{a_{i}}(\hat{X},\hat{X}^{\prime})\land\tau_{\bot}(\hat{X},\hat{X}^{\prime})\right)\lor\hat{\mathit{Tr}}_{\geq\Bbbk}(\hat{X},\hat{X}^{\prime}).$

The addition of these assertions is the reason for the different $\mathsf{pc}$
updates in $\hat{\tau}$ ($\clubsuit$). Namely, an instruction $j\in P$ that
precedes an instruction $i\in\texttt{VInst}$ now needs to precede the
corresponding assertion $a_{i}$.

Now, we can encode constant-time security with respect to speculative
execution as the safety problem $\langle\hat{M},\hat{\mathit{Bad}}(X)\rangle$,
where

$\hat{\mathit{Bad}}(X):=\mathsf{pc}=\bot,$

i.e., the definition of bad states remains unchanged.

#### Properties of the Speculative Execution Semantics

We give some useful properties of the above semantics. The proofs can be found
in Appendix 0.A.

######  Lemma 1 ()

Let $P$ be a program, $M=\langle X,\mathit{Init},\mathit{Tr}\rangle$ its
transition system, and $\hat{M}$ the transition system including speculative
execution semantics. Then, there exists a simulation relation between $M$ and
$\hat{M}$, denoted $M\leq_{\text{sim}}\hat{M}$.

######  Lemma 2 ()

Let $\pi=\sigma_{0},\sigma_{1},\ldots,\sigma_{k}$ be an execution of $\hat{M}$
such that $\sigma_{k}\models\hat{\mathit{Bad}}$. Then the following conditions
hold:  (i) $\sigma_{0}\models\mathsf{spec}=0$ (ii)
$\sigma_{k}\models\mathsf{spec}>0$ (iii) There exists a unique $0\leq j<k$
such that $\sigma_{j}\models\mathsf{spec}=0$ and
$\sigma_{j+1}\models\mathsf{spec}>0$.

######  Lemma 3 ()

Let $P$ be a program, $M=\langle X,\mathit{Init},\mathit{Tr}\rangle$ its
transition system, and $\texttt{VInst}\subseteq P$. Assume that $M$ is
constant-time secure, where observations of the attacker are determined by
VInst. Let
$\hat{M}=\langle\hat{X},\hat{\mathit{Init}},\hat{\mathit{Tr}}\rangle$ be the
transition system of $P$ that includes speculative execution semantics. If
$\hat{M}$ is SAFE wrt. $\hat{Bad}$, then $\hat{M}$ is constant-time secure,
i.e., $P$ does not leak information under speculation.

##  4 Automatic Repair under Speculative Execution

In this section we describe CureSpec, an automatic, model checking based
repair algorithm, that fixes Spectre related information leaks under
speculative execution. All proofs can be found in Appendix 0.A. CureSpec
receives a program $P$ and a set of vulnerable instructions VInst. If CureSpec
detects that an instruction $i\in\texttt{VInst}$ is executed under
speculation, it repairs $P$ by analyzing the leaking execution and adding a
fence instruction that disables speculation in program locations that enabled
the leak. This process is iterative and continues until CureSpec proves that
$P$ is secure.

Given a program $P$, its speculative transition system $\hat{M}$, and the
safety problem $\hat{T}=\langle\hat{M},\hat{\mathit{Bad}}\rangle$ (as defined
in Section 3, w.r.t. a set of vulnerable instructions VInst). Recall that
Algorithm 1 can determine if $\hat{T}$ is SAFE or UNSAFE. When Algorithm 1
returns SAFE, then $\hat{M}$ is constant-time secure with respect to VInst and
speculative execution. Otherwise, a counterexample describing a speculative
execution that may leak information is returned and Algorithm 1 terminates.

CureSpec builds upon Algorithm 1 and extends it such that if $\hat{T}$ is
UNSAFE, instead of terminating, repair is applied. The repair process is
iterative - when a leak is detected, it is analyzed, a fence is added to
mitigate the leak, and verification is reapplied on the repaired program.
However, CureSpec is _incremental_ in the sense that it maintains the state of
Algorithm 1 as much as possible and reuses it when verification re-executes.
To this end, CureSpec includes all rules of Algorithm 1 excluding the Cex
rule, and including two additional rules as described in Algorithm 2: SpecLeak
and AddFence.

####  SpecLeak

This rule replaces the rule Cex from Algorithm 1 and prevents the algorithm
from terminating when a counterexample is found. Instead, the leaking
execution is stored in $\pi$.

####  AddFence

This rule is responsible for the repair. The trace $\pi$ is analyzed, and
based on the misspeculation that leads to a information leak, a fence that
makes $\pi$ unfeasible is added (by letting $\mathsf{fence}_{k}=\textsf{true}$
in $\hat{Init}$ for some $k$). Note that the trace of $F_{i}$ and the
invariant $F_{\infty}$ are unchanged which ensures incrementality of the
overall algorithm.

The Safe rule is amended to additionally return the list of added fences.

Input: A safety problem $\langle\hat{M},\hat{\mathit{Bad}}(\hat{X})\rangle$
with $\hat{M}=\langle\hat{X},\hat{\mathit{Init}},\hat{\mathit{Tr}}\rangle$.

Assumptions: $\hat{\mathit{Init}}$, $\hat{\mathit{Tr}}$ and
$\hat{\mathit{Bad}}$ are quantifier free.

Data: A queue $\mathcal{Q}$ of potential counterexamples, where
$c\in\mathcal{Q}$ is a pair $\langle m,j\rangle$, $m$ is a cube over state
variables, $j\in\mathbb{N}$. A level $N$. A trace $F_{0},\ldots,F_{N}$. An
invariant $F_{\infty}$. A set of reachable states Reach.

Output: A list of added fences $\mathcal{L}$ and a safe inductive invariant
$F_{\infty}$

Initially: $\mathcal{Q}=\emptyset$, $N=0$, $F_{0}=\hat{\mathit{Init}}$,
$\forall j\geq 1\cdot F_{j}=\mathit{true}$, $F_{\infty}=\mathit{true}$,

$\pi=\langle\rangle$, $\mathcal{L}=\emptyset$.

Require: $\hat{\mathit{Init}}\to\neg\hat{\mathit{Bad}}$

repeat

SpecLeak

If $\langle m,j\rangle\in\mathcal{Q}$ and $m\cap\textsc{Reach}\neq\emptyset$.

Let $\pi^{\prime}=\langle m=\sigma_{j},\sigma_{j+1},\ldots,\sigma_{N}\rangle$
be a path of $\hat{M}$ where $\sigma_{N}\models\hat{\mathit{Bad}}$.

Then $\pi^{\prime}$ can be extended into an execution
$\pi=\pi^{*}\pi^{\prime}$ of $\hat{M}$.

* AddFence

If $\pi\neq\langle\rangle$, choose $j\leq k\leq N$ where
$\sigma_{k}\models\mathsf{spec}>0$. Modify $\hat{\mathit{Init}}$

s. t. $\hat{\mathit{Init}}\models\mathsf{fence}_{k}$.
$\mathcal{L}\leftarrow\mathcal{L}\cup\\{\mathsf{fence}_{k}\\}$.
$\mathcal{Q}\leftarrow\emptyset$,
$\textsc{Reach}\leftarrow\hat{\mathit{Init}}$, $\pi\leftarrow\langle\rangle$.

until  _$\infty$_ ;

Algorithm 2 Repair algorithm CureSpec

###  4.1 Analyzing the Leaking Execution $\pi$

When Algorithm 2 detects a potential leak in $\hat{M}$, SpecLeak stores this
execution in $\pi$. In AddFence, Lemma 2 is used to identify where speculation
starts in $\pi$. Based on that, we define the following:

###### Definition 2

Let $\pi=\sigma_{0},\ldots,\sigma_{N},\ldots$ be an execution of $\hat{M}$
such that $\sigma_{N}\models\hat{\mathit{Bad}}$, and $0<k\leq N$ such that
$\sigma_{k-1}\models\mathsf{spec}=0$ and $\sigma_{k}\models\mathsf{spec}>0$.
Then $\pi^{[0..k-1]}=\sigma_{0},\ldots,\sigma_{k-1}$ is called the _non-
speculating prefix_ of $\pi$, and $\pi^{k}=\sigma_{k},\ldots$ the _speculating
suffix_ of $\pi$. We call $k$ the _speculative split point_ of $\pi$.

By construction, we have $\mathsf{spec}=0$ in $\pi^{[0..k-1]}$. Therefore,
letting $\mathsf{fence}_{i}=\textsf{true}$ for any instruction
$i\in\pi^{[0..k-1]}$ has no effect on the transitions in $\pi^{[0..k-1]}$.
However, since $\mathsf{spec}>0$ in $\pi^{k}$, letting
$\mathsf{fence}_{i}=\textsf{true}$ for any $i\in\pi^{k}$ makes $\pi$ an
unfeasible path. In order to formalize this intuition we use the following
definition and lemmas.

###### Definition 3

Let $P$ be a program and
$\hat{M}=\langle\hat{X},\hat{\mathit{Init}},\hat{\mathit{Tr}}\rangle$ its
speculative execution transition system. If for $i\in P$ it holds that
$\hat{\mathit{Init}}\models\neg\mathsf{fence}_{i}$, then adding a fence to $i$
results in a new transition system
$\hat{M}_{i}=\langle\hat{X},\hat{\mathit{Init}}_{i},\hat{\mathit{Tr}}\rangle$
where
$\hat{\mathit{Init}}_{i}:=\hat{\mathit{Init}}[\neg\mathsf{fence}_{i}\leftarrow\mathsf{fence}_{i}]$.

Here,
$\hat{\mathit{Init}}[\neg\mathsf{fence}_{i}\leftarrow\mathsf{fence}_{i}]$
denotes the substitution of $\neg\mathsf{fence}_{i}$ with
$\mathsf{fence}_{i}$. After substitution it holds that
$\hat{\mathit{Init}}_{i}\models\mathsf{fence}_{i}$, and initialization for all
other variables is unchanged. Thus, the initial value of $\mathsf{fence}_{i}$
is the only difference between $\hat{M}_{i}$ and $\hat{M}$.

######  Lemma 4 ()

Let $\pi=\sigma_{0},\ldots,\sigma_{N}$ be an execution of $\hat{M}$ such that
$\sigma_{N}\models\hat{\mathit{Bad}}$ and $k\leq N$ be its speculative split
point. For any instruction $i\in P$ such that $i\in\pi^{k}$ (see Remark 1),
$\hat{\mathit{Init}}\models\neg\mathsf{fence}_{i}$. Moreover, $\pi$ is not an
execution of $\hat{M}_{i}$ and for every execution
$\hat{\pi}=\hat{\sigma}_{0},\ldots,\hat{\sigma}_{m}$ of $\hat{M}_{i}$,
$\hat{\pi}\pi^{k}$ is not an execution of $\hat{M}_{i}$.

By Lemma 4, it is sufficient to let $\mathsf{fence}_{i}=\textsf{true}$ for any
instruction $i\in\pi^{k}$ in order to make $\pi$ an unfeasible path. Then,
CureSpec can be resumed and search for a different leaking execution, or prove
that the added fences make $P$ secure. This results in the following
properties of our repair algorithm.

###  4.2 Properties of CureSpec (Algorithm 2)

As noted earlier, CureSpec is _parametrized_ by the set VInst of possibly
vulnerable instructions. While in this paper we focus on instructions that are
vulnerable to Spectre, CureSpec can detect other kinds of instructions that
are executed under speculation, and as a result, repair such instances where
execution under speculation may lead to unwanted transient behavior.

######  Theorem 4.1 ()

Let $P$ be a program and
$\hat{M}=\langle\hat{X},\hat{\mathit{Init}},\hat{\mathit{Tr}}\rangle$ its
speculative execution transition system. Then, on input
$\langle\hat{M},\hat{\mathit{Bad}}\rangle$, CureSpec terminates and returns a
list $\mathcal{L}$ such that for
$\hat{M}_{s}=\langle\hat{X},\hat{\mathit{Init}}_{s},\hat{\mathit{Tr}}\rangle$,
where $\forall
i\in\mathcal{L}\cdot\hat{\mathit{Init}}_{s}\models\mathsf{fence}_{i}$, it
holds that $\langle\hat{M}_{s},\hat{\mathit{Bad}}\rangle$ is SAFE (as
witnessed by the final invariant $F_{\infty}$).

The proof idea is that we are making progress whenever we add a fence, since
there are only finitely many possible fence positions. Moreover, if we put a
fence before every instruction, then there certainly cannot be any speculative
leaks.

######  Lemma 5 (Incrementality)

Let $P$ be a program and let $M$ and $\hat{M}$ be its transition system and
speculative execution transition system, respectively. For $i\in P$, if
$\hat{\mathit{Init}}\models\neg\mathsf{fence}_{i}$ then
$M\leq_{\text{sim}}\hat{M}_{i}\leq_{\text{sim}}\hat{M}$.

The proof of this lemma relies on the fact that adding a fence can only
exclude executions in $\hat{M}$ that are not possible in $M$.

By Lemma 5, over-approximations computed with respect to $\hat{M}$ are also
over-approximations with respect to $M$. This allows CureSpec to reuse
information between different repair iterations. While rule AddFence resets
$\mathcal{Q}$, Reach, and $\pi$, it does not reset the current level $N$, the
trace $F_{0},\ldots,F_{N}$, and the invariant $F_{\infty}$, where $F_{\infty}$
and $F_{j}$ over-approximate the states that are reachable (in up to $j$
steps). Note that while AddFence resets Reach, in practice parts of Reach can
be retained even after a fence is added. Intuitively, the repair loop
resembles a Counterexample Guided Abstraction Refinement (CEGAR) loop [13].

This _incremental_ way of using Algorithm 1 within CureSpec makes repair
already much more efficient than a _non-incremental_ version that completely
re-starts verification after every modification (see Section 5). However,
allowing the algorithm to add fences after every instruction in $P$ may still
be inefficient, as there are (unnecessarily) many possibilities, and the
repair may add many unnecessary fences. Therefore, in the following we
describe several heuristics for optimizing the way fences are added.

###  4.3 Heuristics and Optimizations

#### Fence placement options

As described in Section 3, speculation can only start at conditional
instructions and the information leak itself happens at an instruction
$i\in\texttt{VInst}$. Thus, we can restrict the set of instructions for which
we introduce fence variables $\mathsf{fence}_{i}$ to one of the following:
(i) after each conditional instruction $i\in C$, in both branches, or  (ii)
before every instruction $i\in\texttt{VInst}$.  In the following, option (i)
will be called the _after-branch_ , and (ii) will be called _before-memory_.
In both cases correctness according to Theorem 4.1 is preserved.

#### Fence activation

When a leaking execution $\pi$ is found, there might be multiple positions for
a fence that would prevent it.We employ a heuristic that activates a fence
variable as close as possible to the bad state. In case that fence placement
option (i) is used, this means that $\pi$ is traversed backwards from the bad
state until a conditional instruction is reached, and a fence is activated in
the branch that appears in $\pi$. Under option (ii), the instruction
$i\in\texttt{VInst}$ that is causing the leak in $\pi$ is the last instruction
in $\pi$, and we activate the fence right before $i$. In both cases, this not
only removes the given leaking execution, but also other executions where
speculation starts before the newly added fence (cp. Lemma 4).

##  5 Implementation and Evaluation

#### Implementation

We implemented CureSpec 444https://github.com/user-28119294/CureSpec in the
SeaHorn verification framework [17]. This gives us direct access to an LLVM
front-end. We compile each benchmark (see below) with
Clang555https://clang.llvm.org/ 10.0.0 to LLVM using optimization level -O2.
The speculative execution semantics is added _after_ these compilation passes,
which is important because they might introduce new vulnerabilities.

The modified program is encoded into Horn rules [6] and then passed to Z3 [25]
version 4.10.2, SeaHorn’s internal solver. Upon termination, our tool can
output the inductive invariant of the repaired program, together with its
speculative semantics, in SMT-LIB format, such that this certificate can be
checked independently by any SMT solver that supports the LIA theory.

#### Evaluation: Benchmarks

We evaluated CureSpec on four sets of benchmarks. The first set consists of
Kocher’s 15 test
cases666https://www.paulkocher.com/doc/MicrosoftCompilerSpectreMitigation.html,
which are simple code snippets vulnerable to Spectre attacks. To show that
CureSpec can also handle complex programs from a domain that handles sensitive
data, we have selected representative and non-trivial (measured in the number
of LLVM instructions and conditional instructions, see Table 1 for details)
benchmarks from OpenSSL
3.0.0777https://github.com/openssl/openssl/tree/openssl-3.0.0 and the HACL*
[30] cryptographic library.

A first set of OpenSSL benchmarks includes two versions of AES block
encryptions:  (i) aes_encrypt, which uses lookup tables and  (ii)
aes_encrypt_ct, a constant-time version.  Both of these only encrypt a single
AES block. We also include both AES encryptions in cipher block chaining mode
(aes_cbc_encrypt and aes_cbc_encrypt_ct, respectively), which encrypt
arbitrarily many blocks, resulting in significantly more complex and
challenging benchmarks. The second set of SSL benchmarks includes functions
used for the multiplication, squaring, and exponentiation of arbitrary-size
integers (bn_mul_part, bn_sqr_part, and bn_exp_part, respectively). Since the
full versions of these include function calls to complex subprocedures (with
an additional 18900 LLVM-instructions and more than 4100 branches), we
abstract these called functions by uninterpreted functions. Finally, the HACL*
benchmarks include the following cryptographic primitives:  (i)
Curve25519_64_ecdh, the ECDH key agreement using Curve25519 [4],  (ii) the
stream cipher Chacha20_encrypt,  (iii) a message authentication code using the
Poly1305 hash family [3] (Poly1305_32_mac).

#### Evaluation: Repair Performance

We present in detail the repair performance of CureSpec based on the strong
threat model (see Section 3), i.e., VInst consists of all memory accesses in
the analyzed program888We did not analyze the benchmarks with respect to the
classical Spectre model, since that requires manual annotations of the code to
determine variables that the attacker can control, which require a deep
understanding of the code to be analyzed., and on the semantics with unbounded
speculation. Similar results for a bounded speculation window can be found in
Appendix 0.B. For each program, we evaluated the performance for all
combinations of the following options:  (a) incremental or non-incremental
repair,  (b) fence placement at every instruction, or according to one of the
heuristics (after-branch or before-memory) from Section 4.3. All experiments
were executed on an Intel® Xeon® Gold 6244 CPU @ 3.60GHz with 251GiB of main
memory.

Table 1: Evaluation results on Kocher’s test cases, OpenSSL, and HACL*
benchmarks. Test cases not in the table have the similar values as test2.
Columns $\\#_{i}$, $\\#_{b}$, and $\\#_{m}$ give the number of instructions,
conditional instructions and memory instructions, respectively, which is also
the maximal number of possible fences for the respective placement option
(every-inst, after-branch, before-memory). The number of inserted fences is
shown in the $\\#_{f}$ columns. Presented times are in seconds, averaged over
3 runs, with a timeout of 2 hours. RSS is the average maximum resident set
size in GiB.

Benchmark | baseline | after-branch | before-memory
---|---|---|---
| $\\#_{i}$ | $\\#_{f}$ | time | RSS | $\\#_{b}$ | $\\#_{f}$ | time | RSS | $\\#_{m}$ | $\\#_{f}$ | time | RSS
test1 | 14 | 5 | 0.4 | 0.12 | 2 | 1 | 0.1 | 0.07 | 2 | 1 | 0.1 | 0.06
test2 (and others) | 18 | 7 | 0.7 | 0.15 | 2 | 1 | 0.1 | 0.07 | 4 | 1 | 0.1 | 0.07
test5 | 20 | 1 | 0.3 | 0.16 | 4 | 2 | 0.2 | 0.08 | 2 | 1 | 0.1 | 0.07
test7 | 23 | 11 | 1.5 | 0.17 | 4 | 2 | 0.2 | 0.07 | 6 | 2 | 0.2 | 0.08
test9 | 21 | 10 | 1.2 | 0.16 | 2 | 1 | 0.1 | 0.06 | 5 | 1 | 0.1 | 0.08
test10 | 20 | 15 | 1.4 | 0.15 | 4 | 2 | 0.2 | 0.07 | 4 | 2 | 0.1 | 0.07
test12 | 20 | 9 | 0.9 | 0.15 | 2 | 1 | 0.1 | 0.06 | 4 | 1 | 0.1 | 0.07
test15 | 19 | 8 | 0.9 | 0.15 | 2 | 1 | 0.1 | 0.07 | 5 | 1 | 0.1 | 0.08
aes_encrypt_ct | 566 | timeout | 4 | 3 | 0.8 | 0.09 | 38 | 3 | 1.7 | 0.32
aes_encrypt | 476 | 116 | 3712.1 | 11.04 | 4 | 3 | 0.7 | 0.10 | 97 | 3 | 4.7 | 0.98
aes_cbc_encrypt_ct | 1302 | timeout | 40 | 15 | 100.7 | 0.65 | 102 | 10 | 80.6 | 1.41
aes_cbc_encrypt | 1122 | timeout | 40 | 15 | 774.5 | 1.51 | 220 | 10 | 135.1 | 4.34
bn_mul_part | 104 | 69 | 48.7 | 0.72 | 24 | 13 | 2.6 | 0.18 | 19 | 7 | 1.3 | 0.16
bn_sqr_part | 161 | 71 | 109.5 | 1.05 | 24 | 13 | 3.4 | 0.19 | 30 | 9 | 2.5 | 0.22
bn_exp_part | 307 | 139 | 1939.3 | 5.60 | 74 | 29 | 57.4 | 0.82 | 49 | 18 | 21.8 | 0.61
Chacha20_encrypt | 3552 | timeout | 6 | 3 | 8.0 | 0.33 | 117 | 2 | 8.4 | 1.90
Poly1305_32_mac | 483 | 93 | 1143.3 | 4.76 | 6 | 4 | 2.2 | 0.12 | 90 | 4 | 6.4 | 0.72
Curve25519_64_ecdh | 351 | timeout | 8 | 3 | 3115.3 | 1.92 | 44 | timeout

Table 1 summarizes the most important results, comparing the baseline (non-
incremental, every-inst fence placement without fence activation heuristic) to
two options that both use incrementality and the heuristic for fence
activation, as well as either after-branch or before-memory for fence
placement. We observe that the latter two perform better than the baseline
option, with a significant difference both in repair time and number of
activated fences, even on the test cases (except for test5, which is solved
with a single fence even without heuristics). Notably, all of the benchmarks
that time out in the baseline version can be solved by at least one of the
other versions, often in under 2 minutes.

While our heuristics make a big difference when compared against the baseline,
a comparison between the two fence placement heuristics does not show a clear
winner. The before-memory heuristic results in the smallest number of
activated fences for all benchmarks, but the difference is usually not big. On
the other hand, for the HACL* benchmarks (and some others), this heuristic
needs more time than the after-branch heuristic, and even times out for
Curver25519_64_ecdh, while after-branch solves all of our benchmarks.

Furthermore, we observe that the fence placement heuristics (after-branch or
before-memory) reduce the repair time by $81.8\%$ or $97.5\%$, respectively.
Incrementality, when considered over all parameter settings, reduces the
repair time on average by $10.3\%$, but on the practically relevant settings
(with fence placement heuristics) it reduces repair time by $21.5\%$.

The results for a bounded speculation window are comparable, except that this
seems to be significantly more challenging for CureSpec: repair times
increase, in some cases drastically, and aes_cbc_encrypt times out regardless
of the selected options. Note however that CureSpec currently does not
implement any optimizations that are specific to the bounded speculation mode.

Overall, our results show that CureSpec can repair complex code such as the
OpenSSL and HACL* examples by inserting only a few fences in the right places.
Note that for the OpenSSL and HACL* functions, the fences inserted by our
repair point to _possible_ vulnerabilities, but they might not correspond to
actual attacks because of over-approximations in the strong threat model.
I.e., CureSpec may add fences that are not strictly necessary to secure the
program.

#### Evaluation: Performance of Repaired Programs

We evaluate the performance impact of inserted fences on an Intel Core™
i7-8565U CPU @1.80GHz by comparing the runtimes of _non-fixed_ programs to
those of repaired programs obtained with after-branch and before-memory fence
placements, respectively. To get meaningful results we only use benchmarks
that have a non-negligible runtime and use 50 random seeds999obtained from
https://www.random.org/ to generate input data.101010Even though CureSpec with
bounded speculation window inserts fewer fences, their impact on performance
is very similar. Therefore, we only give a single table.

Table 2: Impact of inserted fences on performance. The time for the non-fixed
program is the combined runtime (for 50 random seeds), and the impact columns
show the increase in runtime compared to the non-fixed program, for programs
repaired with after-branch and before-memory placements, respectively.

Benchmark | input size | non-fixed | after-branch | before-memory
---|---|---|---|---
| [MiB] | time [s] | impact | impact
aes_cbc_encrypt_ct | 16 | 64.49 | 1.91% | 2.26%
aes_cbc_encrypt | 16 | 5.84 | 53.06% | 51.55%
Chacha20_encrypt | 64 | 9.86 | 6.69% | 7.57%
Poly1305_32_mac | 256 | 10.07 | 67.89% | 49.73%

Results are summarized in Table 2. Note that the performance impact is
negligible on the constant-time version of AES in cipher block chaining mode,
while we have big performance impact on the non-constant time version, even
though the number of instructions is similar, and the number of branches and
added fences (using a given heuristic) is the same. Moreover, in the
Chacha20-implementation, the impact of the three fences from the after-branch
heuristic is smaller than the impact of the two fences from the before-memory
heuristic.

In summary, the number of fences does not seem to have a strong correlation
with the performance impact, which seems to depend more on _where_ the fences
are added, and on properties of $P$ that are not reflected in the number of
instructions or branches. For example, a fence that is placed on an error-
handling branch will have much less of an impact on the overall performance
than a fence that is placed on a branch that is regularly used in non-
erroneous executions of the program. Therefore, we think that optimal
placement of fences with respect to their performance impact will be an
important direction of future research.

##  6 Related Work and Conclusions

#### Related Work

Existing formal methods for detecting speculative information leaks usually
require the program to be repaired manually. This includes the approach by
Cauligi et al. [11], which explicitly models the reorder buffer and the
processor pipeline, potentially achieving a higher precision than our over-
approximating approach. Similarly, the technique developed by Cheang et al.
[12] as well as the SPECTECTOR technique [16] are based on extensions of
standard notions like observational determinism to speculative execution
semantics, and check for these precisely. Moreover, Haunted RelSE [14] extends
symbolic execution to reason about standard and speculative executions at the
same time. In [24] speculative execution and attacker capabilities are
axiomatically modeled in the CAT language for weak memory models, allowing for
easy adaption to new Spectre variants. However, it requires to unroll the
program and thus has the drawback of not handling unbounded loops/recursion.

On the other hand, there are approaches that automatically repair a given
program, but cannot give a formal security guarantee. This includes SpecFuzz
[26], which uses fuzzing to detect and repair out-of-bounds array accesses
under speculation, as well as oo7 [28], which detects and repairs Spectre
leaks by static analysis and a taint tracking approach on the binary level.
However, it cannot give a security guarantee since its binary-level analysis
may be incomplete.

Another line of work that resembles our approach is the automatic insertion of
fences in weak memory models [23, 1, 8]. In contrast to these approaches, our
algorithm is tightly coupled with the model checker, and does not use it as a
black-box. CureSpec allows Spacer to maintain most of its state when
discovering a counterexample, and to resume its operation after adding a
fence.

Finally, Blade [27] implements a type-based approach to repair Spectre leaks.
The typing rules construct a dataflow graph between expressions, similar to
taint tracking, and use it to detect possible information leaks. While this
approach supports automatic repair and comes with a formal security guarantee,
it suffers from the usual drawbacks of type-based approaches: the typing rules
assume a fixed threat model, and any change to the type system requires to
manually prove correctness of the resulting type system. In contrast, our
approach is parameterized in the threat model and can easily be combined with
different techniques that detect the set of vulnerable instructions.

#### Conclusions

We present CureSpec, an automatic repair algorithm for information leaks that
are due to speculative execution, parametric w.r.t. the threat model. It is
implemented in the SeaHorn verification framework and can handle C programs.
When CureSpec detects a leak, it repairs it by inserting a fence. This
procedure is executed iteratively until the program is proved secure. To this
end, CureSpec uses the model checking algorithm Pdr incrementally, maintaining
Pdr’s state between different iterations. This allows CureSpec to handle
realistic programs, as shown by the experimental evaluation on various C
functions from OpenSSL and HACL*. CureSpec also returns an inductive invariant
that enables a simple correctness check of the repair in any SMT solver.

## References

  * [1] Abdulla, P.A., Atig, M.F., Chen, Y., Leonardsson, C., Rezine, A.: Counter-example guided fence insertion under TSO. In: Flanagan, C., König, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7214, pp. 204–219. Springer (2012)
  * [2] Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F., Emmi, M.: Verifying constant-time implementations. In: USENIX Security Symposium. pp. 53–70. USENIX Association (2016)
  * [3] Bernstein, D.J.: The poly1305-aes message-authentication code. In: FSE. Lecture Notes in Computer Science, vol. 3557, pp. 32–49. Springer (2005)
  * [4] Bernstein, D.J.: Curve25519: New diffie-hellman speed records. In: Public Key Cryptography. Lecture Notes in Computer Science, vol. 3958, pp. 207–228. Springer (2006)
  * [5] Bhattacharyya, A., Sandulescu, A., Neugschwandtner, M., Sorniotti, A., Falsafi, B., Payer, M., Kurmus, A.: Smotherspectre: Exploiting speculative execution through port contention. In: CCS. pp. 785–800. ACM (2019)
  * [6] Bjørner, N.S., McMillan, K.L., Rybalchenko, A.: On solving universally quantified horn clauses. In: SAS. Lecture Notes in Computer Science, vol. 7935, pp. 105–125. Springer (2013)
  * [7] Bloem, R., Jacobs, S., Vizel, Y.: Efficient information-flow verification under speculative execution. In: Chen, Y., Cheng, C., Esparza, J. (eds.) Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11781, pp. 499–514. Springer (2019). https://doi.org/10.1007/978-3-030-31784-3_29
  * [8] Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7792, pp. 533–553. Springer (2013)
  * [9] Bradley, A.R.: Sat-based model checking without unrolling. In: VMCAI. Lecture Notes in Computer Science, vol. 6538, pp. 70–87. Springer (2011)
  * [10] Canella, C., Bulck, J.V., Schwarz, M., Lipp, M., von Berg, B., Ortner, P., Piessens, F., Evtyushkin, D., Gruss, D.: A systematic evaluation of transient execution attacks and defenses. In: USENIX Security Symposium. pp. 249–266 (2019)
  * [11] Cauligi, S., Disselkoen, C., von Gleissenthall, K., Tullsen, D.M., Stefan, D., Rezk, T., Barthe, G.: Constant-time foundations for the new spectre era. In: PLDI. pp. 913–926. ACM (2020)
  * [12] Cheang, K., Rasmussen, C., Seshia, S.A., Subramanyan, P.: A formal approach to secure speculation. In: CSF. pp. 288–303. IEEE (2019)
  * [13] Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1855, pp. 154–169. Springer (2000). https://doi.org/10.1007/10722167_15
  * [14] Daniel, L., Bardin, S., Rezk, T.: Hunting the haunter - efficient relational symbolic execution for spectre with haunted relse. In: 28th Annual Network and Distributed System Security Symposium, NDSS 2021, virtually, February 21-25, 2021. The Internet Society (2021), https://www.ndss-symposium.org/ndss-paper/hunting-the-haunter-efficient-relational-symbolic-execution-for-spectre-with-haunted-relse/
  * [15] Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977)
  * [16] Guarnieri, M., Köpf, B., Morales, J.F., Reineke, J., Sánchez, A.: Spectector: Principled detection of speculative information flows. In: IEEE Symposium on Security and Privacy. pp. 1–19. IEEE (2020)
  * [17] Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9206, pp. 343–361. Springer (2015). https://doi.org/10.1007/978-3-319-21690-4_20
  * [18] Hoder, K., Bjørner, N.S.: Generalized property directed reachability. In: SAT. Lecture Notes in Computer Science, vol. 7317, pp. 157–171. Springer (2012)
  * [19] Khasawneh, K.N., Koruyeh, E.M., Song, C., Evtyushkin, D., Ponomarev, D., Abu-Ghazaleh, N.B.: Safespec: Banishing the spectre of a meltdown with leakage-free speculation. In: DAC. p. 60. ACM (2019)
  * [20] Kiriansky, V., Lebedev, I.A., Amarasinghe, S.P., Devadas, S., Emer, J.S.: DAWG: A defense against cache timing attacks in speculative execution processors. In: MICRO. pp. 974–987. IEEE Computer Society (2018)
  * [21] Kocher, P., Horn, J., Fogh, A., Genkin, D., Gruss, D., Haas, W., Hamburg, M., Lipp, M., Mangard, S., Prescher, T., Schwarz, M., Yarom, Y.: Spectre attacks: Exploiting speculative execution. In: IEEE Symposium on Security and Privacy. pp. 1–19. IEEE (2019)
  * [22] Komuravelli, A., Gurfinkel, A., Chaki, S.: Smt-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175–205 (2016)
  * [23] Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. In: Bloem, R., Sharygina, N. (eds.) Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23. pp. 111–119. IEEE (2010)
  * [24] de León, H.P., Kinder, J.: Cats vs. spectre: An axiomatic approach to modeling speculative execution attacks. In: 43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022. pp. 235–248. IEEE (2022). https://doi.org/10.1109/SP46214.2022.9833774
  * [25] de Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: TACAS. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008)
  * [26] Oleksenko, O., Trach, B., Silberstein, M., Fetzer, C.: Specfuzz: Bringing spectre-type vulnerabilities to the surface. In: USENIX Security Symposium. pp. 1481–1498. USENIX Association (2020)
  * [27] Vassena, M., Disselkoen, C., von Gleissenthall, K., Cauligi, S., Kici, R.G., Jhala, R., Tullsen, D.M., Stefan, D.: Automatically eliminating speculative leaks from cryptographic code with blade. Proc. ACM Program. Lang. 5(POPL), 1–30 (2021)
  * [28] Wang, G., Chattopadhyay, S., Gotovchits, I., Mitra, T., Roychoudhury, A.: oo7: Low-overhead defense against spectre attacks via program analysis. IEEE Trans. Software Eng. 47(11), 2504–2519 (2021)
  * [29] Yan, M., Choi, J., Skarlatos, D., Morrison, A., Fletcher, C.W., Torrellas, J.: Invisispec: Making speculative execution invisible in the cache hierarchy (corrigendum). In: MICRO. p. 1076. ACM (2019)
  * [30] Zinzindohoué, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: Hacl*: A verified modern cryptographic library. In: Thuraisingham, B., Evans, D., Malkin, T., Xu, D. (eds.) Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017. pp. 1789–1806. ACM (2017). https://doi.org/10.1145/3133956.3134043

##  Appendix 0.A Proofs

See 1

###### Proof

Follows from the proof of Lemma 5.

See 2

###### Proof

From $\sigma_{0}\models\hat{\mathit{Init}}$ follows (i). Since
$\sigma_{k}\models\hat{\mathit{Bad}}$ we have
$\sigma_{k}\models\mathsf{pc}=\bot$. In order for $\mathsf{pc}$ to get $\bot$,
there needs to be a point where $\mathsf{spec}\neq 0$ holds (see
$\hat{\tau}_{a_{i}}$). Since $\mathsf{spec}$ can never decrease starting from
$0$ in $\sigma_{0}$, $\mathsf{spec}>0$ at that point and (iii) follows. (ii)
holds because $\tau_{\bot}$ never changes $\mathsf{spec}$ afterwards.

See 3

###### Proof

We have already argued that, under the assumption that P is constant-time
secure without speculation, violations of constant-time security under
speculation are only possible at instructions in VInst that are reached under
speculation. Since this is exactly the definition of $\hat{\mathit{Bad}}$, the
statement follows immediately.

See 4

###### Proof

Let $i\in\pi^{k}$ and $j$ such that
$(\sigma_{j-1},\sigma_{j}^{\prime})\models\hat{\tau}_{i}$ (see Remark 1).
Assume $\hat{\mathit{Init}}\models\mathsf{fence}_{i}$. Since the values of
fences never change during execution, we have
$\sigma_{j-1}\models\mathsf{fence}_{i}$. Moreover,
$\sigma_{j-1}\models\mathsf{spec}>0$ and thus,
$\sigma_{j-1}=\sigma_{j}=\sigma_{N}$. We have a contradiction because
$\sigma_{j-1}\models\mathsf{pc}=i$. Thus,
$\hat{\mathit{Init}}\models\neg\mathsf{fence}_{i}$ and $\pi^{k}$ is not a path
of $\hat{M}_{i}$. Therefore, no prefix $\hat{\pi}$ exists such that
$\hat{\pi}\pi^{k}$ is an execution of $\hat{M}_{i}$.

See 4.1

###### Proof

The SpecLeak and AddFence rules are applicable at most $|\mathcal{F}|$ times
each (Lemma 4). Thus, termination follows from the termination of Algorithm 1.
After the final application of rule AddFence, CureSpec analyzes $\hat{M}_{s}$
and constructs an inductive invariant $F_{\infty}$ showing that
$\langle\hat{M}_{s},\hat{\mathit{Bad}}\rangle$ is SAFE.

See 5

###### Proof

Let $\pi$ be an execution of $M$. Since it does not involve speculative
execution there exists a corresponding execution in $\hat{M}_{i}$ because
fences only affect speculative executions. This shows
$M\leq_{\text{sim}}\hat{M}_{i}$. Morever, the additional fence in
$\hat{M}_{i}$ only removes valid executions from $\hat{M}$. So,
$\hat{M}_{i}\leq_{\text{sim}}\hat{M}$ holds, too.

##  Appendix 0.B Additional Experimental Results

We give 4 tables that contain experimental results for all our parameter
settings (except for non-incremental without any heuristic, which is the
baseline from Table 1).

Table 3: incremental solving, with fence activation heuristic

Benchmark | every-inst | after-branch | before-memory
---|---|---|---
| $\\#_{f}$ | time | RSS | $\\#_{f}$ | time | RSS | $\\#_{f}$ | time | RSS
aes_encrypt_ct | 3 | 77.7 | 7.05 | 3 | 0.8 | 0.09 | 3 | 1.7 | 0.32
aes_encrypt | 3 | 99.4 | 7.90 | 3 | 0.7 | 0.10 | 3 | 4.7 | 0.98
aes_cbc_encrypt_ct | 10 | 1300.3 | 30.53 | 15 | 100.7 | 0.65 | 10 | 80.6 | 1.41
aes_cbc_encrypt | 10 | 2143.1 | 34.35 | 15 | 774.5 | 1.51 | 10 | 135.1 | 4.34
bn_mul_part | 7 | 6.8 | 0.76 | 13 | 2.6 | 0.18 | 7 | 1.3 | 0.16
bn_sqr_part | 9 | 15.0 | 1.06 | 13 | 3.4 | 0.19 | 9 | 2.5 | 0.22
bn_exp_part | 18 | 205.1 | 5.16 | 29 | 57.4 | 0.82 | 18 | 21.8 | 0.61
Chacha20_encrypt | 2 | 5802.9 | 81.08 | 3 | 8.0 | 0.33 | 2 | 8.4 | 1.90
Poly1305_32_mac | 4 | 53.8 | 4.70 | 4 | 2.2 | 0.12 | 4 | 6.4 | 0.72
Curve25519_64_ecdh | timeout | 3 | 3115.3 | 1.92 | timeout

Table 4: non-incremental solving, with fence activation heuristic

Benchmark | every-inst | after-branch | before-memory
---|---|---|---
| $\\#_{f}$ | time | RSS | $\\#_{f}$ | time | RSS | $\\#_{f}$ | time | RSS
aes_encrypt_ct | 3 | 86.4 | 7.04 | 3 | 0.8 | 0.09 | 3 | 1.9 | 0.32
aes_encrypt | 3 | 103.1 | 7.90 | 3 | 1.3 | 0.11 | 3 | 5.6 | 1.01
aes_cbc_encrypt_ct | 10 | 1819.8 | 31.63 | 15 | 88.5 | 0.75 | 10 | 91.5 | 1.70
aes_cbc_encrypt | 10 | 2302.9 | 42.97 | 15 | 2539.8 | 2.31 | 10 | 129.9 | 5.18
bn_mul_part | 7 | 7.5 | 0.77 | 13 | 2.9 | 0.18 | 7 | 1.4 | 0.16
bn_sqr_part | 9 | 17.6 | 1.15 | 13 | 3.7 | 0.21 | 9 | 2.8 | 0.24
bn_exp_part | 18 | 249.5 | 5.66 | 29 | 69.6 | 1.05 | 18 | 28.1 | 0.65
Chacha20_encrypt | 2 | 5506.3 | 80.46 | 3 | 9.1 | 0.33 | 2 | 11.3 | 1.93
Poly1305_32_mac | 4 | 72.9 | 4.80 | 4 | 2.6 | 0.12 | 4 | 7.4 | 0.73
Curve25519_64_ecdh | timeout | 3 | 2507.9 | 1.79 | timeout

Table 5: incremental solving, with fence activation heuristic, speculation
window of size 20

Benchmark | every-inst | after-branch | before-memory
---|---|---|---
| $\\#_{f}$ | time | RSS | $\\#_{f}$ | time | RSS | $\\#_{f}$ | time | RSS
aes_encrypt_ct | 3 | 245.0 | 8.40 | 3 | 1.8 | 0.10 | 3 | 3.6 | 0.35
aes_encrypt | 3 | 365.4 | 8.28 | 3 | 2.8 | 0.12 | 3 | 15.6 | 1.12
aes_cbc_encrypt_ct | 8 | 6296.9 | 66.89 | 12 | 1384.0 | 5.16 | 9 | 1080.8 | 14.84
aes_cbc_encrypt | timeout | timeout | timeout
bn_mul_part | 7 | 8.2 | 0.82 | 13 | 3.7 | 0.19 | 7 | 1.7 | 0.17
bn_sqr_part | 9 | 18.5 | 1.27 | 13 | 5.0 | 0.21 | 9 | 3.4 | 0.24
bn_exp_part | 18 | 2046.0 | 8.39 | 29 | 1116.0 | 2.05 | 18 | 383.5 | 1.51
Chacha20_encrypt | timeout | 3 | 89.8 | 0.33 | 2 | 60.0 | 2.01
Poly1305_32_mac | 4 | 100.8 | 4.84 | 4 | 5.5 | 0.13 | 4 | 10.2 | 0.78
Curve25519_64_ecdh | timeout | 3 | 3073.0 | 1.91 | timeout

Table 6: non-incremental solving, with fence activation heuristic, speculation
window of size 20

Benchmark | every-inst | after-branch | before-memory
---|---|---|---
| $\\#_{f}$ | time | RSS | $\\#_{f}$ | time | RSS | $\\#_{f}$ | time | RSS
aes_encrypt_ct | 3 | 299.0 | 8.35 | 3 | 2.9 | 0.10 | 3 | 6.7 | 0.36
aes_encrypt | 3 | 426.2 | 8.13 | 3 | 3.9 | 0.12 | 3 | 24.8 | 1.17
aes_cbc_encrypt_ct | timeout | 12 | 998.9 | 4.57 | 9 | 976.8 | 13.39
aes_cbc_encrypt | timeout | timeout | timeout
bn_mul_part | 7 | 10.0 | 0.84 | 13 | 5.0 | 0.19 | 7 | 2.0 | 0.17
bn_sqr_part | 9 | 23.4 | 1.34 | 13 | 5.9 | 0.22 | 9 | 4.0 | 0.26
bn_exp_part | 18 | 1531.5 | 9.99 | 29 | 1103.9 | 2.24 | 18 | 557.4 | 1.86
Chacha20_encrypt | timeout | 3 | 77.1 | 0.33 | 2 | 58.3 | 2.10
Poly1305_32_mac | 4 | 105.6 | 4.83 | 4 | 7.5 | 0.13 | 4 | 9.7 | 0.78


# Reference-based Texture transfer for Single Image Super-resolution of
Magnetic Resonance images

###### Abstract

Magnetic Resonance Imaging (MRI) is a valuable clinical diagnostic modality
for spine pathologies with excellent characterization for infection, tumor,
degenerations, fractures and herniations. However in surgery, image-guided
spinal procedures continue to rely on CT and fluoroscopy, as MRI slice
resolutions are typically insufficient. Building upon state-of-the-art single
image super-resolution, we propose a reference-based, unpaired multi-contrast
texture-transfer strategy for deep learning based in-plane and across-plane
MRI super-resolution. We use the scattering transform to relate the texture
features of image patches to unpaired reference image patches, and
additionally a loss term for multi-contrast texture. We apply our scheme in
different super-resolution architectures, observing improvement in PSNR and
SSIM for 4x super-resolution in most of the cases.

Index Terms—  Super-resolution, MRI, texture, wavelet transform

##  1 Introduction

Magnetic Resonance (MR) Imaging provides high value in spine clinical
diagnosis, with standard classification and grading schemes for spinal
pathologies built on MRI. Some of these rely on subtle findings specific to
MRI such as end-plate abnormalities and high-intensity zones [1]. While spine
MRI is unmatched for diagnosis and post-operative prognosis [2], surgery
guidance is dominated by radiation imaging: CT and fluoroscopy. A primary
requirement for intra-operative use is geometric accuracy, which is typically
lower in MRI due to acquisition of thicker slices. Super-resolution (SR) could
be an enabler for use of MRI intra-operatively in spine procedures. We take up
deep learning super-resolution as a direct means of improving spine MRI
resolution, leveraging the unique possibility in MRI of acquiring multiple
contrast images and with different slicing direction.

Related work: Some state-of-the-art single image super-resolution (SISR)
techniques for natural images include Residual Channel Attention network
(RCAN) [3] and Residual Feature Distillation Network (RFDN) [4]. Recent work
in MRI super-resolution include [5], which evaluated SSIM improvement in SRCNN
for brain MRI, and showed superior reconstruction compared to fusion of thick
slices of different anatomical orientation. Multi-contrast super-resolution
has been explored in [6] where synergizing multiple contrasts was shown to
achieve better super-resolution results, using a composition of loss terms
including MSE, adversarial, perceptual and textural loss. Other approaches in
literature include residual deep learning [7] and use of cross-plane self-
similarity in MRI [8].

Peculiar to MRI, the different MRI contrast images have similar texture
patterns. State-of-art SISR networks like RCAN, RFDN, can be augmented to
utilize this. Reference based SISR methods have been effective in leveraging
texture details from reference images to assist resolution enhancement [9].
But VGG [10] type feature-maps which are used in natural image SR would not be
suited, as they are known to be sensitive to lower order image
characteristics, capturing structure more than texture. The learnt filters are
also not guaranteed to be orthogonal, making comparison and matching using
simplistic distance metrics questionable.

Fig. 1: Proposed SISR with texture transfer

In our work we emphasize on using textures of multi-contrast MRI images as
reference for super-resolution. Texture transfer (TT) attempts to replace the
texture features of Low Resolution (LR) MRI input with matched textures of the
High Resolution (HR) reference. Before comparing the LR textures with the
reference textures, the reference images are degraded by blurring so that
matching operates in similar sampling frequency.

In place of VGG feature maps like in prior works, we use wavelet scattering to
extract multiscale texture features and use a texture-based loss function for
texture transfer. Our approach achieves texture transfer by extracting wavelet
scattering features, compared using dense matching to an unpaired HR
reference, and combining texture information from the matched reference. Fig.
1 shows a quick overview of the proposed reference-based texture transfer
approach.

We summarize our contributions as follows:

  1. 1.

A module applicable onto baseline architectures like SRCNN [11], RCAN, RFDN,
providing a reference-based, unpaired, texture transfer strategy using wavelet
scattering and texture loss, utilizing multi-contrast MRI.

  2. 2.

We explore the effect of using different kinds of reference images in
improving the resolution quality; for instance, use of axial reference images
to train model for sagittal LR-HR.

  3. 3.

We compare 3 existing SISR architectures: SRCNN, RCAN, RFDN on sagittal and
axial MRI input LR images with different types of MRI reference images.
Results show improvement for most cases across models improving the in-plane
and through-plane resolution (4x) both quantitatively and qualitatively.

(i) (a) SRCNN, (b) RCAN and (c) RFDN with reference-based texture transfer

(ii) Feature swapper

Fig. 2: SISR Architectures of with reference-based texture transfer

##  2 SUPER RESOLUTION THROUGH TEXTURE TRANSFER

###  2.1 Background study for texture transfer

The concept of reference-based texture transfer has been inspired from the
idea of neural style transfer using VGG features [9] in SISR. For MR images,
texture details can be retrieved from the images acquired across multiple
protocols and hence can be used for texture transfer. Wavelet is one of the
best ways to decompose the image into various frequency bands [12], which can
be effectively used in texture extraction. Hence, in our approach of
reference-based texture transfer, we compute the wavelet transform of the LR
image to be super resolved and the high resolution reference to extract
texture features. In the transformed domain, feature swapping is performed
wherein the texture features of LR is replaced with the best matched texture
features of the reference by dense comparison. To minimize the difference
between the swapped texture features and the texture features of super
resolved output, we include a texture loss term in the loss function.

In the proposed method, Morlet wavelet transform [13] is used for computing
the texture features of the image. Morlet wavelet filters are very similar to
Gabor filters [12], which have been widely used in texture extraction. Wavelet
coefficients are computed at different scales, where scale denotes the level
of decomposition of the image.

Additionally, in the proposed approach based on wavelet transform, wavelet
filters at different rotation angles are considered to ensure rotation
invariance in the computed features.

###  2.2 Feature Swapping

There are two main steps in feature swapping - Dense matching and texture
transfer. The LR image ($I_{LR}$) is first upsampled to the actual size using
bicubic interpolation. The HR reference images are down-sampled and up-sampled
using bicubic interpolation to obtain blurred reference images so as to bring
them to the same frequency bandwidth as the LR input. The process of feature
swapping is illustrated in Fig. 2. The wavelet scattering coefficients are
obtained for upsampled LR input ($I_{LR}\uparrow$), HR reference ($I_{Ref}$)
and blurred HR reference ($I_{Ref}\downarrow\uparrow$). The features of LR
input and that of blurred reference are sampled into small dense patches of
size 3x3 with a stride of 1. Each texture patch of $I_{LR}\uparrow$ is
compared with every other texture patches of $I_{Ref}\downarrow\uparrow$, to
get the corresponding reference texture patch index that gives the highest
correlation. To represent this mathematically, let the sampling function be
given as $P$ and the similarity map between the $i^{th}$ input texture patch
and the $j^{th}$ reference texture patch can be given as $s(i,j)$. The
similarity between two patches is calculated as a dot product.

$s(i,j)=\langle\,P_{i}(\phi_{J,L}(I_{LR}\uparrow))\,,\,P_{j}(\phi_{J,L}(I_{Ref}\downarrow\uparrow))\,\rangle$
(1)

Here $\phi_{J,L}$ denotes the texture feature extractor with scale $J$ and
number of rotation angles $L$. The index of the reference texture patch that
gives the maximum similarity is chosen as the texture for that particular LR
image texture patch.

$S(i)=\operatorname*{argmax}_{j}\,s(i,j)$ (2)

$S(i)$ is the index of reference texture patch of maximum correlation. This
operation (called as dense matching operation) is repeated for every LR input
patch to obtain the best matching correspondences in texture and can be
formulated as,

$M(J,L)=D(\phi_{J,L}(I_{LR}\uparrow),\phi_{J,L}(I_{Ref}\downarrow\uparrow)$
(3)

Here, $D$ denotes the dense matching operation and $M(J,L)$ is the matching
correspondences between the features of LR input and that of blurred
reference.

Based on the correspondences, the patches of texture features of HR reference
are placed at the appropriate positions. We call this operation of transfer of
texture information from the HR reference to the LR input as texture transfer.

$F=H(\phi_{J,L}(I_{Ref}),M(J,L))$ (4)

where, $H$ denotes the texture transfer operation and $F$ denotes the
transferred features that can be concatenated to the SISR model during
training at a specified layer (typically at one of the initial layers) of the
model based on its architecture.

###  2.3 Loss functions

We used three loss functions in the proposed approach namely the
reconstruction loss in the image domain, perceptual loss and texture loss in
the feature domain. The reconstruction loss $L_{rec}$ is given as,

$L_{rec}=\|I_{SR}-I_{HR}\|_{1}$ (5)

where $I_{SR}$ is the super resolved (or predicted) image and the $I_{HR}$ is
the HR ground-truth image. The perceptual loss component is applied [14] to
improve the visual quality of the image by enforcing similarity with respect
to the ground truth in the feature space. Typically, we adopt the ReLU5-1
layer of VGG19 [15]. It can be given by,

$L_{p}=\frac{1}{S}\sum_{i=1}^{N}\|\theta_{i}(I_{SR})-\theta_{i}(I_{HR})\|_{F}$
(6)

where $S$ is the features size (width * height * number of channels), $N$ is
the number of channels and $\theta_{i}$ denotes the $i^{th}$ channel of VGG19.
The third loss function enforces texture similarity between the swapped
features of LR (from reference images) and the super resolved image. The
texture loss is computed by taking Frobenius norm of Gram matrix of the
extracted texture features.

$L_{t}=\frac{1}{W}\|Gr(\phi_{J,L}(I_{SR}))-Gr(F)\|_{F}$ (7)

Here, $F$ and $\phi_{J,L}$ are defined in Section 2.2, $W$ is the feature size
and $Gr(.)$ calculates the Gram matrix, which helps in computing the texture
information [16].

##  3 EXPERIMENTS

###  3.1 Data preparation

We have used two publicly available datasets for training and validation -
Zenodo[17] and Dataset1 from SpineWeb [18]. We have chosen 23 volumes of
T2-weighted turbo spin echo 3D MR of Zenodo and 8 MRI T1-weighted volumes of
SpineWeb Dataset1 for training. The HR patches are created by randomly
cropping twenty 64 x 64 patches from each MRI 2D slice making a total of 14000
patches (10920 sagital view patches from Zenodo and 3080 sagittal SpineWeb
patches together) for training. For testing, 312 sagittal view images of
Zenodo and 316 axial view images of SpineWeb are used. Wilcoxon signed-rank
test with an alpha of 0.05 is used to assess statistical significance.

Model name | Sagittal view data | Axial view data
---|---|---
PSNR (dB) | SSIM | PSNR (dB) | SSIM
Bicubic | 35.1682 | 0.9221 | 28.9117 | 0.8827
SRCNN ($L_{1}+L_{p}$) | 37.4923 | 0.9483 | 29.7490 | 0.8985
SRCNN ($L_{1}+L_{p}+L_{t}$)-Sag | 38.0789 | 0.9550 | 30.0975 | 0.9041
SRCNN($L_{1}+L_{p}+L_{t}$)-Ax | 38.1703 | 0.9557 | 30.1647 | 0.9050
RCAN ($L_{1}+L_{p}$) | 38.4679 | 0.9596 | 30.3360 | 0.9066
RCAN ($L_{1}+L_{p}+L_{t}$)-Sag | 38.5239 | 0.9601 | 30.3383 | 0.9072
RCAN ($L_{1}+L_{p}+L_{t}$)-Ax | 38.5320 | 0.9603 | 30.3883 | 0.9078
RFDN ($L_{1}+L_{p}$) | 38.4368 | 0.9586 | 30.3409 | 0.9073
RFDN ($L_{1}+L_{p}+L_{t}$)-Sag | 38.5021 | 0.9587 | 30.1427 | 0.9055
RFDN ($L_{1}+L_{p}+L_{t}$)-Ax | 38.5497 | 0.9594 | 30.2344 | 0.9066
Table 1: Quantitative comparison of SRCNN, RCAN and RFDN without and with
texture transfer (metrics improvements shown in bold). Sagittal view data -
Zenodo images, Axial view data - SpineWeb images. Sagittal and axial texture
transfer models end with ’-Sag’ and ’-Ax’

Fig. 3: Visual comparison of methods SRCNN, RCAN and RFDN with and without
texture transfer

###  3.2 Training details with and without texture transfer

The models chosen for training are the pre-existing SISR models - SRCNN, RCAN
and RFDN with and without texture transfer. For each model we conduct three
trainings - one without TT with only $L_{1}$ and $L_{p}$ loss components.
(denoted by model name followed by ($L_{1}+L_{p}$)) and the other two with TT
based on two different sets of reference images (sagital and axial reference,
denoted by model name followed by ($L_{1}+L_{p}+L_{t}$) with suffix ’-Sag’ or
’-Ax’ respectively ). Before training the baseline models with TT, feature
swapping followed by concatenation of swapped features to one of the initial
layers of the model is performed. The two types of reference images used in
our study are - 1. Sagital TT: Four sagittal reference images from Zenodo for
sagittal reference based training 2. Axial TT: Five Axial reference images for
axial reference based training. For texture extraction we use the Morlet
wavelet transform with J = 2 and L = 8. We have used Adam optimizer with
learning rate 1e-4 for all the models. The batch size is chosen to be 9 for
SRCNN and RFDN, and 16 for RCAN. All the implementations are carried out using
Pytorch.

##  4 RESULTS

The three convolutional neural network (CNN) models (SRCNN, RCAN and RFDN) are
chosen based on the complexity of the architectures. The SRCNN is the simplest
of the three models. RCAN is one of the state-of-the-art deep models with
residual blocks and channel attention layers. RFDN is one of the recent models
having multiple residual feature distillation blocks. Table 1 shows the
quantitative comparison of the proposed approach. From the table, the
following observations are noted. 1) The performance improvement of the
proposed texture transfer has been consistent across the SISR baseline CNN
models in most of the cases under study (highlighted in bold). 2) The axial
texture transfer results are better than sagittal texture transfer. This is an
important observation which emphasizes the purpose of reference based texture
transfer. The reason could be that the texture features taken from high
resolution reference image (in this case axial reference images which are
T1-weighted images of voxel size 0.3 mm x 0.3 mm) are richer as compared to
those with lower resolution. 3) The performance improvements are consistent
across models for sagittal texture transfer. The resulting metrics are found
to be statistically significant (pvalue $<$ 0.05). For axial texture transfer,
the SRCNN and RCAN show improvements while RFDN has shown equivalent
performance in SSIM and a reduction in performance in PSNR. Since RFDN has
multiple dense connections with multi-distillation blocks, we believe that the
layer through which TT is done could be a reason in influencing the overall
performance. As a future work, we are studying more CNN-based SISR models to
understand the consistency of different texture transfer strategies across
layers of the models. Fig. 3 shows the inter-vertebral sections of the lumbar
spine anatomy. The qualitative comparison of bicubic interpolation method and
models with and without TT is shown. From figure it is clear that the linear
structures (highlighted with a box) in the discs are reconstructed with better
agreement to the groundtruth as compared with the baseline CNN models.

##  5 CONCLUSION

Towards enabling the use of MRI in spine surgery intra-operative guidance, we
take up single image super-resolution from clinical MRI, and demonstrated our
novel method of reference-based texture transfer, implemented in 3 baseline
architectures, and evaluated on two public datasets for multi-contrast SR in
different slicing directions. Comparing with the baseline, the proposed
texture transfer with texture loss exhibits good improvements in the
performance evaluation metrics together with visual quality improvement. The
observations show that the proposed neural texture transfer can be a potential
source of improving the resolution of MRI images.

##  6 Compliance with Ethical Standards

This research study was conducted retrospectively using human subject data
made available in open access by Zenodo [17] and SpineWeb - Dataset1 [18].
Ethical approval was not required as confirmed by the license attached with
the open access data.

##  7 Acknowledgements

No funding was received for conducting this study. The authors have no
relevant financial or non-financial interests to disclose.

## References

  * [1] Garrett K Harada, Zakariah K Siyaji, Sadaf Younis, Philip K Louie, Dino Samartzis, and Howard S An,  “Imaging in Spine Surgery: Current Concepts and Future Directions,”  Spine Surgery and Related Research, vol. 4, no. 2, pp. 99–110, Nov. 2019.
  * [2] Seon Jeong Kim, Sang Hoon Lee, and et al. Chung,  “Magnetic resonance imaging patterns of post-operative spinal infection: Relationship between the clinical onset of infection and the infection site,”  Journal of Korean Neurosurgical Society, vol. 60, no. 4, pp. 448–455, 2017.
  * [3] Yulun Zhang, Kunpeng Li, Kai Li, Lichen Wang, Bineng Zhong, and Yun Fu,  “Image super-resolution using very deep residual channel attention networks,”  in Proc. IEEE ECCV. 2018.
  * [4] Jie Liu, Jie Tang, and Gangshan Wu,  “Residual feature distillation network for lightweight image super-resolution,”  arXiv:2009.11551 [cs, eess], 2020.
  * [5] Jakub Jurek, Marek KociÅ„ski, Andrzej Materka, Marcin Elgalal, and Agata Majos,  “CNN-based superresolution reconstruction of 3D MR images using thick-slice scans,”  Biocybernetics and Biomedical Engineering, vol. 40, no. 1, pp. 111–125, Jan. 2020.
  * [6] Q. Lyu, H. Shan, C. Steber, C. Helis, C. Whitlow, M. Chan, and G. Wang,  “Multi-Contrast Super-Resolution MRI Through a Progressive Network,”  IEEE Transactions on Medical Imaging, vol. 39, no. 9, pp. 2738–2749, Sept. 2020.
  * [7] Xiuxiu He, Yang Lei, Yabo Fu, Hui Mao, Walter J. Curran, Tian Liu, and Xiaofeng Yang,  “Super-resolution magnetic resonance imaging reconstruction using deep attention networks,”  in SPIE Medical Imaging 2020: Image Processing. Mar. 2020, SPIE.
  * [8] Jinglong Du, Zhongshi He, Lulu Wang, Ali Gholipour, Zexun Zhou, Dingding Chen, and Yuanyuan Jia,  “Super-resolution reconstruction of single anisotropic 3d MR images using residual convolutional neural network,”  Neurocomputing, vol. 392, pp. 209–220, June 2020.
  * [9] Zhifei Zhang, Zhaowen Wang, Zhe Lin, and Hairong Qi,  “Image super-resolution by neural texture transfer,”  Proc. IEEE CVPR, 2019.
  * [10] Karen Simonyan and Andrew Zisserman,  “Very deep convolutional networks for large-scale image recognition,”  arXiv 1409.1556, 09 2014.
  * [11] Chao Dong, Chen Change Loy, Kaiming He, and Xiaoou Tang,  “Image super-resolution using deep convolutional networks,”  IEEE Transactions on Pattern Analysis and Machine Intelligence, vol. 38, no. 2, pp. 295–307, Feb. 2016.
  * [12] S. Livens, P. Scheunders, G. Van de Wouwer, and D. Van Dyck,  “Wavelets for texture analysis, an overview,”  IEE Conference Publication, , no. 443 pt 2, pp. 581–585, 1997.
  * [13] Mathieu Andreux, Tomás Angles, Georgios Exarchakis, and et al. Leonarduzzi,  “Kymatio: Scattering transforms in python,”  Journal of Machine Learning Research, vol. 21, no. 2012, pp. 2012–2017, 2020.
  * [14] Justin Johnson, Alexandre Alahi, and Li Fei-Fei,  “Perceptual losses for real-time style transfer and super-resolution,”  in Proc. IEEE ECCV. 2016.
  * [15] Shuying Liu and Weihong Deng,  “Very deep convolutional neural network based image classification using small training sample size,”  in 2015 3rd IAPR Asian Conference on Pattern Recognition (ACPR). Nov. 2015, IEEE.
  * [16] Leon A. Gatys, Alexander S. Ecker, and Matthias Bethge,  “Image Style Transfer Using Convolutional Neural Networks,”  in Proc. IEEE CVPR, 2016.
  * [17] “Zenodo: [http://dx.doi.org/10.5281/zenodo.22304],” .
  * [18] “SpineWeb : Main / Datasets : [http://spineweb.digitalimaginggroup.ca/ index.php ?n=main.datasets],” .