Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants)

Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira and 3 others

Cryptographic code is written to be constant-time so its running time never depends on secret keys, but Spectre attacks defeat this by exploiting the CPU's habit of speculatively executing ahead of a guessed branch or return, briefly touching secrets and leaking them through the cache before the guess is undone; earlier work shielded such code from one Spectre variant (v1) cheaply but left the others, especially Spectre-RSB (which abuses the processor's return-address predictor), unguarded; this paper (MPI-SP and collaborators — Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Gregoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang) protects against all known Spectre variants by replacing returns with branch-based return tables (removing the return prediction entirely) and masking secrets with selective speculative load hardening, backed by a new value-dependent information-flow type system proved sound in Coq, at under 2 percent overhead for most primitives.

The argument in one glance

Problem

Constant-time crypto is undone by the CPU speculating ahead and leaking secrets

High-assurance cryptographic code is written to be constant-time: its timing, its memory accesses, and its branches never depend on secret data, so an attacker watching the cache or the clock learns nothing about the key. That discipline defeats classical timing side channels. But modern CPUs execute speculatively — they guess the outcome of a branch or the target of a return and race ahead before the guess is confirmed, rolling back the architectural state if wrong. The problem is that the mis-guessed, transient execution can touch secret data and leave traces in the cache that survive the rollback. Spectre attacks weaponize this: even code that is perfectly constant-time in its normal execution can, during speculation, be steered into leaking secrets. So the CPU's own performance machinery quietly voids the guarantee the cryptographer worked to establish.
What people did

Harden against Spectre-v1 with selective speculative load hardening

Recent work showed how to protect constant-time code against Spectre-v1 — the variant where a mispredicted conditional branch lets execution run past a bounds check — using selective speculative load hardening. It tracks whether the CPU is currently mis-speculating in a flag and masks secret-derived values while a misprediction is in flight, applying the masking only where needed, at remarkably low overhead (often below 1 percent), and integrating it into the Jasmin high-assurance crypto framework.
Why it fell short

That defends only one variant, and leaves Spectre-RSB wide open

The v1 defense addresses only one class of Spectre attack. There are others, and the most stubborn is Spectre-RSB, which abuses the return stack buffer — a small last-in-first-out hardware structure the CPU uses to predict return addresses. By manipulating or underflowing that buffer, an attacker makes the processor speculatively execute at the wrong return target, once again running transient code that can leak secrets, and the v1 masking does not cover this path. Existing RSB countermeasures are unsatisfying: retpolines rely on assumptions about how the return stack buffer behaves that later work showed to be incorrect, and other schemes rewrite returns without a verified guarantee. What was missing was a single, principled approach that protects constant-time code against all known Spectre variants at once — including RSB — with a proof that it works and an overhead low enough to actually use.
This paper's idea

Remove returns, mask secrets, and prove the whole thing sound

This paper protects cryptographic code against all known Spectre variants with a hybrid approach combining a program transformation and selective speculative load hardening, tied together by a new type system and machine-checked proofs. The transformation eliminates the return instruction entirely: each function's returns are compiled into a return table implemented as branches (nested conditional direct jumps to the possible return sites), so there is no return-stack-buffer prediction left to exploit, killing Spectre-RSB by construction. But turning returns into branches reintroduces the conditional-branch speculation that Spectre-v1 exploits, so those branches are then hardened with selective speculative load hardening — masking secret values with a misspeculation flag updated by non-speculating conditional moves. To guarantee correctness, the authors design a value-dependent information-flow type system ensuring no secret leaks even under speculation (the property called speculative constant-time), prove its soundness and the compiler transformation's correctness in the Coq proof assistant, and implement it in Jasmin. The overhead of all Spectre protections together stays below 2 percent for most primitives and only 5 to 7 percent for the post-quantum key-encapsulation mechanism Kyber.

Why this problem is worth solving

Constant-time cryptography is the foundation the whole field of secure implementation rests on, and Spectre pulls that foundation out.

Cryptographic algorithms can be mathematically strong yet leak their secrets through how they run. If the time a routine takes, or which memory addresses it touches, or which way it branches, depends on the secret key, then an attacker who measures those things — often just by observing cache timing — can recover the key without breaking the math. Constant-time programming is the discipline that forbids exactly this: secrets must never influence timing, memory-access patterns, or control flow, so the observable behavior is the same regardless of the key. Implemented carefully, this closes classical timing side channels and is the accepted gold standard for real cryptographic code. Spectre attacks break the assumption underneath it. A constant-time program is constant-time in its intended, architectural execution; but a modern processor also executes speculatively, guessing ahead and running transient instructions that are discarded if the guess was wrong. During that transient window the processor can execute paths the program never architecturally takes — reading secret data and encoding it into the cache — and although the architectural results are rolled back, the cache traces are not, so the secret leaks. In effect Spectre lets an attacker run a little of your code under different, adversarially chosen control flow, defeating the very constant-time property you established, which is why protecting against it is essential to keep cryptographic software actually secure on real hardware.

The reason a piecemeal defense is not enough is that leaving any variant open leaves the secret exposed.

Spectre is not a single bug but a family, because a modern CPU has several predictors, and each is a way to steer speculative execution. Spectre-v1 mispredicts conditional branches (for example, running past a bounds check); other variants mispredict indirect jumps or, in the case of Spectre-RSB, return addresses. From a defender’s standpoint this is unforgiving: a secret protected against v1 but reachable through the return-address predictor is still a leaked secret, so a real guarantee must cover every known avenue at once, not just the most famous one. Spectre-RSB is particularly awkward because it targets the return stack buffer, a small last-in-first-out structure that caches recent return addresses to predict where a function will return. An attacker can drive the CPU to mispredict a return — by overflowing or underflowing that buffer, or otherwise manipulating it — so that execution speculatively continues at a return site of the attacker’s choosing, running transient code there. Countermeasures that depend on assumptions about how this buffer behaves have proven fragile when the hardware does not behave as assumed. So closing Spectre-RSB in a way that does not rest on delicate hardware assumptions, while simultaneously keeping the other variants closed and the overhead low, is the specific and genuinely hard problem this work takes on, and solving it is what lets constant-time cryptography survive on speculating processors.

What people did before, and where it broke

Fences everywhere. Insert speculation barriers (lfence) liberally so the CPU cannot run ahead into secret-touching code. Where it broke. Barriers serialize execution and are very expensive if applied broadly, so blanket fencing carries overheads too high for practical cryptographic code.
Selective speculative load hardening for v1. Track mis-speculation in a flag and mask secret values only where needed, protecting against Spectre-v1 at very low cost. Where it broke. It addresses only one class of Spectre; it does not cover Spectre-RSB or the other variants, so secrets remain reachable through the uncovered predictors.
Retpolines for return and indirect-branch speculation. Replace vulnerable returns/indirect jumps with constructs that steer speculation into a safe trap, relying on how the return stack buffer works. Where it broke. Later work showed the assumptions retpolines make about the return stack buffer are incorrect, so the protection is not reliable.
Return-table schemes (JumpSwitches, Switchpoline). Replace returns and indirect jumps with tables of allowed targets to avoid the vulnerable predictors. Where it broke. They remove the RSB path but come without a verified guarantee of speculative security and do not by themselves compose with a proven, low-overhead defense of the remaining variants.
The gap. No approach protected constant-time cryptographic code against all known Spectre variants together — RSB included — with a machine-checked proof of soundness and an overhead low enough for real cryptographic primitives.

How the approach works

Compiling constant-time crypto to be speculative-constant-time against every known variant

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

The idea

Kill the return-address predictor by having no returns to predict. The cleverest move is structural: Spectre-RSB exists only because the CPU predicts return addresses using the return stack buffer, so the paper removes the target of the attack rather than trying to outwit the predictor. The compiler transforms every function return into a return table built from ordinary conditional direct jumps to the possible return sites, keeping the return address in a dedicated register. Because there are no return instructions left, the return stack buffer is never consulted, and Spectre-RSB is eliminated by construction rather than by fragile assumptions about how the buffer behaves. Rewriting a program at compile time so that a dangerous construct is replaced by a safe equivalent, provably preserving behavior while removing the vulnerability, is the same compiler-transformation-for-security discipline the work on a compiler for vectorizing encrypted arithmetic circuits covered elsewhere on this site embodies, reshaping the generated code to meet a cryptographic goal. Here the goal is that no return prediction can ever be misused.

Compose two defenses so each covers the other’s residue. Removing returns is not free: turning them into conditional branches reintroduces exactly the branch misprediction that Spectre-v1 exploits. The paper embraces this and pairs the transformation with selective speculative load hardening, which masks secret values whenever the CPU is mis-speculating, tracked by a misspeculation flag updated with non-speculating conditional moves. So the two techniques interlock — the transformation closes RSB and shifts the risk to branches, and the hardening closes those branches — and together they cover all known variants. Ensuring that secret information cannot flow to an observable channel even along paths the program does not intend to take is the same information-flow, non-interference reasoning the work on information flow control for privacy-preserving data processing covered elsewhere on this site is built on, guaranteeing that what an attacker can observe is independent of the secret. This paper enforces that independence specifically across speculative execution, the channel Spectre opens.

Make the guarantee a theorem, not a hope. Security patches for speculation are notoriously easy to get subtly wrong, so the paper does not merely implement the defense; it defines precisely what security means — speculative constant-time, no secret leak even under speculation — and builds a value-dependent information-flow type system whose well-typed programs provably have that property, then machine-checks both the type system’s soundness and the compiler transformation’s correctness in the Coq proof assistant. Establishing a program property by rigorous, formal reasoning rather than testing, so the guarantee holds for all executions rather than the ones you happened to try, is the same assurance-through-analysis ambition the work on precise invariant-guided pointer analysis covered elsewhere on this site pursues, proving a property of the code by construction. Here the machine-checked proofs are what let the authors claim protection against all known Spectre variants with confidence, not just against the ones they tested.

Following a function through the defense

Compiling and running a hardened cryptographic function on a speculating CPU

A trace, drawn from the paper, of how a constant-time function is transformed and hardened so it stays secure under speculation.

Step 1 of 5

A constant-time function that returns to its caller

The function is constant-time at the architectural level, but it ends in a return whose target the CPU predicts using the return stack buffer, and it may branch internally — both are speculation points an attacker could steer to leak secrets.

Constant-time protects normal execution, not the transient execution Spectre induces.

Why it works

Removing returns removes the RSB attack surface. Spectre-RSB works only by mispredicting return-stack-buffer entries → but compiling returns into branch-based return tables means no returns are executed → so there is no return prediction left for an attacker to poison.
Selective hardening neutralizes secrets during any misprediction. A mispredicted branch can run transient code that touches secrets → but a misspeculation flag masks secret values whenever speculation is wrong → so even transient execution sees neutralized data and leaks nothing.
The two defenses compose to cover every known variant. The transformation shifts the RSB risk onto conditional branches → but selective hardening already closes conditional-branch leakage → so RSB and v1-style paths are both covered with no gap between them.
A value-dependent type system is precise enough to be cheap. A crude analysis would over-mask and inflate overhead → but tracking security levels that depend on runtime values masks only genuine secrets → so protection stays below a few percent instead of serializing everything.
Machine-checked proofs make the guarantee trustworthy. Hand-argued speculation defenses are easy to get subtly wrong → but proving the type system sound and the transformation correct in Coq covers all executions → so the claim of protecting against all known variants is verified, not merely tested.

What it costs (trade-offs and scope)

It protects against all known Spectre variants, not unknown future ones. The guarantee is precisely stated and proved, but it is relative to the known classes of Spectre attacks and the model of speculation used; a genuinely new speculation channel outside that model would need the model and proofs extended.
The return-table transformation has structural requirements. Replacing returns with branch-based tables uses a dedicated return-address register and a known set of return sites, and the paper notes restrictions on this scheme; it fits the structured, high-assurance setting of Jasmin rather than arbitrary unstructured binaries.
There is a real, if small, overhead. All Spectre protections together cost below 2 percent for most primitives but 5 to 7 percent for the more complex Kyber; the more branching and secret-handling a primitive has, the more masking and return-table branching it incurs, so cost grows with complexity.
It targets cryptographic code in Jasmin. The approach is designed for constant-time cryptographic primitives written in the Jasmin high-assurance framework, where the constant-time discipline and the type system apply; general-purpose software outside that discipline is not the target, and applying the ideas elsewhere would require the same groundwork.
The proofs cover the type system and transformation, within their assumptions. The Coq development establishes soundness and correctness under a formal model of the hardware’s speculative behavior; the end-to-end guarantee is only as strong as that model’s faithfulness to real processors, which the paper argues for but which remains an assumption.

The evaluation

Protecting constant-time cryptographic code against Spectre

Property	v1-only hardening	Retpoline / return tables	This work
Covers Spectre-v1
Covers Spectre-RSB
All known variants
Formal guarantee
Overhead

A qualitative comparison of Spectre defenses for constant-time cryptography. This work protects against all known Spectre variants (including RSB) with machine-checked Coq proofs, at overhead below 2 percent for most primitives and 5 to 7 percent for the post-quantum scheme Kyber.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This explainer is based on the paper’s full text (the IACR ePrint version, 2024/1070, of the ASPLOS 2025 paper). The mechanism described is the paper’s: to protect constant-time cryptographic code against all known Spectre variants, especially Spectre-RSB, it combines a compiler transformation that replaces returns with branch-based return tables (nested conditional direct jumps, using a dedicated return-address register), eliminating the return-stack-buffer prediction, with selective speculative load hardening that masks secret values using a misspeculation flag updated by non-speculating conditional moves; a new value-dependent information-flow type system certifies the property of speculative constant-time; and the type system’s soundness and the compiler transformation’s correctness are proved in the Coq proof assistant, with the whole approach implemented in the Jasmin framework. The overhead figures are the paper’s own: below 2 percent for most cryptographic primitives and about 5 to 7 percent for the post-quantum key-encapsulation mechanism Kyber. The guarantee is against all known classes of Spectre attacks within the paper’s formal model of speculation; exact type-system rules, the transformation’s restrictions, the threat model, and the full benchmark set should be read from the paper.

Background

Why speculation turned a hardware feature into a security problem

It helps to see this work against the broader story of how micro-architecture became a security battleground. For decades, processor designers added speculative execution, caching, and other performance tricks under the assumption that only architecturally visible state mattered for correctness and security; anything speculative was rolled back and considered invisible. Spectre and its relatives shattered that assumption by showing that speculation leaves micro-architectural traces — in caches, buffers, and predictors — that an attacker can read, so the CPU’s performance features became channels for leaking secrets. This forced a rethink across the stack: hardware makers add mitigations and new instructions, and software must now be written and compiled to be secure not just in its intended execution but in every path speculation might take. Cryptographic code is the sharpest case, because it handles the most sensitive secrets and already invests in the constant-time discipline, so it is both the most exposed and the most worth protecting rigorously. The general lesson that seemingly invisible micro-architectural behavior can leak secrets is the same lesson the work on eavesdropping user credentials via GPU side channels covered elsewhere on this site drives home, exposing how much escapes through channels no one designed to carry information. This paper is a defensive answer for the speculative-execution channel, made rigorous for the code that most needs it.

If you remember only three things

1. Constant-time cryptographic code hides secrets from timing side channels by keeping its timing, memory accesses, and branches independent of the key, but Spectre attacks defeat this by exploiting speculative execution: the CPU guesses branch outcomes and return targets and runs transient code that touches secrets and leaks them through the cache before the guess is rolled back. Prior work protected such code against Spectre-v1 cheaply but left the other variants, especially Spectre-RSB (which abuses the return stack buffer that predicts return addresses), unaddressed.
2. This paper protects against all known Spectre variants with a hybrid approach: a compiler transformation replaces every return with a branch-based return table (nested conditional direct jumps using a dedicated return-address register), so there is no return-stack-buffer prediction to exploit and Spectre-RSB is eliminated by construction; this reintroduces conditional-branch speculation, which is then closed with selective speculative load hardening that masks secret values via a misspeculation flag updated by non-speculating conditional moves. A new value-dependent information-flow type system certifies speculative constant-time, and its soundness and the transformation's correctness are proved in Coq.
3. Implemented in the Jasmin high-assurance framework, the combined protections cost below 2 percent for most primitives and only 5 to 7 percent for the post-quantum scheme Kyber. The guarantee covers all known Spectre classes within a formal model of speculation (not unknown future channels), the return-table transformation has structural requirements, and the approach targets constant-time cryptographic code in Jasmin.

Check yourself

Check your understanding

1. Why do Spectre attacks break constant-time cryptographic code?
2. How does the paper eliminate Spectre-RSB specifically?
3. How do the paper's two techniques work together to cover all known Spectre variants?
4. What did the paper prove and achieve, and what are the limits of its guarantee?

Sources

The paper is “Protecting Cryptographic Code Against Spectre-RSB (and, in Fact, All Known Spectre Variants)” by Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Gregoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, and Zhiyuan Zhang (MPI-SP, IMDEA Software Institute, University of Melbourne, Inria, and collaborators), published at ASPLOS 2025, DOI 10.1145/3676641.3716015. It is licensed CC BY.

This explainer is written from the paper’s full text (the IACR ePrint version, 2024/1070). The paper protects constant-time cryptographic code against all known classes of Spectre attacks, in particular Spectre-RSB (attacks exploiting the return stack buffer). Its approach is hybrid: a compiler transformation replaces returns with return tables implemented as nested conditional direct jumps, using a dedicated return-address register, so that no return instructions are executed and the return stack buffer is never used, eliminating Spectre-RSB; because this reintroduces conditional-branch speculation, it is combined with selective speculative load hardening, which masks secret-derived values using a misspeculation flag (set with an lfence, updated after branches by a non-speculating conditional move) so no secret leaks during a misprediction. A new value-dependent information-flow type system ensures that well-typed programs are speculative-constant-time (no secret leaks even under speculation), and the soundness of the type system and the correctness of the compiler transformation are proved in the Coq proof assistant. The approach is implemented in the Jasmin framework for high-assurance cryptography, and the reported overhead of all Spectre protections is below 2 percent for most cryptographic primitives and about 5 to 7 percent for the post-quantum key-encapsulation mechanism Kyber. No numbers beyond the paper’s own have been introduced; the exact type-system rules, the transformation’s restrictions, the threat model, and the full evaluation should be confirmed in the paper.