Lifting Micro-Update Models from RTL for Formal Security Analysis

Attacks like Spectre steal secrets by exploiting hidden hardware behavior — caches, buffers — that a program is never supposed to see, so checking whether software is vulnerable means reasoning about that hidden state, but doing it against the full chip design is far too slow; this work from UC Berkeley and Michigan invents micro-update models, small faithful abstractions that keep only the security-relevant hardware signals, and a tool called PAUL that automatically lifts them out of the raw hardware description, letting security checks run up to eight times faster while still soundly guaranteeing that what holds on the model holds on the real hardware.

The argument in one glance

Problem

Checking software for hardware attacks needs an accurate, scalable model

Attacks like Spectre exploit hidden microarchitectural state (caches, buffers) to leak secrets, so checking software for them requires reasoning about that state. But verifying software against the full hardware description does not scale, and abstract models — which do scale — must be accurate or they can wrongly declare insecure software secure.
What people did

Hand-write abstract models, or reuse existing model types

Manually craft an abstract model keeping only the vulnerability-relevant hardware, or reuse instruction-level models or axiomatic ordering models to verify software against.
Why it fell short

Hand-writing is error-prone; existing models miss what matters

Writing accurate models by hand is tedious, error-prone, and needs deep microarchitecture expertise. Instruction-level models capture only software-visible state and treat instructions in isolation, missing pipeline interactions. Ordering-based models capture interactions but discard functional behavior, so they cannot express properties like non-interference that many attacks require.
This paper's idea

Automatically lift micro-update models from the hardware (PAUL)

Micro-update models are a new formalism that captures the functional behavior of just the user-chosen security-relevant signals, at fine temporal resolution, eliding the rest. Ensuring these signals are functionally equivalent to the source hardware makes the model sound: a property proved on it holds on the real hardware. The tool PAUL lifts such models from the hardware description mostly automatically, using oracle-guided synthesis and hierarchical generation, and analysis on the lifted model runs up to 8 times faster than on the source hardware.

Why this problem is worth solving

Modern hardware attacks live in the parts of a processor that programmers never see, which is what makes them both dangerous and hard to reason about.

Attacks like Spectre and Meltdown, and a steady stream of newer ones, do not exploit bugs in a program’s logic. They exploit the microarchitecture — the hidden machinery a processor uses to run fast, such as caches, store buffers, fill buffers, and branch predictors — which is invisible to the instruction set the software is written against. By manipulating this hidden state and then measuring it, usually through timing, an attacker can leak secret data that the program itself never exposed. To determine whether a given piece of software is vulnerable to such an attack, a security analysis must therefore reason about that hidden microarchitectural state, not just the program’s visible behavior. The natural way to do this rigorously is formal verification against the actual hardware. But real processors are described at the register-transfer level — a detailed, low-level account of every register and signal — and verifying a software program directly against that full description does not scale: the microarchitectural complexity overwhelms the analysis. So the field turns to abstract models of the hardware that keep only the parts relevant to the attack and drop the rest, which are smaller, more interpretable, and tractable to verify against.

But abstraction is only useful if it is faithful, and the existing ways of building these models each fail in an important way.

The danger with any abstract model is inaccuracy: if the model omits or misrepresents a security-relevant behavior, it can declare a vulnerable program secure, which is worse than useless. Yet today these models are written by hand — tedious, error-prone work that demands a deep understanding of the microarchitecture, since an analyst can say which components matter but finds it hard to specify exactly how they must behave to be accurate. Two established kinds of model exist, and neither suffices. Instruction-level models, based on the instruction set, are precise only about software-visible architectural state — the program counter, registers, and memory — so they simply do not represent the caches and buffers that attacks exploit. They also assume instructions execute in isolation, one finishing before the next begins, which misses the crucial fact that in a pipeline, overlapping instructions interact microarchitecturally in ways that matter for security; the paper illustrates this with a load buffer whose leakage depends on the exact cycle a later store flushes it. Axiomatic ordering models take the opposite approach, describing the microarchitecture as ordering constraints over whole executions, which does capture pipeline interactions — but they abstract away the functional behavior of signals. That is fatal for security properties like non-interference, which require knowing the actual values a signal takes to decide whether an attacker’s observations can depend on a secret. So one model type is too coarse and isolated, and the other cannot express the properties that matter.

What people did before, and where it broke

Verify software directly against the full hardware. Check the program against the complete register-transfer-level description of the processor. Where it broke. The microarchitectural complexity of a real processor makes this too detailed to scale as the program grows.
Hand-write abstract hardware models. Manually craft a model that keeps only the vulnerability-relevant components. Where it broke. Writing accurate models by hand is tedious, error-prone, and requires deep microarchitectural expertise, and mistakes can wrongly deem insecure software secure.
Reuse instruction-level or ordering-based models. Apply models from the instruction set, or axiomatic ordering models, to security analysis. Where it broke. Instruction-level models omit microarchitectural state and treat instructions in isolation; ordering models discard functional behavior, so neither can soundly express attacks that need both interactions and functional detail.
The gap. No approach automatically produced abstract models that keep the security-relevant microarchitectural signals with their functional behavior and are provably faithful to the hardware. Doing that by lifting is what this work contributes.

How the approach works

From verifying against full hardware to lifting a faithful abstract model

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

The idea

Abstract the hardware to just the security-relevant signals, and prove the abstraction faithful. The core is a new model formalism, the micro-update model, that keeps only the signals a security analyst cares about and drops the rest of the design, so the model is small enough to verify against — while ensuring those kept signals are functionally equivalent to the source hardware, which makes the abstraction sound, meaning a leak absent on the model is truly absent on the real chip. Verifying software against a compact, sound abstraction of the hardware rather than the full, unmanageable design is the same strategy the speculative-execution testing work covered elsewhere on this site uses, checking programs against an abstract model of what the hardware may leak instead of the full implementation, so the analysis stays tractable without giving up rigor.

Lift the model out of the low-level hardware automatically. Because hand-writing accurate microarchitectural models is error-prone and demands deep expertise, this work generates them by lifting — extracting a higher-level model from the low-level register-transfer-level source while preserving the properties that matter — using oracle-guided synthesis and doing it hierarchically so it scales to larger designs, correct by construction. Recovering a faithful higher-level representation automatically from a low-level implementation, rather than reconstructing it painstakingly by hand, is the same undertaking the binary-lifting work covered elsewhere on this site pursues, extending the idea of lifting from software binaries to the hardware description so that structure buried in a low-level form can be recovered and reasoned about.

Keep functional behavior so the strong security properties are expressible. Unlike ordering-only models, a micro-update model imperatively represents what values the chosen signals actually take over time, which is exactly what properties like non-interference need — the ability to ask whether an attacker’s observations could depend on a secret — and the model is checkable against the source hardware by a functional-equivalence proof. Building a precise, functional model of hardware behavior that a tool can machine-check, so that guarantees about it transfer to the real design, is the same discipline the GPU memory-model work covered elsewhere on this site follows, writing an exact model of what the hardware does so that real behavior can be verified against it rather than argued about informally.

Following a load-buffer analysis through the approach

Checking a program for a load-buffer timing leak

A trace of using a lifted micro-update model to analyze software, following the paper's motivating example.

Step 1 of 5

A hidden feature that leaks by timing

A processor has a load buffer that caches the most recently loaded value — a microarchitectural feature invisible to the instruction set but exploitable as a timing side channel. An analyst wants to check whether a program leaks secrets through it.

Whether it leaks can depend on the exact cycle a store flushes the buffer.

Why it works

Full hardware is too detailed to verify against. Because the register-transfer level captures every register and signal of the design → verifying a program directly against it does not scale → so security analysis needs an abstraction that keeps only what the attack touches.
Abstraction is only safe if it is accurate. Because an imprecise model can call insecure software secure → the abstraction must be provably faithful to the hardware → so functional equivalence of the kept signals is what makes the model sound.
Security needs functional behavior, not just ordering. Because properties like non-interference require reasoning about the actual values signals take → ordering-only models that discard functional behavior cannot express them → so an imperative functional model is necessary for real security analysis.
Microarchitecture needs interactions, not isolation. Because pipelined instructions overlap and their microarchitectural effects depend on one another → per-instruction isolated models miss those interactions → so a finer temporal model that captures interactions is required.
Lifting makes accurate models automatic. Because hand-writing accurate microarchitectural models is tedious and expert-only → lifting them from the hardware with oracle-guided synthesis generates them mostly automatically and correct by construction → so accuracy no longer rests on error-prone manual effort.

What it costs (trade-offs and scope)

Generation is semi-automatic, not fully automatic. The lifting uses oracle-guided synthesis, where an oracle — a human or a tool — provides guidance through a query-and-response interface. So building a model still involves some guidance and the designation of signals-of-interest, rather than being fully hands-off.
The model covers the chosen signals, not the whole design. A micro-update model is faithful only for the signals-of-interest it captures; behaviors outside that slice are elided. Soundness holds for properties over the captured signals, so choosing the right signals for a given attack matters.
Soundness, not completeness, is the guarantee. The framework guarantees that a security property holding on the lifted model holds on the hardware. It is designed to avoid false assurances of security; the emphasis is on not missing real vulnerabilities within the modeled scope.
Synthesis has its own cost and limits. Generating the model requires synthesis effort, and the hierarchical approach is what keeps it scalable to larger designs; very large or unusual designs could still stress the generation, even though analysis on the resulting model is faster.
The evaluation is on specific cores. The approach is demonstrated on the Sodor five-stage processor and components of the CVA6 (Ariane) RISC-V processor, with up to an 8 times analysis speedup; results on other processors and attacks would differ.
It targets security analysis, given the model. The contribution is the modeling formalism and its generation, enabling downstream security analysis; the analyst still must formulate the security property (such as non-interference) to check.

The evaluation

Three kinds of hardware model for software security analysis

Property	Instruction-level model	Ordering model
Captures microarchitectural state (caches, buffers)		Yes
Captures instruction interactions (pipeline)
Preserves functional behavior (for non-interference)	Architectural only
Provably faithful to the hardware	Architectural state only	Needs hard global invariants
Generated automatically	Not applicable	Not applicable

Three kinds of hardware model for analyzing software security, as contrasted in the paper. Verifying software against the full register-transfer-level hardware (not shown) is accurate but does not scale. Instruction-level models capture only software-visible architectural state and treat instructions in isolation, so they miss the caches, buffers, and pipeline interactions that attacks exploit. Axiomatic ordering models capture interactions across whole executions but abstract away functional behavior, so they cannot express security properties like non-interference that need the actual values signals take. Micro-update models keep the functional behavior of just the user-chosen security-relevant signals at fine temporal resolution, eliding the rest, and are ensured functionally equivalent to the source hardware — making them sound, so a property proved on the model holds on the real chip. The tool PAUL lifts these models from the hardware mostly automatically using oracle-guided synthesis and hierarchical generation, demonstrated on the Sodor five-stage processor and components of the CVA6 (Ariane) RISC-V processor. Security analysis on the lifted model runs up to 8 times faster than on the source hardware.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This is a foundational contribution to formal hardware security, and its framing is precise. Microarchitectural attacks exploit hidden state, so checking software for them requires models that expose that state, but verifying against the full hardware does not scale and hand-written abstract models are error-prone and often inadequate: instruction-level models miss microarchitectural state and pipeline interactions, and ordering-based models discard the functional behavior that properties like non-interference need. The paper’s answer, the micro-update model, threads this needle by imperatively capturing the functional behavior of just the signals an analyst designates, at a temporal resolution fine enough to reflect instruction interactions, and by ensuring those signals are functionally equivalent to the source hardware so the abstraction is sound — a property proved on the model genuinely holds on the chip. The crucial enabler is generating these models by lifting them from the hardware description with oracle-guided synthesis, hierarchically for scale, which replaces error-prone manual modeling with a mostly-automatic, correct-by-construction process. The payoff is concrete: analysis on the lifted model runs up to 8 times faster than on the source hardware, demonstrated on the Sodor five-stage core and components of the CVA6 processor. Read the scope precisely. Generation is semi-automatic, needing an oracle’s guidance and the analyst’s choice of signals-of-interest; the model is faithful only for the captured signals, so property soundness is scoped to them; the guarantee is soundness rather than a full performance study of complete systems; and the results are on particular cores. The durable idea is that the right way to make hardware security verification both trustworthy and scalable is not to model the whole chip or to model too little, but to automatically extract a sound, functional abstraction of exactly the part that matters — and that lifting, long used to recover structure from low-level software, can be brought to bear on hardware to do it.

Background

Why sound abstraction is the key to scalable verification

It helps to see this work within a principle that runs through all of formal verification: you can only prove things about systems too complex to reason about directly by abstracting them — throwing away detail — but the abstraction is trustworthy only if it is sound, meaning any property it establishes truly holds of the real system. The whole art is discarding enough to make analysis tractable while keeping enough, and provably faithfully, that the conclusions still transfer. Micro-update models embody this exactly for microarchitectural security: keep the functional behavior of the security-relevant signals, prove them equivalent to the hardware, and elide the rest. The GPU memory-model work covered elsewhere on this site reflects the same instinct from the specification side, capturing precisely what the hardware guarantees about concurrent memory in a form a tool can check, so that reasoning is grounded in an exact model rather than intuition. The common thread is that in hardware — with its caches, pipelines, and buffers interacting in ways no human tracks fully — informal reasoning is untrustworthy and full-detail reasoning is intractable, so progress depends on precise, sound abstractions, ideally generated rather than hand-built. As microarchitectural attacks keep multiplying and processors keep growing more complex, the ability to automatically lift accurate, security-relevant models from real designs is likely to become a standard part of how trustworthy hardware and software are built and checked together.

If you remember only three things

1. Hardware execution attacks (Spectre, Meltdown, and newer ones exploiting store and fill buffers) leak secrets through hidden microarchitectural state — caches, buffers, predictors — that a program is never meant to observe, so checking software for them requires analysis that reasons about that state. Verifying software directly against the full register-transfer-level hardware does not scale because it is too detailed, so the field uses abstract models that keep only the attack-relevant parts. But the model must be accurate, or it can wrongly declare insecure software secure, and hand-writing accurate models is tedious, error-prone, and expert-intensive. Existing model types each fall short: instruction-level models capture only software-visible state and treat instructions in isolation (missing pipeline interactions), while ordering-based models capture interactions but discard the functional behavior that properties like non-interference require.
2. The paper proposes micro-update models, a formalism that imperatively captures the functional behavior of just the user-chosen security-relevant signals, at a fine temporal resolution that reflects instruction interactions, eliding the rest of the design. By ensuring the captured signals are functionally equivalent to the source hardware, the model is sound: any security property (such as non-interference) proved on it also holds on the real hardware. To avoid error-prone manual modeling, the models are generated by lifting them from the register-transfer-level description — extending the lifting idea, long used to recover high-level code from low-level software, to hardware — using oracle-guided synthesis, done hierarchically so it scales to larger designs and is correct by construction. The framework is implemented in a prototype tool called PAUL.
3. Evaluated on the Sodor five-stage RISC-V processor and components of the CVA6 (Ariane) processor, the generated micro-update models let security analysis run up to 8 times faster than analyzing the source hardware, with hierarchical generation extending the approach to larger designs. Scope: generation is semi-automatic (an oracle guides the synthesis and the analyst picks the signals-of-interest), the model is faithful only for the captured signals so soundness is scoped to them, the guarantee is soundness rather than completeness, and the results are on specific cores. The durable lesson is that scalable, trustworthy hardware security verification comes from automatically extracting a sound, functional abstraction of exactly the security-relevant part of a design — not modeling the whole chip and not modeling too little — and that lifting can be brought from software to hardware to do it.

Check yourself

Check your understanding

1. Why must checking software for hardware attacks use a model, and why can't it just use the full hardware?
2. Why do the two existing kinds of model (instruction-level and ordering-based) each fall short?
3. What is a micro-update model, and what makes it sound?
4. How are micro-update models generated, and why is that important?

Sources

The paper is “Lifting Micro-Update Models from RTL for Formal Security Analysis” by Adwait Godbole, Kevin Cheang, Yatin A. Manerkar, and Sanjit A. Seshia, published at ASPLOS 2024, DOI 10.1145/3620665.3640418. The authors are at the University of California, Berkeley and the University of Michigan.

This explainer is based on the full text of the paper, obtained as the open-access (CC-BY) author copy hosted on an author’s university website. The problem framing (hardware execution attacks such as Spectre and Meltdown exploiting hidden microarchitectural state, the unscalability of verifying software directly against the full register-transfer-level hardware, the use of abstract models for scalable analysis, the accuracy requirement and the error-prone nature of hand-written models, and the shortcomings of instruction-level models — capturing only software-visible state and treating instructions in isolation — and axiomatic ordering models — capturing interactions but discarding functional behavior needed for properties like non-interference, illustrated by the load-buffer example), the contributions (micro-update models as an imperative, functional modeling formalism at fine temporal resolution that captures the signals-of-interest and ensures functional equivalence with the source hardware for soundness; the generation of these models by lifting from the register-transfer level using oracle-guided synthesis, performed hierarchically for scalability and correct by construction; and the prototype tool PAUL), and the evaluation (synthesizing micro-update models for the Sodor five-stage processor and components of the CVA6 / Ariane processor, hierarchical generation for scalability, and up to an 8 times run-time improvement when performing analysis with the generated models compared to the source hardware) are all drawn directly from the paper. Background explanations of microarchitecture, side channels, register-transfer-level descriptions, formal abstraction and soundness, lifting, and non-interference are standard and provided to make the paper’s contribution understandable.