Formal Security Evaluation for Microarchitectural Modeling

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.

• Microarchitectural Modeling
• Formal Security Evaluation
• Constant-time Programs
• Post-Quantum Cryptography
• Side-channel Attacks

msigm Follow

Uploaded on Nov 18, 2024 | 0 Views

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. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Pensieve: Microarchitectural Modeling for Formal Security Evaluation Yuheng Yang, Thomas Bourgeat, Stella Lau, Mengjia Yan To appear at ISCA 23

2. 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

3. 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

4. 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

5. 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

6. 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

7. 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

8. 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

9. 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

10. 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

11. 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

12. 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

13. 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

14. 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

15. 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

16. 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

17. 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

18. 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

19. 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

20. 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