0% found this document useful (0 votes)
11 views14 pages

Attack Graph Model for Speculative Execution

Uploaded by

a18257157319
Copyright
© All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
0% found this document useful (0 votes)
11 views14 pages

Attack Graph Model for Speculative Execution

Uploaded by

a18257157319
Copyright
© All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd

2021 IEEE International Symposium on High-Performance Computer Architecture (HPCA)

New Models for Understanding and Reasoning


about Speculative Execution Attacks
Zecheng He Guangyuan Hu Ruby Lee
Princeton University Princeton University Princeton University
zechengh@[Link] gh9@[Link] rblee@[Link]

Abstract—Spectre and Meltdown attacks and their variants example, Spectre breaches the memory isolation provided
exploit hardware performance optimization features to cause within a user application, while Meltdown breaches the
security breaches. Secret information is accessed and leaked memory isolation between the kernel and a user application.
through covert or side channels. New attack variants keep
appearing and we do not have a systematic way to capture the Foreshadow breaches the isolation of Intel SGX secure enclaves.
critical characteristics of these attacks and evaluate why they Foreshadow-OS and Foreshadow-VMM breach the isolation
succeed or fail. provided by the Operating System and the Virtual Machine
In this paper, we provide a new attack-graph model for rea- Monitor, respectively. All of these attacks leverage the specu-
soning about speculative execution attacks. We model attacks as lative execution feature of modern processors, transferring
ordered dependency graphs, and prove that a race condition be-
tween two nodes can occur if there is a missing dependency edge the security-critical information to micro-architecture state
between them. We define a new concept, “security dependency”, observable by an unprivileged attacker through a covert channel.
between a resource access and its prior authorization operation. Unfortunately, while new attack variants are continuously being
We show that a missing security dependency is equivalent to a discovered, we do not have a systematic way to characterize
race condition between authorization and access, which is a root these attacks and reason about them. The attack graph model
cause of speculative execution attacks. We show detailed examples
of how our attack graph models the Spectre and Meltdown we propose serves this goal.
attacks, and is generalizable to all the attack variants published While both industrial and academic solutions have been
so far. This attack model is also very useful for identifying proposed to defend against speculative execution attacks [10],
new attacks and for generalizing defense strategies. We identify [17], [22], [23], [25], [28], [30], [32]–[34], [37], [42], [44],
several defense strategies with different performance-security [46], there is currently no systematic way to show if these
tradeoffs. We show that the defenses proposed so far all fit under
one of our defense strategies. We also explain how attack graphs defenses can defeat speculative attacks, and why. We show that
can be constructed and point to this as promising future work our attack graph model can explain why a defense will work.
for tool designers. The key questions answered in this paper are: x How can
Index Terms—Hardware security, speculative execution at- we systematically model the essential common characteristics
tacks, graph model, security dependency, cache, side channel, of speculative execution attacks and reason about them? y
covert channel, delayed exceptions, prediction, race condition
What defense strategies can be derived from the new models?
z Are the recently proposed defenses effective against these
I. I NTRODUCTION
speculative attacks?
In computer systems, hardware resources like memory, buses, Our key contributions in this paper are:
caches and functional units are often shared among different • We define a new attack graph model to systematically
processes and threads. This sharing increases the utilization capture the critical operations in speculative execution
of resources. However, preventing a secret from being leaked attacks.
via shared resources is a fundamental and challenging security • We theoretically prove that a missing edge in an attack
problem. graph is equivalent to a race condition, which is one of
Memory isolation plays a key role in preventing information the root causes of speculative attacks.
leakage. An application should not be able to read the memory • We define the new concept of “security dependencies”,
of the kernel or another application. Memory isolation is usually which must be observed by the hardware in addition to
enforced by the operating system, to allow multiple applications data dependencies and control dependencies. We show that
to run simultaneously on the shared hardware resources without a missing security dependency is equivalent to a missing
information leakage. It is also enforced by the Virtual Machine edge in an attack graph, capable of causing a security
Monitor to provide isolation between different virtual machines. breach.
Recently, speculative execution attacks, e.g., Spectre [25], • Our model shows that although attacks may look similar,
Meltdown [29], Foreshadow [38], Foreshadow-NG [43] and e.g. the Spectre-type and Meltdown-type attacks, they are
Lazy-FP [36] attacks and their variants are proposed to breach actually quite different in the sense that Meltdown-type
the memory isolation by using a covert channel to exfiltrate attacks have to be investigated through intra-instruction
a secret obtained illegally under speculative execution. For micro-architectural dependencies, while Spectre-type at-

2378-203X/21/$31.00 ©2021 IEEE 40


DOI 10.1109/HPCA51647.2021.00014
tacks only need to consider inter-instruction dependencies. TABLE I: Speculative attacks and their variants.
This can simplify tool development for finding attack Attack CVE Impact
Boundary check by-
graphs and vulnerabilities that can be exploited in attacks. Spectre v1 [25] CVE-2017-5753
pass
• We derive new defense strategies from our attack graph Speculative buffer
Spectre v1.1 [24] CVE-2018-3693
model. These enable us to systematically explain why overflow
Overwrite read-only
a defense will or will not work. We also show that Spectre v1.2 [24] N/A
memory
all currently proposed defenses, from both industry and Spectre v2 [25] CVE-2017-5715
Branch target injec-
academia, can be modelled by our defense strategies. tion
Kernel content leak-
• We show the benefits of our new model for future research Meltdown (Spectre v3)
CVE-2017-5754 age to unprivileged
[29]
for tool creation, discovering new attacks and finding new attacker
defenses. System register
Meltdown variant1 value leakage
CVE-2018-3640
(Spectre v3a) [2] to unprivileged
II. BACKGROUND attacker
Speculative store
A. Speculative Attacks Spectre v4 [3] CVE-2018-3639 bypass, read stale
Speculative execution vulnerabilities affect most modern data in memory
Return mis-predict,
processors. They exploit speculative execution, Out-of-Order Spectre RSB [26] CVE-2018-15572
execute wrong code
(OOO) execution, hardware prediction and caching – all Foreshadow (L1 Termi-
CVE-2018-3615
SGX enclave mem-
essential features for speeding up program execution. They nal Fault) [38] ory leakage
Foreshadow-OS [43] CVE-2018-3620 OS memory leakage
allow an unprivileged adversary to bypass the user-kernel VMM memory leak-
Foreshadow-VMM [43] CVE-2018-3646
isolation or user-defined boundaries. In a speculative execution age
attack, a speculation window is induced to allow transient Lazy FP [36] CVE-2018-3665 Leak of FPU state
Virtual-to-physical
instructions that illegally access a secret, then perform some Spoiler [21] CVE-2019-0162 address mapping
micro-architectural state changes which essentially “send leakage
out the secret” so that it can be observed by the attacker.
Upon detecting mis-speculation, architectural state changes are TABLE II: Industrial defenses against speculative attacks.
discarded, but some micro-architectural state changes are not –
Attack Defense Strategy Defense
thus leaking the secret.
LFence
We give a top-down description of a speculative attack Spectre Serialization
MFence
in Section III and a detailed discussion of the Spectre and KAISER
Meltdown Kernel Isolation
Meltdown attacks in Section IV. We list the first 13 published Kernel Page Table Isolation (KPTI)
attacks and their impacts in Table I. Later, in Section V and Disable branch prediction
Spectre variants Indirect Branch Restricted Speculation
Table III, we also consider the newer attack variants. requiring branch Prevent mis- Single Thread Indirect Branch Predictor
prediction training of branch Indirect Branch Prediction Barrier
B. Industry Defenses Implemented (Spectre v1, v1.1, prediction Invalidate branch predictor during
v1.2, v2) context switch
Table II shows some industry defenses that have been Retpoline
implemented to mitigate some speculative attacks. Spectre boundary
Coarse masking
bypass Address masking
Fences. Fences, including LFENCE and MFENCE [1], are (v1, v1.1, v1.2)
Data-dependent masking
placed before memory operations to serialize the program Speculative Store Bypass Barrier
Serialize stores
execution and prevent speculative execution. Spectre v4
and loads
(SSBB)
Speculative Store Bypass Safe (SSBS)
Kernel Isolation. KAISER (Kernel Address Isolation to have
Prevent RSB
Side-channels Efficiently Removed) and its Linux implementa- Spectre RSB RSB stuffing
underfill
tion named Kernel Page Table Isolation (KPTI) isolate user-
space memory from kernel space to prevent Meltdown attacks,
by unmapping kernel pages from user-space [4]. Address Masking. To address the problem of software-defined
Prevent Mis-training. As many Spectre variants (v1, v1.1, boundary bypass, the V8 JavaScript engine and the Linux kernel
v1.2, v2) leverage the mis-training of the branch predictors, implement software address masking by forcing the accessed
Intel, AMD and ARM have proposed defenses to prevent mis- memory to be within the legal range [24].
training, e.g., Indirect Branch Restricted Speculation (IBRS), Industrial Defenses against Other Specific Variants. ARM
Single Thread Indirect Branch Prediction (STIBP) and Indirect implemented Speculative Store Bypass Barrier (SSBB) and
Branch Predictor Barrier (IBPB). Some AMD CPUs allow proposed Speculative Store Bypass Safe (SSBS) to avoid
invalidating branch predictor and Branch Target Buffer (BTB) speculative store bypass. Intel implemented Return Stack Buffer
on context switches [5]. (RSB) stuffing, e.g., inserting interrupts to increase call depth,
Retpoline. Retpoline is a method where indirect branches, to defend against the Spectre-RSB attack. Intel also announced
which use potentially poisoned BTBs, are replaced by return a silicon-based solution, i.e., the next-generation Cascade Lake
instructions that use the return stack. processor [6].

41
Academia defenses. Recent defenses against speculative instruction at the head of the ROB and the youngest at the
attacks have also been proposed in academia, e.g., Context- tail. Once an instruction’s data dependencies are resolved, the
sensitive fencing [37], Secure automatic bounds checking [30], instruction can be executed. It is not committed (i.e., retired)
SpectreGuard [17], NDA [42], ConTExT [34], Specshield until it reaches the head of the ROB, i.e., instructions are
[10], STT [46], DAWG [23], InvisiSpec [44], Safespec [22], retired in program order. This out-of-order execution speeds
Conditional Speculation [28], Efficient invisible speculative up instruction processing.
execution [33] and CleanupSpec [32]. We discuss and model Speculative execution is a performance optimization feature
them in Section V. that occurs when the hardware micro-architecture predicts
that a certain execution path will be taken on a conditional
C. Cache Timing Channels
branch, or that an instruction will not cause an exception. If the
A speculative attack usually includes a covert or side channel prediction is correct (which is most of the time), performance
attack to leak out the sensitive secret, and a cache covert- is improved. However, if the prediction is wrong, then the
channel is typically used. Hence, we need to understand how hardware rolls back the architecturally-visible state to where it
cache covert channels work. Cache timing channels can be was before the speculation window started. The speculatively
classified, based on “hit” or “miss”, “access” or “operation”. executed instructions appear as if they were never executed, i.e.,
The access-based attacks leverage the difference in timing the mis-predicted instructions are aborted or squashed. While
between a hit and a miss to indicate whether a specific cacheline processors implement speculation correctly as defined, the
is present or absent in the cache, based on a single memory micro-architectural state is not always rolled back completely,
access. The operation based attacks leverage the time difference as this is not supposed to be an architecturally-visible state. In
for a whole operation, e.g., an encryption operation, which particular, caches are considered micro-architecture, and are
depends on the cache hits or misses encountered during the not rolled back.
execution of the operation. Although the exact workflow of a speculative execution
Hit and access based channel, e.g., Flush-reload channel attack may vary, on a high-level, they consist of two parts:
[45]. The initial state of the cacheline is set to absent by a (A) Secret Access: A micro-architectural feature transiently
clflush instruction. Then, if the insider-sender does not use enables the illegal access of a piece of sensitive data.
the shared cacheline, the check by the attacker-receiver after (B) Secret Send or Covert Channel: The sensitive data is
waiting a while, will still find the cacheline absent (indicated transformed into micro-architectural state that can be
by a slow cache miss). If the insider-sender does use the observed by an attacker.
cacheline, then the attacker-receiver will find the cacheline Definition 1: an illegal access is a data or code access that is
present (indicated by a fast cache hit). performed before the required authorization is completed that
Miss and access based channel, e.g., Prime-probe channel indicates that the access is allowed. The required authorization
[19]. The attacker first loads his own data to fill the cache. After is the operation checking if the performer is allowed to access
waiting for the insider-sender to do something, the attacker the data, or execute the code. Authorization can be in different
checks if the cachelines are now absent, i.e., a slow cache miss, forms, e.g., a hardware privilege level check, a software array
because the insider-sender has evicted the attacker’s cachelines. bounds check or a store-load address dependency check.
There are also hit and operation based channels, e.g., cache Since our definition of “authorization” is broader than the
collision channel [11], and miss and operation based channels, standard user-supervisor-hypervisor access checking, we give
e.g., Evict-time channel [31]. examples to illustrate. In the Meltdown attack, the attacker
The Flush-Reload attack is faster and less noisy than the tries to read a memory line before the hardware page-privilege
other cache covert channel attacks. They are used as the default check that indicates the performer of the memory access has
covert channels in most speculative attacks. They do require kernel privilege. In the Spectre v1 attack, the illegal access
the sender and receiver to have some shared memory. is reading out-of-bounds memory at the user level. The array
In the rest of the paper, without loss of generality, we also bounds check (authorization) is the condition checking in a
assume that the Flush-Reload cache covert channel is used in conditional branch instruction. Although the memory access is
the speculative attacks. Our models can also apply to the prime- within the legal program address space, we call it an illegal
probe channel, and other non-cache-based covert channels, with access because the software-enforced array bounds checking
minor changes. has not been completed. In the Spectre v4 attack (store-load
dependency), we call the load operation an illegal access if it
III. OVERVIEW OF S PECULATIVE ATTACKS reads stale data before the authorization completes that says
In speculative attacks, the micro-architectural feature at- the load address is not the same as the address of a previous
tacked is speculative execution, in concert with out-of-order store operation that is still sitting in the store buffer and its
(OoO) execution. Out-of-order execution allows instructions contents have not been written back to the cache.
to be executed once their data operands are ready, i.e., when To defend against speculative attacks, one must prevent
their data dependencies are resolved. This does not need to either part A (Secret Access) or part B (Secret Send or Covert
be in sequential program order. When an instruction is issued, Channel). By preventing A, the access to secrets, there are
it is placed into a Re-Order Buffer (ROB), with the oldest no secrets to leak through any covert or side channel. By

42
preventing B, any secrets present cannot be exfiltrated, nor we show that our attack graph models can be extended to all
can secrets obtained through means other than speculation, be attack variants.
leaked. However, there can be many types of covert channels,
A. Example: Spectre v1 Attack
and stopping all of them is not possible. Although computer
architecture papers have focused on preventing cache covert Spectre attacks exploit the transient instructions which
channels, we believe this is only a near-term solution, since can execute during a speculative execution window. On a
the attacker can easily find other covert channels to leak the mis-speculation, the transient instructions are aborted and all
secret information. We do not want to exclude these other covert architectural-level side effects are rolled back. However, not
channels. Hence, in this paper, we focus on modeling the illegal all micro-architectural state changes are rolled back.
access to secrets through speculative execution, and having our Listing 1 shows an example of the Spectre v1 attack,
attack model capable of modeling any covert channel. bypassing the array bounds checking, thus reading arbitrary
Parts A and B can be broken down into the following content that is not allowed, then sending the transformed secret
finer-grained attack steps that are critical to the success of out using a Flush-Reload cache side-channel.
a speculation attack. There are 5 steps for an actual attack, and 1 // Establish channel by flushing shared Array_A accessible to
6 if we count step (0) where the attacker finds the location attacker
of the desired secret. This is usually done earlier, before the 2 int T[256]
3 char Array_A[256*4K]
actual speculative attack. 4 clflush (Array_A)
• (Step 0): Know where the secret is. 5

• Step 1 (Setup): Receiver (a) establishes a micro- 6 // Train the branch predictor to predict not taken
7 train_branch_predictor ()
architectural covert-channel, e.g., by flushing out cache- 8
lines, and (b) sets up for illegal access, e.g., by mis-training 9 mov rbx, Array_A
the branch predictor. 10 mov rcx, Array_Victim
11 mov rdx, Secret_Location in Array_Victim
• Step 2 (Authorization): The instruction performing the 12
authorization for the subsequent memory or register access 13 // if (x < Array_Victim_Size)
is delayed, thus triggering the start of a speculative 14 // y = Array_A[Array_Victim[x] * 256];
15
execution window. If the authorization turns out to be 16 // rdx stores the queried index x and if x >
negative, then the instructions executed speculatively are 17 // Victim_Array_Size, the branch should be taken
called transient instructions since they are squashed. If 18 cmp rdx, Array_Victim_Size // Authorization
19 ja .BRANCH_TAKEN
authorization turns out to be positive, then the instructions 20 // Speculative Execution window starts
executed speculatively are committed. 21

• Step 3 (Secret Access): Sender (illegally) accesses the 22 // Illegal memory access of Secret_Location
23 mov al, byte [Array_Victim + rdx] // Access
secret. 24
• Step 4 (Use Secret and Send Secret): Sender transforms 25 shl rax , 0xc // Use
the secret into a micro-architectural state that survives 26 mov rbx, qword [rbx + rax] // Send
27
mis-speculation. 28 .BRANCH_TAKEN: ...
• Step 5 (Receive Secret): Receiver retrieves micro- 29

architecture state (the transformed secret) through the 30 // Reload Array_A to recover the secret byte
31 for ( i=0; i<256; i++){
covert-channel. 32 T[i ] = measure_access_time(Array_A + i * 4KB)
Steps 0, 1(b), 2 and 3 form part A. Steps 1(a), 4 and 5 form 33 }
part B. 34 recovered_byte = argmin_i(T[i ]) . // Receive

Listing 1: Code snippet of the Spectre v1 attack to bypass


IV. ATTACK G RAPH AND S ECURITY D EPENDENCY
array bounds checking, using the Flush-Reload channel.
We now look at specific speculative execution attacks, and
model the flow of relevant operations that occur, to help reason Suppose the target victim’s secret is located at
about the attacks, and identify the root causes of their success. Secret_Location. Lines 1-4 prepare the Flush-Reload
In Section IV-A, we model the Spectre v1 attack as a flow side channel by flushing the cachelines of Array_A, which
graph, and confirm that it follows the five steps we identified is accessible to the attacker and the victim. In line 7, the
in Section III. This motivates us to define an attack graph in attacker trains the branch predictor to always predict not
Section IV-B, as a topological sort graph (TSG), which enables taken. Lines 9 and 10 put the base address of shared Array_A
us to formally prove necessary and sufficient conditions for a and private Array_Victim into registers. Line 11 sets rdx
race condition to occur, which we identify as a root cause of such that Array_Victim[rdx] points to Secret_Location. Note
the success of speculative attacks. In Section IV-C, we propose that Array_Victim itself may not have sensitive data, but rdx
the concept of security dependency , and equate this with exceeds the length of Array_Victim_Size and refers to the
inserting a missing edge between two operations in the attack secret.
graph that will defeat the attack. In Section IV-D, we model Lines 13-14 show the high-level C code of the assembly
the Meltdown attack with an attack graph, and in Section IV-E, code in lines 16-26. This is the crux of the Spectre v1 attack.

43
Line 18 is an array bounds checking, where rdx is compared to can be outside the software-defined boundary. Thus it is an
Array_Victim_Size. However, if getting Array_Victim_Size is unauthorized or illegal memory access.
delayed, e.g., not in the cache, the branch predictor will predict The race condition is due to a missing security dependency.
the branch in line 19 as not taken because the attacker has The race condition is because of a missing security dependency
mistrained the predictor in line 7. Line 23 illegally reads the (formally defined in Section IV-C) between branch resolution
secret into the low-order byte of register rax. Line 25 transforms and “Load S”. It is neither a data dependency nor a control
the secret into an index of Array_A (where each value of secret dependency, but a new dependency to decide when an operation
refers to a new page, to avoid unwanted prefetching). Line can be executed. This missing security dependency was first
26 exfiltrates the secret by accessing an entry at Array_A pointed out by Lee [27] as the root cause of speculative
indexed by the secret, thus changing the state of the cacheline execution attacks, since the “No Access without Authorization”
from absent to present for the Flush-Reload attack. When security principle is violated.
Array_Victim_Size finally arrives and the comparison is done,
the processor realizes the mis-prediction in line 19, and discards B. Attack Graph and Races
the values in rax and rbx. However, the cache state is not rolled
back, and the attacker can obtain the secret by checking which We define an Attack Graph to extend and formalize the
entry of Array_A has been fetched (lines 30-34), since this connection between a race condition and a missing dependency.
entry gives a cache hit. We define an attack graph as a Topological Sort Graph (TSG), a
directed acyclic graph with edges between vertices representing
We model the Spectre v1 attack in Figure 1. This is the first
orderings.
example of an Attack Graph. Here, the nodes are instructions
and the links are data or control dependencies. The dotted A vertex in a TSG represents an operation, e.g., accessing
arrows represent the speculative execution path. a memory line, flushing a cacheline or comparing a memory
Figure 1 follows the program flow in Listing 1. It also follows address to a bound. Figure 2 shows an example of a TSG.
the five steps outlined in Section III. First, the receiver sets A directed edge in the TSG represents a dependency of two
up the covert channel by flushing Array_A and mis-training vertices. If there is an edge from u to v, u happens before v.
the branch predictor, such that the branch prediction will A path is a sequence of edges that connects vertices. All paths
predict “not taken” (step 1). During the program execution, the considered in this paper are directed paths.
branch stalls as the branch condition has not been resolved (the An ordering of vertices in a TSG is an ordered list that
authorization operation, step 2). The branch predictor allows contains all vertices in the graph S = (v1 , v2 ...vn ). An ordering
the speculative load of the secret (“Load S”) to be performed of vertices in a TSG is valid, if and only if for every directed
(step 3), bypassing the program-defined authorization. After the edge (vi , v j ) from vertex vi to vertex v j , vi comes before v j in
secret is obtained, the sender exfiltrates it by fetching a secret- the ordering. For example, in Figure 2, S = [A, B,C, D, E, F, G]
related entry in Array_A (step 4). Finally, the receiver retrieves and S = [A,C, E, B, D, F, G] are both valid orderings. S =
the secret by reloading entries in Array_A and measuring the [A, B, D, E,C, F, G] is not a valid ordering.
access time (step 5). A short access time indicates that the
A race condition exists between vertex u and v in a TSG if
entry in Array_A indexed by secret has been fetched into the
there exists two different valid orderings S1 and S2 such that u
cache. Some key observations and insights are:
is before v in S1 , and v is before u in S2 . Take Figure 2 as an
Speculative execution window. Once the branch stalls as example, there is a race condition between D and E, because
the condition has not been resolved, the (possibly incorrect) S = [A, B,C, D, E, F, G] and S = [A,C, E, B, D, F, G], but D is
instructions are speculatively executed in a speculative window. before E is S and D is after E in S .
The speculative window is marked by the red dashed block We prove the following theorem connecting a race condition
in Figure 1. The speculative window starts from the issue of with a missing dependency.
the first speculative (or transient) instruction until the branch Theorem 1. For any pair of vertices u and v, the two
condition ultimately resolves. If mis-predicted, the speculated vertices u and v do not have a race condition, if and only
instructions are squashed; otherwise, they are committed, if there exists a directed path that connects u and v.
improving the performance.
We provide a formal proof in Appendix A.
Speculated Operations Race with the Authorization. The Given a directed graph of operations, there are methods to
speculatively executed instructions and the branch resolution efficiently check whether there is a path between two vertices
(i.e., the authorization) are performed concurrently. In particular, [9], using depth-first search. If none exists, there is a race
whether the two memory load operations or the branch condition between these two operations.
resolution finishes first, is non-deterministic. Hence, there are To build an attack graph, all branch, memory access (load
two race conditions between “Load S” (secret access), “Load and store) and arithmetic instructions need to be included in
R” (micro-architecture state change) and “Branch resolution” the graph. Data dependencies are shown as existing edges in
(software authorization). the attack graph. Since not all operations and race conditions
The race condition allows unauthorized access. The mem- in a computation are relevant, we define four types of vertices
ory operation “Load S” in the speculative window race that must be represented in an attack graph:

44
Flush Array_A Setup must be completed before v, in order to avoid security breaches.
Mistrain predictor
Operation u is typically a security protection operation, which
we call an authorization operation in this paper. Operation v is
Conditional/Indirect Delayed
Branch Instruction Authorization typically an illegal access of data or code.
Following the “No access without Authorization” [27]
Speculative
window security principle strictly means that the authorization has to be
Load S Secret access completed before the protected data access or code execution.
This introduces a security dependency between authorization
Compute load address R
Use Secret and and data access (or code execution), which prevents the race
Send Secret condition that is the root cause of speculative attacks. Like the
Load R to Cache
well-studied data dependencies and control-flow dependencies,
Authorization which must be followed to ensure correct program execution,
Squash or
Resolved Receive Secret security dependencies must be followed to enforce the security
commit
Branch resolution: of program execution.
correct flow Reload Array_A
However, as we will show in Section V-B, some security-
performance tradeoffs can be made that still prevent attacks
Measure time from succeeding, by making sure that even if the secret is

fetched, it is prevented from being used or exfiltrated out to
Fig. 1: Spectre v1/v2 attacks. The speculative execution window an attacker-receiver.
is marked by the red dashed block. “Branch resolution” marks
the completion of the delayed authorization, initiated by the D. Modeling Meltdown Attacks
conditional or indirect branch instruction. “Load S” (secret- We show a code snippet of the Meltdown attack in Listing 2.
accessing) and “Load R” (secret-sending) are unauthorized The front and back parts of the Meltdown attack are similar to
memory accesses if they bypass “Branch resolution” (software- the Spectre v1 attack in setting up the covert channel (step 1,
defined authorization). lines 1-4), using and sending out the secret (step 4, lines 12-14)
A B and testing the covert channel (step 5, lines 16-20). The main
difference is in line 10, which accesses supervisor memory
C D
and should cause an exception. If the exception is delayed,
F
a speculative window is triggered. There is a race condition
E
between the speculative execution of lines 10, 13-14 with the
G raising of the exception in line 10.
Fig. 2: An example of Topological Sort Graph (TSG). 1 // Establish the covert channel by flushing Array_A
2 int T[256]
Authorization Operations. The victim or covert sender’s 3 char Array_A[256*4K]
authorization operations are nodes in the attack graph, represent- 4 clflush (Array_A) \\ Setup
5
ing the permission checking and other forms of authorization, 6 mov rbx, Array_A
e.g., array bounds checking by a conditional branch in the user 7 mov rcx, Security_Critical_Memory_Addr
program. 8
9 // Illegal memory access
Sender’s Secret Access Operation. The sender’s secret access 10 mov al, byte [rcx] \\ Authorize and Access
operation is a node in the attack graph, representing access 11

to the secret. For example, this is the out-of-bounds memory 12 // Speculatively execute the transient instructions
13 shl rax , 0xc \\ Use
access (Load S) in Figure 1. 14 mov rbx, qword [rbx + rax] \\ Send
Sender’s Send (Micro-architecture State Change) Oper- 15
16 // Reload Array_A to recover the security − critical byte
ation. A node where the sender manipulates the micro- 17 for ( i=0; i<256; i++){
architecture state according to the secret, e.g., the memory 18 T[i ] = measure_access_time(Array_A + i * 4KB)
access “Load R to cache” for the Flush-Reload cache covert 19 }
20 recovered_byte = argmin_i(T[i ]) \\ Receive
channel.
Receiver’s Secret Access Operation. This is a node repre- Listing 2: A code snippet of the Meltdown attack.
senting the retrieval of the secret from the micro-architecture
covert-channel. For example, it is a memory read and access Our insight is that in the Meltdown type of attacks, the
time measuring operation in a cache Flush-Reload or Prime- Authorization and the secret Access are actually the same
Probe covert channel. instruction - a memory load instruction. Hence, we need to
look within this instruction and model its micro-architectural
C. Security Dependency operations that may race with each other.
Definition 2: A security dependency of operation v on The attack graph of Meltdown in Figure 3 is similar to
operation u is an ordering of the two operations such that u that for Spectre in Figure 1, except that this time we show the

45
Setup TABLE III: Authorization and Access Nodes of Speculative
Flush Array_A
Attacks.
Delayed Attack Authorization Illegal Access
Load instruction Boundary-check Read out-of-bounds
Authorization Spectre v1 [25]
branch resolution memory
Speculative Boundary-check Write out-of-
window Spectre v1.1 [24]
branch resolution bounds memory
Read S Secret access Page read-only bit Write read-only
Spectre v1.2 [24]
check memory
Compute load address R Execute code not in-
Use Secret and Indirect branch tar-
Spectre v2 [25] tended to be exe-
Send Secret get resolution
Load R to Cache cuted
Meltdown (Spectre Kernel privilege Read from kernel
Authorization v3) [29] check memory
Resolved Load Permission Receive Secret Meltdown variant1 RDMSR instruction Read system regis-
Check
(Spectre v3a) [2] privilege check ter
Reload Array_A
Squash or Store-load address
commit Spectre v4 [3] dependency resolu- Read stale data
Load exception: Measure time tion
Squash pipe
Execute code not in-
Return target resolu-
Spectre RSB [26] tended to be exe-
tion
… cuted
Fig. 3: TSG model of the Meltdown attack. Foreshadow (L1 Read enclave data
Page permission
Terminal Fault) in L1 cache from
check
[38] outside enclave
micro-architecture operations of the load instruction in separate Foreshadow-OS Page permission Read kernel data in
[43] check cache
nodes, rather than just a single node for a conditional branch
Foreshadow-VMM Page permission Read VMM data in
instruction and a separate node for a “Load S” instruction. The [43] check cache
delayed privilege check (authorization) triggers the start of Lazy FP [36] FPU owner check
Read stale FPU
speculative execution, allowing the illegal access of the secret state
Forward data from
in the “Read S” operation. It also allows the micro-architectural RIDL [40] Load fault check fill buffer and load
change of the cacheline from absent to present in the “Load R port
to cache” instruction, which results in a hit on this cacheline, ZombieLoad [35] Load fault check
Forward data from
leaking the secret in the Flush-Reload cache covert channel. fill buffer
Forward data from
Fallout [12] Load fault check
store buffer
E. Modeling Other Attacks Forward data from
micro-architectural
Our attack graphs can be generalized to all the speculative buffers (L1D cache,
LVI [39] Load fault check
attacks, and potentially other micro-architectural security load port, store
buffer and line fill
attacks. In Table III, we summarize the authorization nodes buffer)
and illegal access nodes for all the speculative attack variants, Load data from
TSX Asynchronous
to illustrate that our attack graph model can be generalized. TAA [12]
Abort Completion
L1D cache, store or
We describe these attack variants below, including the newer load buffers
TSX Asynchronous Forward data from
attacks added at the bottom of Table III. Cacheout [41]
Abort Completion fill buffer
x The Foreshadow or “L1 terminal fault” attacks.
The Foreshadow type of attacks exploit a hardware vulner-
ability that allows the attacker, such as in Foreshadow [38] for the present bit or the reserved bit in the page table, which
or Foreshadow-NG [43], to read a secret from the L1 data can cause the address translation to abort prematurely.
cache, instead of from the memory, as in the Meltdown attack. y MDS attacks (RIDL, ZombieLoad and Fallout).
The speculative execution of an instruction accessing a virtual The newer Micro-architectural Data Sampling (MDS) attacks,
address with page table entry marked not present or the reserved e.g., Rogue In-Flight Data Load (RIDL) [40], ZombieLoad [35]
bits set, will read from L1 data cache as if the page referenced and Fallout attacks [12], leverage the hardware mechanisms
by the address bits in the PTE is still present and accessible. that allow a load that results in a fault to speculatively and
The L1 terminal fault attack can be leveraged to breach the aggressively forward stale data from micro-architectural buffers.
SGX isolation, as the speculative load bypasses the extended These attacks use different micro-architectural buffers as the
page table (EPT) protection and the secure enclave protection source for accessing the secret, shown as different attack paths
of SGX and reads secret data from the L1 cache. in Figure 4: RIDL reads a secret from a load port or line
Hence, these attacks can be modeled by the same attack fill buffer, ZombieLoad reads a secret from a line fill buffer
graph as for the Meltdown attack, but the attack flow goes and Fallout reads a secret from a store buffer. To model these
down the “Read from cache” branch in Figure 4 instead of the attacks in the attack graph, we also generalize the “permission
“Read from memory” node. The permission check is performed check” to include the check for hardware faults that may trigger

46
Flush Array_A Setup

Delayed
Load instruction Authorization

Read from Read from Read from load Read from line Read from
Memory Cache port fill buffer store buffer Secret access

① ④ Compute load address R


② Use Secret and
Speculative
③ window Send Secret
Load R to Cache

Authorization
Resolved Load Permission
Check Squash or
commit Reload Array_A

Receive Secret
Load exception:
Squash pipe Measure time

Fig. 4: Attack graph model for the Meltdown, Foreshadow and MDS attacks. The source of the secret can be from: the memory
(Meltdown), cache (Foreshadow), load port (RIDL), line fill buffer (RIDL and ZombieLoad) or store buffer (Fallout). The red
dotted lines indicate different defense strategies that can prevent the attacks from succeeding (discussed in Section V).

this illegal secret access. Flush Array_A Setup

z Special Register attacks (Spectre v3a and Lazy FP).


Another source of secrets is from the reading of special Register Access
Delayed
Authorization
registers, i.e., not the general-purpose registers, rather than
reading from the cache-memory system. We model these attacks
in Figure 5, where the illegal access is reading from these Read from
Special Register
Read from FPU Secret access
registers.
The Spectre v3a (Rogue System Register Read) attack Compute load address R
Use Secret and
can have a delayed authorization due to privilege checking Send Secret
Load R to Cache
(for supervisor privilege) taking longer than reading the
system register. The implied hardware prediction is that the Authorization
privilege checking passes, so the system register is accessed Resolved Permission
Reload Array_A
Check Squash or
speculatively. commit
In the Lazy FP attack, the floating-point registers are not (Illegal Access) Receive Secret
Measure time
Squash
immediately switched on a context switch, but only switched
when a floating-point instruction is actually encountered. Hence, …
there is a delay in the first floating-point instruction encountered
Fig. 5: TSG model of special register triggered attacks.
in a new context that can result in speculatively accessing the
old values of the floating-point registers of the previous context.
We show the missing security dependency as a red arrow from target address is computed and compared with the predicted
authorization to read register. target address.
{ Indirect branch attack (Spectre v2). | Memory disambiguation triggered attack (Spectre v4).
The Spectre v2 attack mis-trains hardware predictors, e.g., The Spectre v4 (Spectre-STL) attack speculatively reads
the branch target buffer (BTB), such that the victim specula- stale data (secret) that should be overwritten by a previous
tively jumps to a wrong address and executes malicious gadgets store. During the speculative load, address disambiguation
(i.e., code) that can access and leak a secret. This attack can mispredicts that the load does not depend on a previous store,
also be modeled by Figure 1. The difference with Spectre v1 i.e., the load address is not the same as any of the addresses of
is that the speculative execution starts because the computation store instructions still sitting in the store buffer. We model this
of the target address is delayed, and so the prediction for the attack in Figure 6. The authorization is address disambiguation
target address (BTB) of the indirect branch instruction is used and the illegal access is “Read S”. A missing dependency is
instead. The “authorization” of the control flow defined by the shown as the red dashed arrow from address disambiguation
indirect branch instruction is completed when the real branch to the illegal access “Read S”.

47
Flush Array_A
Setup Spectre RSB waits for the return address to be determined.
The last two entries in Table III, TAA and Cacheout, are TSX-
Store S Delayed based attacks. TSX uses transactional memory to enforce the
Authorization
atomic execution of a bundle of instructions called a transaction
Load instruction
- either all the instructions are executed or none are executed.
Hence, TSX can also be used to speculatively access a secret
Read S Secret access from the cache, store/load buffers or fill buffers.
Compute load address R Use Secret and V. B ENEFITS OF OUR M ODEL
Send Secret
Load R to Cache Our new attack graph model is useful in enabling us to:
• discover new attacks (Section V-A),
Authorization Memory address
Resolved disambiguation • model defense strategies and consistently explain why a
Squash or specific defense works or does not work (Section V-B),
commit
Reload Array_A Receive Secret
(Illegal Access) • enable tools to discover vulnerabilities and patch them
Squash
(Section V-C).
Measure time

… A. Finding New Attacks


Fig. 6: TSG model of memory disambiguation triggered attack. Our attack graph can be generalized to model or find new
Setup
attacks. We describe three ways: by finding new sources
Place a malicious value
Flush Array_A
M in hardware buffers of secrets, new exploitable hardware features for delaying
authorization, and new covert channels.
Delayed
Load instruction Authorization First, as we have already illustrated in Section IV, the attack
graphs can be extended to incorporate new sources of a secret.
Read M Read M from Read M from Read M from For instance, the micro-architectural data sampling attacks
from Cache line fill buffer load port store buffer
(RIDL [40], Fallout [12], ZombieLoad [35]) use a faulting load
Victim’s control or data
flow diverted by M
to read secret data that is left in micro-architectural data buffers
Load S Secret access by previous memory accesses even from a different thread or
Compute load address R Use Secret and process. They can be identified by analyzing the hardware
Send Secret implementation as the hardware designer should be able to find
Load R to cache
a set of datapaths that read data from different data buffers and
Authorization Load permission forward the data to the faulting load. Each of these datapaths
Resolved check Reload Array_A
Squash or
commit Receive Secret
can be added as a new node in the attack graph (see Figure 4).
(Illegal Access)
Also, in the Meltdown variant1 [2] and LazyFP [36] attacks,
Measure time
Squash the unauthorized access to system registers or floating-point

registers will cause an exception, and can be modeled with the
Fig. 7: TSG model of Load Value Injection (LVI). nodes “Read from Special Register” or “Read from FPU” (see
Figure 5). Other sources of secrets can also be identified to
create new attacks.
} Load Value Injection (LVI) attack. Second, new hardware features can be exploited for delaying
The LVI attack injects the attacker-desired data to the the authorization while allowing the execution to proceed.
victim’s program. In this attack, the attacker attempts to leave Examples include other hardware prediction mechanisms or
the data in the memory buffers. A victim’s faulting load delayed exception mechanisms. Identifying new authorization-
speculatively reads from the buffer and unintentionally uses related features can be achieved by analyzing processor pipeline
the attacker-controlled data for his execution. We model this squash signals. Each cause of a potential pipeline squash can
attack in Figure 7. The missing security dependency is the red be studied for its effect at the instruction (software) level.
dashed arrow from the load fault handling to the access to the In the example of a conditional branch, the cause of the
malicious data M. pipeline squash is due to the resolution of a conditional branch
A few of the entries in Table III have not been specifically prediction. Subsequent load instructions after this conditional
described. Spectre v1.1 and Spectre v1.2 are like Spectre v1 branch instruction can be the access of a secret, followed by
and can be modeled by Figure 1 with a small modification. a covert send through the cache covert channel, which gives
Instead of reading an out-of-bounds memory location, Spectre rise to the Spectre v1 attack.
v1.1 writes an out-of-bounds memory location illegally. Spectre In general, any decision-making operation that can cause
v1.2 tries to write to a read-only memory location. speculative prediction and execution can trigger subsequent
Spectre RSB is like Spectre v2 (indirect branch). Hence, it illegal accesses through a speculatively-executed load instruc-
can also be modeled by Figure 1. Instead of waiting for the tion (or privileged register read). This can be a “software
target address of an indirect branch instruction to be computed, authorization” node that triggers subsequent illegal accesses.

48
Mistrain predictor Flush Array_A Setup Strategy x: Prevent Access before Authorization. This
prevents the illegal access of the secret, until the delayed

Conditional/Indirect Delayed authorization is resolved.
Branch Instruction Authorization LFENCE is an industry defense used to serialize the
instructions before and after it. Adding an LFENCE instruction
Load S
before the speculative load adds a new security dependency
① Secret access
between the “Branch resolution” (software authorization) and
Compute load address R
Use Secret and
“Load S” (secret access), shown as x in Figure 8. Context-
② Send Secret sensitive fencing [37] prevents the speculative access by
Load R to Cache
inserting fences at the micro-operation level, e.g., between
Authorization ③ a conditional branch and a load to defeat the Spectre v1 attack.
Squash or
Resolved Receive Secret This is done in hardware, rather than in software. Secure
commit
Branch resolution: automatic bounds checking (SABC) [30] serialize the branch
correct flow Reload Array_A
and the out-of-bounds access to mitigate the Spectre attack,
by inserting arithmetic instructions with data dependencies
Measure time
… between the branch and the access.
Fig. 8: Four defense strategies against Spectre v1/v2 attacks: Strategy y: Prevent Data Usage before Authorization. This
x Add a security dependency between the “branch resolution” prevents the use of the speculatively accessed secret, until the
(authorization) for bounds checking, and the protected memory delayed authorization is resolved.
access, y avoid the usage of speculative data, z prevent loads NDA [42], SpecShield [10], SpectreGuard [17] and ConTExT
whose address depends on unauthorized data from changing [34] prevent forwarding the speculatively loaded data to the
cache states, { Clear predictor on context switch. following instructions so that the secret cannot be used, e.g.,
to compute the address R. SpectreGuard and ConTExT further
Such decision-making actions can be expressed in any software provide the software interface for software developers to
language. mark memory regions containing the secret as sensitive so
Furthermore, speculative execution is not the only source of the usage of non-sensitive data is allowed to reduce the
transient instructions for illegally accessing secrets. Another performance overhead. Equivalently, this means adding a new
example of transient instructions that may be aborted is TSX, security dependency between the “Branch resolution” (software
for the atomic execution of a transaction, as also described authorization) and “Compute Load Address R” (data usage),
earlier in the last two entries of Table III. shown as y in Figure 8.
Third, our attack graph can also be extended to various Strategy z: Prevent Send before Authorization. This pre-
different covert channels. For the most representative cache vents the micro-architectural state changes of shared hardware
covert channel, we can generalize the cacheline as a resource resources that serve as the Send signal of the covert or side
whose state can be changed by the covert-sender or victim channel, until the delayed authorization is resolved. This
program, and this state change can be observed by the covert- defense strategy improves performance by adopting a looser
receiver (attacker). To extend the analysis to different covert security model where the secret is allowed to be accessed
channels such as the memory bus covert channel, functional unit before authorization as long as it does not leak out.
covert channel or branch target buffer (BTB) covert channel, we This strategy adds the security dependency between “Branch
can also model the covert channel state and find the instructions resolution” and “Load R to cache” (cache state change), shown
that change this state and be detectable by a covert-receiver. as z in Figure 8. Different hardware implementations have been
This method can identify more sender-receiver pairs than the proposed under this strategy. STT [46] and SpecShieldERP+
“Load R to Cache” and “Reload Array_A” pair. [10] prevent loads whose address is based on speculative data.
The key takeaway of this framework is that any new Conditional Speculation [28] and Efficient Invisible Speculative
combination of these three dimensions of an attack gives a Execution [33] both allow a speculative load that hits in the
new attack. cache, because the cacheline state does not change on a hit,
but delay speculative loads that encounter a miss. They further
B. Identifying Defense Strategies reduce the overhead by identifying trusted pages and predicting
A major application of our attack graph model is identifying data, respectively. InvisiSpec [44] and SafeSpec [22] disallow
potential defense strategies, as we illustrate by the red dashed ar- speculative cache state modification but put the speculatively
rows in Figure 8 for the attacks triggered by branch instructions. requested cache line in the shadow buffer. If the prediction is
We illustrate potential defenses that essentially add security later found to be correct, InvisiSpec and SafeSpec reissue the
dependencies to the system to defeat the attacks. We also show memory access to fetch the proper cache lines. CleanupSpec
that our defense strategies cover the recently proposed defenses [32] allows speculative cache state modification but restores
in industry and academia to defeat speculative execution the cache state on a mis-speculation.
attacks. Strategy {: Clearing Predictions. This strategy prevents the

49
sharing of predictor states between different contexts.  
For example, the industry solution from Intel, Indirect Branch
Predictor Barrier (IBPB) [7], prevents the code before the    
barrier from affecting the branch prediction after it by flushing
the Branch Target Buffer (BTB). It introduces a new operation, 
   "
i.e., “flush predictor”, to the attack graph and adds a security
dependency between “flush predictor” and the indicated branch
  #     #
instruction. Context-sensitive fencing [37] also shows the  
feasibility of inserting micro-ops by hardware during a privilege
 
change, to prevent a predictor being mistrained from a different !   
 
! 
 
      
context.       
   
We show that our attack graph can model not only the
defenses that work, but also the defenses that do not work.    
In Figure 4, we show that a security dependency can be 
 

 
added at four different places to defend against the Meltdown
attack, shown as red dashed lines. Defense strategies x, y, z
are similar to Figure 8. Typically, only one of these defense   

  

strategies is needed.
However, sometimes a defense is not sufficient, as we now Fig. 9: The flow chart to generate the attack graph for different
illustrate with a hypothetical Meltdown attack coupled with an types of speculative execution attacks. This also shows how the
attacker induced cache hit for the secret, like the L1 Terminal vulnerability can be plugged by adding a security dependency.
Fault [38]. If the secret is already in the cache, the load
instruction will fetch it from the cache rather than from the
recognize the authorization operation such as a prior conditional
main memory. So while dependency x can defend against
or indirect branch instruction (software authorization), or a
the baseline Meltdown attack that speculatively loads a secret
load or store instruction (hardware privilege check or address
from main-memory in Figure 4, this is insufficient when x
disambiguation check). A flow chart to generate the attack
can no longer prevent the secret access from the cache. In
graph for speculative execution attacks is shown in Figure 9.
this case, an additional dependency { in Figure 4, i.e. from
“Authorization” to “Read S from cache”, has to be jointly added For the control-flow misprediction attacks triggered by a
with x to provide a valid defense. Hence, it is important to put conditional or indirect branch instruction (the left side of
security dependencies in the correct places, otherwise we get Figure 9), we propose a major simplification where these
a false sense of security, especially when micro-architectural misprediction-based attacks can be modeled at the instruction
performance optimizations (like load from cache on a hit) level where the nodes are just instructions, and the edges are
can bypass an insecure security dependency like x. In fact, control flow and data-flow dependencies between instructions.
there has to be a security dependency arrow between the This means that the tool just needs to look for subsequent
“authorization resolved” node to every node that can be a memory loads or special register access instructions after branch
source of the secret in Figure 4, such as load ports, line fill (conditional or indirect) nodes as the secret access.
buffers and store/load buffers. The number of such ports and For the faulty memory/register access attacks where the
buffers suggests that the defense strategy “Prevent Data Usage authorization and the secret access are done in the same
before Authorization” may be a solution that is not only more instruction, the tool needs to break down such instructions
efficient but also more secure. into their micro-architectural level in the attack graph model,
as shown in Figure 4. These instructions to be broken down
C. Tools for Constructing Attack Graphs are the memory load instructions, the Read Privileged Register
A tool can be designed to construct attack graphs and find instructions and the instructions that Read or Write Floating-
the missing security dependencies. To achieve this, the memory point or SIMD registers.
locations (with secret or sensitive data and code) to be protected After identifying the secret access and the potential covert
should be identified. OS and hypervisor data and code must sending operations, the tool can automatically generate edges
automatically be protected from less-privileged software. For by looking for existing dependencies, e.g., data dependencies,
user-level data and code, the most secure way is for the user fences and address dependencies. Missing security depen-
to initially specify what data and code should be protected as dencies (races) between the authorization and the secret
in [17], [34]. Then the tool can trace all direct and indirect access instruction and its subsequent chain of data-dependent
accesses to these protected data and code as potential secret instructions, which can be executed in the speculative execution
accesses. window, can be found by automatically searching the graph.
Then, the tool needs to identify attack nodes as we introduced Such a missing security dependency between an authorization
in Section IV. By providing a threat model that specifies node and a secret access node in a program shows a vulnera-
the range of attacks that are to be defeated, the tool can bility that can lead to a potential attack. These vulnerabilities

50
can be flagged by the tool. The tool can also proactively insert attacks, Disselkoen et al. [16] proposed a memory model based
a security dependency, e.g., a lightweight fence, to prevent on pomsets to allow speculative evaluation. However, this model
attacks. only covers speculative secret access, but does not show how
The main challenges for extending the above methodology to the secret is sent through a cache covert channel. Canella et al.
a fully-functional tool appear to be the initial identification of [13] summarized and evaluated speculative execution attacks
secrets in user code, and modelling at the intra-instruction level and some defenses. However, their work does not provide a
which is different for each micro-architecture implementation. systematic model for attacks and defenses that provides insights
The former can leverage the use of other tools, and we have on designing and evaluating new secure defenses. On the formal
shown that the latter is only necessary for a few instructions modeling side, Guarnieri et al. [18] proposed the speculative
where the authorization and access are in the same instruction, non-interference property to verify that a program behaves the
e.g., load instructions. same with and without speculation. Cheang et al. [14] proposed
trace property-dependent observational determinism (TPOD)
VI. I NSIGHTS AND TAKEAWAYS
to verify that two traces of execution are not distinguishable.
Based on our new models of speculative execution attacks, These formal methods cannot reason about the defenses, while
our major new insights are: we can show why defenses work and which ones will not
1) The root cause of speculative attacks succeeding is a work.
missing edge in the attack graph between the authorization Previous work has been proposed to evaluate caches’ re-
operation and the secret access operation. silience against (non-speculative) side-channel attacks. He et
2) We define the term “security dependency”, and equate al. [20] proposed the probabilistic information flow graph
this to a missing edge in an attack graph that enforces (PIFG) to model the cache, attacker and victim simultaneously.
the correct ordering of the authorization node before Zhang et al. [47] quantified information leakage via mutual
subsequent operation nodes. information. Demme et al. [15] proposed the Side-channel
3) These security dependencies can give us “defense strate- Vulnerability Factor (SVF) and Zhang et al. [48] refined it
gies”. Each defense strategy can be implemented through as the Cache Side-channel Vulnerability (CSV) for access-
many different architectural mechanisms. More impor- based attacks. However, none of these past work on cache
tantly, the currently proposed hardware and software side-channel attacks covers speculative execution attacks.
defenses all fall under one of our defense strategies.
4) Falling under one of our defense strategies also explains VIII. C ONCLUSIONS
why the defense works. The defense is equivalent to Information leakage due to speculative execution has been
implementing a missing security dependency and thus a serious and unsolved problem. In this paper, we provide
preventing a critical attack step from succeeding. This is new attack graph models for speculative execution attacks. We
the first time a reason for the success of a defense can identify the common characteristics of speculative attacks as
be systematically given. illegal access of secrets during speculative execution and covert
5) A security dependency can sometimes be “relaxed” to channel exfiltration of this secret information, and break these
reduce the performance overhead (e.g., allow accessing down further into 5-6 critical attack steps.
the secret but prevent leaking the secret) for security- We propose the attack graph as a topological sort graph
performance tradeoffs. This is illustrated in Section V-B (TSG), where the critical attack steps can be identified.
by our defense strategies y prevent data usage before Fundamentally, the speculation vulnerability is due to a race
authorization and z prevent send before authorization. condition, shown as a missing edge in a TSG, between
6) Attacks that look similar, e.g., the Spectre-type and authorization and secret access nodes. In a looser security but
Meltdown-type attacks are actually different, in the sense higher performance scenario, this missing edge can be between
that the Meltdown-type attacks have authorization and the authorization node and the nodes that use or send out the
access in the same instruction, while the Spectre-type “not-yet-authorized” data. We are the first to define the concept
attacks do not. This results in the Meltdown-type attacks of a security dependency, which enforces the proper ordering
having to be investigated through intra-instruction oper- of authorization before access, or authorization before use, or
ations, while Spectre-type attacks only need to consider authorization before send operations. Security dependencies
inter-instruction operations. This makes attack graph and prevent race conditions that lead to security breaches.
tool construction simpler. To show the effectiveness of our proposed models, we
Our new attack graph is useful in finding new attacks, generate attack graphs for the Spectre and Meltdown attacks,
identifying new defense strategies and systematically explaining and then generalize them to all known attack variants. From
why a defense works or not, and facilitating the design of tools our attack graphs, we show how to generate new attacks, how
to discover vulnerabilities and patch them. to derive new defense strategies and why they work. In fact, all
proposed solutions from both industry and academia fall under
VII. R ELATED W ORK one of our defense strategies. We have also shown how to
Speculative execution attacks have been defined, e.g., in design a tool that can help construct attack graphs and uncover
[8], [24]–[26], [29], [36], [38]. To model speculative execution vulnerabilities in the software-hardware system.

51
We have provided a generalizable framework to model and [3] [Link]
analyze the speculative execution attacks, and hope this helps speculative-store-bypass-cve-2018-3639/, 2018.
[4] [Link] 2018.
advance more secure micro-architecture defenses and designs. [5] [Link]
SoftwareTechniquesforManagingSpeculation_WP_7-18Update_
ACKNOWLEDGEMENTS [Link], 2018.
This work is supported in part by NSF SaTC #1814190, SRC [6] [Link]
showing-the-ankle-of-cascade-lake, 2018.
Hardware Security Task 2844.002 and a Qualcomm Faculty [7] [Link]
Award for Prof. Lee. We thank the anonymous reviewers for dive-indirect-branch-predictor-barrier, 2018.
their insightful comments and feedback. [8] [Link] 2018.
[9] A. Aggarwal, R. J. Anderson, and M.-Y. Kao, “Parallel depth-first search
A PPENDIX A in general directed graphs,” in ACM Symposium on Theory of Computing
(STOC), 1989.
P ROOF OF T HEOREM 1 [10] K. Barber, A. Bacha, L. Zhou, Y. Zhang, and R. Teodorescu, “Specshield:
Proof: Necessity (<=). It can be proved by contradiction. Shielding speculative data from microarchitectural covert channels,” in
International Conference on Parallel Architectures and Compilation
Assume there is not a path from u to v. Let Techniques (PACT), 2019.
S = [s1 , s2 ...sk , v, sk+1 ...sn ] (1) [11] J. Bonneau and I. Mironov, “Cache-collision timing attacks against aes,”
= [Sv , v, sk+1 ...sn ] (2) in International Workshop on Cryptographic Hardware and Embedded
Systems (CHES), 2006.
be a valid ordering sequence, where Sv = [s1 , s2 ...sk ] represents [12] C. Canella, D. Genkin, L. Giner, D. Gruss, M. Lipp, M. Minkin,
the vertices before v in S. Split Sv into two subsequences with D. Moghimi, F. Piessens, M. Schwarz, B. Sunar et al., “Fallout: Leaking
the same order in S data on meltdown-resistant cpus,” in ACM SIGSAC Conference on
k Computer and Communications Security (CCS), 2019.
S1 = [s11 , s21 ...s11 ] (3) [13] C. Canella, J. Van Bulck, M. Schwarz, M. Lipp, B. Von Berg, P. Ortner,
k
S2 = [s12 , s22 ...s22 ] (4) F. Piessens, D. Evtyushkin, and D. Gruss, “A systematic evaluation of
transient execution attacks and defenses,” in USENIX Security Symposium,
where S1 contains vertices that have a path to v, S2 contains 2019.
vertices that do not have a path to v. By assumption, u does [14] K. Cheang, C. Rasmussen, S. Seshia, and P. Subramanyan, “A formal
not have a path to v, therefore u ∈ S2 . Note that k1 + k2 = k. approach to secure speculation,” in Computer Security Foundations
Construct another sequence Symposium (CSF), 2019.
[15] J. Demme, R. Martin, A. Waksman, and S. Sethumadhavan, “Side-
S = [S1 , v, S2 , sk+1 ...sn ] channel vulnerability factor: a metric for measuring information leakage,”
k k
= [s11 , s21 ...s11 , v, s12 , s22 ...s22 , sk+1 ...sn ] in International Symposium on Computer Architecture (ISCA), 2012.
 k [16] C. Disselkoen, R. Jagadeesan, A. Jeffrey, and J. Riely, “The code
We claim that ordering S is also valid: For any s1i ∈ S1 and that never ran: Modeling attacks on speculative evaluation,” in IEEE
kj k j ki Symposium on Security and Privacy (SP), 2019.
s2 ∈ S2 , there is not an edge (s2 , s1 ) in the graph. Otherwise,
k [17] J. Fustos, F. Farshchi, and H. Yun, “Spectreguard: An efficient data-
k
[s2 j → s1i → v] is a path, contradicting the definition of S2 . For centric defense mechanism against spectre attacks,” in ACM/IEEE Design
k Automation Conference (DAC), 2019.
the same reason, there is not an edge (s2 j , v) in the graph. We [18] M. Guarnieri, B. Köpf, J. F. Morales, J. Reineke, and A. Sánchez,
categorize any edge (z, x) into 3 cases, i.e. x ∈ S1 , x = v and “Spectector: Principled detection of speculative information flows,” in
x ∈ S2 . We show z comes before x in S in all cases: IEEE Symposium on Security and Privacy (SP), 2020.
[19] D. Gullasch, E. Bangerter, and S. Krenn, “Cache games–bringing access-
x for any edge (z, v) in the graph, z can only be in S1 , and based cache attacks on aes to practice,” in IEEE Symposium on Security
thus z is before v in S . and Privacy (SP), 2011.
k
y For any edge (z, s1i ) in the graph, z can only be in [20] Z. He and R. B. Lee, “How secure is your cache against side-channel
attacks?” in ACM/IEEE International Symposium on Microarchitecture
(s1 , ...s1 ), and thus z is also before s1i in S .
k1 ki−1 k
(MICRO), 2017.
z Since S2 are moved backward and sk+1 ...sn are kept in the [21] S. Islam, A. Moghimi, I. Bruhns, M. Krebbel, B. Gulmezoglu, T. Eisen-
k barth, and B. Sunar, “Spoiler: Speculative load hazards boost rowhammer
same position from S to S , for any edge (z, s2 j ), z is before and cache attacks,” in Usenix Security Symposium, 2019.
kj [22] K. N. Khasawneh, E. M. Koruyeh, C. Song, D. Evtyushkin, D. Ponomarev,
the s2 .
and N. Abu-Ghazaleh, “Safespec: Banishing the spectre of a meltdown
From x,y and z, the ordering S is valid. Meanwhile, v is with leakage-free speculation,” in ACM/IEEE Design Automation Con-
before u ∈ S2 in S , contradicting to u is before v in all valid ference (DAC), 2018.
orderings. Therefore, the assumption is not true and there must [23] V. Kiriansky, I. Lebedev, S. Amarasinghe, S. Devadas, and J. Emer,
“Dawg: A defense against cache timing attacks in speculative execution
be a path connecting u and v.  processors,” in ACM/IEEE International Symposium on Microarchitecture
Sufficiency (=>). The sufficiency is relatively obvious. (MICRO), 2018.
Without loss of generality, assume there exists a directed path [24] V. Kiriansky and C. Waldspurger, “Speculative buffer overflows: Attacks
and defenses,” arXiv preprint arXiv:1807.03757, 2018.
from u to v, i.e. P=(u, w1 , ...wk , v). Then for any valid ordering [25] P. Kocher, J. Horn, A. Fogh, , D. Genkin, D. Gruss, W. Haas, M. Hamburg,
S, u is before w1 , w1 is before w2 , ... ,wk is before v. Therefore M. Lipp, S. Mangard, T. Prescher, M. Schwarz, and Y. Yarom, “Spectre
u is before v in any valid ordering.  attacks: Exploiting speculative execution,” in IEEE Symposium on
Security and Privacy (SP), 2019.
R EFERENCES [26] E. M. Koruyeh, K. N. Khasawneh, C. Song, and N. Abu-Ghazaleh,
“Spectre returns! speculation attacks using the return stack buffer,” in
[1] [Link] USENIX Workshop on Offensive Technologies (WOOT), 2018.
technology/64-ia-32-architectures-software-developer-system- [27] R. B. Lee, “Security aware microarchitecture design,” IEEE/ACM
[Link], 2016. International Symposium on Microarchitecture (MICRO), Keynote
[2] [Link] 2018. Speech, [Link] 2018.

52
[28] P. Li, L. Zhao, R. Hou, L. Zhang, and D. Meng, “Conditional speculation:
An effective approach to safeguard out-of-order execution against spectre
attacks,” in International Symposium on High Performance Computer
Architecture (HPCA), 2019.
[29] M. Lipp, M. Schwarz, D. Gruss, T. Prescher, W. Haas, A. Fogh,
J. Horn, S. Mangard, P. Kocher, D. Genkin, Y. Yarom, and M. Hamburg,
“Meltdown: Reading kernel memory from user space,” in Usenix Security
Symposium, 2018.
[30] E. J. Ojogbo, M. Thottethodi, and T. Vijaykumar, “Secure automatic
bounds checking: prevention is simpler than cure,” in ACM/IEEE
International Symposium on Code Generation and Optimization (CGO),
2020.
[31] D. A. Osvik, A. Shamir, and E. Tromer, “Cache attacks and countermea-
sures: the case of aes,” in Cryptographers track at the RSA conference,
2006.
[32] G. Saileshwar and M. K. Qureshi, “Cleanupspec: An undo approach to
safe speculation,” in IEEE/ACM International Symposium on Microar-
chitecture (MICRO), 2019.
[33] C. Sakalis, S. Kaxiras, A. Ros, A. Jimborean, and M. Själander,
“Efficient invisible speculative execution through selective delay and
value prediction,” in International Symposium on Computer Architecture
(ISCA), 2019.
[34] M. Schwarz, M. Lipp, C. Canella, R. Schilling, F. Kargl, and D. Gruss,
“Context: A generic approach for mitigating spectre,” in Network and
Distributed System Security Symposium (NDSS), 2020.
[35] M. Schwarz, M. Lipp, D. Moghimi, J. Van Bulck, J. Stecklina, T. Prescher,
and D. Gruss, “Zombieload: Cross-privilege-boundary data sampling,” in
ACM SIGSAC Conference on Computer and Communications Security
(CCS), 2019.
[36] J. Stecklina and T. Prescher, “Lazyfp: Leaking fpu register state using
microarchitectural side-channels,” arXiv preprint arXiv:1806.07480,
2018.
[37] M. Taram, A. Venkat, and D. Tullsen, “Context-sensitive fencing: Secur-
ing speculative execution via microcode customization,” in International
Conference on Architectural Support for Programming Languages and
Operating Systems (ASPLOS), 2019.
[38] J. Van Bulck, M. Minkin, O. Weisse, D. Genkin, B. Kasikci, F. Piessens,
M. Silberstein, T. F. Wenisch, Y. Yarom, and R. Strackx, “Foreshadow:
Extracting the keys to the intel sgx kingdom with transient out-of-order
execution,” in Usenix Security Symposium, 2018.
[39] J. Van Bulck, D. Moghimi, M. Schwarz, M. Lipp, M. Minkin, D. Genkin,
Y. Yarom, B. Sunar, D. Gruss, and F. Piessens, “Lvi: Hijacking transient
execution through microarchitectural load value injection,” in IEEE
Symposium on Security and Privacy (SP), 2020.
[40] S. Van Schaik, A. Milburn, S. Österlund, P. Frigo, G. Maisuradze,
K. Razavi, H. Bos, and C. Giuffrida, “Ridl: Rogue in-flight data load,”
in IEEE Symposium on Security and Privacy (SP), 2019.
[41] S. van Schaik, M. Minkin, A. Kwong, D. Genkin, and Y. Yarom,
“Cacheout: Leaking data on intel cpus via cache evictions,” arXiv preprint
arxiv:2006.13353, 2020.
[42] O. Weisse, I. Neal, K. Loughlin, T. F. Wenisch, and B. Kasikci, “Nda:
Preventing speculative execution attacks at their source,” in ACM/IEEE
International Symposium on Microarchitecture (MICRO), 2019.
[43] O. Weisse, J. Van Bulck, M. Minkin, D. Genkin, B. Kasikci, F. Piessens,
M. Silberstein, R. Strackx, T. F. Wenisch, and Y. Yarom, “Foreshadow-
ng: Breaking the virtual memory abstraction with transient out-of-order
execution,” Technical report, Tech. Rep., 2018.
[44] M. Yan, J. Choi, D. Skarlatos, A. Morrison, C. W. Fletcher, and J. Tor-
rellas, “Invisispec: Making speculative execution invisible in the cache
hierarchy,” in ACM/IEEE International Symposium on Microarchitecture
(MICRO), 2018.
[45] Y. Yarom and K. Falkner, “Flush+ reload: A high resolution, low noise,
l3 cache side-channel attack.” in Usenix Security Symposium, 2014.
[46] J. Yu, M. Yan, A. Khyzha, A. Morrison, J. Torrellas, and C. W.
Fletcher, “Speculative taint tracking (stt) a comprehensive protection for
speculatively accessed data,” in ACM/IEEE International Symposium on
Microarchitecture (MICRO), 2019.
[47] T. Zhang and R. B. Lee, “New models of cache architectures characteriz-
ing information leakage from cache side channels,” in Annual Computer
Security Applications Conference (ACSAC), 2014.
[48] T. Zhang, F. Liu, S. Chen, and R. B. Lee, “Side channel vulnerability
metrics: the promise and the pitfalls,” in International Workshop on
Hardware and Architectural Support for Security and Privacy (HASP),
2013.

53

You might also like