Pensieve: Microarchitectural Modeling for Security Evaluation
Traditional modeling approaches in computer architecture aim to obtain an accurate estimation of performance, area, and energy of a processor design. With the advent of speculative execution attacks and their security concerns, these traditional modeling techniques fall short when used for security...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Published: |
Massachusetts Institute of Technology
2024
|
| Online Access: | https://hdl.handle.net/1721.1/153853 https://orcid.org/0000-0001-8695-5139 |
| _version_ | 1826209816232591360 |
|---|---|
| author | Yang, Yuheng |
| author2 | Yan, Mengjia |
| author_facet | Yan, Mengjia Yang, Yuheng |
| author_sort | Yang, Yuheng |
| collection | MIT |
| description | Traditional modeling approaches in computer architecture aim to obtain an accurate estimation of performance, area, and energy of a processor design. With the advent of speculative execution attacks and their security concerns, these traditional modeling techniques fall short when used for security evaluation of defenses against these attacks.
This thesis presents Pensieve, a security evaluation framework targeting early-stage microarchitectural defenses against speculative execution attacks. At the core, it introduces a modeling discipline for systematically studying early-stage defenses. This discipline allows us to cover a space of designs that are functionally equivalent while precisely capturing timing variations due to resource contention and microarchitectural optimizations. We implement a model checking framework to automatically find vulnerabilities in designs. We use Pensieve to evaluate a series of state-of-the-art invisible speculation defense schemes, including Delay-on-Miss, InvisiSpec, and GhostMinion, against a formally defined security property, speculative non-interference. Pensieve finds Spectre-like attacks in all those defenses, including a new speculative interference attack variant that breaks GhostMinion, one of the latest defenses. |
| first_indexed | 2024-09-23T14:31:22Z |
| format | Thesis |
| id | mit-1721.1/153853 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T14:31:22Z |
| publishDate | 2024 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1538532024-03-22T03:22:01Z Pensieve: Microarchitectural Modeling for Security Evaluation Yang, Yuheng Yan, Mengjia Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Traditional modeling approaches in computer architecture aim to obtain an accurate estimation of performance, area, and energy of a processor design. With the advent of speculative execution attacks and their security concerns, these traditional modeling techniques fall short when used for security evaluation of defenses against these attacks. This thesis presents Pensieve, a security evaluation framework targeting early-stage microarchitectural defenses against speculative execution attacks. At the core, it introduces a modeling discipline for systematically studying early-stage defenses. This discipline allows us to cover a space of designs that are functionally equivalent while precisely capturing timing variations due to resource contention and microarchitectural optimizations. We implement a model checking framework to automatically find vulnerabilities in designs. We use Pensieve to evaluate a series of state-of-the-art invisible speculation defense schemes, including Delay-on-Miss, InvisiSpec, and GhostMinion, against a formally defined security property, speculative non-interference. Pensieve finds Spectre-like attacks in all those defenses, including a new speculative interference attack variant that breaks GhostMinion, one of the latest defenses. S.M. 2024-03-21T19:10:46Z 2024-03-21T19:10:46Z 2024-02 2024-02-21T17:10:21.546Z Thesis https://hdl.handle.net/1721.1/153853 https://orcid.org/0000-0001-8695-5139 In Copyright - Educational Use Permitted Copyright retained by author(s) https://rightsstatements.org/page/InC-EDU/1.0/ application/pdf Massachusetts Institute of Technology |
| spellingShingle | Yang, Yuheng Pensieve: Microarchitectural Modeling for Security Evaluation |
| title | Pensieve: Microarchitectural Modeling for Security Evaluation |
| title_full | Pensieve: Microarchitectural Modeling for Security Evaluation |
| title_fullStr | Pensieve: Microarchitectural Modeling for Security Evaluation |
| title_full_unstemmed | Pensieve: Microarchitectural Modeling for Security Evaluation |
| title_short | Pensieve: Microarchitectural Modeling for Security Evaluation |
| title_sort | pensieve microarchitectural modeling for security evaluation |
| url | https://hdl.handle.net/1721.1/153853 https://orcid.org/0000-0001-8695-5139 |
| work_keys_str_mv | AT yangyuheng pensievemicroarchitecturalmodelingforsecurityevaluation |