AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures

Bo Fu, Leo Tenenbaum, David Adler, Assaf Klein, Arpit Gogia, Alaa R. Alameldeen and 4 others

Chipmakers keep proposing hardware fixes for Spectre — the attack that steals secrets by exploiting a CPU's habit of guessing ahead — and those fixes keep getting broken within months; this work from Toronto and collaborators builds AMuLeT, the first tool that automatically stress-tests such defenses while they are still prototypes in a simulator, by running random programs and checking whether the chip ever leaks more than a formal rulebook allows, and it uncovered nine bugs and vulnerabilities across four published defenses in just three hours.

The argument in one glance

Problem

Hardware Spectre defenses keep being proposed, and keep being broken

Spectre attacks exploit a CPU running ahead on guesses to leak secrets through microarchitectural side channels. Architects propose many secure-speculation defenses, but a great many are shown insecure within months, even ones from CPU makers. There is no easy way to test a defense early, so flaws are found only after publication.
What people did

Test defenses with formal methods or hardware-description tools

Use formal-methods approaches to prove properties about a countermeasure, or use hardware-description testing tools that check a design once it is written in a hardware description language.
Why it fell short

Both miss the design phase where defenses are prototyped

Formal methods require rewriting the countermeasure in a special modeling language and deep expertise, which most architects lack. Hardware-description testing tools only apply after a design is written in a hardware description language — far too late, since defenses are first prototyped in microarchitectural simulators. Neither tests a simulator prototype easily and early.
This paper's idea

Test defenses in the simulator against a leakage contract (AMuLeT)

AMuLeT is the first tool to test secure-speculation defenses at design time, inside microarchitectural simulators. It adapts model-based relational testing — which found leaks in real CPUs — to simulators: it runs random programs on both an ISA-level leakage contract and the simulated defense, and flags any leak beyond what the contract allows. It grounds the attacker in a realistic cache-and-TLB observer, runs tests without restarting the simulator for a 10-times speedup, and shrinks structures to surface rare leaks — finding 3 unknown bugs, 3 unknown vulnerabilities, and 3 known ones across four defenses in three hours.

Why this problem is worth solving

Spectre turned a performance trick that every fast CPU relies on into a security hazard, and patching it in hardware has proven treacherous.

Modern processors run fast partly through speculative execution: rather than wait to learn which way a branch will go, the CPU guesses and races ahead, doing work speculatively. If the guess was right, that work is kept; if wrong, the processor discards the architectural results, as if the speculation never happened. The problem is that the speculative work is not entirely erased — it leaves traces in the microarchitectural state, such as which lines are now in the caches or the address-translation buffers. Spectre attacks exploit exactly this: they trick the CPU into speculatively accessing secret data it should never reach, and even though the architectural effects are rolled back, the secret leaks out through a microarchitectural side channel, for example by measuring which cache lines became fast to access. Because speculation is fundamental to CPU performance, this is not a bug in one chip but a hazard in the whole design style. Hardware architects have responded with many secure-speculation countermeasures — invisible speculation, undo-based approaches, tracking speculative data flows — but the track record is sobering: a great many of these defenses have been shown insecure, often within months of publication, and even countermeasures proposed by CPU manufacturers have later been broken.

The reason flaws surface so late is that architects have no good way to test a defense while they are still building it.

To build defenses that actually hold, architects need tools that automatically test a countermeasure’s security, and to be adopted such a tool must satisfy two requirements. First, it must be usable early, during the design phase, because the large majority of secure-speculation countermeasures are first prototyped in microarchitectural simulators, so catching flaws there enables rapid iteration. Second, it must be easy to use on existing design artifacts, without demanding deep expertise. Existing tools fail one or the other. Formal-methods approaches can reason rigorously about leaks, but they require formalizing the countermeasure in a dedicated modeling language and specialized skill that most computer architects do not have. Hardware-description testing tools are scalable and enable pre-silicon testing, but they only apply once a design has been written in a hardware description language — too late for the simulator stage where defenses are actually prototyped. A key concept that makes automated testing possible is a leakage contract: an instruction-set-level specification that states, for any program and input, exactly what information a CPU is permitted to leak microarchitecturally. A defense is secure with respect to a contract if it never leaks more than the contract allows; any leak beyond it is a violation, and a candidate vulnerability.

What people did before, and where it broke

Argue a new defense is secure and publish it. Reason informally about why a countermeasure blocks known attacks. Where it broke. Many defenses were broken within months, because informal reasoning misses subtle leaks; security by argument is unreliable here.
Use formal methods to reason about leaks. Apply formal analysis to prove properties of a countermeasure. Where it broke. These require rewriting the countermeasure in a dedicated modeling language and expert skill most architects lack, so they fail the ease-of-use requirement.
Use hardware-description testing tools. Test the design once it is expressed in a hardware description language. Where it broke. They apply only after the design is written in hardware description, far too late for the simulator prototypes where defenses are first built.
The gap. No tool tested a secure-speculation defense automatically, early, inside the microarchitectural simulator where it is prototyped, using a realistic attacker model. Providing that is what AMuLeT does.

How AMuLeT works

From publish-then-get-broken to automated design-time leakage testing

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Turn security into a checkable comparison against a contract. AMuLeT’s core is relational testing: it runs random programs through two things at once — an instruction-set-level leakage contract that says what the CPU is allowed to leak, producing a contract trace, and the simulated defended CPU, producing a microarchitectural trace of what actually leaked — and any information present in the second but not permitted by the first is a contract violation, a candidate vulnerability. Checking a real system’s observed behavior against a precise, formal specification of what it is permitted to do, and treating every discrepancy as a bug to investigate, is the same method the GPU memory-model work covered elsewhere on this site uses, comparing real executions against an exact contract of allowed behaviors so that violations are surfaced mechanically rather than by manual inspection.

Test the defense where and when it is actually built. The crucial move is applying this method inside the microarchitectural simulator, at design time, without intrusive changes to the simulator or the countermeasure — exactly the stage where architects prototype defenses and where earlier tools could not reach. Exercising a hardware design in a fast simulated environment to find its flaws before any silicon exists, so problems are caught during rapid prototyping rather than after fabrication, is the same strategy the pre-silicon fuzzing work covered elsewhere on this site takes, hunting for bugs in a processor design while it is still a simulated model rather than waiting for a manufactured chip.

Make the search fast and make rare leaks appear. Two engineering insights make the approach practical: the real bottleneck is not running a test but restarting the simulator, so AMuLeT keeps the simulator warm and overwrites registers and memory between tests to amortize startup — over a ten-times throughput gain — and, because speculative leaks need contention on microarchitectural resources, it shrinks those structures (fewer cache ways, fewer outstanding-miss slots) to force the contention and make leaks appear. Avoiding a heavy, repeated cold-start cost by keeping a warm instance and reusing it across many requests is the same efficiency the stateful-serverless work covered elsewhere on this site is built on, holding warm state across invocations so that each new request need not pay the full startup price.

Following a defense through an AMuLeT test

Testing a secure-speculation countermeasure for leaks

A trace of one AMuLeT relational test, following the paper's method on a defense implemented in the gem5 simulator.

Step 1 of 5

Pick a defense and a leakage contract

Choose a secure-speculation countermeasure implemented in the simulator and a leakage contract that states exactly what leakage is allowed — for example, only the addresses of loads and stores on the true program path.

The contract is the security specification the defense must meet.

Why it works

Defenses are wrong too often to trust by argument. Because many secure-speculation defenses have been broken within months of publication → arguing that a defense is secure is unreliable → so automatically testing it against a precise leakage model is essential.
A contract turns security into a checkable comparison. Because a leakage contract states exactly what a CPU is allowed to leak → any information the defense leaks beyond it is a violation by definition → so finding vulnerabilities becomes a mechanical trace comparison rather than a manual audit.
Testing must happen where defenses are built. Because architects prototype countermeasures in simulators, not yet in a hardware description → a tool that works in simulators at design time catches flaws earliest → so it fits the workflow that formal and hardware-description tools miss.
Realistic observation makes findings exploitable. Because the attacker model is a snapshot of cache and translation-buffer state, matching real memory-system side channels → the leaks AMuLeT reports correspond to attacks feasible on a real CPU → so the violations are meaningful, not artifacts of an omniscient simulator.
Speed and amplification decide what is found. Because speculative leaks are rare and simulators are slow → amortizing startup for a ten-times throughput gain and shrinking structures to force contention → so many more tests run and rare leaks that would otherwise stay hidden are triggered.

What it costs (trade-offs and scope)

Testing finds bugs; it does not prove their absence. AMuLeT is a testing tool, not a formal proof. Passing its campaign means no violation was found within the tests run, not that the defense is provably secure — undiscovered leaks may remain.
The attacker model bounds what it can find. The default microarchitectural trace captures memory-system (cache and translation-buffer) side channels. Catching other channels, such as those based on branch prediction, requires exposing more state, which the paper supports but at the cost of reduced testing throughput.
The realism of findings depends on the observer model. Violations are only exploitable in practice if the observer model reflects a real attacker; an unrealistically powerful observer could flag leaks that do not correspond to feasible attacks, so the observer must be chosen carefully (as the authors do).
Coverage depends on the random tests. Like any random testing approach, effectiveness depends on generating programs that exercise the vulnerable behavior, aided here by structure-shrinking to amplify contention; a leak that no generated test triggers will be missed.
It targets simulator prototypes. AMuLeT tests countermeasures implemented in microarchitectural simulators. A flaw introduced later, when translating the design to a hardware description or silicon, is outside its scope and would need hardware-description or post-silicon testing.
Findings can reflect the implementation, not only the design. Some discovered issues are implementation bugs in a specific simulator model rather than flaws in the underlying idea; both matter, but distinguishing an implementation bug from a fundamental design vulnerability requires interpretation.

The evaluation

Three ways to test a secure-speculation defense

Property	Formal methods	Hardware-description testing
Works at design time in simulators
Easy to use without special expertise		Moderate
Finds realistic, exploitable leaks
Guarantee offered		Testing
Demonstrated outcome	Not applicable	Not applicable

Three approaches to testing a secure-speculation defense, as framed by the paper. Formal methods can prove properties but require formalizing the countermeasure in a dedicated language and expert skill (failing the ease-of-use requirement). Hardware-description testing tools work pre-silicon but only after a design is written in a hardware description language, too late for the simulator prototypes where defenses are built (failing the early-design requirement). AMuLeT fills the gap: it applies model-based relational testing inside microarchitectural simulators at design time, comparing a program's microarchitectural trace (a realistic cache-and-translation-buffer observer) against an instruction-set-level leakage contract, without intrusive changes. It amortizes simulator startup for over a 10-times throughput gain and shrinks structures to amplify rare leaks. In the first large-scale campaign against four defenses (InvisiSpec, CleanupSpec, STT, and SpecLFB) in the gem5 simulator, it detected Spectre-v1 and Spectre-v4 in an unprotected CPU within minutes and, within three hours, found 3 unknown implementation bugs, 3 unknown design vulnerabilities, and confirmed 3 known vulnerabilities — including a stronger single-threaded variant of the speculative interference attack and a new Spectre-v1-like flaw in a 2024 defense. As a testing tool, it finds vulnerabilities but does not prove their absence.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

AMuLeT addresses a genuinely painful gap: secure-speculation defenses are notoriously hard to get right — many are broken within months of publication — yet architects had no easy way to test them at the stage where they are actually built, in microarchitectural simulators. The insight is to take model-based relational testing, which had found speculative leaks in commercial CPUs, and bring it to simulators without intrusive changes. The method is clean: run random programs against both a leakage contract (what the CPU may leak) and the simulated defense (what it actually leaks), and any excess leakage is a violation. Three practical contributions make it work — a realistic attacker model based on a cache-and-translation-buffer snapshot so the leaks it finds are exploitable, a testing harness that keeps the simulator warm across tests for over a ten-times throughput gain, and shrinking microarchitectural structures to force the contention rare leaks need. The payoff is concrete and impressive: a first large-scale campaign against four published defenses that, in three hours, found nine issues — three previously unknown implementation bugs, three previously unknown design vulnerabilities, and three confirmed known ones — including breaking one defense in a single-threaded setting where prior attacks needed multiple threads, and a new Spectre-like flaw in a defense from 2024. Read the scope precisely. AMuLeT is a testing tool: it finds bugs but does not prove their absence; what it can find is bounded by its attacker model (memory-system channels by default, more at a throughput cost) and by whether its random tests exercise the vulnerable behavior; it targets simulator prototypes, so flaws introduced later in hardware description or silicon are out of scope; and some findings are implementation bugs rather than fundamental design flaws. The durable idea is that a security defense should be adversarially and automatically tested from the moment it is prototyped, because in this domain confident reasoning is repeatedly proven wrong.

Background

Why adversarial testing against a contract belongs early in the design

It helps to see AMuLeT within a broad and recurring lesson: for properties that are easy to get subtly wrong — security, correctness, consistency — the reliable path is not to argue that a design is right but to test it, automatically and adversarially, against a precise specification, and to do so as early as possible. Here the specification is a leakage contract and the property is the absence of unexpected speculative leaks, but the shape is familiar. The hardware side-channel work covered elsewhere on this site studies the same underlying hazard from the attacker’s side, showing how ordinary performance features of a processor can quietly leak secret data unless the design is specifically checked and hardened against it. The common thread is that microarchitectural optimizations — speculation, data-dependent shortcuts, caching — create leakage paths that human reasoning routinely overlooks, so systematic, automated checking against an explicit model of allowed behavior is what actually catches them. AMuLeT adds two lessons worth carrying: that such checking must meet designers where they work, inside the simulators they prototype in, rather than demanding they adopt a new formalism or wait for silicon; and that the practical obstacles to testing — speed and the rarity of the bug — are themselves engineering problems worth solving, through warm reuse and deliberate stress amplification. As speculation and specialization make processors ever more complex, testing defenses this way, this early, is likely to become standard practice rather than the exception.

If you remember only three things

1. Spectre attacks exploit speculative execution — a CPU guessing which way branches go and running ahead — to trick the processor into speculatively touching secret data and leaking it through microarchitectural side channels like cache timing, even though the architectural effects are rolled back. Hardware architects have proposed many secure-speculation defenses, but a great many are broken within months, even ones from CPU makers. The reason flaws surface so late is that there was no tool to test a defense early: formal methods need the countermeasure rewritten in a special language and expert skill, and hardware-description testing tools only apply after a design is written in a hardware description language — too late for the simulator prototypes where defenses are actually built.
2. AMuLeT is the first tool to test secure-speculation defenses at design time inside microarchitectural simulators. It adapts model-based relational testing (which found leaks in real CPUs): it runs random programs on both an instruction-set-level leakage contract, which specifies exactly what the CPU may leak, and the simulated defended CPU, and flags any leak beyond the contract as a violation and candidate vulnerability. Three contributions make it work: a realistic attacker model built from a snapshot of the final cache and address-translation-buffer state (so leaks are exploitable, extensible to branch-prediction channels at a throughput cost), a harness that runs tests without restarting the simulator by overwriting registers and memory (amortizing the dominant startup cost for over a 10-times throughput gain), and shrinking microarchitectural structures (fewer cache ways, fewer outstanding-miss slots) to force the contention that speculative leaks need.
3. In the first large-scale campaign against four defenses (InvisiSpec, CleanupSpec, STT, and SpecLFB) in the gem5 simulator, AMuLeT detected Spectre-v1 and Spectre-v4 in an unprotected CPU within minutes and, within three hours, found 3 previously unknown implementation bugs, 3 previously unknown design vulnerabilities, and confirmed 3 known ones — including a stronger single-threaded variant of the speculative interference attack (prior attacks needed multiple threads) and a new Spectre-v1-like flaw in a 2024 defense caused by an undocumented optimization. It was responsibly disclosed and open-sourced. Scope: it is a testing tool that finds bugs but does not prove their absence, its reach is bounded by the attacker model and the random tests, it targets simulator prototypes, and some findings are implementation bugs rather than design flaws. The durable lesson is that security defenses should be adversarially and automatically tested against a precise contract from the moment they are prototyped.

Check yourself

Check your understanding

1. How do Spectre attacks leak secrets despite speculative work being rolled back?
2. What is a leakage contract, and how does AMuLeT use it to test a defense?
3. Why is AMuLeT designed to work inside microarchitectural simulators at design time?
4. What did AMuLeT actually find, and what does that demonstrate?

Sources

The paper is “AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures” by Bo Fu, Leo Tenenbaum, David Adler, Assaf Klein, Arpit Gogia, Alaa R. Alameldeen, Marco Guarnieri, Mark Silberstein, Oleksii Oleksenko, and Gururaj Saileshwar, published at ASPLOS 2025, DOI 10.1145/3676641.3716247. The authors are affiliated with the University of Toronto, the Technion, Microsoft, IMDEA Software Institute, and Simon Fraser University.

This explainer is based on the full text of the paper, obtained from the authors’ open-access arXiv version (arXiv:2503.00145). The problem framing (Spectre attacks exploiting speculative execution to leak secrets through microarchitectural side channels, the repeated breaking of proposed hardware countermeasures, and the two requirements that a testing tool be usable early in the design phase and easy to use, which formal methods and hardware-description testing tools respectively fail), the method (adapting model-based relational testing from tools like Revizor to microarchitectural simulators; leakage contracts and the CT-SEQ, CT-COND, and ARCH-SEQ contracts; the model producing contract traces and the executor producing microarchitectural traces; and contract violations as candidate vulnerabilities), the three challenges and their solutions (the realistic cache-and-translation-buffer observer model and its extensibility to branch-prediction channels; the testing harness that amortizes simulator startup for over a ten-times throughput improvement; and the shrinking of microarchitectural structures to amplify contention), and the evaluation results (the campaign against InvisiSpec, CleanupSpec, STT, and SpecLFB in gem5; the detection of Spectre-v1 and Spectre-v4 in an unprotected CPU within minutes; the discovery of 3 unknown implementation bugs, 3 unknown design vulnerabilities, and 3 confirmed known vulnerabilities within three hours; the single-threaded variant of the speculative interference attack against InvisiSpec; and the new Spectre-v1-like vulnerability in SpecLFB) are all drawn directly from the paper. The tool is open-sourced by the authors. Background explanations of speculative execution, side channels, leakage contracts, and microarchitectural simulation are standard and provided to make the paper’s contribution understandable.