AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912253158096896 |
|---|---|
| author | Fu, Bo Tenenbaum, Leo Adler, David Klein, Assaf Gogia, Arpit Alameldeen, Alaa R. Guarnieri, Marco Silberstein, Mark Oleksenko, Oleksii Saileshwar, Gururaj |
| author_facet | Fu, Bo Tenenbaum, Leo Adler, David Klein, Assaf Gogia, Arpit Alameldeen, Alaa R. Guarnieri, Marco Silberstein, Mark Oleksenko, Oleksii Saileshwar, Gururaj |
| contents | In recent years, several hardware-based countermeasures proposed to mitigate Spectre attacks have been shown to be insecure. To enable the development of effective secure speculation countermeasures, we need easy-to-use tools that can automatically test their security guarantees early-on in the design phase to facilitate rapid prototyping. This paper develops AMuLeT, the first tool capable of testing secure speculation countermeasures for speculative leakage early in their design phase in simulators. Our key idea is to leverage model-based relational testing tools that can detect speculative leaks in commercial CPUs, and apply them to micro-architectural simulators to test secure speculation defenses. We identify and overcome several challenges, including designing an expressive yet realistic attacker observer model in a simulator, overcoming the slow simulation speed, and searching the vast micro-architectural state space for potential vulnerabilities. AMuLeT speeds up test throughput by more than 10x compared to a naive design and uses techniques to amplify vulnerabilities to uncover them within a limited test budget. Using AMuLeT, we launch for the first time, a systematic, large-scale testing campaign of four secure speculation countermeasures from 2018 to 2024--InvisiSpec, CleanupSpec, STT, and SpecLFB--and uncover 3 known and 6 unknown bugs and vulnerabilities, within 3 hours of testing. We also show for the first time that the open-source implementation of SpecLFB is insecure. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_00145 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures Fu, Bo Tenenbaum, Leo Adler, David Klein, Assaf Gogia, Arpit Alameldeen, Alaa R. Guarnieri, Marco Silberstein, Mark Oleksenko, Oleksii Saileshwar, Gururaj Cryptography and Security Hardware Architecture In recent years, several hardware-based countermeasures proposed to mitigate Spectre attacks have been shown to be insecure. To enable the development of effective secure speculation countermeasures, we need easy-to-use tools that can automatically test their security guarantees early-on in the design phase to facilitate rapid prototyping. This paper develops AMuLeT, the first tool capable of testing secure speculation countermeasures for speculative leakage early in their design phase in simulators. Our key idea is to leverage model-based relational testing tools that can detect speculative leaks in commercial CPUs, and apply them to micro-architectural simulators to test secure speculation defenses. We identify and overcome several challenges, including designing an expressive yet realistic attacker observer model in a simulator, overcoming the slow simulation speed, and searching the vast micro-architectural state space for potential vulnerabilities. AMuLeT speeds up test throughput by more than 10x compared to a naive design and uses techniques to amplify vulnerabilities to uncover them within a limited test budget. Using AMuLeT, we launch for the first time, a systematic, large-scale testing campaign of four secure speculation countermeasures from 2018 to 2024--InvisiSpec, CleanupSpec, STT, and SpecLFB--and uncover 3 known and 6 unknown bugs and vulnerabilities, within 3 hours of testing. We also show for the first time that the open-source implementation of SpecLFB is insecure. |
| title | AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures |
| topic | Cryptography and Security Hardware Architecture |
| url | https://arxiv.org/abs/2503.00145 |