Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures

Bo Fu, Leo Tenenbaum, David Adler, Assaf Klein, Arpit Gogia, Alaa R. Alameldeen, Marco Guarnieri, Mark Silberstein, Oleksii Oleksenko, Gururaj Saileshwar

TL;DR

AMuLeT introduces the first design-time tool for automatically testing secure speculation countermeasures inside cycle-accurate simulators. By adapting model-based relational testing (Revizor) to μ-architectural simulators, it uses a leakage contract and an executor to detect violations where contract traces diverge from actual μ-architectural traces, thereby revealing exploitable leaks. Through large-scale campaigns against InvisiSpec, CleanupSpec, STT, and SpecLFB, AMuLeT uncovers multiple known and unknown vulnerabilities within hours and demonstrates the open-source framework and methodology for rapid defense evaluation. The approach accelerates secure-countermeasure prototyping, highlights previously undiscovered weaknesses, and provides a practical path toward more robust hardware defenses before silicon implementation. AMuLeT’s open-source availability and modular design facilitate broader adoption for next-generation speculative defenses across ISAs and simulators.

Abstract

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.

AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures

TL;DR

AMuLeT introduces the first design-time tool for automatically testing secure speculation countermeasures inside cycle-accurate simulators. By adapting model-based relational testing (Revizor) to μ-architectural simulators, it uses a leakage contract and an executor to detect violations where contract traces diverge from actual μ-architectural traces, thereby revealing exploitable leaks. Through large-scale campaigns against InvisiSpec, CleanupSpec, STT, and SpecLFB, AMuLeT uncovers multiple known and unknown vulnerabilities within hours and demonstrates the open-source framework and methodology for rapid defense evaluation. The approach accelerates secure-countermeasure prototyping, highlights previously undiscovered weaknesses, and provides a practical path toward more robust hardware defenses before silicon implementation. AMuLeT’s open-source availability and modular design facilitate broader adoption for next-generation speculative defenses across ISAs and simulators.

Abstract

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.

Paper Structure

This paper contains 41 sections, 9 figures, 11 tables.

Table of Contents

  1. Introduction
  2. Background: Testing for speculative leaks
  3. Leakage contracts modeling speculative leaks
  4. Modeling attackers in speculation-based attacks
  5. Detecting unexpected leakages
  6. Model-based relational testing: Revizor
  7. AMuLeT Design
  8. Overview of AMuLeT
  9. Test Generator.
  10. Leakage Model
  11. Executor
  12. $\mu$arch Trace Design - Challenges and Solutions
  13. Analyzing Violations
  14. Amplifying Leakages in Simulators
  15. Implementation
  16. ...and 26 more sections

Figures (9)

  • Figure 1: Overview of AMuLeT. We leverage the test-generation and leakage models from prior works revizorHideSeekSpectrehofmann2023SpecAtFault and design a new executor in AMuLeT capable of testing target defenses in a $\mu$arch simulator.
  • Figure 2: Design of $\mu$arch trace extraction in AMuLeT-Opt.
  • Figure 3: Analyzing violations discovered with AMuLeT.
  • Figure 4: Example of Test Asm Causing Violation in InvisiSpec due to Speculative L1D-cache Evictions.
  • Figure 5: Bug in InvisiSpec's Gem5 implementation discovered by AMuLeT that leaks addresses of speculative loads via L1D-cache evictions and breaks its security guarantees.
  • ...and 4 more figures

Theorems & Definitions (1)

  • definition 1: Contract violation hw_sw_contracts