# SemPat: Using Hyperproperty-based Semantic Analysis to Generate
Microarchitectural Attack Patterns

Adwait Godbole ${}^{\text{(\Letter)}}$ 0000-0001-7704-304X<EMAIL_ADDRESS>University of California, BerkeleyBerkeleyCAUSA ,  Yatin A. Manerkar
0000-0002-6954-2292<EMAIL_ADDRESS>University of MichiganAnn ArborMIUSA
and  Sanjit A. Seshia  0000-0001-6190-8707<EMAIL_ADDRESS>University of
California, BerkeleyBerkeleyCAUSA

###### Abstract.

Microarchitectural security verification of software has seen the emergence of
two broad classes of approaches. The first is based on semantic security
properties (e.g., non-interference) which are verified for a given program and
a specified abstract model of the hardware microarchitecture. The second is
based on attack patterns, which, if found in a program execution, indicates
the presence of an exploit. While the former uses a formal specification that
can capture several gadget variants targeting the same vulnerability, it is
limited by the scalability of verification. Patterns, while more scalable,
must be currently constructed manually, as they are narrower in scope and
sensitive to gadget-specific structure.

This work develops a technique that, given a non-interference-based semantic
security hyperproperty, automatically generates attack patterns up to a
certain complexity parameter (called the skeleton size). Thus, we combine the
advantages of both approaches: security can be specified by a hyperproperty
that uniformly captures several gadget variants, while automatically generated
patterns can be used for scalable verification. We implement our approach in a
tool and demonstrate the ability to generate new patterns, (e.g., for
SpectreV1, SpectreV4) and improved scalability using the generated patterns
over hyperproperty-based verification.

††conference: ArXiv; May 2024; N.A.††copyright: none††ccs: Security and
privacy Formal security models††ccs: Security and privacy Logic and
verification††ccs: Security and privacy Side-channel analysis and
countermeasures††ccs: Theory of computation Verification by model
checking††ccs: Theory of computation Logic and verification††ccs: General and
reference Verification

##  1\. Introduction

Modern processors are packed with performance-improving microarchitectural
mechanisms such as caches, speculation, prefetching. These lead to subtle
microarchitectural-level interactions that can be exploited by hardware
execution attacks to leak sensitive data from a victim (e.g., (Kocher, 2018;
Kocher et al., 2019; Lipp et al., 2018; Canella et al., 2019b; Schwarz et al.,
2019a)). Recently, several techniques have been proposed to detect the
presence of such vulnerabilities in software and/or verify their absence (e.g.
(Cheang et al., 2019; Guarnieri et al., 2020; Guanciale et al., 2020; Mosier
et al., 2022; Ponce-de Leon and Kinder, 2022; Daniel et al., 2023, 2021)).
While sharing the goal of security verification, these approaches adopt
different (hardware) platform models, security specifications, and have
different strengths.

We observe the emergence of two broad classes of approaches based on the
security specification they adopt: semantic hyperproperty ($\mathrm{SH}$)
based approaches (e.g., (Cheang et al., 2019; Guarnieri et al., 2020;
Guanciale et al., 2020; Guarnieri et al., 2021; Fabian et al., 2022)) perform
verification with respect to a hyperproperty-based (Clarkson and Schneider,
2008) security specification, while attack pattern ($\mathrm{AP}$) based
approaches (e.g., (Mosier et al., 2022; Ponce-de Leon and Kinder, 2022;
Trippel et al., 2019)) perform verification using patterns that indicate the
existence of an exploit. $\mathrm{SH}$ approaches provide advantages of
uniform specification and formal guarantees, while $\mathrm{AP}$ approaches
have better scalability. In this work, we enable automated generation of
attack patterns given a hyperproperty-based specification, thereby combining
their strengths.

$\mathrm{SH}$ approaches (e.g., (Cheang et al., 2019; Guarnieri et al., 2020;
Guanciale et al., 2020; Guarnieri et al., 2021; Fabian et al., 2022)) identify
a transition system-based platform model and define program security
semantically as a hyperproperty (e.g., non-interference (NI) (Goguen and
Meseguer, 1984; Clarkson and Schneider, 2008)) over executions of this
transition system. This hyperproperty is verified using approaches such as
model checking (Clarke et al., 1994) or symbolic execution (King, 1976). By
semantically characterizing vulnerabilities, hyperproperties allow uniform
specification: i.e., specification that captures several exploit gadgets that
target the same vulnerability, while differing in syntactic structure. This
results in strong, high-coverage security guarantees. However, these
approaches are often limited by scalability owing to microarchitectural
platform model complexity.

$\mathrm{AP}$ approaches (e.g. (Mosier et al., 2022; Ponce-de Leon and Kinder,
2022; Trippel et al., 2019)) use attack patterns to detect vulnerabilities.
Patterns identify execution fragments that are indicative of an exploit;
program executions embedding these patterns are flagged as vulnerable.
Patterns can be defined (and checked) over a platform model that is more
abstract than the microarchitectural models used by $\mathrm{SH}$ approaches.
This abstraction leads to simpler verification queries which scale better with
program size. However, each pattern captures specific execution scenarios and
is sensitive to structural variability in exploit gadgets, even when the
gadgets target the same microarchitectural feature. Covering the attack vector
requires an enumeration of all possible patterns that it encompasses. This can
be tedious to perform manually, leading to incomplete coverage.

SemPat. The above discussion motivates the question: Can we combine the
scalability of $\mathrm{AP}$ approaches with the uniform specification and
guarantees of $\mathrm{SH}$ approaches? This work aims to resolve this
question in the context of microarchitectural vulnerabilities by developing
algorithms to generate attack patterns given a platform model and a non-
interference-based hyperproperty. Our key insight is to use the hyperproperty
as the specification against which to check whether a candidate pattern
represents an exploit. Our technique (§5) ensures that the generated patterns
capture all executions in which there is a dependency-closed sub-execution of
size $k$ that violates the hyperproperty. This property, termed as
$k$-completeness (Eq. 1), enables combining formal specification via
hyperproperties with scalable verification via patterns.

Our pattern generation is guided by a grammar (§5.3) that identifies the space
of constraints that patterns are defined over. The choice of grammar captures
the tradeoff between generality and the precision (false positives) of the
generated patterns. Specialized grammars result in patterns which have fewer
false positives but are microarchitectural-implementation dependent. Our
approach traverses the grammar-induced search space, checking candidates
against the hyperproperty, a la grammar-based synthesis ((Alur et al., 2013;
Jha and Seshia, 2015)).

Contributions. Our contributions are as follows:

  1. (1)

Formally relating semantic hyperproperty and attack pattern based approaches:
We compare and formally relate $\mathrm{SH}$ and $\mathrm{AP}$ approaches to
exploit detection. Based on the insight that hyperproperties can serve as a
specification for patterns, we propose the problem of generating the latter
given the former.

  2. (2)

$k$-complete automatic pattern generation: We develop a grammar-based search
algorithm for automatic pattern generation that ensures that the generated
patterns capture all non-interference violations up to a certain complexity
parameter $k$ (termed skeleton size).

  3. (3)

Implementation and Evaluation - new patterns and improved verification
performance: We develop a prototype tool implementing our pattern generation
technique and for verifying software binaries using the generated patterns. We
evaluate our approach by generating attack patterns and using them to analyze
variants of Spectre-style exploits. We demonstrate: (a) the ability to
generate previously unknown patterns for existing (e.g., Spectre-BCB, Spectre-
STL) attacks as well as variants targetting alternative (e.g. computation-
unit-based) side-channels, and (b) upto 2 orders-of-magnitude performance
improvement on litmus tests with better scaling using the generated patterns
compared to hyperproperty-based analysis.

Outline. In §2 we provide background on $\mathrm{SH}$ and $\mathrm{AP}$ and
motivate our contribution. We provide our programming model in §3, followed by
the problem formulation in §4. In §5 we describe SemPat, our approach to
generate attack patterns based on a semantic platform model and security
hyperproperty. We describe the evaluation methodology in §6 and present
experimental results in §7. We discuss our approach, and its limitations in
§8, related work in §9, and §10 concludes. We provide proofs/algorithm
pseudocode in the supplementary material appendix.

##  2\. Background and Motivation

###  2.1. Microarchitectural Execution Attacks

We provide background on microarchitectural execution attacks using the
Spectre Bounds Check Bypass (BCB) vulnerability. We refer the reader to
literature (e.g., (Kocher et al., 2019; Ge et al., 2018; Canella et al.,
2019b)) for extensive surveys.

####  2.1.1. Spectre-BCB

The victimA function in Fig. 1 shows the Spectre-BCB (also known as SpectreV1)
vulnerability gadget. In Spectre-BCB, an attacker induces an invocation of the
victimA function with an argument i which is out-of-bounds of array arr1.
While architecturally this is an illegal access, branch mis-speculation can
allow arr1[i], followed by arr2[arr1[i] << CL_INDEX] to be accessed
speculatively. In particular, the second load leaves a residue in the cache
which is a function of the accessed address (i.e., arr2+arr1[i] << CL_INDEX).
This residue is preserved even after speculative rollback, and can be observed
by the attacker (e.g., using a Prime+Probe primitive (Liu et al., 2015)). Thus
the attacker can observe the value of arr1[i] for an out-of-bounds index i,
leading to a security vulnerability. The key aspect of this vulnerability is
that it leverages microarchitectural features \- branch (mis)-speculation and
cache side-channels - to leak information.

####  2.1.2. Variant Vulnerabilities

Over the years several variants of microarchitectural hardware execution
attacks have been demonstrated. These vary both at the software level (e.g.,
the structure of the vulnerability gadget occurring in the program
library/executable) as well as at the microarchitectural level (e.g., the
underlying speculative mechanism/side-channel that is exploited).

The function victimC in Fig. 1 shows a variant of victimA, that replaces a
cache-based side channel with a computation unit-based side channel. Like
victimA, victimC also exploits branch speculation to perform an out-of-bounds
load of arr1fp[i] (a floating-point array). The loaded value is used in a
floating-point multiply operation. If the microarchitectural implementation of
this operation has data-operand dependent timing (e.g., (Sanchez Vicarte et
al., 2021; Ge et al., 2018)) then an execution time measurement leaks the
value of arr1fp[i]. Computation units have been targeted in this manner by
previously demonstrated exploits (e.g., NetSpectre (Schwarz et al., 2019b)
uses AVX-based timing side channels) as well as conjectured vulnerabilities
(e.g., (Sanchez Vicarte et al., 2021)).

Figure 1. Left: Variants of speculative exploits targeting branch
(mis)-speculation with cache-based (victimA, victimB) and computation unit-
based (victimC, victimD) side channels. Centre: While attack patterns that can
detect these exploits, variants of the same (Spectre-BCB) vulnerability -
victimA and victimB \- require different patterns, as do victimC and victimD.
In (A, C), the load arr1[i] is performed within the speculative window (after
the branch), while in (B, D) it is before the branch. Right: Unlike attack
patterns, a semantic hyperproperty uniformly characterizes several exploits
aimed a particular microarchitectural vulnerability. The Speculative Non-
Interference (Guarnieri et al., 2020) (SNI) Hyperproperty
$\text{H}_{\text{AB}}$ can identify both victimA and victimB (as well as
others) as exploits, while the SNI Hyperproperty $\text{H}_{\text{CD}}$
identifies both victimC and victimD. While the hyperproperty changes with the
platform’s microarchitectural features (e.g., speculation and side-channels),
it is robust to variances in the exploit (program) structure itself.

###  2.2. Analyzing Software for Vulnerabilities

Analyzing programs for the existence of microarchitectural vulnerabilities is
an important yet challenging problem.

####  2.2.1. $\mathrm{AP}$: Attack Pattern-based Analysis

One family of approaches, which we call $\mathrm{AP}$ approaches, detect
vulnerabilities using attack patterns. An attack pattern is a small execution
fragment which, if embedded in some (larger) program execution, indicates the
presence of a vulnerability. Pattern A (Fig. 1) illustrates one such pattern
from existing work (Mosier et al., 2022). Pattern A matches executions where a
load (A2) is speculatively executed following a branch (A1), and where the
address of a subsequent load (A3) depends on the value loaded by A2. Fig. 2
(Match A) shows the compiled victimA, and depicts how the instruction nodes
A1, A2, A3 in pattern A match instructions in the binary execution.

$\mathrm{AP}$-approach | Execution model | Attack pattern variant
---|---|---
CheckMate (Trippel et al., 2019) |  $\mu$hb graphs (Lustig et al., 2016) | Bad execution patterns
Cats vs. Spectre (Ponce-de Leon and Kinder, 2022) |  cat (Alglave et al., 2014) based event structures |  $\mathsf{sec}\rightarrow^{*}\textit{{Obs}}$ paths
Axiomatic HW/SW Contracts (Mosier et al., 2022) |  Leakage containment models (LCMs) | Transmitters

Table 1. Examples of execution modelling choices and pattern variants used in
some $\mathrm{AP}$-approaches.

####  $\mathrm{AP}$ approach variants

Existing $\mathrm{AP}$-based detection approaches identify a set of such
patterns, and then analyze programs for the existence of pattern embeddings.
These approaches model executions and define patterns either at the
architectural (Mosier et al., 2022; Ponce-de Leon and Kinder, 2022) or the
microarchitectural (Trippel et al., 2019) level. Architecture-level approaches
are augmented with sufficient microarchitectural detail to capture the
vulnerability-specific features (e.g. xstate from Mosier et. al. (Mosier et
al., 2022)). Table 1 provides a summary of these differences.

Patterns defined at the architectural level abstract away complex
microarchitectural details of the platform. This results in simpler
verification queries, allowing analysis to scale to larger programs (e.g., see
(Mosier et al., 2022; Ponce-de Leon and Kinder, 2022)).

Figure 2. Patterns A, B, C, D matched against executions of programs
victimA,victimB,victimC,victimD respectively.

#### Patterns are tied to gadget-specific structure 111Which is why we call
these attack patterns, since they only capture specific attack executions, and
not the common underlying vulnerability.

While attack pattern-based analysis has the benefit of greater scalability,
patterns do not generalize well to other gadget variants that exploit the same
underlying microarchitectural features. To illustrate this, function victimB
in Fig. 1 is a modified version of victimA, where the load arr1[i] is
performed non-speculatively, i.e. before the branch. Due to this load$-$branch
inversion, pattern A does not match the execution of victimB, even though both
victimA and victimB exploit the same (Spectre-BCB) mechanism. In Fig. 1 we
provide pattern B that reorders the branch with the first load, and thus can
capture victimB (depicted in Fig. 2 Match B). This highlights the fact that
attack patterns are tied to gadget-specific structure.

$\mathrm{SH}$-approach | Non-interference (NI) variant
---|---
A Formal Approach to to Secure Speculation (Cheang et al., 2019) |  Trace-property dependent observational-determinism
Spectector (Guarnieri et al., 2020) | Speculative non-interference
InSpectre (Guanciale et al., 2020) | Conditional non-interference
Hardware-software contracts (Guarnieri et al., 2021) | Contract conditioned NI
Automated detection of speculative attack combinations (Fabian et al., 2022) | Speculative NI

Table 2. Summary of non-interference variants used in some $\mathrm{SH}$
approaches.

####  2.2.2. $\mathrm{SH}$: Semantic Hyperproperty-based Analysis

Non-interference-based hyperproperties (Clarkson and Schneider, 2008) allow
security specifications such as confidentiality (“secret variables should not
affect public outputs”) and integrity (“public inputs should not affect
protected variables”). $\mathrm{SH}$-approaches, e.g., (Cheang et al., 2019;
Guarnieri et al., 2020; Guanciale et al., 2020), formulate security
semantically using hyperproperties and verify them against a platform model.

#### Hyperproperties allow uniform security specification

The hyperproperty $\text{H}_{\text{AB}}$ (Fig. 1 (right)) specifies the memory
outside (public) arrays arr1, arr2 as being secret, and the cache tags as
being public output. This captures a cache-based side channel where the tags
are attacker-observable (e.g., using Prime+Probe (Liu et al., 2015)). victimA
violates $\text{H}_{\text{AB}}$, since the cache state is tainted with the
(speculatively loaded) address of the second load which is a value outside
arr1, arr2. Although it has a different structure than victimA, victimB also
violates $\text{H}_{\text{AB}}$ as it too leaves a cache residue. Thus, unlike
attack patterns, hyperproperties such as $\text{H}_{\text{AB}}$ are agnostic
to gadget-specific structure. By uniformly capturing several exploit-variants
targetting a particular microarchitectural vulnerability,
$\mathrm{SH}$-approaches provide wide-scoped, strong guarantees.

#### Hyperproperty verification

$\mathrm{SH}$-approaches base their analysis on variants of non-interference,
which we summarize in Tab. 2, and discuss in more detail in §4.1. They verify
this hyperproperty against a semantic platform model, which identifies (a)
system state (variables in the system), and (b) execution semantics of
operations. Fig. 3 illustrates a platform fragment with register file, memory
and cache state, and load and alu operations. Non-interference-based
hyperproperties can be converted into a single trace property by performing
self-composition, i.e., composing together copies of the platform ((Clarkson
and Schneider, 2008; Terauchi and Aiken, 2005)). This single trace property
can be checked by invoking a model checking or software verification
procedure.

Self-composition-based verification against a semantic model has two
drawbacks. Firstly, microarchitectural detail in the platform model results in
large verification queries. (e.g., a query for $\text{H}_{\text{AB}}$ over the
platform from Fig. 3 would have to encode the cache state). In comparison,
architectural level pattern-based queries (e.g., with pattern A) are smaller,
enabling faster verification. Secondly, self-composition results in a further
increase in the state-space (and query) and consequentially adversely affects
performance.

⬇

1// System state

2var regs : [regindex_t]word_t

3var cData : [index_t]word_t

4var cTag : [index_t]tag_t

5var mem : [word_t]word_t

6// Load operation

7operation load (rs, rd, imm) {

8 addr = regs[rs] + imm; // Compute the address

9 if (cacheTag(addr_to_tag(addr)) == addr) {

10 ... // Load from cache if hit

11 } else {

12 data = mem[addr]; // Load from memory

13 }

14 regs[rd] = data; // Register writeback

15}

16

17// Generic ALU Register-Register operation

18operation alu (rs1, rs2, rd, op) {

19 if (op == ADD) regs[rd] = regs[rs1] + regs[rs2];

20 ...

21}

Figure 3. Fragment of a platform model with state variables and load and alu
operation semantics.

###  2.3. Why convert from $\mathrm{SH}$ to $\mathrm{AP}$?

#### Manual pattern generation is error-prone

While more scalable, $\mathrm{AP}$ approaches require creation of several
patterns, due to their gadget-specificity. To avoid unsound analysis (e.g.,
using only pattern A on victimB), it is important that patterns are not
missed, e.g., pattern B which we have not observed being formulated
previously.

Moreover, patterns need to be recreated for newer microarchitectures (with
newer vulnerabilities). Consider victimC (Fig. 1 left) which replaces a cache-
based side channel (as in victimA) with a computation unit-based channel. Its
variant victimD inverts the first load and the branch (as in victimB). These
examples are inspired from (Sanchez Vicarte et al., 2021), which hypothesizes
the existence of computation-unit based side-channels on microarchitectures
with data-operand-dependent timing (Intel, 2023; Ge et al., 2018; Sanchez
Vicarte et al., 2021). Existing work, which targets cache-based side channels,
misses patterns C and D (Fig. 1 center) that capture victimC and victimD.
Automating pattern generation can make patterns more comprehensive and cover
newer microarchitectural features.

#### Semantic hyperproperties as a specification for automated pattern
generation

In this work, we propose a technique to automatically generate patterns for a
given hyperproperty and microarchitecture. As an example we were able to
automatically generate patterns C and D from the (shared) hyperproperty
$\text{H}_{\text{CD}}$.

Our key insight is using the semantic hyperproperty as a specification to
guide pattern generation. Since a hyperproperty can capture an entire class of
exploits targetting a vulnerability, we can use it to determine whether a
given pattern yields an exploit by checking it against the hyperproperty. By
automatically checking several candidates, we can identify a comprehensive set
of patterns for that hyperproperty. Thus, our technique replaces manual
pattern creation with the requirement of specifying a hyperproperty and
platform model. To summarize, by developing an automated conversion technique
from $\mathrm{SH}$-specifications to $\mathrm{AP}$-based patterns, we combine
the low-overhead, uniform specifications and formal guarantees of
$\mathrm{SH}$ with the superior verification scalability of $\mathrm{AP}$ to
get the best of both worlds.

##  3\. System Model

In this section, we introduce our formal model for hardware platforms, which
we later use to develop our problem formulation (§4). At a high level, the
hardware platform is an operational transition system over architectural and
microarchitectural state variables. Instructions executed on the platform
induce transitions over this state. We summarize these elements in Table 3.

####  3.0.1. State

The platform consists of variables $\mathrm{V}$ which take values from a
domain $\mathbb{D}$. $\mathrm{V}$ includes architectural
($\mathrm{V}_{\mathsf{a}}$) and microarchitectural ($\mathrm{V}_{\mathsf{m}}$)
variables. The platform state is an assignment to these variables,
$\sigma:\mathrm{V}\rightarrow\mathbb{D}$. We denote the set of all assignments
as $\Sigma=\mathrm{V}\rightarrow\mathbb{D}$.

Variables (arch. and march.) | $v:$ | $\mathrm{V}=\mathrm{V}_{\mathsf{a}}\cup\mathrm{V}_{\mathsf{m}}$
---|---|---
States (variable assignments) | $\sigma:$ | $\Sigma=\mathrm{V}\rightarrow\mathbb{D}$
Operation code | $\mathsf{op}:$ | $\mathsf{Op}$
Instructions | $\mathsf{inst}:$ | $\mathsf{Inst}=\\{\mathsf{op}(\omega)\\}_{\mathsf{op},\omega}$
Full (speculative) semantics |  $\mathsf{T}$ : | $\mathsf{Inst}\times\Sigma\rightarrow\Sigma$
Non-speculative semantics |  $\mathsf{T}_{\mathsf{ns}}$ : | $\mathsf{Inst}\times\Sigma\rightarrow\Sigma$
Table 3. Platform state and operational semantics.

####  3.0.2. Instruction semantics

The platform executes a set of instructions of form
$\mathsf{inst}=\mathsf{op}(\omega)$, where $\mathsf{op}$ is the instruction
opcode, and $\omega$ are operands. The platform assigns two transition
semantics to each instruction: a full semantics (allowing speculation) denoted
as $\mathsf{T}$ and a non-speculative semantics denoted as
$\mathsf{T}_{\mathsf{ns}}$. Both semantics can be viewed as functions taking
an instruction and the current platform state as input and returning the next
platform state (obtained after executing the instruction). The full semantics
defines the behaviour when the platform can speculate (not necessarily
enforcing speculative behaviour at all times) while the non-speculative
semantics defines behaviours when speculation is disabled.

###### Example 0.

For the platform model in Fig. 3, the architectural and microarchitectural
variables are
${{\mathrm{V}_{\mathsf{a}}=\\{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{mem}}}}}},\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{regs}}}}}}\\}$
and
${{\mathrm{V}_{\mathsf{m}}=\\{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{cacheTag}}}}}},\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{cacheData}}}}}}\\}$,
with $\mathrm{V}=\mathrm{V}_{\mathsf{a}}\cup\mathrm{V}_{\mathsf{m}}$. The
semantics of the load instruction updates the register file regs and the cache
state variables (cacheData, cacheTag) as defined in Fig. 3.

####  3.0.3. Modelling speculation

Instructions, e.g., branches or loads (store-to-load forwarding), signal that
they are initiating speculation by setting a variable
$\mathit{spec}\in\mathrm{V}$. Internally, the full semantics $\mathsf{T}$
defines instruction behaviour by conditioning on $\mathit{spec}$:
$\mathit{spec}$ being set implies that the platform is currently speculating.
Indeed, $\mathit{spec}$ can be set only in the full semantics ($\mathsf{T}$)
and not in $\mathsf{T}_{\mathsf{ns}}$. Prior work considers specialized
semantics that define when $\mathit{spec}$ is set (e.g., oracle-based
semantics (Guarnieri et al., 2020)). Since we adopt a hardware-oriented model,
we assume that this is explicitly defined in the transition semantics of the
speculating instruction. Despeculation is assumed to be similarly defined
(this time, however, by unsetting $\mathit{spec}$).

In our current implementation, we restrict speculation to a single frame, and
do not support nested speculation (e.g., speculative loads within a branch
speculation context). However, this is not a fundamental limitation of our
approach; extension to nested speculation is possible by defining a stack of
frames storing architectural state.

####  3.0.4. Executions

The platform consumes a stream of instructions, and transitions on them,
thereby producing a trace of states. Then, an input instruction stream
$C=\mathsf{inst}_{0},\mathsf{inst}_{1},\ldots,\mathsf{inst}_{n}$, starting in
state $\sigma_{0}$ leads to a sequence of states
$\pi=\sigma_{0}\leavevmode\nobreak\ \sigma_{1}\leavevmode\nobreak\
\ldots\leavevmode\nobreak\ \sigma_{n+1}$, where
$\sigma_{i+1}=\mathsf{T}(\mathsf{inst}_{i},\sigma_{i})$ (under the full
semantics) and
$\sigma_{i+1}=\mathsf{T}_{\mathsf{ns}}(\mathsf{inst}_{i},\sigma_{i})$ (under
the non-speculative semantics). The execution generated by instruction stream
$C$ from initial state $\sigma$ is denoted as $\llbracket
C\rrbracket(\sigma)$. We similarly define non-speculative executions
$\llbracket C\rrbracket_{\mathsf{ns}}(\sigma)$ in which instructions follow
the $\mathsf{T}_{\mathsf{ns}}$ transition relation.

##  4\. Specifications and Problem Formulation

In this section we formalize hyperproperty specifications (§4.1) and the
notion of attack patterns that our approach aims to generate (§4.2). We then
discuss a technical limitation of pattern-based approaches in §4.3, and
formulate the problem statement in §4.4.

###  4.1. Hyperproperty-based Security Specification

We follow existing work ((Clarkson and Schneider, 2008; Guarnieri et al.,
2020)) to formalize non-interference-based security specifications.

Non-interference ((Clarkson and Schneider, 2008)) states that any pair of
executions which begin in states with equivalent values of public (non-secret)
variables ($\mathrm{V}_{\mathsf{pub}}$) continue to have states with
equivalent values of observable variables ($\mathrm{V}_{\mathsf{obs}}$): 222
Here, $\sigma_{1}\equiv_{\mathrm{V}^{\prime}}\sigma_{2}$ for
$\mathrm{V}^{\prime}\subseteq\mathrm{V}$ means that
$\sigma_{1}(v)=\sigma_{2}(v)$ for all $v\in\mathrm{V}^{\prime}$ (the
assignments agree on all variables in $\mathrm{V}^{\prime}$). For traces
$\pi_{1}$ and $\pi_{2}$, $\pi_{1}\equiv_{\mathrm{V}^{\prime}}\pi_{2}$ holds if
$\pi_{1}[i]\equiv_{\mathrm{V}^{\prime}}\pi_{2}[i]$ for all $i$.

$\displaystyle C\models$ $\displaystyle\leavevmode\nobreak\
\mathsf{NI}(\Sigma_{\mathsf{init}},\mathrm{V}_{\mathsf{pub}},\mathrm{V}_{\mathsf{obs}})\overset{\Delta}{=}\forall\sigma_{1},\sigma_{2}\in\Sigma_{\mathsf{init}}.$
$\displaystyle\sigma_{1}\equiv_{\mathrm{V}_{\mathsf{pub}}}\sigma_{2}\implies\llbracket
C\rrbracket(\sigma_{1})\equiv_{\mathrm{V}_{\mathsf{obs}}}\llbracket
C\rrbracket(\sigma_{2})$

This property is parameterized by the choice of $\Sigma_{\mathsf{init}}$,
$\mathrm{V}_{\mathsf{pub}}$ and $\mathrm{V}_{\mathsf{obs}}$ and intuitively
says that the observable variables are not affected by the secret
($\mathrm{V}_{\mathsf{sec}}=\mathrm{V}\setminus\mathrm{V}_{\mathsf{pub}}$)
variables. Non-interference expresses security against an attacker that tries
to infer the values of $\mathrm{V}_{\mathsf{sec}}$ by observing
$\mathrm{V}_{\mathsf{obs}}$.

Speculative non-interference enforces non-interference only if the program is
non-interfering under non-speculative semantics:

$\displaystyle C\models$ $\displaystyle\leavevmode\nobreak\
\mathsf{SNI}(\Sigma_{\mathsf{init}},\mathrm{V}_{\mathsf{pub}},\mathrm{V}_{\mathsf{obs}})\overset{\Delta}{=}\forall\sigma_{1},\sigma_{2}\in\Sigma_{\mathsf{init}}.$
$\displaystyle(\sigma_{1}\equiv_{\mathrm{V}_{\mathsf{pub}}}\sigma_{2}\land\llbracket
C\rrbracket_{\mathsf{ns}}(\sigma_{1})\equiv_{\mathrm{V}_{\mathsf{obs}}}\llbracket
C\rrbracket_{\mathsf{ns}}(\sigma_{2}))\implies$ $\displaystyle\llbracket
C\rrbracket(\sigma_{1})\equiv_{\mathrm{V}_{\mathsf{obs}}}\llbracket
C\rrbracket(\sigma_{2})$

Intuitively, SNI restricts the scope of non-interference enforcement, we refer
the reader to (Guarnieri et al., 2020; Cheang et al., 2019) for more details.

Conditional/contract-based non-interference (Guarnieri et al., 2021) is
another variant which also restricts the scope of non-interference using an
architectural semantics. It requires that a program be non-interfering in the
full semantics if it is non-interfering in the architectural semantics. While
we focus our presentation on non-interference our technique also applies to
these variants, as demonstrated in §7.

###  4.2. Attack Pattern-based Security

####  4.2.1. Patterns

A pattern $\mathsf{p}$ is a pair $(w,\phi)$ of a template $w$ and a constraint
($\phi$), i.e., a boolean formula. The template is a sequence over opcodes
$w=\mathsf{op}_{0}\cdot\mathsf{op}_{1}\cdots\mathsf{op}_{k}$ that structurally
restricts executions the pattern can be embedded in, to those with an opcode
subsequence matching the template. The constraint ($\phi$) further
semantically constrains matching executions to those satisfying it.

Figure 4. A pattern for a computation-based side channel.

###### Example 0 ($\texttt{MulOp}-\texttt{LdOp}-\texttt{MulOp}$ pattern).

The pattern from Fig. 4 is formalized as $(w,\phi)$ where,
$w=(0:\texttt{MulOp})\cdot(1:\texttt{LdOp})\cdot(2:\texttt{MulOp})$ and the
constraint is
$\phi\equiv\mathsf{datadep}(1:\texttt{LdOp},2:\texttt{MulOp})\land\mathsf{highresult}(1:\texttt{LdOp})$,
i.e., there is a data dependency between the load and the second
multiplication operation, and a the loaded result is high (secret dependent).
Intuitively, this pattern matches executions satisfying $\phi$ with a
$\texttt{MulOp}-\texttt{LdOp}-\texttt{MulOp}$ instruction subsequence.

####  4.2.2. Execution-embedding

Now we formalize when a pattern embeds (matches) an execution, which
determines which programs the pattern flags as exploits. Consider pattern
$\mathsf{p}=(w,\phi)$ with template
$w=\mathsf{op}^{*}_{1}\cdots\mathsf{op}^{*}_{k}$, and an execution
$\pi=\sigma_{0}\cdot\sigma_{1}\cdots\sigma_{n}$. Let the sequence of opcodes
in $\pi$ be $\mathsf{op}_{1}\cdots\mathsf{op}_{n}$, i.e., the transition from
$\sigma_{i}$ to $\sigma_{i+1}$ is performed by executing an instruction with
opcode $\mathsf{op}_{i+1}$. The pattern $\mathsf{p}$ embeds in execution $\pi$
at a subsequence given by indices $(i_{1}<\cdots<i_{k})$ if the corresponding
opcodes match the template $w$: $\mathsf{op}_{i_{j}}=\mathsf{op}^{*}_{j}\text{
for }j\in[1\cdots k]$, and the execution $\pi$ satisfies the constraint
$\phi$. We denote the fact that $\mathsf{p}$ embeds at indices
$(i_{1},\cdots,i_{k})$ in trace $\pi$ as
$\pi\models_{(i_{1},\cdots,i_{k})}\leavevmode\nobreak\ (w,\phi)$. Execution
$\pi$ embeds $(w,\phi)$ if there is a matching subsequence:

$\pi\models(w,\phi)\overset{\Delta}{=}\exists
i_{1},\cdots,i_{k}.\leavevmode\nobreak\ \leavevmode\nobreak\
\pi\models_{(i_{1},\cdots,i_{k})}(w,\phi)$

Attack pattern $\mathsf{p}=(w,\phi)$ matches instruction sequence $C$ if there
is some execution of $C$ that embeds it:

$C\models\mathsf{p}\overset{\Delta}{=}\exists\sigma\in\Sigma_{\mathsf{init}}.\leavevmode\nobreak\
\llbracket C\rrbracket(\sigma)\models\mathsf{p}$

Fig. 2 provides examples of patterns matching instructions.

###  4.3. Non-interference Violation Skeleton

Given a hyperproperty, we aim to generate a set of patterns such that any
hyperproperty violation is detected by atleast one of the patterns in this
set. However, as illustrated in Example 2 the fact that patterns have fixed
length is a fundamental limitation in the violations they can detect.

Figure 5. Buffer chain in $\textsc{PlatSynth}(k)$ with operations.

###### Example 0 (Large skeletons: the $\textsc{PlatSynth}(k)$ platform).

Consider the pedagogical example microarchitecture illustrated in Fig. 5 with
$k+1$ state variables (e.g., buffers):
${{\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{buf}}}}}}}_{0},\cdots,\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{buf}}}}}}}_{k}\in\mathrm{V}$,
and $k$ corresponding operations
$\mathsf{op}_{1},\mathsf{op}_{2},\cdots,\mathsf{op}_{k}\in\mathsf{Op}$.
Operation $\mathsf{op}_{i}$ moves data from
${\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{buf}}}}}}}_{i-1}$
to
${\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{buf}}}}}}}_{i}$.
Now, consider a non-interference property with
${{\mathrm{V}_{\mathsf{pub}}=\\{\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{buf}}}}}}}_{1},\cdots,\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{buf}}}}}}}_{k}\\}$,
and
${\mathrm{V}_{\mathsf{obs}}=\\{\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{buf}}}}}}}_{k}\\}$.
That is we want to identify whether the secret input
${\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{buf}}}}}}}_{0}$
affects the observable output
${\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{buf}}}}}}}_{k}$.
While the operation sequence $\mathsf{op}_{1}\cdots\mathsf{op}_{k}$ violates
this property (it moves data from
${\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{buf}}}}}}}_{0}$
to
${\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{buf}}}}}}}_{k}$),
any sequence of length $k-1$ or less does not.

Given the possibility of large non-interference violations that would be
greater than the size of any fixed set of patterns, we qualify our problem
statement to detecting those violations with small skeletons, as we now
define.

Consider an instruction sequence $C=\mathsf{inst}_{0}\leavevmode\nobreak\
\mathsf{inst}_{1}\leavevmode\nobreak\ \cdots$, and a corresponding execution
trace $\pi=\llbracket C\rrbracket(\sigma)$. For a trace index $i$, we denote
the variables that $\mathsf{inst}_{i}$ depends on as
$\mathsf{dep}_{\pi}(i)\subseteq\mathrm{V}$. We denote the last writer of a
variable $v\in\mathrm{V}$ at index $i$, denoted as
$\mathsf{lw}_{\pi}(v,i)\in\\{\mathsf{inst}_{0},\cdots,\mathsf{inst}_{i-1}\\}$
as the last instruction that writes to $v$ before $\mathsf{inst}_{i}$.
Finally, the set of all (instruction) dependencies of an instruction
$\mathsf{inst}_{i}$ is the union of the last writers of all variables it
depends on:
$\mathsf{idep}_{\pi}(i)=\bigcup_{v\in\mathsf{dep}_{\pi}(i)}\mathsf{lw}_{\pi}(v,i)$.
For a trace $\pi$, we say that $i_{1},\cdots,i_{k}$ is a subsequence that is
closed under dependencies if for all $j\in[1\cdots k]$,
$\mathsf{idep}(i_{j})\in\\{i_{1},\cdots,i_{k}\\}$.

###### Definition 0 (Skeleton).

Suppose the sequence of instructions
$\mathsf{inst}_{1}\cdots\mathsf{inst}_{n}$ violates a non-interference
property $\mathsf{NI}$. Then, $C$ has an $\mathsf{NI}$-violation skeleton of
size $k$, denoted as $C\not\models_{k}\mathsf{NI}$ if there exist traces
$\pi_{1},\pi_{2}$ with subsequences of length $k$ which are closed under
dependencies and also violate $\mathsf{NI}$.

###  4.4. Formal Problem Statement

Formally, given (a) a platform model (with state $\mathrm{V}$ and semantics
$\mathsf{T}$), and (b) a non-interference security specification
$\mathsf{NI}$($\Sigma_{\mathsf{init}}$, $\mathrm{V}_{\mathsf{pub}}$, and
$\mathrm{V}_{\mathsf{obs}}$), and (c) a given skeleton size $k$, we generate a
set of patterns $\mathsf{P}$ such that any instruction sequence $C$ that
violates the non-interference property with a skeleton of size $k$ is detected
by one of the patterns in $\mathsf{P}$:

(1) $\forall C.\leavevmode\nobreak\ \leavevmode\nobreak\
C\not\models_{k}\mathsf{NI}(\Sigma_{\mathsf{init}},\mathrm{V}_{\mathsf{pub}},\mathrm{V}_{\mathsf{obs}})\implies\exists\mathsf{p}\in\mathsf{P}.\leavevmode\nobreak\
C\models\mathsf{p}$

We refer to Eq. 1 as the $k$-completeness property.

##  5\. The SemPat Approach

Figure 6. The SemPat approach.

In this section we discuss our approach to automatically generate attack
patterns satisfying $k$-completeness (Eq. 1). We provide an overview in §5.1,
followed by details in §5.2 and §5.4.

⬇

1type rentry_t = record { op1: word_t, op2: word_t, result: word_t };

2var reuse_buf : [instr_ind_t]rentry_t;

3

4operation mulop (rd, rs1, rs2) {

5 op1 = regfile[rs1]; op2 = regfile[rs2];

6 // Check for reuse

7 if ($\exists$ i. reuse_buf[i].op1 == op1 &&

8 reuse_buf[i].op2 == op2) {

9 result = reuse_buf[i].result; // Reuse result

10 } else { // Otherwise invoke multiplier unit

11 result = multiplier(op1, op2);

12 mulcount = mulcount + 1;

13 }

14 // Replace reuse_buf entry (at index ind_)

15 reuse_buf[ind_] = rentry_t {op1, op2, result};

16 regfile[rd] = result;

17}

Figure 7. PlatCR: Fragment of the computation reuse platform model.

###  5.1. Pattern Generation Overview

#### Operation

Figure 6 provides a high-level overview of our approach. We take in a
transition system-based platform model (§3), a non-interference specification
(§4.1), a constraint grammar $G$ and depth $d$. We generate a set of patterns
$\mathsf{P}$ up to depth $d$, with constraints sourced from $G$ (discussed in
§5.3). Our approach has two components: template generation (§5.2) and
grammar-based specialization (§5.4). We explain these elements using a running
example.

#### Running Example: Computation Reuse

We use the running example of the generation of the
$\texttt{MulOp}-\texttt{LdOp}-\texttt{MulOp}$ pattern from Fig. 4. We generate
this pattern based on the computation-reuse platform model (PlatCR), an
excerpt of which is provided in Fig. 7. The PlatCR microarchitecture includes
a reuse buffer (reuse_buf) that stores the operands and results of previous
multiplication (mul) instructions. Future mul instructions matching operands
of previous instructions, can reuse results from the buffer instead of
reinvoking the multiplier. We encode the security property that secret data
from the memory should not affect the count of multiplier invocations as the
property
${\mathsf{NI}_{\textsc{PlatCR}}(\mathsf{init}_{\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{reuse\textunderscore
buf}}}}}}}},\texttt{mem},\texttt{mulcount})$ where
${\mathsf{init}_{\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{reuse\textunderscore
buf}}}}}}}}$ constrains all entries in the reuse_buf to be initially invalid
and $\texttt{mulcount}\in\mathrm{V}$ counts multiplier invocations.

###  5.2. Template Generation

The first phase of our approach uses an overapproximate analysis to generate
templates up to the user-specified depth $d$. This is performed by the
GenerateTemplates procedure. We discuss GenerateTemplates intuitively and
illustrate it with an example, while defering its pseudocode to the appendix.
GenerateTemplates scans over all templates starting with size 1 (single
operations) up to size $d$. For each template, we first perform
(overapproximate) taint analysis to check whether the template propagates
taint from the secret inputs ($\mathrm{V}_{\mathsf{sec}}$) to the public
outputs ($\mathrm{V}_{\mathsf{obs}}$). If it does not, then the template will
also not violate the target non-interference property, and we can skip over
it. If it does propagate taint from $\mathrm{V}_{\mathsf{sec}}$ to
$\mathrm{V}_{\mathsf{obs}}$, we check if the template violates the target non-
interference property semantically. We do this by reducing non-interference to
a safety query (e.g., (Rushby, 1992; Clarkson and Schneider, 2008)), and
solving this query using SMT-based model checking ((McMillan, 1993; Barrett et
al., 2009)).

###### Example 0 (Template generation for
$\texttt{MulOp}-\texttt{LdOp}-\texttt{MulOp}$).

Consider invoking GenerateTemplates for the PlatCR platform (Fig. 7) with
$\mathsf{NI}_{\textsc{PlatCR}}$ as the non-interference property and a search
depth of 3. GenerateTemplates first considers single operation templates.
However, none of them propagate taint from mem to mulcount. Subsequently,
GenerateTemplates finds the two-operation template
$\texttt{LdOp}-\texttt{MulOp}$ does propagate taint from mem to mulcount.
However, this template does not (semantically) violate non-interference as the
reuse_buf is initially empty, and the multiplier must be invoked in all
executions. Eventually, GenerateTemplates considers the size 3 template
$\texttt{MulOp}-\texttt{LdOp}-\texttt{MulOp}$. This template both, propagates
taint and semantically violates $\mathsf{NI}_{\textsc{PlatCR}}$. This is
because the first MulOp ‘primes’ the reuse buffer, and the second MulOp uses
the primed buffer entry. This will lead to two executions with different
mulcount values, i.e., a non-interference violation.

GenerateTemplates generates all operation sequences (up to length $d$) that
violate the non-interference property:

###### Lemma 0.

For $k\leq d$, if
$\mathsf{inst}_{1}\cdots\mathsf{inst}_{k}\not\models\mathsf{NI}$ where
instruction $\mathsf{inst}_{i}=\mathsf{op}_{i}(\omega_{i})$, then,
$\mathsf{op}_{1}\cdots\mathsf{op}_{k}\in\textbf{GenerateTemplates}{}(M,\mathsf{NI},d)$.

Input: Semantic platform definition $M$, non-interference property
$\mathsf{NI}$, pattern template $w$, and a grammar $G$

Output: A set of patterns

Data: acc: an accumulated set of patterns

1

2Function  _ConsHelper(_$\phi,i,L$_)_:

/* Exhausted all atomic predicates? */

3 if  _$i >|L|$_ then acc.append($(w,\phi)$)

/* Does adding $\neg L[i]$ eliminate all violations? */

_4_ _ _ else if  _
$\forall\mathsf{inst}_{1},\cdots,\mathsf{inst}_{|w|}.\leavevmode\nobreak\
\mathsf{inst}_{1}\cdots\mathsf{inst}_{|w|}\models(w,\phi\land\neg
L[i])\implies\mathsf{inst}_{1},\cdots,\mathsf{inst}_{|w|}\models\mathsf{NI}$ _

5  __ then ConsHelper(_$\phi\land L[i]$ , $i+1,L$_) /* add $L[i]$ */

6 else ConsHelper(_$\phi,i+1,L$_);

7 /* skip over $L[i]$ */

$L$ = ApplyPredicates($w,G$)

/* Create all atoms in $L$ */

ConsHelper(_$\texttt{true},0,L$_)

/* Counterfact. addition */

return acc

Algorithm 1 ConstraintSpecialize($M,\mathsf{NI},w,G$)

Predicate Atom | Meaning | Encoding (assuming RISC-V ISA)
---|---|---
$\mathsf{datadep}(\mathsf{inst}_{1},\mathsf{inst}_{2})$ | Data operand of $\mathsf{inst}_{2}$ depends on result of $\mathsf{inst}_{1}$ | Last write to $\mathsf{inst}_{2}.\texttt{rs1}$ or $\mathsf{inst}_{2}.\texttt{rs2}$ is by $\mathsf{inst}_{1}$
$\mathsf{addrdep}(\mathsf{inst}_{1},\mathsf{inst}_{2})$ | Address operand of $\mathsf{inst}_{2}$ depends on result of $\mathsf{inst}_{1}$ | Last write to $\mathsf{inst}_{2}.\texttt{rs1}$ is by $\mathsf{inst}_{1}$
$\mathsf{sameaddr}(\mathsf{inst}_{1},\mathsf{inst}_{2})$ | Address operands of $\mathsf{inst}_{1}$ and $\mathsf{inst}_{2}$ are the same |  $\mathsf{inst}_{2}.\texttt{addr}=\mathsf{inst}_{1}.\texttt{addr}$ (for memory operations)
$\mathsf{diffaddr}(\mathsf{inst}_{1},\mathsf{inst}_{2})$ | Address operands of $\mathsf{inst}_{1}$ and $\mathsf{inst}_{2}$ are different |  $\mathsf{inst}_{2}.\texttt{addr}\neq\mathsf{inst}_{1}.\texttt{addr}$ (for memory operations)
$\mathsf{srcdata}_{\texttt{reg}}(\mathsf{inst}_{1})$ | Data operand is read from register reg | e.g., $\mathsf{inst}_{1}.\texttt{rs1}=\texttt{reg}$, $\mathsf{inst}_{1}.\texttt{rs2}=\texttt{reg}$ (depends on opcode)
$\mathsf{srcaddr}_{\texttt{reg}}(\mathsf{inst}_{1})$ | Address operand is read from register reg |  $\mathsf{inst}_{1}.\texttt{rs1}=\texttt{reg}$ (for memory operations)
$\mathsf{destreg}_{\texttt{reg}}(\mathsf{inst}_{1})$ | Result is written to a register reg | $\mathsf{inst}_{1}.\texttt{rd}=\texttt{reg}$
$\mathsf{speculative}(\mathsf{inst})$ | Instruction $\mathsf{inst}$ initiates speculation |  $\mathsf{inst}$ sets the $\mathit{spec}$ variable
$\mathsf{lowoperands}(\mathsf{inst}_{1})$ | Operands of $\mathsf{inst}_{1}$ is independent of $\mathrm{V}_{\mathsf{sec}}$ ($=\mathrm{V}\setminus\mathrm{V}_{\mathsf{pub}}$) | e.g., $\sigma_{1}(\mathsf{regfile}[\texttt{rs1}])=\sigma_{2}(\mathsf{regfile}[\texttt{rs1}])$ (depends on opcode)
$\mathsf{lowresult}(\mathsf{inst}_{1})$ | Result of $\mathsf{inst}_{1}$ is independent of $\mathrm{V}_{\mathsf{sec}}$ ($=\mathrm{V}\setminus\mathrm{V}_{\mathsf{pub}}$) | $\sigma_{1}(\mathsf{regfile}[\texttt{rd}])=\sigma_{2}(\mathsf{regfile}[\texttt{rd}])$

Table 4. Pattern predicate grammar: we generate patterns with constraints as
conjunctions of these predicate atoms.

###  5.3. Conjunction-based Pattern Grammar

While templates alone are too overapproximate to be useful, augmenting
(specializing) them with constraints ($\phi$) leads to more precise patterns
with fewer false positives. Specialization is performed using the user
provided grammar $G$ that identifies the space of these constraints.

####  5.3.1. Conjunction of Predicate Atoms

We consider constraints which are conjunctions of atoms.333In formal logic, an
atom (atomic formula) is a single (indivisible) logical proposition. That is,
$\phi$ has form: $\phi=\bigwedge_{i}f_{i}$, where each $f_{i}$ is an atom.
These atoms ($f_{i}$) are generated by applying predicates from a grammar $G$,
such as the one in Table 4, which we use as the default. Each predicate from
the grammar is applied to some number of instructions from the pattern, as
indicated by its arity (e.g., $\mathsf{datadep}$ is an arity-2 (binary)
predicate). To identify the instructions a predicate is applied to, we
distinguish apart identical opcodes using their position (e.g., the
$\mathsf{datadep}$ predicate is applied to ($0:\texttt{MulOp}$),
($2:\texttt{MulOp}$) in Example 1).

####  5.3.2. Precision vs. Robustness Tradeoff

A grammar that only allows high-level (architectural) predicates (e.g., Tab.
4) leads to patterns which are less sensitive to microarchitectural
implementation details, but have more false positives. Conversely, a grammar
that exposes low-level microarchitectural constraints leads to more precise
patterns (with fewer false positives). However, these patterns are then
specific to the platform microarchitecture. Thus, the pattern grammar exposes
a tradeoff between the robustness and expressivity/precision of generated
patterns. While our specialization technique (§5.4) requires a conjunction-
based grammar (§5.3.1), we are not fundamentally limited to the predicates
from Table 4. We explore this further in §7.4 where we augment the default
grammar with additional predicates to improve precision.

###  5.4. Template Specialization with Predicates

The goal of template specialization is making patterns as precise as possible
using the pattern grammar (§5.3), while ensuring that they do not miss any
violating executions (as required by Eq. 1). Specialization is performed by
invoking the ConstraintSpecialize procedure (Alg. 1) on every pattern template
generated by GenerateTemplates. At a high level, starting with the true
constraint (line 0), ConstraintSpecialize continues adding predicate atoms to
the constraint.

####  5.4.1. Candidate predicate atoms

As introduced in §5.3, the pattern constraint is a conjunction of predicate
atoms from grammar $G$. We apply each predicate to operations from the
template to get a set of atoms. For example, the binary $\mathsf{datadep}$
predicate with the $(0:\texttt{MulOp})-(1:\texttt{LdOp})-(2:\texttt{MulOp})$
template results in three atoms:
$\mathsf{datadep}(0:\texttt{MulOp},1:\texttt{LdOp})$,
$\mathsf{datadep}(1:\texttt{LdOp},2:\texttt{MulOp})$ or
$\mathsf{datadep}(0:\texttt{MulOp},2:\texttt{MulOp})$ (we ignore backwards
dependencies). ConstraintSpecialize first collects all such atoms in a list
$L$ using the ApplyPredicates helper function (line 6).

####  5.4.2. Counterfactual-based atom addition

Adding an atom strengthens the pattern constraint, resulting in it capturing
fewer executions. To ensure that the generated pattern does not miss any non-
interference violations (and thereby violate Eq. 1) we use counterfactual atom
addition. Counterfactual addition adds an atom only if adding the negation of
the atom leads to only non-violating executions. Intuitively, if the negation
leads to only non-violating executions, then adding the atom preserves all
violating executions:

###### Observation 1.

Consider a pattern $(w,\phi)$, where $|w|=k$, and an atom $f$. We have, for
all $C=\mathsf{inst}_{1}\cdots\mathsf{inst}_{k}$:

$\displaystyle\big{(}C\models(w,\phi\land\neg f)\implies
C\models\mathsf{NI}\big{)}\implies$
$\displaystyle\quad\quad\big{(}(C\models(w,\phi)\land
C\not\models\mathsf{NI})\implies C\models(w,\phi\land f)\big{)}$

For each atom in $L$, we check (Alg. 1 line 3) if it satisfies the
counterfactual addition condition, specializing the pattern (line 4) if so. If
not, we skip over it (line 5) and move to the next atom in $L$.

###### Example 0.

For the $(0:\texttt{MulOp})-(1:\texttt{LdOp})-(2:\texttt{MulOp})$ template,
ConstraintSpecialize adds the
$f=\mathsf{datadep}(1:\texttt{LdOp},2:\texttt{MulOp})$ atom to the constraint,
since if $(2:\texttt{MulOp})$ does not depend on $(1:\texttt{LdOp})$, then its
operands are not secret, and the non-interference property is not violated. In
a further iteration, ConstraintSpecialize adds the atom
$\mathsf{highresult}(1:\texttt{LdOp})$ which says that the loaded value is
secret-dependent. Once again, the negation of this would lead to a non-
violating execution. This gives us the final pattern with
$w=(0:\texttt{MulOp})-(1:\texttt{LdOp})-(2:\texttt{MulOp})$ and
$\phi=\mathsf{datadep}(1:\texttt{LdOp},2:\texttt{MulOp})\land\mathsf{highresult}(1:\texttt{LdOp})$.

####  5.4.3. Multiple counterfactuals and branching

Counterfactual addition relies on a strong condition which may not hold for
single atoms. In such cases, we consider multiple counterfactual atoms:

###### Observation 2 (Multiple counterfactuals).

For pattern $(w,\phi$), atoms $\\{f_{i}\\}_{i}$, and for any
$C=\mathsf{inst}_{1}\cdots\mathsf{inst}_{|w|}$:

$\displaystyle\big{(}C\models(w,\phi\land\bigwedge_{i}\neg f_{i})\implies
C\models\mathsf{NI}\big{)}\implies$
$\displaystyle\quad\quad\big{(}(C\models(w,\phi)\land
C\not\models\mathsf{NI})\implies{\boldsymbol{\bigvee}_{i}}(C\models(w,\phi\land
f_{i}))\big{)}$

Considering multiple counterfactuals $\\{f_{i}\\}$ results in a disjunctive
branching (bolded $\bigvee_{i}$) over atoms. ConstraintSpecialize recursively
invokes ConsHelper on $(w,\phi\land f_{i})$ for each $i$. This is sound as the
collection of patterns together continue to cover all violating executions. We
do not include multi-counterfactuals in Alg. 1 pseudocode for brevity; we
provide full pseudocode in the appendix.

###### Example 0 (Multiple counterfactuals for PlatSynth).

Consider the platform $\textsc{PlatSynth}(k)$ from Ex. 2, with parameter $k=2$
and grammar depth $d=3$. GenerateTemplates returns the template
$(0:\mathsf{op}_{0})-(1:\mathsf{op}_{0})-(2:\mathsf{op}_{1})$ for which
neither atom $\mathsf{datadep}(0:\mathsf{op}_{0},2:\mathsf{op}_{1})$ nor
$\mathsf{datadep}(1:\mathsf{op}_{0},2:\mathsf{op}_{1})$ can be added alone.
This is because, even if one is negated, the other might be true, leading to a
non-interference violation. However, on adding both negations, the violation
is blocked. Our approach then will branch and specialize each case further.

By Lem. 2 and Obs. 1,2, we have $k$-completeness of our approach up to
skeleton size $k=d$. This is formalized through the following theorem and
proved by induction on the number of specialization iterations. We provide a
proof in the appendix.

###### Theorem 5.

Let $W=\textbf{GenerateTemplates}{}(M,\mathsf{NI},d)$ be the templates for
depth $d$, and let
$\mathsf{P}_{i}=\textbf{ConstraintSpecialize}{}(M,\mathsf{NI},w_{i},G)$ be the
specialized patterns for each $w_{i}\in W$. Then, for all instruction
sequences $C=\mathsf{inst}_{1}\cdots\mathsf{inst}_{k}$, with $k\leq d$, we
have:

$C\not\models\mathsf{NI}\implies\exists\mathsf{p}\in\bigcup_{i}\mathsf{P}_{i}.\leavevmode\nobreak\
C\models\mathsf{p}$

##  6\. Evaluation Methodology

###  6.1. Tool Prototype

We implement our approach in a prototype tool SECANT. SECANT allows us to
generate patterns, and analyze program binaries using these patterns. For
pattern generation, SECANT allows the user to specify the platform description
(§3), and the non-interference specification (§4.1). By default pattern
generation uses the predicate grammar from Tab. 4. However, we also allow the
user specify custom predicates. Based on these inputs the tool generates a set
of patterns as described in §5. The resulting patterns can be inspected by the
user, and used for binary analysis. Analysis can either be performed using
patterns or the hyperproperty specification. We discuss the details of this
analysis in §6.3.

SECANT uses the UCLID5 (Polgreen et al., 2022) verification engine as the
backend model checker for both, the non-interference checks involved in
pattern generation as well as binary analysis. UCLID5 internally compiles
model checking queries into SMT (Barrett et al., 2016, 2009) queries, and
invokes an SMT solver (e.g. Z3 (de Moura and Bjørner, 2008), CVC5 (Barbosa et
al., 2022)) on them.

###  6.2. Platform Designs

While users can specify their own platform models, we describe the models
considered in our experimentation.

####  6.2.1. PlatCR: Computation Reuse

The computation reuse platform (PlatCR, Fig. 7) was introduced in §5.1. It is
based on microarchitectural optimizations that enable dynamic reuse of results
of previous high-latency computations. Our model includes a reuse buffer
(reuse_buf), which records operands and results of multiply operations, which
are then reused by future operations with matching operands. Dynamic (in-
hardware) optimization schemes have been proposed in the literature (e.g.,
(Mutlu et al., 2005; Sodani and Sohi, 1997; Charles et al., 2002)) and also
have been hypothesized to be vulnerable to computational side-channel attacks
(Sanchez Vicarte et al., 2021). Our model is based on the scheme proposed in
(Sodani and Sohi, 1997).

####  6.2.2. PlatSS: Store Optimization

The store optimization platform (PlatSS) models microarchitectural
optimizations related to the store unit in the memory hierarchy. PlatSS models
the silent stores (Lepak and Lipasti, 2000a; Lepak et al., 2001) and store-to-
load forwarding optimizations. The former squashes (makes silent) stores that
would rewrite the same value to the memory. Store-to-load forwarding serves
store values to subsequent loads on the same address. While these
optimizations have several implementation variants (e.g. (Sha et al., 2005,
2006; Subramaniam and Loh, 2006)), we base our model on the relatively simple
LSQ cache (load-store queue cache) (Lepak and Lipasti, 2000b) which allows
combining these optimizations.

We illustrate the LSQ cache through an excerpt of our model in Fig. 8. The LSQ
cache is a FIFO buffer that records load and store requests. On a load, the
buffer is checked for store requests to the same address. If there exists such
a request (with no subsequent stores to the same address), then the load can
be sourced with this store. On a store too, the buffer is checked for a
request, and the store is squashed (silenced) if the request payload matches
the value written by the store. If a valid entry is not found, the new
load/store performs a full memory request as usual and the LSQ cache is
updated.

⬇

1type lsqc_entry_t = record { valid: boolean,

2 is_load: boolean, addr: word_t, data: word_t }

3var lsqc : [lsqc_index_t]lsqc_entry_t;

4var lptr : lsqc_index_t; // Pointer into LSQC

5var lscount : int; // Number of memory accesses

6

7operation store (rs2, rs1, imm) {

8 addr = addrgen(regfile[rs1], imm);

9 data = regfile[rs2];

10 if (lsqc[lptr].valid && lsqc[lptr].addr == addr

11 && lsqc[lptr].data == data) {

12 // Store squashing (silent store)

13 } else { // Perform memory access

14 mem[addr] = data; lscount += 1;

15 lsqc = ... // Update the lsqc

16 }

17}

18operation load (rd, rs1, imm) {

19 addr = addrgen(regfile[rs1], imm)

20 if (lsqc[lptr].addr == addr && lsqc[lptr].valid){

21 data = lsqc[lptr].data; // Data forwarding

22 } else { // Perform memory access

23 data = mem[data]; lscount += 1;

24 lsqc = ... // Update the LSQC

25 }

26 regfile[rd] = data;

27}

Figure 8. PlatSS: Excerpt of the abstract platform modelling load-store
optimizations in the microarchitecture.

####  6.2.3. Speculation primitives

In addition to the above optimizations, our consider platform models have
branch and store-to-load forwarding speculative features. We model speculation
non-deterministically, abstracting away from the speculative choice mechanism
(e.g. branch predictor). An instruction that speculates moves the platform
into speculative mode by setting the $\mathit{spec}$ variable (described in
§3). Our current implementation only supports a single speculative frame. For
example, we do not allow speculating on loads within a branch speculation
context. However, this is not a fundamental limitation of our approach.

###  6.3. Binary Analysis

We first disassemble the binary to obtain the control flow graph (CFG). We
unroll the control flow graph up to a fixed depth, starting from a particular
entry point. We instrument the unrolling at the branch instructions with
assumptions corresponding to the branch condition, allowing bypassing the
condition when speculating (i.e., if $\mathit{spec}$ is set). For example “if
(x == 0) stmt” is instrumented as “assume(x == 0 || $\mathit{spec}$); stmt”.
Each instrumented unrolling is analyzed using a pattern/hyperproperty based
check.

Pattern-based analysis. Given an unrolling, the pattern-based analysis
implements the pattern check described in §2.2.1. That is, we first identify
all subsequences in that unrolling that match the pattern template. For each
such subsequence, we formulate an SMT query that checks whether the
subsequence satisfies the pattern constraint, and solve it using the UCLID5
model checker (Polgreen et al., 2022).

Hyperproperty-based analysis. The hyperproperty-based analysis follows
existing approaches (e.g., (Cheang et al., 2019; Guarnieri et al., 2020)) by
encoding the hyperproperty as a safety property over a self-composition
((Terauchi and Aiken, 2005; Clarkson and Schneider, 2008)) of the platform
model. The copies in the self-composition execute identical unrolled programs.
Once again we use the UCLID5 model checker to solve the generated safety
query.

##  7\. Experimental Results

#### Experimental Setup

We perform experiments on a machine with an Intel i9-10900X CPU with 64GB RAM
rated at 3.70GHz and running Ubuntu 20.04. As mentioned in §6, we use the
UCLID5 model checker (Polgreen et al., 2022) and Z3 (version 4.8.7) (de Moura
and Bjørner, 2008) as the backend SMT solver for the queries that UCLID5
generates. We mention timeouts for each experiment in its respective section.

#### Research Questions

We aim to answer the following questions through our evaluation: (a) Can the
approach generate new patterns, can these patterns be used to detect attacks,
do they provide performance advantages? (b) How well does our approach scale
with platform complexity, and the pattern generation search depth? (c) How
does the choice of grammar affect false positives?

Figure 9. Pattern for store-to-load forwarding. Explanation: The store address
matches the load, however, due to address computation latency, the load is
speculatively (incorrectly) served from memory while the store is still in the
store buffer and has not propagated to memory.

Figure 10. Modification of SpectreV1 (left) and SpectreV4 (right) litmus tests
from (Daniel et al., 2021) to target a computation-unit side channel (instead
of cache-based side channel). Figure 11. Verification of Branch and STL
speculation litmus tests (see Fig. 10) with hyperproperties and generated
patterns.

###  7.1. RQ1: Can we generate patterns for new vulnerability variants?

To answer RQ1, we considered two extensions to the computation reuse platform
(PlatCR) introduced in §6. In these extensions we modelled branch speculation
and store-to-load forwarding respectively (as discussed in §6.2.3). We then
generated patterns for these platforms based on the speculative non-
interference property $\text{H}_{\text{CD}}$ (§2). We used a reuse_buf of size
4 (i.e., 4 buffer entries), and grammar search depth $d=3$.

Platform |  Gen. time (ww=16) |  Gen. time (ww=20) |  Gen. time (ww=24) |  Gen. time (ww=32)
---|---|---|---|---
Branch + CR | – | 69s
STL + CR | 92s | 334s | TO (1 hour)

Table 5. Generation times for branch speculation and store-to-load forwarding
patterns.

Our approach was able to generate Pattern C and Pattern D from Fig. 1 for
branch speculation with the computation-unit side channel. For store-to-load
forwarding, we obtain the pattern shown in Fig. 9. We provide the time
required to generate these patterns in Table 5. Our STL+CR generation timed
out on a particular non-interference check query with a machine word width of
32 bits, hence, we used lower word widths.444 We believe that this is an
underlying issue with the solver and are investigating it further. The same
hyperproperty ($\text{H}_{\text{CD}}$) was used for both (Branch and STL)
cases, demonstrating that hyperproperties allow uniform vulnerability
specification. This demonstrates the ability of our approach to generate new
patterns.

###  7.2. RQ2: Can the generated patterns efficiently find exploits or prove
their absence?

To answer RQ2, we evaluate whether the generated patterns provide advantages
over hyperproperty-based detection. For this, we considered modified versions
of SpectreV1 and SpectreV4 litmus tests from (Kocher, 2018; Daniel et al.,
2021). In each of these examples, we replaced the secret-dependent load with a
multiply operation (targetting the computation-based side channel). We call
these examples SpectreV1-CR and SpectreV4-CR respectively, and illustrate two
tests (one for V1 and one for V4) in Fig. 10. We consider 9 such tests (8
unsafe, 1 safe) for SpectreV1-CR and 4 tests (all unsafe) for SpectreV4-CR.

We then evaluated both hyperproperty-based and pattern-based detection
approaches on these tests with a timeout of 15 mins per test. We provide the
results in Fig. 11. For each SpectreV1-CR variant test, we considered two
platform configurations: one with a non-associative cache, (denoted as br:<n>
a0) and one with an associative cache (these are marked as br:<n> a1). The
pattern-based approach is able to check all test cases (unsafe and safe)
correctly within ($\sim$5 seconds). In contrast, the hyperproperty-based
approach often takes upwards of 2 mins, with some tests (e.g., br:2, br:3)
even timing out (i.e., taking greater than 15 mins). An interesting
observation is that there are some cases (e.g., br:1, br:4) where the
hyperproperty-based check converges in a reasonable time ($\sim$10s) with the
non-associative cache (a0), while taking much longer (or times out) with the
associative cache (a1). The pattern-based approach is resilient to these
differences since it operates over architectural state. This experiment
demonstrates how, by abstracting away complex platform microarchitecture,
patterns enable security verification that scales much better that
hyperproperties.

###  7.3. RQ3: How well does pattern generation scale?

We explore the scalability of our approach with the complexity of the platform
and the depth of the pattern grammar.

Figure 12. Scalability of pattern generation vs. platform complexity and
grammar depth: (a, b) varying set and way index width of the LSQ Cache (Fig.
8), (c) varying size of the reuse buffer (reuse_buf in Fig. 7), and (d)
generation time and number of generated patterns for PlatSynth with varying
microarchitectural ($\mathsf{pdep}$) and grammar ($\mathsf{gdep}$) depths (Ex.
2).

####  7.3.1. Scalability with model parameters

To evaluate this, we experiment on the PlatSS (§6.2.2) and PlatCR (§6.2.1)
platforms. For PlatSS, we specify a non-interference hyperproperty with
$\mathrm{V}_{\mathsf{sec}}=\\{\texttt{mem}\\}$, as the secret input, and
${\mathrm{V}_{\mathsf{obs}}=\\{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{lscount}}}}}}\\}$
(number of memory operations propagating to memory) as the public output. For
PlatCR, we specify a non-interference property with
$\mathrm{V}_{\mathsf{sec}}=\\{\texttt{mem}\\}$, and
${\mathrm{V}_{\mathsf{obs}}=\\{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{mulcount}}}}}}\\}$,
i.e., number of multiplier invocations as the public output. We vary size
parameters of the LSQ cache (§6.2.2) and reuse buffer (§6.2.1) components
respectively. For the LSQ cache we sweep through the set index width (same
associativity, larger number of sets), and the way index width (same sets,
larger associativity) and present results in Fig. 12 (a, b). For the reuse
buffer, we sweep through different buffer sizes and present the results in
Fig. 12 (c). We perform generation with depths 3 and 4, and a timeout of 30
mins.

Observations: In Fig. 12(a, b), we observe that while generation time grows
with both set and way width, the increase with way index width is more rapid.
Our hypothesis for this is that a larger number of sets increases the width of
indexing bitvectors, while larger associativity increases the number case-
splits (conditionals) since ways are iterated over. The former increase is
slower due to the use of word-level reasoning in SMT solvers, while the latter
has an explicit if-then-else encoding, and hence a larger formula. We observe
a similar increase for the reuse buffer. While the runtime increases
exponentially, our approach is reasonably efficient and is able to generate
patterns on the order of minutes for realistic sizes.

####  7.3.2. Scalability with search depth

In order to investigate the scalability of our approach with the depth of the
grammar, we perform experimentation with the synthetic platform
$\textsc{PlatSynth}(k)$ introduced in Ex. 2. This platform is parameterized by
a platform depth $k=\mathsf{pdep}$, which is the number of microarchitectural
buffers. The non-interference property specifies
${\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{buf}}}}}}}_{0}$
as the secret input, and
${\text{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{buf}}}}}}}_{\mathsf{pdep}-1}$
as public output. We run our pattern generation algorithm on this platform
with varying values of $\mathsf{pdep}$ and corresponding grammar depths
$\mathsf{gdep}\in\\{\mathsf{pdep},\mathsf{pdep}+1,\mathsf{pdep}+2\\}$.

Fig. 12(d) presents the results. We observe that for the case where
$\mathsf{gdep}=\mathsf{pdep}$, we generate only one pattern with skeleton
$\mathsf{op}_{1}\cdot\mathsf{op}_{2}\cdots\mathsf{op}_{\mathsf{pdep}}$ and
constraint $\land_{i}\mathsf{datadep}(\mathsf{op}_{i},\mathsf{op}_{i+1})$
signifying data propagation through these operations. Higher grammar depths,
however, require multiple counterfactuals (Ex. 4), and produce more patterns.
In the $\mathsf{gdep}=\mathsf{pdep}+1$ case, we require 2 counterfactuals at a
time, while in the $\mathsf{gdep}=\mathsf{pdep}+2$ case we require 3
counterfactuals at-a-time. While this leads to a blowup in generation time as
evidenced in the figure, the times are still reasonable ($\sim$10m even in the
$\mathsf{pdep}+2$ case). Moreover we observe that in the realistic platforms
considered in previous sections, smaller depths were still able to provide us
with useful patterns.

Figure 13. (F) Pattern using default grammar (Tab. 4). (G) More precise
pattern after adding the $\mathsf{diffindex}$ predicate. Figure 14. Example
illustrating false positives with patterns.

###  7.4. RQ4: How does the choice of grammar affect false positives?

To explore this, we consider a variant of the PlatSS platform. As in the
original model (Fig. 8), a load is sourced from the LSQ cache if there exists
a valid entry with the same address. Otherwise, it is sourced from memory and
updates the LSQ cache. However, in this variant, a store invalidates all LSQ
entries with the same set index (to avoid loading stale values). We perform
pattern generation with the memory access count (lscount) as public output,
with grammar depth 3. We get Pattern F (Fig. 13) with an address dependency
between (0:Ld) and (2:Ld), (as in SpectreV1), and where the intervening store
(1:St) does not invalidate the LSQ entry (captured by $\mathsf{diffaddr}$). If
1:St invalidated the LSQ entry, 2:Ld would access the memory in all
executions, leading to no violating behaviours.

This pattern flags the code in Fig. 14 due to a match on instructions Ld0,
St0, Ld1. However, we note that while the address of the store in Fig. 14 is
different from the first load, the set index can be the same. This is because
the set index is a slice (sub-word) of the address. Thus, under the condition
that $\texttt{K}>\texttt{SET\\_W}+2$, the store will be in the same set as the
first load, and the LSQ entry will be invalidated. Consequently, under this
condition, the program is actually safe, and Pattern F produces a false
positive.

To address this, we can add a new predicate $\mathsf{diffindex}$ to the
grammar that checks if the set indices (defined as an address slice) of two
addresses are different. Performing generation with this augmented grammar, we
obtain Pattern G (Fig. 13). This pattern only flags test_K if
$\texttt{K}\leq\texttt{SET\\_W}+2$, and is hence more precise. We summarize
these observations in Tab. 6. Thus, grammars over (high-level) architectural
state result in patterns with more false positives. Through the grammar, we
expose a precision-complexity tradeoff - more precise patterns can be
generated at the cost of a carefully tailored, microarchitecture-specific
grammar.

Check | Result with test_K (Fig. 14) and SET_W set index
---|---
$\texttt{K}>\texttt{SET\\_W}+2$ | $\texttt{K}\leq\texttt{SET\\_W}+2$
Hyperproperty | SAFE | UNSAFE
Pat. F (Fig. 13) | UNSAFE | UNSAFE
Pat. G (Fig. 13) | SAFE | UNSAFE

Table 6. Precision of patterns on test_K (Fig. 14).

##  8\. Discussion and Limitations

#### Applicability and Scope

We have applied pattern generation to speculative (e.g., §7.1, Fig. 9) and
non-speculative (e.g., §7.3, Fig. 13) execution, and multiple side channels
(§6.2.1, §6.2.2). Crucially, this is possible due to the power of non-
interference-based specifications: they can express varied attacker scenarios
(e.g., secure-programming, constant-time (Guarnieri et al., 2021; Cauligi et
al., 2020)) and platform semantics. While our approach is general, it requires
formulating non-interference specifications that accurately captures the
threat model. This requires care and expertise. The effort in writing these
specifications can be amortized over many different patterns generated and
corresponding verification and exploit-finding tasks.

#### Platform complexity

In §7 we considered abstract platform models (introduced in §6) that are
similar to those adopted in $\mathrm{SH}$ approaches (e.g., (Cheang et al.,
2019; Guarnieri et al., 2020; Zeng et al., 2022)). These models, while
exposing security relevant microarchitectural detail, are simpler than full
processor RTL. While the latter being more complex will likely result in
larger generation times, this is not a fundamental limitation of our approach.
Our main requirement is that the platform model be amenable to symbolic
analysis. This can be performed on RTL using off-the-shelf model checkers
(e.g., JasperGold, SymbiYosys (Claire Wolf, et. al., 2022)). Additionally,
there is work that extracts abstract models from RTL ((Zeng et al., 2022;
Godbole et al., 2024)).

#### Pattern Grammar and False Positives

While patterns using architecture level predicates are more
robust/microarchitecture-independent, they lead to more false positives. As
demonstrated in §7.4, using specialized grammars that expose
microarchitectural execution details (e.g., cache-indexing,
replacement/prediction policies) helps reduce false positives. However, this
is at the cost of (a) less performant analysis (it is abstraction that makes
pattern-based approaches scale) and (b) more microarchitecture-dependent
patterns. Opinion in literature is divided on whether or not to expose
microarchitectural detail to software analyses (e.g., (Cauligi et al., 2022)).
We view the grammar as a tradeoff: a generic grammar leads to abstract and
thus efficient analysis at the cost of more false positives, while a
specialized grammar is more precise at the cost of being more
microarchitecture-specific. While our current approach requires a user-
specified grammar (Fig. 6), future work could automate this, e.g., by using
counter-example guided predicate discovery (Das and Dill, 2002; Ball et al.,
2001).

##  9\. Related Work

#### Microarchitectural optimizations and vulnerabilities

Our work targets hardware execution vulnerabilities, from Spectre and Meltdown
and their variants (Kocher et al., 2019; Lipp et al., 2018; Schwarz et al.,
2019b; Koruyeh et al., 2024) to more recent attacks (e.g., targeting
store/line-fill buffers (Canella et al., 2019b; van Schaik et al., 2019;
Schwarz et al., 2019a; Maisuradze and Rossow, 2018)). Good overviews of these
vulnerabilities may be found in (Hu et al., 2021; Ge et al., 2018; Canella et
al., 2019a). These vulnerabilities are possible because of microarchitectural
optimizations such as instruction reuse (Sodani and Sohi, 1997) and silent
stores (Lepak et al., 2001; Lepak and Lipasti, 2000b) which we have used in
our experiments. Attacks exploiting these mechanisms were hypothesized in
(Sanchez Vicarte et al., 2021) amongst which some have recently been
demonstrated on actual hardware (e.g., (Moghimi, 2023)).

#### Software Analysis

Several approaches perform software analysis, adopting different
specifications, models, and techniques.

Semantic hyperproperty-based verification. Semantic hyperproperty-based
approaches (e.g., (Cheang et al., 2019; Guarnieri et al., 2020; Guanciale et
al., 2020; Fabian et al., 2022)) formulate security as a hyperproperty
(Terauchi and Aiken, 2005; Clarkson and Schneider, 2008; Rushby, 1992; Kozyri
et al., 2022) over executions of the program on an abstract platform model.
These serve as inputs to our approach.

Symbolic software analysis. While the earlier works develop high-level
hyperproperties that capture varied microarchitectural mechanisms, other
approaches adopt more specific security models (e.g., constant-time
execution). This allows them to develop specialized and more efficient
analysis techniques (see (Geimer et al., 2023) for a systematic evaluation and
comparison), based on symbolic execution (SE) (King, 1976; Wang et al., 2020;
Guo et al., 2019; David et al., 2016) or relational symbolic execution (RelSE)
(Farina et al., 2019; Daniel et al., 2023, 2021). Our work is orthogonal to
these: (a) our main goal is pattern generation, not binary analysis and (b) we
are not limited to a specific (e.g., constant-time) leakage model.

Pattern-based detection. Previous work performing pattern-based detection
(e.g., (Mosier et al., 2022; Ponce-de Leon and Kinder, 2022; Trippel et al.,
2019)) manually defines patterns. We develop an approach to systematically
generate patterns that are complete (up to a skeleton size), thus
complementing these approaches.

#### Microarchitectural verification/abstraction

The patterns that we generate can be thought of as software-side abstractions
extracted based on our semantic platform analysis.

Contract-based abstractions. Approaches (e.g., (Guarnieri et al., 2021; Wang
et al., 2023)) develop security contracts at the hardware/software interface.
By proving that (a) the hardware refines the contract and (b) software
satisfies the contract, these approaches guarantee software security. While
the contract can also be viewed as a hardware/software abstraction, it is of a
different nature than the patterns we generate.

Security verification/side-channel analysis. Several approaches directly
verify hardware RTL w.r.t. security properties either formally (using symbolic
techniques) (Fadiheh et al., 2018; von Gleissenthall et al., 2019; v.
Gleissenthall et al., 2021) or using faster but incomplete techniques (e.g.,
fuzzing) (Nilizadeh et al., 2018; Noller and Tizpaz-Niari, 2021; Oleksenko et
al., 2022; Tyagi et al., 2022). Finally, there are approaches that perform
automated extraction/validation of side-channels with white/black box designs
(Oleksenko et al., 2023; Nemati et al., 2020; Gras et al., 2020; Weber et al.,
2021). While this too can be seen as extracting security relevant hardware
abstractions, it needs to be paired with software analysis techniques to be
useful for software security verification.

##  10\. Conclusion

In this work, we presented an approach to convert a given platform model and
non-interference-based security hyperproperty into a set of attack patterns.
Our automatic generation approach improves on manual pattern creation (which
can result in missed patterns) by guaranteeing that the generated patterns
capture all non-interference violations up to a certain size. We implemented
our approach in a prototype tool. Our evaluation resulted in the
identification of, to our knowledge, previously unknown patterns for Spectre
BCB and Spectre STL, and other vulnerability variants. We also demonstrated
improved verification performance using generated patterns as compared to the
original hyperproperty. By providing a systematic way to generate patterns,
our work combines the best of both worlds: formal guarantees of hyperproperty-
based specification and scalability of pattern-based verification.

## References

  * (1)
  * Alglave et al. (2014) Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014\.  Herding cats: modelling, simulation, testing, and data-mining for weak memory.  _Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (2014).
  * Alur et al. (2013) Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013.  Syntax-guided synthesis. In _2013 Formal Methods in Computer-Aided Design_. IEEE, 1–8.  https://doi.org/10.1109/fmcad.2013.6679385
  * Ball et al. (2001) Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani. 2001.  Automatic predicate abstraction of C programs. In _Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation_ (Snowbird, Utah, USA) _(PLDI ’01)_. Association for Computing Machinery, New York, NY, USA, 203–213.  https://doi.org/10.1145/378795.378846
  * Barbosa et al. (2022) Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022\.  cvc5: A Versatile and Industrial-Strength SMT Solver. In _TACAS_.
  * Barrett et al. (2016) Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2016\.  The Satisfiability Modulo Theories Library (SMT-LIB).  www.SMT-LIB.org.
  * Barrett et al. (2009) Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2009.  Satisfiability Modulo Theories. In _Handbook of Satisfiability_.
  * Canella et al. (2019a) Claudio Canella, Jo Van Bulck, Michael Schwarz, Moritz Lipp, Benjamin von Berg, Philipp Ortner, Frank Piessens, Dmitry Evtyushkin, and Daniel Gruss. 2019a.  A Systematic Evaluation of Transient Execution Attacks and Defenses.  (Aug. 2019), 249–266.  https://www.usenix.org/conference/usenixsecurity19/presentation/canella
  * Canella et al. (2019b) Claudio Canella, Daniel Genkin, Lukas Giner, Daniel Gruss, Moritz Lipp, Marina Minkin, Daniel Moghimi, Frank Piessens, Michael Schwarz, Berk Sunar, Jo Van Bulck, and Yuval Yarom. 2019b.  Fallout: Leaking Data on Meltdown-resistant CPUs.  _Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security_ (2019).
  * Cauligi et al. (2020) Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe. 2020.  Constant-time foundations for the new spectre era. In _Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation_ _(PLDI ’20)_. ACM.  https://doi.org/10.1145/3385412.3385970
  * Cauligi et al. (2022) Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, and Deian Stefan. 2022\.  SoK: Practical Foundations for Software Spectre Defenses. In _2022 IEEE Symposium on Security and Privacy (SP)_. IEEE, 666–680.  https://doi.org/10.1109/sp46214.2022.9833707
  * Charles et al. (2002) Desiree Charles, Ali R. Hurson, and Narayanan Vijaykrishnan. 2002\.  Improving ILP with instruction-reuse cache hierarchy.  _Fifth International Conference on Algorithms and Architectures for Parallel Processing, 2002. Proceedings._ (2002), 206–213.
  * Cheang et al. (2019) Kevin Cheang, Cameron Rasmussen, Sanjit Seshia, and Pramod Subramanyan. 2019.  A Formal Approach to Secure Speculation. In _2019 IEEE 32nd Computer Security Foundations Symposium (CSF)_. IEEE, 288–28815.  https://doi.org/10.1109/csf.2019.00027
  * Claire Wolf, et. al. (2022) Claire Wolf, et. al. 2022\.  SymbiYosys.  https://github.com/YosysHQ/sby.
  * Clarke et al. (1994) Edmund M. Clarke, Orna Grumberg, and David E. Long. 1994\.  Model checking and abstraction.  _ACM Trans. Program. Lang. Syst._ 16, 5 (Sep. 1994), 1512–1542.  https://doi.org/10.1145/186025.186051
  * Clarkson and Schneider (2008) Michael R. Clarkson and Fred B. Schneider. 2008.  Hyperproperties.  _2008 21st IEEE Computer Security Foundations Symposium_ (2008), 51–65.
  * Daniel et al. (2021) Lesly-Ann Daniel, Sébastien Bardin, and Tamara Rezk. 2021\.  Hunting the Haunter - Efficient Relational Symbolic Execution for Spectre with Haunted RelSE.  _Proceedings 2021 Network and Distributed System Security Symposium_ (2021).  https://api.semanticscholar.org/CorpusID:231878700
  * Daniel et al. (2023) Lesly-Ann Daniel, Sébastien Bardin, and Tamara Rezk. 2023\.  Binsec/Rel: Symbolic Binary Analyzer for Security with Applications to Constant-Time and Secret-Erasure.  _ACM Trans. Priv. Secur._ 26, 2, Article 11 (Apr 2023), 42 pages.  https://doi.org/10.1145/3563037
  * Das and Dill (2002) Satyaki Das and David L. Dill. 2002.  Counter-Example Based Predicate Discovery in Predicate Abstraction. In _Formal Methods in Computer-Aided Design_ , Mark D. Aagaard and John W. O’Leary (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 19–32.  https://doi.org/10.1145/378795.378846
  * David et al. (2016) Robin David, Sébastien Bardin, Thanh Dinh Ta, Laurent Mounier, Josselin Feist, Marie-Laure Potet, and Jean-Yves Marion. 2016.  BINSEC/SE: A Dynamic Symbolic Execution Toolkit for Binary-Level Analysis.  _2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER)_ 1 (2016), 653–656.  https://api.semanticscholar.org/CorpusID:7488274
  * de Moura and Bjørner (2008) Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008.  Z3: An Efficient SMT Solver. In _International Conference on Tools and Algorithms for Construction and Analysis of Systems_.
  * Fabian et al. (2022) Xaver Fabian, Marco Guarnieri, and Marco Patrignani. 2022\.  Automatic Detection of Speculative Execution Combinations.  _Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security_ (2022).
  * Fadiheh et al. (2018) Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra, and Wolfgang Kunz. 2018\.  Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking.  _2019 Design, Automation & Test in Europe Conference & Exhibition (DATE)_ (2018), 994–999.
  * Farina et al. (2019) Gian Pietro Farina, Stephen Chong, and Marco Gaboardi. 2019\.  Relational Symbolic Execution. In _Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming_ _(PPDP ’19)_. ACM.  https://doi.org/10.1145/3354166.3354175
  * Ge et al. (2018) Qian Ge, Yuval Yarom, David A. Cock, and Gernot Heiser. 2018\.  A survey of microarchitectural timing attacks and countermeasures on contemporary hardware.  _J. Cryptogr. Eng._ 8, 1 (2018), 1–27.  https://doi.org/10.1007/S13389-016-0141-6
  * Geimer et al. (2023) Antoine Geimer, Mathéo Vergnolle, Frédéric Recoules, Lesly-Ann Daniel, Sébastien Bardin, and Clémentine Maurice. 2023\.  A Systematic Evaluation of Automated Tools for Side-Channel Vulnerabilities Detection in Cryptographic Libraries. In _Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security_ (Copenhagen, Denmark) _(CCS ’23)_. Association for Computing Machinery, New York, NY, USA, 1690–1704.  https://doi.org/10.1145/3576915.3623112
  * Godbole et al. (2024) Adwait Godbole, Kevin Cheang, Yatin A. Manerkar, and Sanjit A. Seshia. 2024.  Lifting Micro-Update Models from RTL for Formal Security Analysis. In _Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2_ (La Jolla, CA, USA) _(ASPLOS ’24)_. Association for Computing Machinery, New York, NY, USA, 631–648.  https://doi.org/10.1145/3620665.3640418
  * Goguen and Meseguer (1984) Joseph A. Goguen and José Meseguer. 1984.  Unwinding and Inference Control.  _1984 IEEE Symposium on Security and Privacy_ (1984), 75–75.
  * Gras et al. (2020) Ben Gras, Cristiano Giuffrida, Michael Kurth, Herbert Bos, and Kaveh Razavi. 2020.  ABSynthe: Automatic Blackbox Side-channel Synthesis on Commodity Microarchitectures. In _27th Annual Network and Distributed System Security Symposium, NDSS 2020, San Diego, California, USA, February 23-26, 2020_. The Internet Society.  https://www.ndss-symposium.org/ndss-paper/absynthe-automatic-blackbox-side-channel-synthesis-on-commodity-microarchitectures/
  * Guanciale et al. (2020) Roberto Guanciale, Musard Balliu, and Mads Dam. 2020.  InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis. In _Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security_ _(CCS ’20)_. ACM.  https://doi.org/10.1145/3372297.3417246
  * Guarnieri et al. (2020) Marco Guarnieri, Boris Köpf, José Francisco Morales, Jan Reineke, and Andrés Sánchez. 2020\.  Spectector: Principled Detection of Speculative Information Flows. In _2020 IEEE Symposium on Security and Privacy (SP)_. IEEE, 1–19.  https://doi.org/10.1109/sp40000.2020.00011
  * Guarnieri et al. (2021) Marco Guarnieri, Boris Köpf, Jan Reineke, and Pepe Vila. 2021\.  Hardware-Software Contracts for Secure Speculation.  _2021 IEEE Symposium on Security and Privacy (SP)_ (2021), 1868–1883.
  * Guo et al. (2019) Shengjian Guo, Yueqi Chen, Peng Li, Yueqiang Cheng, Huibo Wang, Meng Wu, and Zhiqiang Zuo. 2019.  SPECUSYM: Speculative Symbolic Execution for Cache Timing Leak Detection.  _2020 IEEE/ACM 42nd International Conference on Software Engineering (ICSE)_ (2019), 1235–1247.  https://api.semanticscholar.org/CorpusID:207869919
  * Hu et al. (2021) Guangyuan Hu, Zecheng He, and Ruby B. Lee. 2021.  SoK: Hardware Defenses Against Speculative Execution Attacks. In _2021 International Symposium on Secure and Private Execution Environment Design (SEED)_. IEEE, 108–120.  https://doi.org/10.1109/seed51797.2021.00023
  * Intel (2023) Intel. 2023.  Data Operand Independent Timing Instruction Set Architecture (ISA) Guidance.  https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/best-practices/data-operand-independent-timing-isa-guidance.html Accessed: 2023-11-23.
  * Jha and Seshia (2015) Susmit Jha and Sanjit A. Seshia. 2015.  A theory of formal synthesis via inductive learning.  _Acta Informatica_ 54 (2015), 693–726.
  * King (1976) James C. King. 1976\.  Symbolic execution and program testing.  _Commun. ACM_ 19, 7 (Jul 1976), 385–394.  https://doi.org/10.1145/360248.360252
  * Kocher (2018) Paul Kocher. 2018\.  _Spectre Mitigations in Microsoft’s C/C++ Compiler_.  https://www.paulkocher.com/doc/MicrosoftCompilerSpectreMitigation.html
  * Kocher et al. (2019) Paul C. Kocher, Daniel Genkin, Daniel Gruss, Werner Haas, Michael Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2019\.  Spectre Attacks: Exploiting Speculative Execution.  _2019 IEEE Symposium on Security and Privacy (SP)_ (2019), 1–19.
  * Koruyeh et al. (2024) Esmaeil Mohammadian Koruyeh, Khaled N. Khasawneh, Chengyu Song, and Nael Abu-Ghazaleh. 2024.  Spectre Returns! Speculation Attacks Using the Return Stack Buffer.  _IEEE Design & Test_ 41, 2, 47–55.  https://doi.org/10.1109/mdat.2024.3352537
  * Kozyri et al. (2022) Elisavet Kozyri, Stephen Chong, and Andrew C. Myers. 2022\.  Expressing Information Flow Properties.  _Found. Trends Priv. Secur._ 3 (2022), 1–102.
  * Lepak et al. (2001) Kevin M. Lepak, Gordon B. Bell, and Mikko H. Lipasti. 2001\.  Silent Stores and Store Value Locality.  _IEEE Trans. Computers_ 50 (2001), 1174–1190.
  * Lepak and Lipasti (2000a) Kevin M. Lepak and Mikko H. Lipasti. 2000a.  On the value locality of store instructions.  _Proceedings of 27th International Symposium on Computer Architecture (IEEE Cat. No.RS00201)_ (2000), 182–191.
  * Lepak and Lipasti (2000b) Kevin M. Lepak and Mikko H. Lipasti. 2000b.  Silent stores for free.  _Proceedings 33rd Annual IEEE/ACM International Symposium on Microarchitecture. MICRO-33 2000_ (2000), 22–31.
  * Lipp et al. (2018) Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul C. Kocher, Daniel Genkin, Yuval Yarom, and Michael Hamburg. 2018\.  Meltdown: Reading Kernel Memory from User Space. In _USENIX Security Symposium_.
  * Liu et al. (2015) Fangfei Liu, Yuval Yarom, Qian Ge, Gernot Heiser, and Ruby B. Lee. 2015.  Last-Level Cache Side-Channel Attacks are Practical. In _2015 IEEE Symposium on Security and Privacy_. IEEE, 605–622.  https://doi.org/10.1109/sp.2015.43
  * Lustig et al. (2016) Daniel Lustig, Geet Sethi, Margaret Martonosi, and Abhishek Bhattacharjee. 2016.  COATCheck: Verifying Memory Ordering at the Hardware-OS Interface. In _Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems_ (Atlanta, Georgia, USA) _(ASPLOS ’16)_. Association for Computing Machinery, New York, NY, USA, 233–247.  https://doi.org/10.1145/2872362.2872399
  * Maisuradze and Rossow (2018) Giorgi Maisuradze and Christian Rossow. 2018.  ret2spec: Speculative Execution Using Return Stack Buffers.  _Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security_ (2018).  https://api.semanticscholar.org/CorpusID:51804116
  * McMillan (1993) Kenneth L. McMillan. 1993\.  _Symbolic model checking_.  Kluwer.  https://doi.org/10.1007/978-1-4615-3190-6_3
  * Moghimi (2023) Daniel Moghimi. 2023\.  Downfall: Exploiting Speculative Data Gathering. In _32nd USENIX Security Symposium (USENIX Security 23)_. USENIX Association, Anaheim, CA, 7179–7193.  https://www.usenix.org/conference/usenixsecurity23/presentation/moghimi
  * Mosier et al. (2022) Nicholas Mosier, Hanna Lachnitt, Hamed Nemati, and Caroline Trippel. 2022.  Axiomatic hardware-software contracts for security. In _Proceedings of the 49th Annual International Symposium on Computer Architecture_ _(ISCA ’22)_. ACM.  https://doi.org/10.1145/3470496.3527412
  * Mutlu et al. (2005) Onur Mutlu, Hyesoon Kim, Jared Stark, and Yale N. Patt. 2005\.  On Reusing the Results of Pre-Executed Instructions in a Runahead Execution Processor.  _IEEE Computer Architecture Letters_ 4 (2005), 2–2.
  * Nemati et al. (2020) Hamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale, and Swen Jacobs. 2020\.  Validation of Abstract Side-Channel Models for Computer Architectures.  _Computer Aided Verification_ 12224 (2020), 225 – 248.  https://api.semanticscholar.org/CorpusID:211567271
  * Nilizadeh et al. (2018) Shirin Nilizadeh, Yannic Noller, and Corina S. Pasareanu. 2018\.  DifFuzz: Differential Fuzzing for Side-Channel Analysis.  _2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE)_ (2018), 176–187.
  * Noller and Tizpaz-Niari (2021) Yannic Noller and Saeid Tizpaz-Niari. 2021.  QFuzz: quantitative fuzzing for side channels.  _Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis_ (2021).
  * Oleksenko et al. (2022) Oleksii Oleksenko, Christof Fetzer, Boris Köpf, and Mark Silberstein. 2022.  Revizor: testing black-box CPUs against speculation contracts.  (Feb. 2022).  https://doi.org/10.1145/3503222.3507729
  * Oleksenko et al. (2023) Oleksii Oleksenko, Marco Guarnieri, Boris Köpf, and Mark Silberstein. 2023.  Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing. In _2023 IEEE Symposium on Security and Privacy (SP)_. IEEE.  https://doi.org/10.1109/sp46215.2023.10179391
  * Polgreen et al. (2022) Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, and Sanjit A. Seshia. 2022.  UCLID5: Multi-modal Formal Modeling, Verification, and Synthesis. In _34th International Conference on Computer Aided Verification (CAV)_ _(Lecture Notes in Computer Science, Vol. 13371)_. Springer, 538–551.
  * Ponce-de Leon and Kinder (2022) Hernán Ponce-de Leon and Johannes Kinder. 2022.  Cats vs. Spectre: An Axiomatic Approach to Modeling Speculative Execution Attacks.  (May 2022).  https://doi.org/10.1109/sp46214.2022.9833774
  * Rushby (1992) John Rushby. 1992\.  _Noninterference, Transitivity, and Channel-Control Security Policies_.  Technical Report.  http://www.csl.sri.com/papers/csl-92-2/
  * Sanchez Vicarte et al. (2021) Jose Rodrigo Sanchez Vicarte, Pradyumna Shome, Nandeeka Nayak, Caroline Trippel, Adam Morrison, David Kohlbrenner, and Christopher W. Fletcher. 2021.  Opening Pandora’s Box: A Systematic Study of New Ways Microarchitecture Can Leak Private Data. In _2021 ACM/IEEE 48th Annual International Symposium on Computer Architecture (ISCA)_. IEEE, 347–360.  https://doi.org/10.1109/isca52012.2021.00035
  * Schwarz et al. (2019a) Michael Schwarz, Moritz Lipp, Daniel Moghimi, Jo Van Bulck, Julian Stecklina, Thomas Prescher, and Daniel Gruss. 2019a.  ZombieLoad: Cross-Privilege-Boundary Data Sampling. In _Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security_ _(CCS ’19)_. ACM.  https://doi.org/10.1145/3319535.3354252
  * Schwarz et al. (2019b) Michael Schwarz, Martin Schwarzl, Moritz Lipp, and Daniel Gruss. 2019b.  NetSpectre: Read Arbitrary Memory over Network.  _ArXiv_ abs/1807.10535 (2019).
  * Sha et al. (2006) Tingting Sha, Milo M.K. Martin, and Amir Roth. 2006.  NoSQ: Store-Load Communication without a Store Queue.  _2006 39th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO’06)_ 27, 1, 285–296.  https://doi.org/10.1109/mm.2007.17
  * Sha et al. (2005) Tingting Sha, Milo M. K. Martin, and Amir Roth. 2005.  Scalable store-load forwarding via store queue index prediction.  _38th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO’05)_ (2005), 12 pp.–170.
  * Sodani and Sohi (1997) Avinash Sodani and Gurindar S. Sohi. 1997.  Dynamic Instruction Reuse.  _Conference Proceedings. The 24th Annual International Symposium on Computer Architecture_ (1997), 194–205.
  * Subramaniam and Loh (2006) Samantika Subramaniam and Gabriel Loh. 2006.  Fire-and-Forget: Load/Store Scheduling with No Store Queue at All. In _2006 39th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO’06)_. IEEE, 273–284.  https://doi.org/10.1109/micro.2006.26
  * Terauchi and Aiken (2005) Tachio Terauchi and Alex Aiken. 2005.  Secure Information Flow as a Safety Problem. In _Proceedings of the 12th International Conference on Static Analysis_ (London, UK) _(SAS’05)_. Springer-Verlag, Berlin, Heidelberg, 352–367.  https://doi.org/10.1007/11547662_24
  * Trippel et al. (2019) Caroline Trippel, Daniel Lustig, and Margaret Martonosi. 2019\.  Security Verification via Automatic Hardware-Aware Exploit Synthesis: The CheckMate Approach.  _IEEE Micro_ 39 (2019), 84–93.
  * Tyagi et al. (2022) Aakash Tyagi, Addison Crump, Ahmad-Reza Sadeghi, Garrett Persyn, Jeyavijayan Rajendran, Patrick Jauernig, and Rahul Kande. 2022\.  TheHuzz: Instruction Fuzzing of Processors Using Golden-Reference Models for Finding Software-Exploitable Vulnerabilities.  _ArXiv_ abs/2201.09941 (2022).
  * v. Gleissenthall et al. (2021) Klaus v. Gleissenthall, Rami Gökhan Kıcı, Deian Stefan, and Ranjit Jhala. 2021.  Solver-Aided Constant-Time Hardware Verification. In _Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security_ (Virtual Event, Republic of Korea) _(CCS ’21)_. Association for Computing Machinery, New York, NY, USA, 429–444.  https://doi.org/10.1145/3460120.3484810
  * van Schaik et al. (2019) Stephan van Schaik, Alyssa Milburn, Sebastian Osterlund, Pietro Frigo, Giorgi Maisuradze, Kaveh Razavi, Herbert Bos, and Cristiano Giuffrida. 2019\.  RIDL: Rogue In-Flight Data Load. In _2019 IEEE Symposium on Security and Privacy (SP)_. IEEE, 88–105.  https://doi.org/10.1109/sp.2019.00087
  * von Gleissenthall et al. (2019) Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, and Ranjit Jhala. 2019.  IODINE: Verifying Constant-Time Execution of Hardware.  _ArXiv_ abs/1910.03111 (2019).  https://api.semanticscholar.org/CorpusID:197672843
  * Wang et al. (2020) Guanhua Wang, Sudipta Chattopadhyay, Arnab Kumar Biswas, Tulika Mitra, and Abhik Roychoudhury. 2020\.  KLEESpectre: Detecting Information Leakage through Speculative Cache Attacks via Symbolic Execution.  _ACM Transactions on Software Engineering and Methodology_ 29, 3 (June 2020), 1–31.  https://doi.org/10.1145/3385897
  * Wang et al. (2023) Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, and Marco Guarnieri. 2023.  Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts. In _Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security_ (, Copenhagen, Denmark,) _(CCS ’23)_. Association for Computing Machinery, New York, NY, USA, 2128–2142.  https://doi.org/10.1145/3576915.3623192
  * Weber et al. (2021) Daniel Weber, Ahmad Ibrahim, Hamed Nemati, Michael Schwarz, and Christian Rossow. 2021.  Osiris: Automated Discovery of Microarchitectural Side Channels. In _30th USENIX Security Symposium (USENIX Security 21)_. USENIX Association, 1415–1432.  https://www.usenix.org/conference/usenixsecurity21/presentation/weber
  * Zeng et al. (2022) Yu Zeng, Aarti Gupta, and Sharad Malik. 2022.  Automatic generation of architecture-level models from RTL designs for processors and accelerators. In _Proceedings of the 2022 Conference & Exhibition on Design, Automation & Test in Europe_ (Antwerp, Belgium) _(DATE ’22)_. European Design and Automation Association, Leuven, BEL, 460–465.

##  Appendix A Appendix

We provide the complete versions of the algorithms and proofs.

###  A.1. Template Generation

####  A.1.1. GenerateTemplates Algorithm

We provide the full description of the template generation procedure in
Algorithm 2. This algorithm generates a set of pattern templates up to a
certain depth $d$ given a semantic platform definition $M$, a non-interference
property
$\mathsf{NI}(\mathrm{V}_{\mathsf{pub}},\mathrm{V}_{\mathsf{obs}},\Sigma_{\mathsf{init}})$,
and depth $d\in\mathbb{N}$.

As discussed in the main text, the algorithm iterates over all templates,
first checking if the template propagates taint from the source variables to
the observed variables, and if so, performing a semantic analysis to check
whether the template violates the non-interference property.

1

Input: Semantic platform definition $M$, non-interference property
$\mathsf{NI}(\mathrm{V}_{\mathsf{pub}},\mathrm{V}_{\mathsf{obs}},\Sigma_{\mathsf{init}})$,
depth $d\in\mathbb{N}$

Output: A set of pattern templates

Data: acc: the accumulated set of pattern templates

2

3Function  _TemplateHelper(_$w$_)_:

/* Search depth not reached? */

4 if  _$|w| <d$_ then

5 for  _$\mathsf{op}\in\mathsf{Op}$_ do

6 if  _$\mathsf{op}\cdot w$ propagates taint from
$\mathrm{V}_{\mathsf{pub}}^{C}$ to $\mathrm{V}_{\mathsf{obs}}$_ then

7 if  _$\mathsf{op}\cdot w\not\models\mathsf{NI}$_ then
acc.append($\mathsf{op}\cdot w$)

8

9 TemplateHelper(_$\mathsf{op}\cdot w$_)

10

11

/* Search over depth $d$ templates */

12 TemplateHelper(_$\epsilon$_)

return acc

Algorithm 2 GenerateTemplates($M$, $\mathsf{NI}$, $d$)

Input: Semantic platform definition $M$, non-interference property
$\mathsf{NI}$, pattern template $w$, and a grammar $G$

Output: A set of patterns

Data: acc: an accumulated set of patterns

1

2Function  _ConsHelper(_$\phi,i,L$_)_:

3 if  _$i >|L|$_ then

acc.append($(w,\phi)$)

/* Exhausted all atomic predicates? */

4

5 else

$\mathsf{atom}_{0}=L[i]$; $\mathsf{atom}_{1}=L[i+1]$;
$\mathsf{atom}_{2}=L[i+2]$

/* Choose atoms to branch on */

/* Does adding $\neg\mathsf{atom}_{0}$, i.e., $(=\neg L[i])$ eliminate
violations? */

_6_ _ _ if  _
$\forall\mathsf{inst}_{1},\cdots,\mathsf{inst}_{|w|}.\leavevmode\nobreak\
\mathsf{inst}_{1}\cdots\mathsf{inst}_{|w|}\models(w,\phi\land\neg\mathsf{atom}_{0})\implies\mathsf{inst}_{1},\cdots,\mathsf{inst}_{|w|}\models\mathsf{NI}$
_

7  __ then ConsHelper(_$\phi\land L[i]$ , $i+1,L$_) /* add $L[i]$ */

/* Does adding $\neg\mathsf{atom}_{0}\land\neg\mathsf{atom}_{1}$ eliminate all
violations? */

_8_ _ _ else if  _
$\forall\mathsf{inst}_{1},\cdots,\mathsf{inst}_{|w|}.\leavevmode\nobreak\
\mathsf{inst}_{1}\cdots\mathsf{inst}_{|w|}\models(w,\phi\land\neg\mathsf{atom}_{0}\land\neg\mathsf{atom}_{1})\implies\mathsf{inst}_{1},\cdots,\mathsf{inst}_{|w|}\models\mathsf{NI}$
_

9  __ then

/* add $L[i],L[i+1]$ disjuncts (multi-counterfactual branching) */

10 ConsHelper(_$\phi\land L[i]$ , $i+2,L$_); ConsHelper(_$\phi\land L[i+1]$ ,
$i+2,L$_);

/* Does adding
$\neg\mathsf{atom}_{0}\land\neg\mathsf{atom}_{1}\land\neg\mathsf{atom}_{2}$
eliminate all violations? */

_11_ _ _ else if  _
$\forall\mathsf{inst}_{1},\cdots,\mathsf{inst}_{|w|}.\leavevmode\nobreak\
\mathsf{inst}_{1}\cdots\mathsf{inst}_{|w|}\models(w,\phi\land\neg\mathsf{atom}_{0}\land\neg\mathsf{atom}_{1}\land\neg\mathsf{atom}_{2})\implies\mathsf{inst}_{1},\cdots,\mathsf{inst}_{|w|}\models\mathsf{NI}$
_

12  __ then

/* add $L[i],L[i+1],L[i+2]$ disjuncts (multi-counterfactual branching) */

13 ConsHelper(_$\phi\land L[i]$ , $i+3,L$_); ConsHelper(_$\phi\land L[i+1]$ ,
$i+3,L$_); ConsHelper(_$\phi\land L[i+2]$ , $i+3,L$_);

14 else ConsHelper(_$\phi,i+1,L$_);

15 /* skip over $L[i]$ */

16

$L$ = ApplyPredicates($w,G$)

/* Create all atoms in $L$ */

ConsHelper(_$\texttt{true},0,L$_)

/* Counterfact. addition */

return acc

Algorithm 3 ConstraintSpecialize($M,\mathsf{NI},w,G$)

####  A.1.2. Proof of Lemma 2

The proof of Lemma 2 is a direct consequence of the algorithm
GenerateTemplates and the soundness of a taint-based overapproximation. We
rely on the fact that, if a template $w$ does not propagate taint from
$\mathrm{V}_{\mathsf{pub}}$ to $\mathrm{V}_{\mathsf{obs}}$, then it also does
not violate the non-interference property
$\mathsf{NI}(\mathrm{V}_{\mathsf{pub}},\mathrm{V}_{\mathsf{obs}},\Sigma_{\mathsf{init}})$.

###  A.2. Constraint-based Template Specialization

####  A.2.1. Counterfactual-based Addition

Counterfactual-based addition is based on Observations 1 and 2 which can be
shown through simple propositional logic. We will only prove Observation 2
since it is a generalization of Observation 1.

###### Proof of Observation 2.

Consider a partially specialized template $(w,\phi)$, and a set of atoms
$\\{f_{i}\\}_{i}$. Let $S$ be the set of programs: $S=\\{C\leavevmode\nobreak\
|\leavevmode\nobreak\ C\models(w,\phi)\\}$. Also for each $f_{i}$, let $S_{i}$
be the set of programs: $S_{i}=\\{C\leavevmode\nobreak\ |\leavevmode\nobreak\
C\models(w,\phi\land f_{i})\\}$. Finally, let $T$ be the programs:
$T=\\{C\leavevmode\nobreak\ |\leavevmode\nobreak\ C\models\mathsf{NI}\\}$.
Then, the set $U$ of programs satisfying

$C\models(w,\phi\land\bigwedge_{i}\neg f_{i})$

can we described as $U=S\setminus\bigcup_{i}S_{i}$.

Now, suppose to the contrary that the statement was not true. Then there
exists a program $C$, such that the following holds:

(2) $C\models(w,\phi)\land C\not\models\mathsf{NI}\quad\text{ i.e., }C\in
S\cap\overline{T}$

and

(3) $\neg\bigvee_{i}(C\models(w,\phi\land f_{i}))\quad\text{i.e.,
}C\not\in\bigcup_{i}S_{i}$

Then, by (3) and (4),
$C\in(S\cap\overline{T}\cap\overline{\bigcup_{i}S_{i}})$, which implies, by
the definition of $U$, that $C\in U\cap\overline{T}$. However, this means that
the antecedent of the observation (which corresponds to $\overline{U}\cup T$)
does not infact hold, which is a contradiction. ∎

####  A.2.2. Full ConstraintSpecialize Algorithm

We provide the full description of the constraint-based template
specialization procedure (Algorithm 3).

####  A.2.3. $k$-completeness of ConstraintSpecialize

Theorem 5 is proven by induction on the number of specialization iterations.

###### Proof of Theorem 5.

Suppose ConstraintSpecialize is invoked with arguments $(w,\mathsf{NI},M,G)$.
We claim that in Alg. 3, at each recursive call of $\mathsf{ConsHelper}$ with
arguments $(\phi,i,L)$, the following property holds:

$\displaystyle\forall C.\leavevmode\nobreak\ \leavevmode\nobreak\
(C\models(w,\mathsf{true})\land C\not\models\mathsf{NI})$
$\displaystyle\quad\implies\exists(w,\phi^{\prime})\in\text{acc}\cup\\{(w,\phi)\\}.\leavevmode\nobreak\
C\models(w,\phi^{\prime})$

In words, the partially specialized patterns maintained in the accumulator
queue form an overapproxiation of the violating programs for skeleton $w$.

Base case: At the start, $\mathsf{ConsHelper}(\mathsf{true},0,L)$ immediately
implies the property.

Inductive step: Let the property hold for $\mathsf{ConsHelper}(\phi,i,L)$.
Then, either we (a) add $(w,\phi)$ to acc, (b) we skip over $L[i]$ or (c)
reinvoke $\mathsf{ConsHelper}$ with an incremented $i$. The property holds
immediately in cases (a) and (c). In case (b), we note that the set of
programs $C$ that satisfying $(w,\phi)$ and violating $\mathsf{NI}$ is
identical to those that violate $(w,\phi\land L[i])$ due to Observation 1. A
similar argument holds for the multi-counterfactual case (using Obs. 2).

Therefore, by induction, the property holds for all recursive calls of
$\mathsf{ConsHelper}$, and hence, the final set of patterns in acc (when there
are no more calls to $\mathsf{ConsHelper}$) is a $k$-complete set of patterns
for $w$. ∎