Formal Security Evaluation for Microarchitectural Modeling
P
e
n
s
i
e
v
e
:
M
i
c
r
o
a
r
c
h
i
t
e
c
t
u
r
a
l
M
o
d
e
l
i
n
g
f
o
r
F
o
r
m
a
l
S
e
c
u
r
i
t
y
E
v
a
l
u
a
t
i
o
n
Y
u
h
e
n
g
Y
a
n
g
,
T
h
o
m
a
s
B
o
u
r
g
e
a
t
,
S
t
e
l
l
a
L
a
u
,
M
e
n
g
j
i
a
Y
a
n
To appear at ISCA’23
“
C
o
n
s
t
a
n
t
-
t
i
m
e
P
r
o
g
r
a
m
”
m
i
g
h
t
n
o
t
r
u
n
i
n
C
o
n
s
t
a
n
t
-
t
i
m
e
i
n
H
a
r
d
w
a
r
e
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
2
P
r
o
b
l
e
m
:
t
h
e
C
a
t
-
a
n
d
-
M
o
u
s
e
G
a
m
e
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
3
2018
2019
2021
2020
P
r
o
b
l
e
m
:
W
e
a
k
S
e
c
u
r
i
t
y
E
v
a
l
u
a
t
i
o
n
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
4
W
e
n
e
e
d
a
p
r
i
n
c
i
p
l
e
d
,
t
r
u
s
t
w
o
r
t
h
y
s
e
c
u
r
i
t
y
e
v
a
l
u
a
t
i
o
n
t
o
o
l
!
S
t
e
p
1
:
Defense
Proposal
S
t
e
p
2
:
The defense works
for all possible
Spectre gadget.
B
a
c
k
g
r
o
u
n
d
:
F
o
r
m
a
l
S
e
c
u
r
i
t
y
P
r
o
p
e
r
t
y
•
Only consider constant-time program
•
Avoid secret affecting
•
Execution Time
•
Cache footprint
•
…
•
Speculative Non-Interference Property:
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
5
C
h
a
l
l
e
n
g
e
:
B
r
i
d
g
e
t
h
e
G
a
p
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
6
E
v
a
l
u
a
t
i
o
n
T
o
o
l
s
JasperGold
Rosette
Coq
ACL2
Isabelle/HOL
CVC5
Boolector
z3
A
l
i
g
n
e
d
w
i
t
h
a
r
c
h
i
t
e
c
t
u
r
a
l
d
e
s
i
g
n
f
l
o
w
.
M
o
d
e
l
D
e
f
e
n
s
e
D
e
s
i
g
n
f
l
o
w
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
7
Example: delay speculative requests
Memory
Decode &
Rename
Dispatch
Commit
Fetch
P
e
n
s
i
e
v
e
M
o
d
e
l
i
n
g
•
Decouple timing and functionality using the hand-shaking interface
•
Represent a space of timing behavior
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
8
Func
Memory System
Time
U
n
i
n
t
e
r
p
r
e
t
e
d
F
u
n
c
t
i
o
n
(
U
F
)
•
A UF represents space of functions with the same input/output types
•
Example:
Bool UF(Bool, Bool)
•
UF helps us
•
s
t
a
t
e
“
w
h
a
t
”
a
f
f
e
c
t
s
t
h
e
o
u
t
p
u
t
,
•
a
b
s
t
r
a
c
t
a
w
a
y
t
h
e
d
e
t
a
i
l
s
o
n
“
h
o
w
”
t
h
e
i
n
p
u
t
a
f
f
e
c
t
s
t
h
e
o
u
t
p
u
t
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
9
r
e
p
r
e
s
e
n
t
s
P
e
n
s
i
e
v
e
M
o
d
e
l
i
n
g
:
U
s
i
n
g
U
F
s
•
Examples:
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
10
Multiply_req_latency = UF(historyOf(in_valid))
Multiply_req_latency = UF(historyOf(in_valid, in_operands))
Memory_req_latency = UF(historyOf(in_valid, in_addr))
P
e
n
s
i
e
v
e
c
a
n
u
s
e
s
i
m
p
l
e
m
o
d
e
l
s
t
o
c
o
v
e
r
s
p
a
c
e
o
f
m
i
c
r
o
a
r
c
h
i
t
e
c
t
u
r
e
s
w
i
t
h
c
o
m
p
l
e
x
t
i
m
i
n
g
b
e
h
a
v
i
o
r
s
P
e
n
s
i
e
v
e
M
o
d
e
l
i
n
g
•
Decouple timing and functionality using the hand-shaking interface
•
Represent a space of timing behavior with uninterpreted functions
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
11
Func
Memory System
Time
U
F
P
e
n
s
i
e
v
e
S
e
c
u
r
i
t
y
E
v
a
l
u
a
t
i
o
n
F
r
a
m
e
w
o
r
k
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
12
Model
Checker
FAIL: Attack Program
PASS: Security for k Cycles
Micro-Arch Model
(Speculative Non-interference)
P
e
n
s
i
e
v
e
f
i
n
d
s
u
n
k
n
o
w
n
s
e
c
u
r
i
t
y
v
u
l
n
e
r
a
b
i
l
i
t
i
e
s
i
n
t
h
e
l
a
t
e
s
t
s
p
e
c
u
l
a
t
i
v
e
e
x
e
c
u
t
i
o
n
d
e
f
e
n
s
e
,
i
.
e
.
,
G
h
o
s
t
M
i
n
i
o
n
[
2
0
2
1
]
G
h
o
s
t
M
i
n
i
o
n
#1: Invisible Speculation
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
13
s
S
p
e
c
t
r
e
v
1
if (false)
ld
sec
//transmitter
s
S
p
e
c
u
l
a
t
i
v
e
I
n
t
e
r
f
e
r
e
n
c
e
A
t
t
a
c
k
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
14
y = ……
//delay
ld y
// transmitter
if (false)
ld
sec
// interfere
MSHR
•
Y
o
u
n
g
e
r
s
p
e
c
u
l
a
t
i
v
e
l
o
a
d
s
i
n
t
e
r
f
e
r
e
w
i
t
h
o
l
d
e
r
b
o
u
n
d
-
t
o
-
c
o
m
m
i
t
l
o
a
d
s
.
•
Many other contention structures: non-pipelined ALU, cache port, bank
contention, network-on-chip, etc.
s
s
y
x
x
G
h
o
s
t
M
i
n
i
o
n
#1: Invisible Speculation
#2: Prioritize Older Instructions through Timestamps
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
15
y = ……
//delay
ld y
//transmitter
if (false)
ld
sec
//interfere
speculative
interference
attack
MSHR
S
o
F
a
r
…
Use Pensieve
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
16
2018
2019
2021
2020
P
e
n
s
i
e
v
e
F
o
u
n
d
A
N
e
w
A
t
t
a
c
k
V
a
r
i
a
n
t
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
17
if (true)
ld y
// transmitter
else
ld
sec
// interfere
1
mispredict
Speculative load is older this time!
Speculative load can interfere with bound-to-commit load
N
e
w
A
t
t
a
c
k
o
n
G
h
o
s
t
M
i
n
i
o
n
S
u
m
m
a
r
y
speculative interference attack
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
18
y = ……
ld y
// transmitter
if (false)
ld
sec
// interfere
new attack variant
T
a
k
e
a
w
a
y
:
M
a
n
u
a
l
e
v
a
l
u
a
t
i
o
n
c
a
n
e
a
s
i
l
y
b
e
u
n
s
o
u
n
d
,
w
e
n
e
e
d
P
e
n
s
i
e
v
e
,
a
t
r
u
s
t
w
o
r
t
h
y
e
v
a
l
u
a
t
i
o
n
t
o
o
l
if (true)
ld y
// transmitter
else
ld
sec
// interfere
C
h
e
c
k
i
n
g
T
i
m
e
a
n
d
S
c
a
l
a
b
i
l
i
t
y
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
19
•
Microarchitecture Setup
•
5 types of instructions
•
4-entry register file
•
4-entry data memory
•
16-entry instruction memory
•
8-entry ROB
•
GhostMinion defense
•
Problem: Checking time increases
exponentially as the number of simulated
cycles increases
•
Future work: Combine Penseive with more
powerful formal verification backend
P
e
n
s
i
e
v
e
S
u
m
m
a
r
y
FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
20
P
e
n
s
i
e
v
e
p
r
o
v
i
d
e
s
a
m
o
d
e
l
i
n
g
p
r
i
n
c
i
p
l
e
t
h
a
t
a
l
i
g
n
s
w
i
t
h
a
r
c
h
i
t
e
c
t
u
r
e
d
e
s
i
g
n
f
l
o
w
,
a
n
d
l
i
n
k
s
c
o
m
p
u
t
e
r
a
r
c
h
i
t
e
c
t
s
t
o
a
c
c
e
s
s
i
b
l
e
f
o
r
m
a
l
-
m
e
t
h
o
d
s
t
o
o
l
s
.
“
C
o
n
s
t
a
n
t
-
t
i
m
e
P
r
o
g
r
a
m
”
W
I
L
L
r
u
n
i
n
C
o
n
s
t
a
n
t
-
t
i
m
e
i
n
H
a
r
d
w
a
r
e
Hello everyone, I’m Yuheng Yang. Today I will talk about our recent work, Pensieve: Microarchitectural Modeling for Formal Security Evaluation.
Basically, the security is targeting speculative execution attacks.
It is a joint work by me, Thomas, Stella, and Mengjia.
I am very happy to present this work to our post-quantum side-channel analysis workshop.
Because I hope can give you a sense why the microarchitecutre, the speculation scheme would play such an important role to achieve side-channel free, or to achieve constant-time cryptography program.
To start, what is the role of the microarchitecture here?
Isn’t all programmers’ job to guarantee the program runs in constant time?
This content discusses the challenges and defenses in evaluating formal security for microarchitectural modeling. It covers topics such as constant-time programs, speculative machines, post-quantum cryptography, side-channel attacks, and defense proposals against vulnerabilities like Spectre and GhostMinion. The aim is to bridge the gap between defenses and evaluation tools to ensure robust security measures. Various models and observation techniques are explored to enhance the security evaluation process, emphasizing the need for trustworthy security evaluation tools.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Pensieve: Microarchitectural Modeling for Formal Security Evaluation Yuheng Yang, Thomas Bourgeat, Stella Lau, Mengjia Yan To appear at ISCA 23
Constant-time Program might not run in Constant-time in Hardware Constant-time on Sequential Machine Not Constant-time Speculative Machine Never branch on Secrets for i in range(n): if pub[i] == 0: // side-effects-1 else: // side-effects-2 for i in range(n): if sec[i] == 0: // side-effects-1 else: // side-effects-2 Pub[n] can be leaked! 2 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Problem: the Cat-and-Mouse Game Spectre 2018 InvisiSpec Delay-on-Miss 2019 Spectre rewind Speculative interference 2020 GhostMinion 2021 3 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Problem: Weak Security Evaluation Step 1: Step 2: The defense works for all possible Spectre gadget. Defense Proposal Spectre Gadget We need a principled, trustworthy security evaluation tool! 4 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Background: Formal Security Property Only consider constant-time program Avoid secret affecting Execution Time Cache footprint Speculative Non-Interference Property: ????,??????,??? ???, IF ???????????(????) THEN?????????(????,??????) = ?????????(????,??? ???) Observation Models IF??????? ????,?????? = ??????? (????,??? ???) 5 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Challenge: Bridge the Gap Defenses Evaluation Tools Rosette Delay-on-Miss SafeSpec Model JasperGold invisiSpec CVC5 Boolector Muontrap Coq z3 GhostLoads Isabelle/HOL GhostMinion ACL2 Aligned with architectural design flow. 6 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Defense Design flow Fetch Decode & Rename Example: delay speculative requests Memory Dispatch An architecture modeling method should be 1. Modular 2. Precise on describing timing behaviors 3. Represent a space of designs Commit 7 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Pensieve Modeling Decouple timing and functionality using the hand-shaking interface Represent a space of timing behavior in_valid out_valid in_ready out_ready M[addr] M[addr] Func addr timing signals Time functional signals Memory System An architecture modeling method should be 1. Modular 2. Precise on describing timing behaviors 3. Represent a space of designs 8 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Uninterpreted Function (UF) A UF represents space of functions with the same input/output types Example: Bool UF(Bool, Bool) UF helps us state what affects the output, abstract away the details on how the input affects the output represents Unspecified function body AND OR 9 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Pensieve Modeling: Using UFs Examples: Multiply_req_latency = UF(historyOf(in_valid)) Multiply_req_latency = UF(historyOf(in_valid, in_operands)) Memory_req_latency = UF(historyOf(in_valid, in_addr)) Pensieve can use simple models to cover space of microarchitectures with complex timing behaviors 10 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Pensieve Modeling Decouple timing and functionality using the hand-shaking interface Represent a space of timing behavior with uninterpreted functions in_valid out_valid UF in_ready out_ready M[addr] M[addr] Func addr timing signals Time functional signals Memory System 11 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Pensieve Security Evaluation Framework Security Property (Speculative Non-interference) FAIL: Attack Program Model Checker Micro-Arch Model PASS: Security for k Cycles Pensieve finds unknown security vulnerabilities in the latest speculative execution defense, i.e., GhostMinion [2021] 12 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
GhostMinion #1: Invisible Speculation Insecure Baseline Invisible Speculation Spectre v1 s s Core Core if (false) ld sec //transmitter Invisible Buffer L1 L1 Rest of Memory System Rest of Memory System 13 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Speculative Interference Attack Younger speculative loads interfere with older bound-to-commit loads. Many other contention structures: non-pipelined ALU, cache port, bank contention, network-on-chip, etc. Invisible Speculation y Core s x y = //delay Invisible Buffer L1 ld y // transmitter MSHR s x if (false) ld sec // interfere Rest of Memory System 14 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
GhostMinion #1: Invisible Speculation #2: Prioritize Older Instructions through Timestamps y Timestamp (based on decode time) 1 Core speculative interference attack s y = //delay 0 3 Invisible Buffer L1 ld y //transmitter 1 MSHR s y if (false) 2 3 1 ld sec //interfere 3 Rest of Memory System 15 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
So Far Spectre 2018 InvisiSpec Delay-on-Miss 2019 Spectre rewind Speculative interference attack 2020 GhostMinion 2021 Use Pensieve 16 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Pensieve Found A New Attack Variant Timestamp (before squash) Timestamp (after squash) 0 mispredict 0 if (true) 2 ld y // transmitter else ld sec // interfere 1 1 squash Speculative load is older this time! Speculative load can interfere with bound-to-commit load 17 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
New Attack on GhostMinion Summary new attack variant speculative interference attack y = if (true) Older ld y // transmitter ld y // transmitter if (false) else ld sec // interfere No Order ld sec // interfere Younger Takeaway: Manual evaluation can easily be unsound, we need Pensieve, a trustworthy evaluation tool 18 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Checking Time and Scalability Microarchitecture Setup 5 types of instructions 4-entry register file 4-entry data memory 16-entry instruction memory 8-entry ROB GhostMinion defense Problem: Checking time increases exponentially as the number of simulated cycles increases Future work: Combine Penseive with more powerful formal verification backend ROB Size = 16 ROB Size = 8 ROB Size = 4 ROB Size = 2 no counterexample no counterexample counterexample ROB Size = 16 counterexample ROB Size = 8 ROB Size = 4 ROB Size = 2 no counterexample counterexample ROB Size = 8 Checking Time (min) 104 104 104 104 Checking Time (min) 104 104 104 104 104 Checking Time (min) 104 104 104 103 103 103 103 103 103 103 103 103 103 103 103 100 100 100 100 100 100 100 100 100 100 100 100 10 10 10 10 10 10 10 10 10 1 1 1 1 10 10 10 1 1 1 1 1 0.1 0.1 0.1 0.1 1 1 1 0.1 0.1 0.1 0.1 0.1 4 5 6 7 8 9 4 5 6 7 8 9 4 5 6 7 8 9 4 5 6 7 8 9 0.1 0.1 0.1 Simulated Cycle (a) Baseline O3 Processor 4 5 Simulated Cycle (b) Delay-on-miss 4 Simulated Cycle (c) Invisible Speculation 8 9 Simulated Cycle (d) GhostMinion 8 4 4 5 5 6 6 7 7 8 9 9 4 5 6 7 8 9 4 5 6 7 8 9 4 5 6 7 8 9 4 5 6 7 8 9 6 7 8 9 5 6 7 Simulated Cycle (a) Baseline O3 Processor (d) GhostMinion Simulated Cycle (b) Delay-on-miss Simulated Cycle (c) Invisible Speculation Simulated Cycle (d) GhostMinion Simulated Cycle (a) Baseline O3 Processor Simulated Cycle (b) Delay-on-miss Simulated Cycle (c) Invisible Speculation Simulated Cycle 19 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
Pensieve Summary Pensieve provides a modeling principle that aligns with architecture design flow, and links computer architects to accessible formal-methods tools. Security Property (Speculative Non-interference) FAIL: Attack Program Model Checker Micro-Arch Model PASS: Security for k Cycles Constant-time Program WILL run in Constant-time in Hardware 20 FCCM 2023 Workshop: Post-Quantum Cryptography Side-channel Attack Analysis
