Processors guess ahead to go faster, and when they guess wrong the discarded work leaves traces an attacker can read — so the field wrote down precise contracts saying what a chip must not leak, but proving an actual circuit obeys one means running four copies of a processor in a model checker, which nothing finishes; this paper (Princeton and MIT) notices that two of those four copies are redundant, because a correct processor already contains the simple machine it is being compared against, and proves designs that previously ran for seven days without an answer.
The argument in one glance
-
Problem
Speculation leaves evidence of work that was supposed to vanish
To go fast, a processor executes instructions before it knows whether they should run, and squashes them when the guess turns out wrong. Squashing removes their architectural effects but not their traces — caches have been filled, predictors trained, queues occupied — and those traces can be measured from another program. Attacks exploiting this keep arriving, through branch prediction, store-to-load forwarding, value prediction and more, because there is no way to enumerate every structure that might carry a signal out.
-
What people did
Write down precisely what the hardware must not leak
Rather than chase individual attacks, the field defines software-hardware contracts. A contract states that if a program obeys some rule — say, never accessing memory it should not — then the hardware guarantees an attacker learns nothing from running it. This separates the software's obligations from the hardware's cleanly, and turns "is this design secure" into a question with a definite answer.
-
Why it fell short
Checking a real circuit against a contract does not finish
Security here is a property of pairs of executions, so a model checker must run two copies of the processor differing only in the secret. And deciding whether a program was allowed to reveal something requires two more copies of a simple idealised machine that defines the permitted behaviour. Four state machines advancing together is more than the tools can handle for anything but the simplest designs — on secure out-of-order processors, the standard scheme produces no answer at all in seven days.
-
This paper's idea
Two of the four machines are already inside the other two
This paper (Qinhan Tan, Yuheng Yang, Thomas Bourgeat, Sharad Malik and Mengjia Yan) observes that a processor which correctly implements its instruction set already contains the idealised machine — the sequence of committed instructions is exactly what that machine would have produced. So the two extra copies can be deleted and their traces recovered instead, from verification-only logic watching the processors commit.
Why this problem is worth solving
The thing being verified needs stating precisely, because its shape is what causes the trouble.
A
CONTRACT for secure speculation is a conditional. It says that for any program, if that program
would reveal nothing when executed straightforwardly — one instruction after another, no
guessing ahead — then it must also reveal nothing when executed on this particular
microarchitecture, with all its speculation and buffering. The condition is the software’s
obligation and the conclusion is the hardware’s. What makes this awkward to verify is that
“reveals nothing” is not a property of one execution. It says that an observer cannot
distinguish the case where the secret is one value from the case where it is another, which is
a statement about a PAIR of executions. Model checkers verify properties of single traces, so
the standard construction is to instantiate two copies of the design differing only in the
secret and assert that their observable behaviour matches. Both halves of the contract need
this, so both halves cost a pair.
The mechanism the paper uses to escape that is a standard verification tool.
SHADOW
LOGIC is circuitry added to a design purely so that a verification tool can observe something
the design does not otherwise expose. It reads internal signals, computes whatever the property
needs, and drives no outputs that the original design uses — so the design behaves identically
whether it is present or not. In practice it is written inside a preprocessor guard so that it
is compiled in during verification and stripped out before the design is synthesised into a
chip. This is common practice for functional verification: a typical use is watching whether a
committed instruction wrote the value the instruction set says it should, which requires
tracking through register renaming to work out which physical register is the architectural
one. The paper’s contribution is to use it for something larger — not to observe a property but
to reconstruct an entire machine that would otherwise have to be simulated alongside.
What people did before, and where it broke
-
The direct construction: four machines. Instantiate two copies of an idealised one-instruction-per-cycle machine to decide what the program was allowed to reveal, and two copies of the real processor to check what it actually reveals, and advance all four together.
-
The gap. It does not scale. On the secure designs evaluated here, this scheme returns no proof within seven days, which is the baseline the paper is measured against.
-
Hand-written invariants from experts. The strongest prior result proves a secure speculation scheme on a substantial out-of-order processor, using inductive verification assisted by invariants written by formal methods experts.
-
The gap. The key invariant is that secret data never propagates anywhere in the design at all — which is true only for one very conservative defence, where speculative loads wait for every preceding branch to resolve. Most defences proposed by architects deliberately let speculative state spread while controlling what escapes, and the invariant does not hold for them. That approach also requires the user to name the source of speculation, and its prototype considers only branch misprediction, so it cannot find every attack.
-
Search for invariants automatically. More recent work reduces the manual effort by generating candidate invariants mechanically.
-
The gap. It is effective on in-order pipelines and struggles on even a simple out-of-order processor, where either the generation algorithm needs improving or a human must supply invariants after all.
-
Verify an abstract model instead of the circuit. Reason about a high-level description of the microarchitecture, where the state space is tractable.
-
The gap. The vulnerabilities live in details the abstraction omits. Verification at register-transfer level is what the paper insists on, and it notes that several published defences had never been evaluated as actual circuits at all before this work.
How four machines become two
Verifying a processor against a contract
-
-
-
new
-
new
-
new
-
new
The idea
A correct processor already contains the machine it is being compared against. The observation that halves the problem is almost a tautology once stated. The idealised machine in the verification scheme exists to say what a program does when executed one instruction at a time — and a processor that correctly implements its instruction set produces exactly that sequence, in exactly that order, at its commit stage. The out-of-order machinery reorders execution but not retirement. So the second pair of machines is not adding information; it is recomputing something the first pair already contains, in a form the verification tool cannot see. Making it visible is a matter of watching the commit stage and reconstructing the trace — which instructions retired, what addresses they touched — from information the reorder buffer can be extended to carry. Removing redundancy that exists only because two representations of the same thing were being maintained separately is the same move as the tensor compiler work covered elsewhere on this site, though here what gets eliminated is half a verification problem rather than half a memory hierarchy.
Two requirements make the naive version wrong, and both come from timing. Deleting the idealised machines introduces problems the original construction did not have, and the paper is careful about them. The first is INSTRUCTION INCLUSION. The contract check now happens when instructions commit, while the leakage check happens as soon as observable behaviour differs — and commit lags execution. So a detected leak might be blamed on a program that the contract would have excluded, had the relevant instructions got far enough to be examined. In the original scheme this could not happen, because the idealised machine always ran ahead. The second is SYNCHRONISATION. The two processor copies can commit the same instruction at wildly different times, since a load that hits the cache in one copy may miss to memory in the other — possibly a hundred cycles apart — so the two reconstructed traces are no longer aligned and comparing them cycle by cycle is meaningless. Both difficulties are peculiar to reconstructing a reference machine rather than running one, which is why they never arise for the black-box contract fuzzing work covered elsewhere on this site — it tests a real chip against the same formalism and simply observes what the hardware does.
Fix both by changing what happens after a divergence is seen. The solution is to split verification into two phases. In the first, both checks run cycle by cycle as before. The moment the two processors’ observable behaviour diverges — the moment a leak is suspected — the scheme switches to a second phase whose job is to determine whether that program should have been excluded in the first place. In-flight instructions are allowed to drain so the contract check sees them, which settles instruction inclusion. And whichever processor is running ahead is stalled by gating its clock until both are committing at the same rate, which realigns the traces and settles synchronisation. Neither fix requires understanding the defence being verified, which is what makes the scheme reusable where invariant-based approaches are not — the same shadow logic verified five different defence mechanisms on one processor without modification. Replacing expert-authored invariants with a construction that works uniformly is the same trade as the hardware repair work covered elsewhere on this site, which swapped a slow search for a solver query.
What happens when a leak is suspected
The two-phase check, from divergence to verdict
Two copies of the same processor, differing only in the value of the secret.
Step 1 of 5
Both checks run together, cycle by cycle
The two processors execute the same program from the same public memory, differing only in the secret. Shadow logic reconstructs each one's permitted trace from its committed instructions while the observable microarchitectural behaviour is compared.
This is the ordinary case and most of the verification time is spent here. Nothing has gone wrong; the tool is exploring all reachable states looking for one where the two copies become distinguishable.
Why it works
- The idealised machine is derivable, not independent. A correct processor retires instructions in program order → its commit stream is exactly what a one-instruction-per-cycle machine would produce → two of the four state machines carry no information the other two lack and can be removed.
- Shadow logic makes the derivation visible without changing behaviour. Verification-only circuitry reading the reorder buffer → the trace becomes available to the model checker while the design is untouched → it can be stripped before synthesis, so nothing about the shipped chip changes.
- A drain phase restores the ordering the deletion broke. Letting in-flight instructions commit once a divergence is seen → the contract check catches up with the leakage check → a suspected leak cannot be wrongly attributed to a program the contract had already excluded.
- Clock gating restores alignment. Stalling whichever copy is ahead until both retire in step → the two reconstructed traces become comparable again → cache timing differences stop producing spurious mismatches.
- Nothing in the construction depends on the defence. The scheme reasons about commit behaviour rather than about how speculation is contained → the same shadow logic verifies five different defence mechanisms unchanged → where invariant-based approaches must be reworked for each one.
The evaluation
| Property | What was measured | The result | What it tells you |
|---|---|---|---|
| Against the direct construction | |||
| Against expert-invariant verification | |||
| Against automatic invariant search | |||
| How much work the shadow logic is | |||
| What still cannot be proved |
Check yourself
Check your understanding
1. Why does the direct verification construction require four state machines?
2. What is the observation that lets two of the four machines be deleted?
3. Why must in-flight instructions be drained after a divergence is detected?
4. Predict why the two processor copies must be stalled relative to each other before their reconstructed traces are compared.
Sources
RTL Verification for Secure Speculation Using Contract Shadow Logic. Qinhan Tan, Yuheng Yang, Thomas Bourgeat, Sharad Malik, Mengjia Yan. ASPLOS 2025, Volume 1, pages 970 to 986. DOI 10.1145/3669940.3707243. Full text read from the authors’ preprint, arXiv 2407.12232.