一句话：提出 AMuLeT，首个在设计阶段于模拟器中自动测试安全推测防御并发现漏洞的工具。
多种缓解 Spectre 攻击的硬件防御事后被证明不安全，需要能在设计早期自动测试其安全保证的工具。本文提出 AMuLeT，首个可在微架构模拟器的设计阶段测试安全推测防御的工具。其核心是将检测商用 CPU 推测泄漏的模型驱动关系测试工具迁移到模拟器，并解决攻击者观察模型、仿真速度和微架构状态搜索等挑战。AMuLeT 将测试吞吐量提升 10 倍以上，并用漏洞放大技术在有限预算内发现泄漏。对 InvisiSpec、CleanupSpec、STT、SpecLFB 的测试在 3 小时内发现 3 个已知和 6 个未知缺陷，并首次证明 SpecLFB 开源实现不安全。
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.
@inproceedings{FuTAKGAGSOS25,
title = {AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures},
author = {Bo Fu and Leo Tenenbaum and David Adler and Assaf Klein and Arpit Gogia and Alaa R. Alameldeen and Marco Guarnieri and Mark Silberstein and Oleksii Oleksenko and Gururaj Saileshwar},
booktitle = {ASPLOS},
year = {2025},
doi = {10.1145/3676641.3716247}
}