Velosiraptor: Code Synthesis for Memory Translation

An operating system's security rests on correctly programming the machine's memory-translation and protection hardware — page tables, MMUs, and the like — but that low-level configuration code must be hand-written by an expert for every new memory hardware unit, taking weeks and risking subtle bugs that silently break isolation; this paper (University of British Columbia — Reto Achermann, Em Chu, Ryan Mehri, Ilias Karimalis, Margo I. Seltzer) presents Velosiraptor, which lets a developer write only a high-level description of the hardware's mapping behavior and the OS environment, then automatically synthesizes verified low-level code that programs the hardware — using divide-and-conquer to shrink the synthesis search space by orders of magnitude so it adds negligible time to a kernel build, and even generating a simulated hardware model from the same spec to prototype new translation mechanisms.

The argument in one glance

Problem

An OS's isolation depends on hand-written code that programs the memory hardware

Operating systems keep applications isolated from each other, and that isolation ultimately rests on correctly configuring the machine's memory hardware — the translation and protection units, such as page tables and memory management units (MMUs), that decide which physical memory each access may reach and with what permissions. A single memory access may pass through several such units, each of which the OS must program with exactly the right entries and permission bits, or the integrity and isolation guarantees the OS promises simply break. Writing that low-level configuration code is the OS developer's job, and it demands precise knowledge of every memory hardware unit and its idiosyncrasies. It is manual and painstaking, and getting a single bit wrong can silently open a security hole. Because it sits directly under the OS's security guarantees, this is mission-critical code — and it is written by hand.
What people did

Have OS developers hand-write the configuration code per platform

The standard practice is exactly this: for each memory hardware unit on each platform, an expert developer studies the hardware manual and writes the low-level code that programs it — filling page table entries, setting permission bits, issuing the maintenance operations. When the OS is ported to new hardware, or the hardware adds a new translation or protection mechanism, a developer writes new code for it. This is how memory-hardware support has always been built.
Why it fell short

Hand-coding is slow, repetitive, and a source of security-critical bugs

Manual configuration code has three problems. It is slow and repetitive: writing the code to program a single memory hardware unit can take weeks, and modern platforms have many such units with subtly different features and configuration options. It is a recurring cost, not a one-off: hardware designers constantly develop new translation and protection mechanisms, so the OS code must be adapted for every new platform, again and again. And it is dangerous: the code is intricate and its correctness is security-critical, so subtle mistakes — a wrong permission bit, a missed maintenance operation — introduce bugs that break the very isolation and integrity guarantees the OS exists to provide, and such bugs are easy to make and hard to catch. What is missing is a way to produce correct memory-hardware configuration code without relying on error-prone expert hand-coding for every unit and every platform.
This paper's idea

Describe the hardware's behavior, and synthesize verified code from it

Velosiraptor automatically generates correct, low-level OS code that programs a machine's memory hardware. Instead of hand-writing the code, a developer writes only a high-level description — in a domain-specific language — of the memory hardware's mapping behavior (how it translates and protects addresses) together with the OS environment. Velosiraptor models memory hardware abstractly: a unit either maps an input address to an output (given an access mode and its configuration state) or raises an exception, so map behavior is a partial function, and the synthesis task is to find a sequence of hardware-configuration operations that makes the actual behavior match the spec for operations like map, unmap, and protect. The toolchain, implemented in Rust and using the Z3 solver, generates candidate programs from a grammar and verifies each against the specification, producing a verified implementation that links directly into the OS. Naive program search would be intractable, so Velosiraptor exploits the domain's structure with a divide-and-conquer strategy that shrinks the search space by orders of magnitude, making synthesis fast enough that it adds negligible time to a kernel build (about a second for x86-64 page tables versus a 154-second kernel build). And because the same behavioral specification also describes the hardware, Velosiraptor can generate a simulated hardware component from it, letting researchers prototype entirely new translation and protection mechanisms.

Why this problem is worth solving

The code that programs memory hardware is small, obscure, and load-bearing for the entire security of a system.

Every memory access a program makes is mediated by hardware that decides where it actually goes and whether it is allowed. Translation hardware, such as the page tables walked by a memory management unit, maps the virtual addresses a program uses to physical addresses in memory; protection hardware attaches permissions, deciding whether a given access mode (read, write, execute) is permitted. Modern platforms have many such units — MMUs for CPUs, translation and protection units for other chip components — and a single access may traverse several of them before reaching memory. The operating system is responsible for programming all of this: it fills in the page table entries and permission bits so that each application can reach only its own memory and only in permitted ways, which is exactly what enforces isolation between untrusted applications sharing a machine. This makes the configuration code mission-critical: it is the concrete mechanism behind the OS’s abstract promise of integrity and isolation. Yet it is also low-level, fiddly, and hardware-specific — the developer must know each unit’s exact layout and configuration protocol. Because so much rides on code that is this detailed and this easy to get subtly wrong, automating its production correctly is valuable out of proportion to the code’s size, which is what motivates treating memory-hardware configuration as a synthesis problem.

The reason hand-coding is a persistent burden is that the target keeps moving and the mistakes are catastrophic.

Two forces make manual configuration code painful. The first is churn: memory hardware is not fixed. Vendors continually introduce new translation and protection mechanisms — new page table formats, new protection units, new features and configuration interfaces — so an OS being ported to a new platform, or updated for new silicon, needs fresh low-level code for each unit, and writing that code for even one unit can take weeks of an expert’s time studying manuals and testing. This work is repetitive across units and platforms, yet it cannot be skipped, because without it the hardware is not correctly programmed. The second force is fragility: the code’s correctness is security-critical in a way ordinary code is not. A single wrong permission bit or a forgotten cache-maintenance or barrier operation does not just cause a functional bug; it can silently break the isolation and integrity guarantees that keep untrusted applications from reading or corrupting each other’s memory, and such a flaw may go unnoticed until it is exploited. So the OS community pays, over and over, for hand-writing intricate code where errors are both easy to make and disastrous. That combination — a moving target and unforgiving stakes — is precisely the situation where automatic generation of provably correct code, from a description of what the hardware does rather than how to program it, would pay off enormously, which is the opportunity Velosiraptor pursues.

What people did before, and where it broke

Hand-write configuration code per hardware unit. An expert reads the manual and writes the low-level code that programs each memory hardware unit. Where it broke. It takes weeks per unit, is intensely repetitive across many units and platforms, and its security-critical correctness is easy to get subtly wrong.
Reuse and adapt existing OS memory code. Port and tweak code written for a previous platform. Where it broke. New hardware has different formats, features, and configuration protocols, so adaptation is itself manual, error-prone work, and subtle mismatches reintroduce security bugs.
Test the configuration code. Rely on testing to catch mistakes in hand-written memory-hardware code. Where it broke. Testing samples behaviors and can miss the specific corner cases where a permission bit or maintenance operation is wrong, exactly the silent failures that break isolation.
General program synthesis. Apply off-the-shelf synthesis to generate the code. Where it broke. The space of candidate low-level programs is astronomically large, so generic synthesis does not scale to producing memory-hardware configuration code efficiently.
The gap. No system let developers describe memory hardware’s mapping behavior at a high level and then automatically synthesized verified low-level configuration code from it, efficiently enough to fit into a normal build and general enough to cover diverse and new hardware.

How Velosiraptor works

From a behavioral spec of memory hardware to verified configuration code

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

The idea

Describe what the hardware does, and let synthesis figure out how to program it. The central shift in Velosiraptor is to raise the developer’s task from writing low-level configuration code to writing a high-level behavioral specification of the memory hardware’s mapping, and then automatically generating the code. The developer says what the hardware should do — how it translates and protects addresses — and Velosiraptor synthesizes the sequence of configuration operations that achieves it, verified against the spec. Reasoning about memory translation and how the OS should program it, and doing that work for the developer rather than leaving it as hand-tuned low-level code, is the same concern the work on direct memory translation for virtualized clouds covered elsewhere on this site engages, treating address translation as a systems problem to be handled well rather than by rote. Velosiraptor recasts it as a synthesis problem, where the input is a description of behavior and the output is correct code.

Synthesize the code with a solver, from a grammar of operations. The engine is program synthesis: Velosiraptor formulates the problem for an SMT solver, generates candidate programs from a grammar of hardware-configuration operations, and verifies each candidate against the specified behavior with Z3, emitting only a program it can prove correct. Using a solver to search for and validate an implementation that provably meets a high-level specification, rather than writing it by hand, is the same solver-aided synthesis discipline the work on a solver-aided compiler for packet-processing pipelines covered elsewhere on this site is built on, letting a solver construct correct low-level code from intent. Velosiraptor applies it to the specific domain of memory-hardware configuration, where the correctness obligation is the map behavior the hardware must realize.

Produce verified code, because the stakes are security. Because a bug in memory-hardware configuration silently breaks isolation, Velosiraptor does not just generate plausible code; it generates a verified implementation, checking each synthesized program against the specification so the result is provably correct by construction. Producing low-level code that is formally guaranteed to preserve a security-critical property, rather than trusting hand-written code and hoping tests catch the holes, is the same assurance-by-construction goal the work on protecting cryptographic code against Spectre with machine-checked proofs covered elsewhere on this site pursues, generating code whose security is proved, not assumed. Velosiraptor gives the OS memory-configuration layer that same guarantee, which matters precisely because this is the code isolation depends on.

Following a spec through Velosiraptor

Synthesizing page-table code from a hardware description

A trace, drawn from the paper, of how Velosiraptor turns a behavioral spec into verified memory-hardware configuration code.

Step 1 of 5

Write the memory hardware's behavior in the DSL

The developer describes, in Velosiraptor's domain-specific language, how the target unit (say an x86-64 page table) maps addresses: what state permits an access, what output an input maps to under a given mode, and when it raises an exception, along with the OS environment.

The developer specifies behavior, not the low-level programming sequence.

Why it works

A behavioral spec is easier and safer than hand-coding. Writing low-level configuration code by hand is slow and error-prone → but describing the hardware’s mapping behavior once is concise and captures intent → so the developer avoids the fiddly, security-critical coding entirely.
Verification makes the generated code trustworthy. Synthesized code could be wrong in subtle, isolation-breaking ways → but Velosiraptor proves each candidate matches the specification with an SMT solver → so the result is correct by construction, not by testing.
Divide-and-conquer makes synthesis tractable. The space of candidate low-level programs is astronomically large → but exploiting the domain structure of memory hardware shrinks it by orders of magnitude → so synthesis finishes in about a second and adds negligible time to a build.
Feasibility checking avoids hopeless searches. Some hardware simply cannot express an operation like unmapping → but an up-front feasibility query detects this → so Velosiraptor reports no program instead of searching forever.
One spec serves software and hardware. A behavioral description of memory hardware could be used only to generate code → but the same spec also defines the hardware itself → so Velosiraptor can emit a simulated hardware model, enabling research on new translation mechanisms.

What it costs (trade-offs and scope)

Someone must write an accurate behavioral specification. Velosiraptor replaces hand-written configuration code with a high-level description of the hardware’s mapping behavior and the OS environment; producing a correct specification is real work and expertise, and the generated code’s correctness is relative to that specification faithfully capturing the hardware.
Correctness is with respect to the spec and the solver. The verification proves the synthesized code realizes the specified behavior using Z3; it does not guarantee anything the specification omits or misstates, and it rests on the solver and the operational model being sound.
Synthesis is fast but not free, and depends on the hardware. Divide-and-conquer keeps synthesis to about a second for x86-64 page tables, but more complex mechanisms (the paper notes x86 segmentation is markedly slower) take longer; the runtime is negligible relative to a kernel build for the cases shown, but it varies with the hardware’s complexity.
It targets memory translation and protection configuration. Velosiraptor synthesizes the code that programs memory translation and protection units; it is not a general OS-code generator, and other parts of porting an OS remain the developer’s responsibility.
The evaluation covers specific units and a specific backend. The results (for example x86-64 page tables and x86 segmentation, and hardware generation for the Arm Fast Models) are for the memory hardware and toolchain the authors implemented; other units, formats, and platforms would need their specifications and may exercise the synthesizer differently.

The evaluation

Producing memory-hardware configuration code for an OS

Property	Hand-written per platform	Generic program synthesis	Velosiraptor
Developer effort
Correctness
Synthesis scalability
Adapts to new hardware
Reported outcome

A qualitative comparison of ways to produce memory-hardware configuration code. Velosiraptor synthesizes verified code from a high-level behavioral specification, with divide-and-conquer keeping synthesis fast (about a second for x86-64 page tables versus a 154-second kernel build), and can generate a simulated hardware model from the same spec.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 (arXiv:2608.07966). The mechanism described is the paper’s: Velosiraptor automatically generates correct, low-level OS code that programs a machine’s memory hardware from a high-level, domain-specific-language description of the hardware’s mapping behavior and the OS environment; it models memory hardware as a partial map function (mapping an input address to an output under an access mode and state, or raising an exception), formulates synthesis of the configuration operations for map, unmap, and protect, checks feasibility and verifies candidate programs with the Z3 SMT solver, and uses a divide-and-conquer strategy (plus a query cache and handling of caches, maintenance operations, and barriers) to reduce the search space by orders of magnitude; it is implemented in Rust and can also generate a simulated hardware module (for the Arm Fast Models) from the same specification. The reported results are the paper’s own: synthesis is fast relative to kernel compilation (about one second for x86-64 page tables versus a build of more than 154 seconds), with x86 segmentation notably slower, and the same specification supports both OS-code and hardware generation. Exact DSL and synthesis details, the full set of evaluated hardware, and the complete results should be read from the paper.

Background

Why systems are turning low-level code into synthesis problems

It helps to see Velosiraptor as part of a broad movement to replace hand-written, error-prone, low-level systems code with code synthesized from high-level specifications and formally verified. For decades, the most security- and correctness-critical pieces of a system — memory-management code, device drivers, network dataplanes, cryptographic routines — were written by experts by hand, precisely because they are intricate and hardware-specific, and precisely there the cost of a subtle bug is highest. The maturing of solver-based synthesis and verification changed the calculus: if you can capture what the code must do as a specification, a solver can often search for an implementation and prove it correct, turning a fragile manual effort into a repeatable, trustworthy pipeline. This is attractive wherever the domain is narrow enough to make synthesis tractable and the correctness stakes high enough to justify verification — and memory-hardware configuration fits both, because its behavior is describable as address mapping and its bugs break isolation. A recurring bonus, which Velosiraptor exploits, is that a behavioral specification is dual-use: the same description that generates the software can generate a model of the hardware, tightening the hardware-software co-design loop. That broader effort to rethink how the memory system is specified and mapped, treating address mapping itself as something to design and generate rather than hard-wire, is the same spirit the work on software-defined address mapping covered elsewhere on this site shares. Velosiraptor brings synthesis and verification to the OS code that programs the memory hardware, where correctness is not optional.

If you remember only three things

1. An operating system's isolation and integrity guarantees depend on correctly programming the machine's memory-translation and protection hardware (page tables, MMUs, and other units), but that low-level configuration code is written by hand for each unit and platform. Hand-coding is slow (weeks per unit) and repetitive, must be redone as vendors introduce new translation and protection mechanisms, and is a source of subtle, security-critical bugs that silently break isolation.
2. Velosiraptor lets a developer write only a high-level, domain-specific-language description of the memory hardware's mapping behavior and the OS environment, then automatically synthesizes verified low-level configuration code. It models a unit as a partial map function (input address plus access mode and state either maps to an output or raises an exception), formulates synthesis of the map, unmap, and protect operations, and generates candidate programs verified against the spec with the Z3 SMT solver. A divide-and-conquer strategy exploits the domain's structure to shrink the search space by orders of magnitude, and the same specification can also generate a simulated hardware model.
3. The verified code links directly into the OS, so porting to new memory hardware needs no hand-written configuration code, and synthesis is fast enough to be negligible in a build (about a second for x86-64 page tables versus a 154-second kernel build), while the dual hardware generation (for the Arm Fast Models) enables research into new translation mechanisms. Velosiraptor requires an accurate behavioral spec, its guarantees are relative to that spec and the solver, synthesis time grows with hardware complexity, and it targets memory-translation-and-protection configuration specifically.

Check yourself

Check your understanding

1. Why is hand-writing memory-hardware configuration code such a problem for OS developers?
2. What is Velosiraptor's core idea?
3. Why does Velosiraptor use divide-and-conquer, and why does it verify the generated code?
4. What did Velosiraptor achieve beyond generating OS code, and what are its limits?

Sources

The paper is “Velosiraptor: Code Synthesis for Memory Translation” by Reto Achermann, Em Chu, Ryan Mehri, Ilias Karimalis, and Margo I. Seltzer (University of British Columbia, with work done there by co-authors now at JuliaHub and Replit), published at ASPLOS 2025, DOI 10.1145/3676641.3711998. It is licensed CC BY.

This explainer is written from the paper’s full text (arXiv:2608.07966). The paper presents Velosiraptor, a system that automatically generates correct, low-level OS code that programs a machine’s memory hardware, addressing the problem that a secure runtime relies on the OS to correctly configure memory translation and protection hardware, that adapting the OS code to new hardware is manual, repetitive, and time-consuming, and that it may introduce subtle but security-critical bugs. With Velosiraptor, developers write only a high-level, domain-specific-language description of the memory hardware’s mapping behavior and the OS environment, and the toolchain transforms this specification into a verified implementation that links directly with the rest of the operating system; the same specification can also be used to generate hardware components, enabling research into new translation mechanisms. Velosiraptor models memory hardware as a partial map function (an input address, access mode, and state either map to an output or raise an exception), formulates the synthesis of configuration operations, checks feasibility and verifies candidate programs with the Z3 SMT solver, and uses a divide-and-conquer strategy that exploits domain specificity to reduce the candidate search space by orders of magnitude; it is implemented in Rust and includes a backend that generates memory-hardware modules for the Arm Fast Models. The reported results are the paper’s own: synthesis is fast relative to kernel compilation (about one second for x86-64 page tables versus a build of more than 154 seconds, with x86 segmentation notably slower), the search-space reduction is effective, and the same specification supports both software and hardware generation. No numbers beyond the paper’s own have been introduced; exact DSL and synthesis details, the full set of evaluated hardware, and the complete evaluation should be confirmed in the paper.