Rage Against the State Machine: Type-Stated Hardware Peripherals for Increased Driver Correctness

Tyler Potyondy, Anthony Tarbinian, Leon Schuermann, Eric Mugnier, Adin Ackerman, Amit Levy and 1 other

A hardware chip's datasheet says exactly which commands are legal in which state, but the actual interface (memory-mapped registers) lets a driver poke anything at any time, so drivers routinely break the device's rules — dropping packets, hanging the bus, even igniting batteries; this paper (UC San Diego and Princeton — Tyler Potyondy, Amit Levy, Pat Pannuto, and colleagues) presents Abacus, which encodes a device's protocol into Rust's type system so the compiler rejects illegal commands, and crucially models the fact that modern hardware changes its own state behind the driver's back.

The argument in one glance

Problem

Hardware lets a driver do far more than it should ever do

A device driver is the software that controls a hardware peripheral, and it sits at a treacherous boundary: on one side, the hardware's datasheet is a strict specification — a device protocol saying exactly which operations are legal, often depending on what state the device is currently in — and on the other side, the actual interface the hardware exposes is wildly permissive. Devices are controlled through memory-mapped input-output (MMIO): their control registers appear as memory addresses, and the driver just reads and writes those addresses. Nothing stops the driver from writing anything, anywhere, at any time. So there is a yawning gap between what a driver is allowed to do and what it can do, and the only description of the rules is a natural-language PDF datasheet with no machine-checkable guardrails. When a driver crosses that line — issuing a command the specification forbids in the current state — it commits a device protocol violation. The consequences range from benign (the device ignores the command, or drops a packet), to crippling (powering off a peripheral while it has an active DMA transfer can hang the system bus and force a watchdog reset), to catastrophic (in the worst cases, igniting batteries). Drivers are also 70 percent or more of a modern operating system's code, written by many contributors, so these bugs are common and costly.
What people did

Write drivers in a safe language and constrain register access

The natural modern response is to use a memory-safe systems language like Rust, which by construction eliminates whole classes of bugs — out-of-bounds accesses, data races — and to add libraries that make the register interface less error-prone. Strongly-typed register libraries (such as tock-registers) constrain each register and bitfield access to be legal: you cannot write to a read-only field, and the types describe the layout. This closes off memory-safety bugs and illegal individual accesses, so the reasoning goes that safe languages plus typed registers should make drivers much more correct.
Why it fell short

Safety and typed registers still miss protocol violations

Memory safety and typed registers are necessary but not sufficient, because driver correctness is about more than any single access being well-formed — it is about the sequence and context of operations obeying the device's state-dependent protocol. Typed register libraries can say "this field is read-only," but they cannot express "this command is only legal while the device is in the idle state," because they do not track state. Traditional type-state programming — encoding the object's current state in its type so the compiler only permits operations valid in that state — can express state-dependent rules, and it works well when only software changes the state. But that assumption is exactly what modern hardware breaks: capable peripherals transition between states concurrently and independently of the software driver, for performance, parallelism, and power savings, often without notifying the driver. This creates "joint custody" of the state machine, shared between hardware and software. Standard type-states assume they alone control the state, so when the hardware moves the state on its own, the type system's belief about the current state becomes wrong, and it can no longer soundly enforce state-specific rules. Full formal verification could guarantee correctness, but it demands rare expertise and prohibitive effort for practical systems. What was missing was a lightweight, statically-checked way to encode a device's protocol that remains sound even when the hardware changes state behind the driver's back.
This paper's idea

Type-states that model hardware changing state on its own

Abacus is a Rust framework that statically prevents drivers from violating device protocols, by refining type-state programming so it can model hardware-software concurrency. Its central idea is a formalization of hardware states into two families: stable states, which only software can transition out of, and transient states, which can be exited by either software or the hardware itself. This distinction is what lets the type system reason soundly under joint custody: for a stable state, the compiler knows the device stays put until the driver acts, so it can enforce state-specific rules as usual; for a transient state, it accounts for the possibility that the hardware has already moved on, and constrains the driver accordingly. On top of this model, Abacus provides a domain-specific language in which a developer encodes a device's protocol invariants — bitfield rules, read-only and write-only restrictions, state transitions triggered by reads or writes, and state-specific register and bitfield access — in just tens of lines of code. Abacus then generates type-states from that specification, so the Rust compiler statically rejects any driver code that would violate the protocol, turning device-protocol bugs into compile errors. The authors integrate Abacus into drivers in two Rust operating systems (Tock and Redox) and find it imposes minimal to no overhead in code size and runtime, statically catches real device-protocol violations, and even makes it practical to use hardware features that were previously too complex to handle safely.

Why this problem is worth solving

Drivers are the largest and least-guarded part of an operating system, and their bugs reach from dropped packets to physical danger, so a way to make them provably obey the hardware is high-leverage.

Device drivers make up the majority of a modern operating system’s code — 70 percent or more — and they are written by a wide array of contributors with varying expertise, at the exact boundary where software meets physical hardware. That combination makes them a notorious and disproportionate source of operating-system faults and security exploits. And unlike a logic bug in an application, a driver bug can have physical consequences: issuing the wrong command to a peripheral can drop data, hang the system bus and force a reset, or in extreme cases damage hardware or ignite a battery. The root difficulty is that the hardware offers no guardrails at all — the interface is a permissive set of memory-mapped registers, and the rules for using them correctly live only in a human-readable datasheet. So every driver author is trusted to manually respect a complex, state-dependent protocol with nothing checking their work until something breaks at runtime, possibly catastrophically. Making the device protocol machine-checkable, so that violations are caught at compile time rather than in the field, therefore attacks one of the largest and riskiest surfaces in systems software. And because it works by construction, it protects even code written by contributors who do not fully understand the hardware’s subtleties, which is exactly the population that writes most drivers.

The key realization is that the state machine has two owners, and the type system must model that shared custody to stay sound.

Type-state programming is a beautiful fit for driver correctness in principle: encode the device’s state in the type, and the compiler will refuse to let you call an operation that is illegal in that state. But the whole approach rests on a hidden assumption — that the entity holding the type knows the true state, which is only true if nothing else changes it. In ordinary software-to-software use that holds. Hardware shatters it, because a capable peripheral advances its own state machine concurrently for performance and power reasons, sometimes without telling the software. Once the hardware can move the state independently, the driver’s type no longer reliably reflects reality, and any rule the type system enforces based on the assumed state may be wrong. Abacus’s insight is to make the shared custody explicit in the model itself, by splitting states into two kinds. Stable states are ones the hardware will not leave on its own, so the software’s knowledge of them is trustworthy and the compiler can enforce state-specific rules confidently. Transient states are ones the hardware might exit at any moment, so the type system must treat the software’s knowledge as provisional and only permit operations that remain safe regardless of whether the hardware has already transitioned. This two-family formalization is precisely what lets a static type system remain sound in the face of asynchronous hardware behavior — recovering the guarantees of type-state programming for the messy reality of modern devices, without resorting to full formal verification.

What people did before, and where it broke

Write drivers carefully by hand against the datasheet. Trust the author to follow the natural-language specification. Where it broke. There are no guardrails; the permissive MMIO interface lets any illegal command through, and violations surface only at runtime.
Use a memory-safe language like Rust. Eliminate out-of-bounds accesses and data races by construction. Where it broke. Memory safety does not cover device-protocol correctness — a memory-safe driver can still issue commands the hardware forbids in its current state.
Constrain registers with typed libraries. Use libraries like tock-registers so each register and bitfield access is legal. Where it broke. They validate individual accesses but do not track state, so they cannot express or enforce state-dependent protocol rules.
Apply traditional type-state programming. Encode the state in the type to enforce state-specific operations. Where it broke. It assumes only software changes the state; modern hardware transitions states independently, so the type’s belief about the state becomes wrong and enforcement becomes unsound.
The gap. No lightweight, static approach encoded a device protocol in a way that stays sound when hardware changes state on its own — leaving driver authors to respect complex state machines with no compile-time checking, short of prohibitively expensive full formal verification.

How Abacus works

From an unguarded register interface to compiler-enforced protocols

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

The idea

Encode the device’s state-dependent protocol in the type system so the compiler enforces it. Abacus makes a driver’s legal operations depend on the device’s state at the type level, so illegal commands become compile-time errors rather than runtime disasters. Using type-state reasoning to statically pin down which operations are valid in which state and catch violations before the code runs is the same principle the work on path-sensitive, alias-aware typestate analysis for detecting operating-system bugs (typestate analysis) covered elsewhere on this site is built on, turning a state-machine contract into a checkable property. Abacus brings that discipline to the driver-to-hardware protocol, where the state machine is the device’s own.

Formalize the hardware’s independent state transitions so the model stays sound. The heart of Abacus is modeling that hardware advances its own state machine concurrently, capturing this with the stable-versus-transient distinction so the type system reasons correctly under joint custody. Building an explicit model of how the hardware’s own state changes, so that software reasoning about correctness accounts for what the hardware does on its own, is the same undertaking the work on lifting micro-update models from RTL for formal security analysis (micro-update models) covered elsewhere on this site pursues, extracting the hardware’s state-transition behavior to reason about it rigorously. Abacus encodes that hardware behavior directly into the driver’s types.

Make it a lightweight, low-effort correctness tool, not heavyweight verification. Rather than full formal proofs, Abacus lets a developer specify a protocol in tens of lines of a domain-specific language and get static guarantees at essentially no runtime cost. Providing strong, machine-checked correctness through a modest, accessible specification effort instead of the rare expertise and prohibitive cost of full verification is the same trade-off the work on lightweight modular verification for WebAssembly-to-native compilation (lightweight modular verification) covered elsewhere on this site strikes, making rigorous guarantees practical for real systems. Abacus positions type-state refinement as that pragmatic middle ground between testing and proof for device drivers.

Following a driver operation through Abacus

Compiling a driver that talks to a stateful device

A trace, drawn from the paper, of how Abacus turns a protocol violation into a compile error.

Step 1 of 5

The developer encodes the device protocol

Using Abacus's domain-specific language, the developer writes the device's invariants in tens of lines — which registers and bitfields are legal in which state, which operations trigger state transitions, and which states are stable versus transient.

This replaces relying on the natural-language datasheet alone.

Why it works

Encoding state in the type makes illegal operations unrepresentable. A permissive interface lets any command through at runtime → but carrying the device’s state in the type and gating operations on it → so the compiler rejects illegal commands before the code runs.
The stable-transient split keeps the model sound under concurrency. Ordinary type-states assume software owns the state → but marking transient states the hardware can exit and constraining the driver accordingly → so the type system stays correct even when hardware transitions on its own.
A small DSL captures the protocol without heavy effort. Full verification needs rare expertise and huge effort → but encoding invariants in tens of lines of a domain-specific language → so real protocols are specified accessibly and checked automatically.
Static enforcement means zero runtime cost. Runtime checks would add overhead to hot driver paths → but resolving protocol legality entirely at compile time → so Abacus imposes minimal to no code-size or runtime overhead.
Compile-time guarantees protect non-expert authors. Most drivers are written by many contributors who may miss subtleties → but making violations fail to compile → so correctness holds by construction regardless of who writes the code.

What it costs (trade-offs and scope)

The protocol must be specified. Abacus’s guarantees come from a developer encoding the device’s invariants in its DSL; someone has to read the datasheet and write those tens of lines, and the guarantee is only as good as that specification.
It targets device-protocol violations, not all driver bugs. Abacus statically prevents commands that violate the hardware specification; it complements memory safety and typed registers rather than replacing them, and does not address bugs outside the protocol contract.
It is built on Rust’s type system. The approach refines type-state programming in Rust, so its benefits accrue to Rust-based drivers; applying the idea elsewhere would require comparable type-system support.
Modeling accuracy bounds the guarantee. The stable-versus-transient formalization and the encoded invariants must faithfully reflect the real hardware; a mis-modeled transition could let a violation through or reject legal code.
Reported results are from specific integrations. The minimal-overhead and bug-catching claims come from integrating Abacus into drivers in Tock and Redox on particular devices (Ethernet, UART, a wireless radio); other devices and systems may differ.

The comparison

Preventing device-protocol violations in drivers

Property	Memory-safe language + typed registers	Traditional type-state	Abacus
Catches illegal single access
Enforces state-dependent rules
Handles hardware changing state
Effort and expertise
Runtime overhead

A comparison of ways to prevent device-protocol violations in drivers. Memory-safe languages and typed registers catch illegal individual accesses but not state-dependent rules; traditional type-state enforces state-specific rules only when software alone changes the state. Abacus refines type-states with a stable-versus-transient formalization so protocols stay soundly enforced even when hardware transitions state independently, specified in tens of lines of a DSL with minimal to no runtime overhead. Exact details should be read from the paper.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 authors’ hosted copy at patpannuto.com). The described system is the paper’s: Abacus is a Rust framework that statically prevents drivers from violating device protocols. It refines type-state programming to model hardware-software concurrency and formalizes hardware states into two families: stable states, which only software can transition out of, and transient states, which can be exited by software or hardware. Abacus provides a domain-specific language in which developers encode device-protocol invariants — the paper’s Table 1 lists invariants such as bitfield modify, write-1-to-clear, write-only and read-only restrictions, state transitions on write and on read, and state-specific register and bitfield access — in tens of lines of code, and generates type-states that statically prevent device-protocol bugs. The paper motivates the work with real correctness and performance deficiencies in Ethernet, UART, and wireless-radio drivers in Rust-based OSes (Tock and Redox), and reports that integrating Abacus imposes minimal to no code-size and runtime overhead, statically detects device-protocol violations, and enables using hardware features that would otherwise be prohibitively complex. Background on device drivers, memory-mapped input-output, device protocols and datasheets, type-state programming, and DMA is standard context provided to make the approach intuitive. The step-by-step walkthrough is an illustration of the described mechanism. Exact formalization, the DSL design, and the full evaluation should be read from the paper.

Background

Why the hardware-software boundary keeps demanding better ways to encode contracts

It helps to see Abacus within a broad and persistent problem in systems: the interfaces between components carry contracts that are easy to state informally and hard to enforce mechanically, and the boundary between software and hardware is the most unforgiving instance of all. A device datasheet is a contract, but it is prose in a PDF; the hardware interface is a set of registers that will happily accept any write. The recurring lesson across systems research is that turning these informal contracts into machine-checkable ones — through types, static analysis, or verification — is what prevents whole classes of bugs by construction rather than by testing and hoping. The tension is always cost versus power: full formal verification is the strongest but is too expensive for most code, while pure testing is cheap but weak, so the field keeps searching for accessible, static methods that give real guarantees. Abacus is a clean instance aimed squarely at device drivers, the largest and buggiest part of an OS: it lifts the device protocol into the type system so the compiler enforces it, and its novelty is handling the fact that the other party to the contract — the hardware — can act on its own. This drive to catch software bugs early by encoding rich correctness properties into the type system, rather than discovering violations at runtime, is the same terrain the work on hybrid, sensitivity-aware type inference for type-assisted bug detection (Manta) covered elsewhere on this site occupies, using types to surface bugs before they run. Abacus’s particular contribution is to make type-state programming sound for the asynchronous, jointly-owned state machines that real hardware presents.

If you remember only three things

1. Device drivers sit between a strict hardware specification and a wildly permissive interface: hardware is controlled through memory-mapped registers that accept any read or write, while the rules for using them correctly — which operations are legal in which device state — live only in a natural-language datasheet with no guardrails. When a driver issues a command the protocol forbids in the current state, that device-protocol violation can range from benign (dropped packets) to crippling (powering off a peripheral mid-DMA hangs the bus) to catastrophic (igniting batteries). Because drivers are 70 percent or more of an OS's code and are written by many contributors, these bugs are common and dangerous. Memory-safe languages like Rust and typed register libraries help, but they catch illegal individual accesses, not state-dependent protocol rules — and traditional type-state programming, which can enforce state-specific rules, assumes only software changes the state, which modern hardware breaks by transitioning states on its own.
2. Abacus is a Rust framework that statically prevents device-protocol violations by refining type-state programming to model hardware-software concurrency. Its core idea is to formalize hardware states into two families: stable states, which only software can leave, and transient states, which the hardware can also exit at any time. This distinction lets the type system reason soundly under "joint custody" of the state machine — trusting the software's knowledge in stable states and treating it as provisional in transient ones. Developers encode a device's protocol invariants (read-only and write-only restrictions, bitfield rules, state transitions on reads or writes, and state-specific access) in tens of lines of a domain-specific language, and Abacus generates type-states so the Rust compiler rejects any driver code that would violate the protocol — turning protocol bugs into compile errors.
3. Integrated into drivers in two Rust operating systems (Tock and Redox), Abacus imposes minimal to no code-size or runtime overhead, statically catches real device-protocol violations, and makes previously too-complex hardware features practical to use safely — because the guarantees are entirely static, they cost nothing at run time and protect even non-expert driver authors by construction. The trade-offs and scope: the protocol must be specified in the DSL (and the guarantee is only as sound as that specification and the hardware model), Abacus targets device-protocol violations rather than all driver bugs, it builds on Rust's type system, and the reported results come from specific device and OS integrations. This explainer is based on the paper's full text.

Check yourself

Check your understanding

1. What is a device-protocol violation, and why are drivers prone to them?
2. Why do memory safety and traditional type-state programming not fully solve this?
3. What is Abacus's key idea for making type-states sound despite hardware changing state?
4. What does Abacus achieve, and what are the limits of the approach?

Sources

The paper is “Rage Against the State Machine: Type-Stated Hardware Peripherals for Increased Driver Correctness” by Tyler Potyondy, Anthony Tarbinian, Leon Schuermann, Eric Mugnier, Adin Ackerman, Amit Levy, and Pat Pannuto (UC San Diego and Princeton University), published at ASPLOS 2026, DOI 10.1145/3779212.3790207. A full-text copy is hosted by the authors at patpannuto.com.

This explainer is written from the paper’s full text (the authors’ hosted copy). Abacus is a Rust framework that statically prevents drivers from violating device protocols by refining type-state programming to model hardware-software concurrency, formalizing hardware states into stable states (only software can leave) and transient states (hardware or software can leave). Developers encode device-protocol invariants in tens of lines of a domain-specific language, and Abacus generates type-states so the Rust compiler rejects violating code. Integrated into drivers in two Rust OSes (Tock and Redox), the paper reports minimal to no code-size and runtime overhead, static detection of device-protocol violations, and the ability to use otherwise prohibitively complex hardware features. Background on device drivers, memory-mapped I/O, device protocols, and type-state programming is standard context. The numbers and claims are the paper’s own; exact mechanisms and full results should be confirmed in the paper.