Compass: Navigating the Design Space of Taint Schemes for RTL Security Verification

To prove a chip does not leak secrets, engineers tag secret data and track where the tag spreads, but the tracking machinery can be cheap-and-imprecise (raising false alarms) or precise-and-huge (too slow to verify), and you can mix precisions across the chip's blocks — except the number of ways to do that is astronomically large; this paper (MIT, Princeton, EPFL) builds Compass, which starts with the cheapest tracking everywhere and, whenever the verifier raises a false alarm, automatically traces back to the exact spot causing it and makes only that spot more precise, turning a week-long proof into minutes.

The argument in one glance

Problem

To prove a chip does not leak secrets, you track a tag — but the tracking itself is the hard part

A recurring class of hardware attacks lets an attacker learn a secret by watching subtle microarchitectural effects, and the cleanest way to rule such leaks out is to prove an information-flow property: that a secret in the victim can never affect anything the attacker observes. The standard tool is taint analysis, or information flow tracking. You mark the secret as tainted, add taint logic that propagates the tag through the circuit as data flows, and check whether the tag ever reaches an attacker-observable sink; if it never does, the design is proven leak-free. The catch is that the taint logic is itself hardware you have to build and then verify, and there is a painful trade-off in how you build it. Cheap, coarse taint logic is small but imprecise: it over-approximates, sometimes flagging a flow that does not really exist, which shows up as a false alarm that stalls the proof. Precise taint logic avoids the false alarms but can be enormous — in the worst case exponentially larger than the circuit — making verification hopelessly slow. So you are stuck between tracking that lies and tracking that will not finish.
What people did

Pick one taint scheme and apply it everywhere

The usual practice is to choose a single taint scheme — one of several established ones that sit at different points on the precision-versus-cost curve — and apply it uniformly to every gate in the design. You pick a scheme precise enough to avoid false alarms, accept its cost, and run the verifier.
Why it fell short

One global scheme is wrong everywhere at once, and mixing has too many options

A uniform scheme forces a single compromise on a design whose parts have very different needs. Consider a processor with a speculative-execution defense meant to keep a secret out of the branch predictor. If the defense is correct, no bit inside the branch predictor should ever be tainted — so tracking it bit by bit, with taint logic linear in the size of a huge modern predictor, is pure waste; a single coarse taint bit for the whole module would do, and would still catch a leak if the defense were broken. But you cannot coarsen everything: the reorder buffer's entries and fields genuinely hold different taint statuses, so a too-coarse scheme there raises false alarms. The right answer is to mix schemes — precise where it matters, coarse where it does not. The problem is the size of that choice. A single processor can have hundreds of thousands of gates, and with even a few taint options per gate the number of possible mixed schemes is astronomically large. A designer confronted with that space has no idea where to begin.
This paper's idea

Start cheap everywhere, and refine only the spot a false alarm points to

Compass is a framework that guides a user to a taint scheme that is as lightweight as possible while still precise enough to prove the property. It first gives a unified terminology that organizes all existing taint schemes into a three-dimensional design space — the level at which a scheme operates (gate, cell, or module), how coarsely taint bits are grouped, and how much dynamic signal information the taint logic uses. It then navigates that space with counterexample-guided abstraction refinement: begin with the cheapest, coarsest tracking everywhere, run a model checker, and whenever the checker raises a spurious counterexample, an automated backward trace through the taint graph pinpoints the exact taint logic whose imprecision caused it, and only that spot is made more precise, in a prioritized order. Iterating this yields a taint scheme tailored to the property, refined precisely where needed and cheap everywhere else — turning proofs that took days into minutes.

Why this problem is worth solving

The whole method rests on a trade-off that a single global choice handles badly.

To verify that a hardware design has no secret-to-attacker information flow — a non-interference property — taint analysis marks the secret as a taint source, attaches a taint bit to circuit elements, and adds taint-propagation logic so the tag spreads as data does; if the tag never reaches an attacker-observable sink, no flow exists. This is far cheaper than the alternative of duplicating the whole design and comparing two runs, because it needs only a single trace. But every practical taint scheme over-approximates: making taint exactly precise would require taint logic that grows exponentially with the circuit, which is infeasible, so real schemes conservatively capture flow. That conservatism is a feature and a bug. It guarantees soundness — the scheme never misses a real leak, so it has no false negatives — but it admits false positives, reporting a flow that does not truly exist. Different established schemes trade precision against complexity differently: a coarser scheme has smaller, faster taint logic but more over-approximation and thus more false alarms; a finer scheme is more precise but larger and slower to verify. A false alarm is not a harmless nuisance here, because it stalls a formal proof, and excess logic is not free, because it inflates the very verification you are trying to run. Choosing well is the crux.

The real leverage is that different parts of a chip deserve different treatment, but the choice explodes combinatorially.

A processor is not homogeneous. Some modules, under a correct defense, should never carry any tainted bit at all — a branch predictor guarded by a speculative-execution mitigation, for instance — so they can be tracked with a single coarse taint bit for the whole module, which is adequate because if the defense is broken that one bit still lights up and even helps localize the bug. Other modules, like a reorder buffer whose entries and fields legitimately hold different taint statuses, need fine-grained tracking or they will produce false alarms. So the efficient thing is to apply different taint schemes to different components, precise only where precision is required. But the number of ways to do that is staggering: a Rocket processor has around 193,000 gates, and with even three taint options per gate the configuration space is three raised to the 193,000 — vastly beyond anything a person could search by hand. A designer facing that space has no principled starting point and no way to know which of the countless combinations is both lightweight and sufficient. Turning that intractable search into a guided, mechanical process is what Compass is for.

What people did before, and where it broke

Apply a single precise taint scheme uniformly (for example CellIFT). Use one scheme precise enough to avoid false alarms across the whole design. Where it broke. It pays the cost of precision everywhere, even in modules that never carry taint, inflating the taint logic and slowing verification.
Apply a single coarse taint scheme uniformly. Use one cheap scheme to keep the taint logic small. Where it broke. Its over-approximation raises false alarms in modules that genuinely need precision, like a reorder buffer, stalling the proof.
Mix schemes by hand. Manually assign a precise scheme where needed and a coarse one elsewhere. Where it broke. The space of mixed schemes across hundreds of thousands of gates is astronomically large, and choosing it manually demands deep expertise with no guidance on where to start.
Naive counterexample exclusion. When a false alarm appears, just exclude that specific counterexample. Where it broke. A similar counterexample recurs next iteration because the underlying imprecision was never addressed, and finding the coarsest sufficient refinement is NP-hard.
The gap. No framework systematically navigated the space of mixed taint schemes to find one that is lightweight yet precise enough for a given property. Organizing that space and refining it with counterexample guidance is what Compass contributes.

How Compass works

From a coarse start to a property-tailored taint scheme, guided by counterexamples

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

The idea

Give the sprawl of taint schemes a coordinate system, and treat the choice as points in it. Compass’s first move is conceptual: rather than a grab-bag of named taint schemes, it defines a single three-dimensional space in which they all live. One axis is the unit level a scheme works at — an individual netlist gate, a higher-level hardware-description cell like an adder or multiplier, or a whole module such as a branch predictor. A second axis is taint-bit granularity — one taint bit per bit, per multi-bit word, or per group of registers — where coarser grouping means fewer bits but more over-approximation. A third is logic complexity, how much dynamic signal value the taint computation uses, from a naive scheme that just ORs input taints to a fully dynamic one that exploits that a zero input blocks influence. Because every existing scheme is a point in this space, the problem of choosing a scheme becomes the problem of navigating it. Reducing a hardware design to a formal representation on which security properties can be systematically reasoned about, rather than treating each analysis as bespoke, is the same foundational move the work on lifting micro-update models from RTL for formal security analysis covered elsewhere on this site makes, building the structured abstraction that everything else stands on.

Refine the abstraction only where a false alarm proves it is too coarse. The core algorithm applies counterexample-guided abstraction refinement to taint. A coarse taint scheme is an over-approximation, easier to verify but prone to false alarms, exactly like an abstract model in program verification; so Compass runs the classic loop — start coarse, model-check, and when the checker returns a spurious counterexample, refine — but adapted to taint. Crucially, it automates the hardest step: locating what to refine. An algorithm traces the taint-propagation graph backward from the falsely-tainted sink to find the taint logic responsible for the imprecision, so precision is added only at that one spot rather than globally. Driving a formal tool with counterexamples to automatically build up just enough of a hardware model to settle a property, instead of hand-crafting the whole thing, is the same automated-formal-reasoning discipline the work on automated synthesis of microarchitectural axioms covered elsewhere on this site embodies, letting the verifier itself guide what needs to be made precise.

Tailor the scheme to the specific property, so it is lightweight by construction. Because refinement is driven by the counterexamples a particular property generates, the taint scheme Compass converges on is property-specific: it is precise exactly at the handful of locations that property’s proof requires and coarse everywhere else, which is why it is far lighter than a uniformly precise, property-agnostic scheme. This matters most for the security properties people actually care about, like proving a speculative-execution defense keeps secrets out of the covert channels attackers exploit. Verifying that a hardware countermeasure against speculative-execution leakage genuinely holds, at the register-transfer level where the real design lives, is the same target the work on automated design-time testing of secure speculation countermeasures covered elsewhere on this site pursues, and Compass supplies a way to make the underlying taint verification tractable enough to actually complete.

Following a false alarm through Compass

Refining a coarse taint scheme to clear a spurious counterexample

A trace, following the paper's design, of one refinement iteration on a processor verifying a speculative-execution information-flow property.

Step 1 of 5

Start coarse and check the property

Compass applies the cheapest, coarsest taint scheme across the processor and runs a model checker on the information-flow property — for instance, that the secret cannot influence attacker-observable signals through the speculative-execution machinery.

The coarse scheme is fast to check but over-approximates heavily.

Why it works

Coarse taint is sound, so refining only where needed is safe. A coarse scheme over-approximates and never misses a real flow → but that means starting coarse can only produce false alarms, never false silence → so Compass can safely begin cheap and add precision solely to clear the false alarms.
A counterexample points at the imprecision, so refinement is targeted. Blindly making everything precise is prohibitively expensive → but a spurious counterexample encodes exactly where the coarse logic over-approximated → so backward-tracing it locates the one spot to refine, keeping the rest cheap.
Backward tracing turns location into an algorithm. Manually finding what to refine demands deep expertise and does not scale → but traversing the taint graph from the false sink upstream, using the counterexample’s values, mechanically identifies the responsible taint logic → so the hardest CEGAR step is automated.
Property-driven refinement yields a property-tailored, lightweight scheme. A uniform scheme must be precise enough for the worst case everywhere → but Compass only refines where a given property’s counterexamples demand it → so the final scheme is precise at a few spots and coarse elsewhere, far lighter than a property-agnostic one.
A three-dimensional space makes refinement a small ordered choice. Without structure, choosing a more precise scheme is open-ended → but organizing schemes by unit level, granularity, and logic complexity gives a finite, ordered set of more-precise options at each spot → so refinement is a bounded, prioritized step rather than a search.

What it costs (trade-offs and scope)

Refinement choice is not fully automated. Compass automates locating the imprecise spot, but choosing which more-precise option to apply there currently needs human intervention in the implementation, and module-level taint schemes in particular require domain knowledge to construct.
The refinement is heuristic, not optimal. Finding the coarsest sufficient refinement is NP-hard, and multiple counterexamples can each demand different cuts, so Compass uses a practical heuristic rather than a globally minimal solution; the resulting scheme is lightweight but not provably the lightest.
It is property-specific. The scheme is tailored to the particular property being verified, which is what makes it lightweight, but it means a new property generally requires re-running the refinement, and a scheme tuned for one property may be insufficient for another.
Model-checking scalability is improved, not unbounded. Compass makes verification far more tractable — turning days into minutes on one core — but for large designs it may still only reach a deeper bounded proof rather than a full unbounded one, so it pushes the frontier without eliminating the underlying hardness.
The result is a sound over-approximation, with the usual caveat. Like all practical taint schemes, Compass’s output has no false negatives but may retain false positives it did not need to eliminate; it guarantees it never misses a leak, not that every reported flow is real, though refinement removes the ones that block the proof.

The evaluation

Verifying speculative-execution information-flow properties

Property	Uniform precise scheme (CellIFT)	Uniform coarse scheme
Taint logic cost
False alarms
Simulation overhead		n/a
Model-checking scalability	Baseline	False alarms block it
Sodor unbounded proof time		n/a

From the paper's evaluation on open-source RISC-V processors verifying speculative-execution information-flow properties. Compass produces taint schemes with significantly less taint logic than the state-of-the-art CellIFT, cutting simulation overhead from 351 to 205 percent, and improves model-checking scalability across tasks: it reduces the Sodor core's unbounded proof from hours to 5.2 minutes (including refinement), and on the Rocket core improves the bounded-model-checking cycle bound from 41 (baseline scheme, 7 days) to 159 (Compass, 25.3 hours).Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

The contribution is a systematic way to make hardware information-flow verification practical by choosing taint precision intelligently rather than uniformly. Compass organizes all taint schemes into a three-dimensional space (unit level, bit granularity, logic complexity), then applies counterexample-guided abstraction refinement: start with the cheapest tracking everywhere, and whenever the model checker raises a false alarm, an automated backward trace pinpoints the imprecise taint logic and only that spot is refined. The result is a property-tailored scheme, precise where it must be and cheap elsewhere, cutting simulation overhead from 351 to 205 percent versus the state of the art and turning proofs that took days into minutes. Read it within scope. Only the location of imprecision is automated; choosing the more precise option, and building module-level schemes, still needs human expertise. The refinement is a heuristic, not provably minimal, since the optimal version is NP-hard. It is property-specific, so a new property means re-refining. It improves model-checking scalability but does not remove the underlying hardness, sometimes reaching only a deeper bounded proof. And the output is a sound over-approximation — never missing a leak, but not certifying every reported flow is real. Within those bounds it convincingly makes taint-based RTL security verification tractable where it was not.

Background

Why hardware security verification is getting formal

It helps to see why a paper about navigating taint schemes matters now. A decade of microarchitectural attacks — from cache side channels to speculative execution — has shown that a processor can be functionally correct and still leak secrets through timing and other subtle effects, and that these leaks are extraordinarily hard to find by inspection or ordinary testing. The response has been a push toward formal methods at the register-transfer level, proving that a design has no secret-to-attacker information flow rather than hoping testing catches it. Information-flow tracking is the workhorse of that effort, but it has been held back by exactly the trade-off Compass addresses: precise enough to trust means too big to verify, cheap enough to verify means too imprecise to trust. Making these proofs actually complete on real processors is what turns hardware security from a reactive scramble after each disclosed attack into something that can be checked before tape-out. That larger project of subjecting the microarchitecture to rigorous, mechanized security analysis is the same one the work on mitigating memory-timing side channels covered elsewhere on this site is part of, and Compass contributes the piece that makes the verification underneath it scale, so that the security properties designers want to guarantee can actually be proven.

If you remember only three things

1. Hardware information-flow verification proves a chip cannot leak secrets by tagging the secret and tracking where the tag spreads with taint logic, but every practical taint scheme over-approximates — it is sound (never misses a real leak) yet can raise false alarms — and a single global scheme forces a bad compromise: coarse tracking is cheap but floods the verifier with false alarms, while precise tracking can be exponentially large and too slow to verify; mixing precise and coarse schemes across a chip's modules is far better, but for a processor with around 193,000 gates the space of mixed schemes is astronomically large.
2. Compass makes this tractable by first organizing all taint schemes into a three-dimensional design space — the unit level a scheme operates at (gate, hardware cell, or module), the taint-bit granularity (per bit, per word, or per register group), and the logic complexity (how much dynamic signal value it uses) — and then navigating that space with counterexample-guided abstraction refinement: it starts with the cheapest coarse tracking everywhere, runs a model checker, and whenever the checker returns a spurious counterexample it automatically traces the taint-propagation graph backward from the falsely-tainted sink to pinpoint the exact taint logic causing the imprecision, refining only that spot to a more precise option in a prioritized order.
3. Because refinement is driven by a specific property's counterexamples, the resulting scheme is property-tailored — precise at the few locations the proof needs and cheap everywhere else — and on open-source RISC-V processors verifying speculative-execution properties it cuts simulation overhead from 351 to 205 percent versus the state-of-the-art CellIFT and greatly improves formal scalability, reducing the Sodor core's unbounded proof from hours to 5.2 minutes and improving the Rocket core's bounded-proof cycle depth from 41 (in 7 days) to 159 (in 25.3 hours); the caveats are that choosing the refinement option and building module-level schemes still need human expertise, the refinement is a heuristic since the optimum is NP-hard, it is property-specific, and it improves but does not remove model-checking's underlying hardness.

Check yourself

Check your understanding

1. Why does a single global taint scheme force a bad trade-off in hardware information-flow verification?
2. If mixing taint schemes per module is better, why is it hard to do by hand?
3. How does Compass navigate the taint design space?
4. What did Compass achieve, and what are its limits?

Sources

The paper is “Compass: Navigating the Design Space of Taint Schemes for RTL Security Verification” by Yuheng Yang, Qinhan Tan, Thomas Bourgeat, Sharad Malik, and Mengjia Yan (Massachusetts Institute of Technology, Princeton University, and EPFL), published at ASPLOS 2026 (Volume 2), DOI 10.1145/3779212.3790144. It is released under a Creative Commons Attribution license and open-sourced.

This explainer is written from the full text of the authors’ version. Everything above comes from the paper’s own sections: the introduction on microarchitectural attacks, information-flow (non-interference) properties, and taint analysis as a single-trace alternative to self-composition; the precision-versus-complexity trade-off among schemes like GLIFT, CellIFT, and RTLIFT, the impossibility of exact precision without exponential taint logic, and the resulting over-approximation with soundness (no false negatives) but false positives; the motivation for mixing schemes per module (the coarse single-bit branch-predictor example and the fine-grained reorder-buffer counterexample) and the combinatorial explosion (a Rocket processor with around 193,000 gates giving three raised to the 193,000 configurations); the three-dimensional taint space of unit level (gate, cell, module), taint-bit granularity (per bit, per word, per register group), and logic complexity (naive, partially dynamic, fully dynamic), with the note on correlation-based imprecision from composing lower-level schemes; the application of counterexample-guided abstraction refinement to taint, the automated backward-tracing algorithm to locate the imprecise taint logic, and the prioritized, human-assisted refinement step; and the evaluation on open-source RISC-V processors reporting reduced taint-logic overhead versus CellIFT with simulation overhead cut from 351 to 205 percent, a Sodor unbounded proof reduced from hours to 5.2 minutes, and a Rocket bounded-model-checking cycle bound improved from 41 (baseline, 7 days) to 159 (Compass, 25.3 hours).