Revizor: testing black-box CPUs against speculation contracts

Spectre-style leaks hide inside processors for years because nobody can test for them, so Revizor writes down what leaking is allowed as a contract and then fuzzes a real processor until it finds a program that leaks more than the contract permits.

Why a hidden leak inside a processor is expensive

One word first. The paper’s title says CPU, short for central processing unit. This page says processor everywhere instead, and means the same thing.

Now start with what a processor actually does when it runs a program.

It does not simply execute one instruction, then the next, then the next. It guesses. When it reaches a branch — a point where the program can go two ways — it does not wait to learn which way is correct. Waiting would waste many cycles. Instead it predicts a direction and starts running instructions along that path immediately.

If the prediction was right, time was saved. If it was wrong, the processor discards the results and restarts on the correct path.

This is called speculative execution. Every fast processor built in the last twenty-five years does it. Without it, processors would be far slower.

The word “discards” is where the trouble begins. The processor undoes the architectural results. Registers and memory return to the values they should have. A programmer can never see that the wrong path ran.

But the processor does not undo everything. A value that was read from memory during the wrong guess is still sitting in the cache, the small fast memory that holds recently used data. Reading that address again is now faster than reading a fresh one. Anyone who can measure time can notice the difference.

That is a side channel: information that escapes not through what the program prints, but through a physical effect of running it. The program never revealed the secret. The processor’s own optimisation revealed it, written in the shape of which cache lines became fast.

The specification has a hole in it

Here is the root cause, and it is worth stating carefully.

A processor is specified by its instruction set architecture, usually shortened to ISA. The instruction set says what each instruction computes. Add two registers. Load eight bytes from this address. Jump if the flag is set.

The instruction set deliberately says nothing about how the processor does this. That silence is the point. It lets a chip designer add caches, predictors and out-of-order execution without breaking any existing software.

The paper names the consequence directly. The same silence that permits fast hardware also hides the security effect of that hardware. The specification has nothing to say about caches, so a leak through the cache violates nothing. There is no written rule to break, and therefore nothing to test against.

This is why these vulnerabilities stay hidden for years. It is not that testing is hard. It is that there was no statement of what a correct answer looks like.

What people built before, and where it stopped

Two families of tools existed, and both were reasonable.

The first family searches for one known attack on real hardware. Medusa is a fuzzer for variants of Microarchitectural Data Sampling. SpeechMiner analyses speculative vulnerabilities. These tools run on a processor you can buy, which is exactly what a security auditor needs. Their limit follows from that same choice. They search for a shape that somebody already described, so they do not report a leak of a new shape.

The second family checks the design itself. CheckMate searches processor designs for stored vulnerability patterns. Fadiheh and colleagues use a model checker on

There was also a third thing, and it is the one Revizor builds on. In 2021, Guarnieri and colleagues proposed speculation contracts: a written statement of what a processor is allowed to expose. The idea was right. But at that point contracts had only been used on small, fully visible models of processors with toy instruction sets. Nobody knew how to check a contract against a real chip running real x86 binaries.

The idea, one term at a time

A hardware trace is what actually leaked

Run a program on a real processor. Watch it through a side channel. Write down everything you observe. That list is the hardware trace.

Revizor watches the level-1 data cache, written L1D. It uses a standard attack called Prime+Probe. The attacker first fills every cache set with its own data. That is the prime. Then it runs the victim program. Then it reads its own data back and checks which reads became slow. That is the probe. A slow read means the victim used that cache set.

So a hardware trace here is a row of 64 bits, one per cache set, saying whether the program touched it. The paper gives this example, which reports accesses to sets 0, 4 and 5:

10001100000000000000000000000000

The trace depends on the input. That dependence is the leak. The attacker already knows the program. Any difference between two hardware traces therefore tells the attacker something about the input.

A contract is what leaking is allowed

A speculation contract is a document. For each instruction in the instruction set, it states two things.

The observation clause says what that instruction may expose. The execution clause says what speculation that instruction may trigger.

Revizor uses three observation clauses, each one more permissive than the last:

• MEM — the addresses of loads and stores may be exposed. This models an attacker watching the data cache.
• CT, short for constant-time — MEM plus the program counter. This models an attacker watching both the data cache and the instruction cache.
• ARCH — CT plus the values read from memory. This models an attacker sharing the same address space as the victim.

And four execution clauses, again from most restrictive to most permissive:

• SEQ — observations count only during normal, in-order execution. Nothing may leak from a speculative path at all.
• BPAS — leakage is also permitted from execution where every store is speculatively skipped. This is Spectre V4 declared as expected behaviour.
• COND — leakage is also permitted from the wrong path of a mispredicted conditional branch. This is Spectre V1 declared as expected behaviour.
• COND-BPAS — both are permitted.

A full contract joins one of each: MEM-SEQ, CT-COND, ARCH-SEQ, CT-COND-BPAS, and so on. Run a program under a contract and write down every observation the contract permits, in order. That list is the contract trace.

Compliance is an equality between two inputs

Now the definition that makes the whole tool work.

A processor complies with a contract when this holds for every program and every pair of inputs:

If the two inputs produce the same contract trace, they must also produce the same hardware trace.

Read it as a promise. If the contract says an attacker cannot distinguish two inputs, then the real chip must not let the attacker distinguish them either.

A counterexample is a program together with two inputs that break the promise. Same contract trace, different hardware trace. It means the chip leaked something the contract did not permit.

Here is the key observation, and it is the reason a black-box processor becomes testable. Contract traces are compared only to contract traces. Hardware traces are compared only to hardware traces. The two kinds never meet. So no model that translates one kind into the other is ever needed. And such a model is exactly what a commercial chip refuses to give you.

The authors call the resulting technique Model-based Relational Testing, abbreviated MRT. “Relational” because a verdict needs two runs, not one. A single run leaks nothing by itself; leakage is a difference between runs.

Tracing one violation from start to finish

The paper’s own example is three lines long. Line 1 reads from array1 using index x. Line 2 tests whether y is less than 10. Line 3 reads from array2 using index y. In the example, array1 begins at address 0x100 and array2 begins at address 0x200.

This is the classic Spectre V1 shape. Follow it through the whole loop.

line 1:  z = array1[x]     # array1 begins at 0x100
line 2:  if (y less than 10)
line 3:  z = array2[y]     # array2 begins at 0x200

Why this works

The causal chain is short, and each link depends on the one before it.

Because a contract trace is compared only to another contract trace, and a hardware trace only to another hardware trace, no translation between them is required. → Because no translation is required, no model of the processor internals is required, so a shipped commercial chip can be tested. → Because inputs are grouped into classes by contract trace, any difference found inside a class is by definition information the contract did not permit. → Because that is an equality check on two lists, the verdict needs no expert judgement, and the search can run unattended. → Because the executor replays the same input sequence to prepare the predictors, the microarchitectural context is varied but repeatable. Hardware traces are therefore stable enough to compare for equality. → Therefore random programs of 8 instructions, run on an ordinary desktop, are enough to reveal Spectre V1, Spectre V4, MDS and LVI-Null.

That last step deserves a sentence of its own, because it is the surprise of the paper. The search space is enormous: hundreds of instructions, dozens of registers, a large memory space. Random search across that space should fail. It does not fail, and the authors explain why. Speculative leaks are not rare events hidden in one exotic program. They appear in a large fraction of ordinary programs, and finding a single one is enough.

What it costs

Every design gives something up. This one gives up four things.

• You must write the contract first. Revizor never answers “is this processor secure?”. It answers “does this processor disagree with this document?”. A leaky chip will satisfy a weak contract, and that is not a bug in the tool. It is the price of turning security into an equality check.
• No violation is not a proof. The paper is explicit: 24 hours with no violation shows only that the sampled programs and inputs contained no counterexample. It does not show the leak is absent.
• The emulator must be exactly right. A contract trace comes from Unicorn. If Unicorn emulates an instruction incorrectly, the resulting disagreement looks like a processor leak. The authors excluded bit count, bit test and shift instructions from testing for this reason.
• The generator restricts itself heavily. To make two random inputs likely to share a contract trace, Revizor uses only four registers, confines memory to one or two pages of 4 KB, aligns accesses to the 64-byte cache line, and starts with only 2 bits of input entropy. Every one of those restrictions narrows what can be found.

What the measurements showed

The authors tested two machines: an Intel Core i7-6700, a Skylake processor, and an Intel Core i7-9700, a Coffee Lake processor. They ran Skylake with the Spectre V4 microcode patch both enabled and disabled. Coffee Lake carries a hardware patch against Microarchitectural Data Sampling.

The generator built test cases from subsets of x86, and the subset controls what can be found. Arithmetic only gives 325 unique instructions. Adding memory operands raises it to 678. Adding conditional branches and variable-latency division raises it to 719, more than double the arithmetic-only subset. Generation started small — 8 instructions, 2 memory accesses, 2 basic blocks and 50 inputs per test case — and grew over rounds. Each target ran for 24 hours, or until the first violation appeared.

One more Skylake experiment sits outside that table, and it produced the second new variant. The authors tested arithmetic, memory and division together, with the Spectre V4 patch disabled. Revizor broke CT-BPAS and CT-COND-BPAS, and the counterexample was a previously unknown variant of Spectre V4. It leaks division timing through the same race condition as the new V1 variant.

They then repeated exactly that experiment with the V4 patch enabled. Revizor found no violation of any contract, including none of the new variant. That is a useful second result. The tool can also confirm that a deployed fix works, not only that a leak exists.

A stronger attacker model changed the result again. The executor was allowed to trigger microcode assists, which are internal processor routines invoked for operations such as updating a page table bit. Revizor then found violations of all four contracts on Skylake, and identified them as Microarchitectural Data Sampling. The same experiment on Coffee Lake, which carries a hardware patch against that attack, still produced violations of all four contracts. Those were LVI-Null.

How long it took

Three things are worth noting in that table.

First, every entry except the two Spectre V4 rows is under 10 minutes, against a budget of 24 hours. Second, a second permitted leak barely slows detection. Finding MDS took 5 min 35 s when nothing was permitted, and 7 min 3 s when Spectre V1 leakage was permitted. That is an increase of about a quarter. Third, Spectre V4 is genuinely the hard case, at 73 minutes against under 5 minutes for Spectre V1.

The authors also measured how many random inputs a handwritten gadget needs before the violation appears. Most needed very few: 2 inputs for Spectre V5-ret, 4 for Spectre V2, 6 for Spectre V1. Spectre V4 again needed far more, at 62 inputs, about 31 times the easiest cases. Even 62 inputs takes less than a second. The cost is therefore dominated by generating the right program, not by testing inputs against it.

Using the tool to check somebody else’s assumption

One evaluation is worth describing separately, because it shows a second use for the whole approach.

Two defence proposals, Speculative Taint Tracking and KLEESpectre, share an assumption. They assume that a store does not change the cache state until it retires, meaning until the processor makes it permanent. The authors wrote that assumption into a contract and tested it.

On Skylake, Revizor found no violation. On Coffee Lake, it found a counterexample: a speculative store did change the cache state. The assumption is false on that processor, and a defence that depends on it would be weaker than believed.