Velosiraptor: Code Synthesis for Memory Translation

Velosiraptor: Code Synthesis for Memory Translation Reto Achermann

Em Chu∗

Ryan Mehri∗

University of British Columbia Vancouver, BC, Canada

JuliaHub Boston, MA, USA

Replit San Francisco, CA, USA

Ilias Karimalis

Margo Seltzer

University of British Columbia Vancouver, BC, Canada

University of British Columbia Vancouver, BC, Canada

arXiv:2608.07966v1 [cs.OS] 8 Aug 2026

Abstract Security is among the top concerns of operating system (OS) developers. A secure runtime environment relies on the OS to correctly configure the memory hardware on which it runs. This is mission-critical as it provides essential securityrelevant features and abstractions that ensure the integrity and isolation of untrusted applications running alongside each other. Configuring a platform’s memory hardware is not a one-off effort as designers constantly develop new mechanisms for translation and protection with different features and means of configuration. Adapting the OS code to the new hardware is not only a manual, repetitive and timeconsuming task, it may also introduce subtle, but securitycritical bugs that break security and isolation guarantees. We present Velosiraptor, a system that automatically generates correct, low-level OS code that programs the memory hardware of a machine. Velosiraptor leverages software synthesis techniques and exploits the domain specificity of the problem to make the synthesis process efficient. With Velosiraptor, developers write only a high-level description of the memory hardware’s mapping behavior and OS environment. The Velosiraptor toolchain transforms this specification into a verified implementation that can be linked directly with the rest of the operating system. Incorporating the OS environment into this process allows porting an OS to new hardware platforms without worrying about writing code to configure the memory hardware. We can also use the same specification to generate hardware components. This enables research in new translation mechanisms, freeing up OS developers from manually writing OS code. CCS Concepts: • Software and its engineering → Virtual memory; Automatic programming; Functionality. ∗ Work done while at The University of British Columbia.

This work is licensed under a Creative Commons Attribution 4.0 International License. ASPLOS ’25, Rotterdam, Netherlands © 2025 Copyright held by the owner/author(s). ACM ISBN 979-8-4007-1079-7/25/03 https://doi.org/10.1145/3676641.3711998

ACM Reference Format: Reto Achermann, Em Chu, Ryan Mehri, Ilias Karimalis, and Margo Seltzer. 2025. Velosiraptor: Code Synthesis for Memory Translation. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2 (ASPLOS ’25), March 30-April 3, 2025, Rotterdam, Netherlands. ACM, New York, NY, USA, 17 pages. https://doi.org/ 10.1145/3676641.3711998

1

Introduction

Today’s computer systems contain many memory protection units (MPUs), memory management units (MMUs), and other memory hardware or features that mediate access to memory resources. A single memory access may traverse multiple hardware units until it reaches its destination. Generally, those hardware components provide mapping functionality that can be split up into protection and translation [6]. Protection determines if a specific memory access is permitted. This involves checking whether the input address is valid and the access mode or source of the memory access is permissible given the protection attributes (e.g., write, privilege level, or a specific device). Translation is the process of transforming the address of a memory access. Mapping is a partial function from an input address to an output address, i.e., the mapping attempt can fail due to an invalid address or insufficient permissions. The OS must program all memory hardware units of the machine correctly, including the processor’s MMUs, the System MMU, and other memory translation and protection units isolating individual hardware components to ensure the security of applications [26–28]. This means that OS developers must have precise knowledge of all the memory hardware and all its subtle differences in their features and configuration options. For example, the OS must set the right permission flags or memory attributes in the page table entry. Therefore, the developer has to manually write the low-level OS code that programs the mapping hardware. Unfortunately, writing code to configure memory hardware is not a one-time effort and can take weeks [54]. Modern platforms have many different memory hardware units mediating access to and from various chip subsystems. Those units have a diverse set of features and means of configuration that the developer needs to understand. Thus, the

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands

developer has to spend a significant amount of time repeating the same task: reading the hardware manual and then manually writing and debugging configuration code – a process that easily introduces subtle bugs [34, 45, 46, 48–51] amplified by the repetition. Any error in the configuration sequence can break system security, allowing applications to inadvertently corrupt data or obtain unauthorized access to resources of other applications. We build upon previous work [5] and present Velosiraptor 1 , a system that automatically generates correct memory configuration code. In Velosiraptor, developers no longer need to manually and tediously write this code. Instead, they obtain a behavioral specification of the memory hardware as part of the technical hardware manual, or they write a specification that closely matches the description in the manual. This behavioral specification defines how the memory hardware performs address mapping. The Velosiraptor toolchain then constructs a model of the memory hardware and uses software synthesis to automatically generate the OS code that configures the memory hardware. The behavioral specification needs to be written once per mapping unit. Velosiraptor then tailors the generated code to a target environment by using an OS specification that describes, for instance, the memory allocation functions or capability invocations. Velosiraptor leverages domain-specific knowledge to make software synthesis efficient. Velosiraptor uses divide-andconquer to reduce the search space of candidate programs by orders of magnitude, resulting in a negligible kernel compilation time overhead. This makes Velosiraptor a viable approach to automatically generating correct, low-level, memory hardware configuration code. Velosiraptor also enables research into new memory translation and protection mechanisms by generating a simulated hardware component from the same behavioral specification. This lets developers evaluate the utility of proposed, but non-existent memory hardware [15, 29, 40]. Researchers no longer have to build a hardware implementation to evaluate the efficacy of a newly proposed translation and/or protection mechanism. Currently, Velosiraptor supports the Arm Fast Models [10], a functionally accurate platform simulator. We make the following contributions: • A methodology to efficiently synthesize code interfacing with memory hardware (Section 4 and Section 6.2), • a domain-specific language to concisely express the behavior of memory hardware (Section 3), • the implementation of Velosiraptor in Rust that uses Z3 for program verification (Section 5), • a backend for Velosiraptor that generates memory hardware modules for the Arm Fast Models (Section 5.6), • a quantitative evaluation showing the effectiveness of the search space reduction and the efficiency of the synthesis process (Section 6.3), and 1 Velosiraptor is a wordplay on VLSI – synthesis for hardware logic.

Reto Achermann, Em Chu, Ryan Mehri, Ilias Karimalis, and Margo Seltzer

• a qualitative demonstration of the functionality of the generated memory hardware module and the adaption of the generated code to the OS environment (Section 6.5).

2

Modeling Memory Hardware Behavior

Modern memory hardware is diverse in both the features it provides (e.g., means of translation and protection) and how the hardware is programmed (e.g., registers and translation descriptors). For example, both Arm and x86 use an in-memory page table to define virtual-to-physical address translation. They offer similar functionality but have different layouts. The Xeon Phi co-processor [36] uses an array of registers to control memory accesses to the host memory. Despite their heterogeneity, they share many common characteristics that allow for a common, abstract model that expresses their mapping behavior. For example, determining if the hardware maps a given input depends on state that is stored either in registers or an in-memory data structure. We use the term map to encompass both translation and access control. From the behavioral model, we define an operational model that captures the concrete state and software visible interface. Finally, we define the basic building block and composition rules with well-defined semantics. 2.1

Behavioral Model

Abstractly, all memory hardware units either successfully map an address or raise an exception. Thus, we can model map behavior as a partial function from an input address, an access mode (e.g., read, write, execute, . . . ), and the memory hardware state (e.g., register contents) to an output address. map :: 𝑖𝑛𝑎𝑑𝑑𝑟 → 𝑚𝑜𝑑𝑒 → 𝑠𝑡𝑎𝑡𝑒 ⇀ 𝑜𝑢𝑡𝑎𝑑𝑑𝑟 Input and output addresses may be ordinary memory addresses or they may also contain source information, e.g., which core or device initiated the memory access. The set of possible access modes can be defined per mapping unit, e.g., to include processor modes such as user and supervisor mode. The state includes everything that can influence translation (e.g., registers and in-memory data structures such as page tables). The map() function produces an output address if and only if the state permits access to the input address under the current access mode. Mathematically, the map() function produces an output address if and only if the input values are part of the function’s domain: (𝑖𝑛𝑎𝑑𝑑𝑟, 𝑚𝑜𝑑𝑒, 𝑠𝑡𝑎𝑡𝑒) ∈ 𝑑𝑜𝑚(map). For example, the corresponding entry in the page table must be valid and have the right permission bits set, otherwise, an exception is raised. We currently focus on the mapping behavior and leave triggering a specific exception class (e.g., the distinction between a translation fault and a write fault) for future work. 2.2

Operational Model

Figure 1 depicts the operational model of a mapping unit (we use this term to refer to any memory hardware component

Velosiraptor : Code Synthesis for Memory Translation Software data plane

load/store Input

addmap()/setperms()/delmap() interface operations reg

(inaddr,mode)

exception

map()

(outaddr,mode)

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands

state query

mem mmio instr

Interface state update reg

control plane

mem

State

Output

Unit

Figure 1. The behavioral model of a mapping unit. fn addmap ( va : vaddr , sz : size , f : flags , pa : paddr , s: State ) -> (s ': State ) ensures forall v : vaddr , m : mode :: 4 inrange (va ,sz , v ) == > ( translate (s ' , v ) == pa +( v - va ) && ( allows (f , m ) <== > (v ,m ,s ') in dom ( map ) ) )

2

6

fn setperms ( va : vaddr , sz : size , f : flags , pa : paddr s: State ) -> (s ': State ) ensures forall v : vaddr , m : mode :: 10 inrange (va ,sz , v ) == > ( translate (s ' , v ) == translate (s , v ) && ( allows (f , m ) <== > (v ,m ,s ') in dom ( map ) ) ) 8

12

fn delmap ( va : vaddr , sz : size , f : flags , pa : paddr s: State ) -> (s ': State ) ensures forall v : vaddr , m : mode :: 16 inrange (va ,sz , v ) == > (v ,m ,s ') not in dom ( map ) 14

Listing 1. Synthesis target function specifications where map() refers to the map-function defined in Section 2.1 that mediates memory accesses through address translation or access control). The operational model of a mapping unit consists of three main components: map(), state, and interface (shown by the dark boxes in Figure 1). It resembles a state machine where each state has a well-defined mapping behavior. The state consists of registers and memory locations, and the OS triggers state transitions by reading or writing special or MMIO registers or memory locations or executing specific instructions. Similar to a network switch, the operational model consists of a data plane and a control plane, but instead of processing network packets, it processes memory accesses, i.e., load or store instructions or DMA transfers. 2.2.1 Synthesis Target Specifications. The memory management subsystem must provide three functions: addmap adds a new mapping from an input address range to an output address range with specified permissions, setperms changes the access permissions of an address range, and delmap removes a mapping. Listing 1 shows the corresponding function signatures, which serve as the specifications for our synthesis targets. The predicate allows(f, m) defines whether the access mode is permitted given the supplied permission flags. The synthesis task is then to find an implementation by finding a sequence of state machine transitions (i.e., interface interactions) that produces the goal state defined as post-conditions. Note, that there is an implicit postcondition ensuring that the behavior outside of the specified address range is not changed. 2.2.2 Control Plane. We model the control interface as a state machine. The state of a mapping unit is a sequence

of bits, stored in registers or memory locations and includes all relevant parts that define the mapping behavior. For example, on x86, the page table defines the virtual-to-physical address translation, whereas the CR4 (control register 4) defines whether the mapping is enabled [37]. The control interface of the mapping unit defines the transitions of the state machine. Each transition is atomic, takes a sequence of arguments and an input state, and produces a well-defined, new state. Examples include updating a page table entry, writing the translation base register, or executing the tlbwr instruction on the MIPS R4700 [35]. Formally, this is: transition :: 𝑆𝑒𝑞<𝑎𝑟𝑔> → 𝑠𝑡𝑎𝑡𝑒 → 𝑠𝑡𝑎𝑡𝑒 We expect that most transitions take zero or one machineword-sized argument, representing the payload of load, store or other instructions. A special init-transition defines the bit pattern of the initial state. The control interface then consists of a set of transitions and the init transition. In the model, the OS cannot access the state of the mapping unit directly. Instead, the OS interacts with the control interface – the mapping unit’s public API. To change a unit’s mapping behavior, the OS puts the state machine into the desired state by applying the right sequence of atomic transitions. This notion becomes important in Section 4.3 as the available state transitions correspond to the grammar of the programs that are needed to configure the mapping behavior. 2.2.3 Data Plane. Recall, that the mapping has two parts: translation and access control. A boolean expression distinguishes whether the map() function produces an error or an exception (we do not model different exception types). We express access control checks as boolean predicates in conjunctive normal form. The conjuncts are boolean functions defined over the input address, access mode, and state. Output address computation occurs if, and only if, all the conjuncts evaluate to true; otherwise the unit raises an exception. Formally, we express this as: Û (𝑎𝑑𝑑𝑟, 𝑚𝑜𝑑𝑒, 𝑠𝑡𝑎𝑡𝑒) ∈ 𝑑𝑜𝑚(map) ⇔ 𝑝 (𝑎𝑑𝑑𝑟, 𝑚𝑜𝑑𝑒, 𝑠𝑡𝑎𝑡𝑒) 𝑝 ∈𝑃

If the input address is outside of the valid range or the access mode is not permitted, at least one of the conjuncts evaluates to false, rendering the map() function undefined for the input arguments. The formalization using the conjuncts helps us state the problem of synthesizing the correct configuration program for the mapping unit (Section 4.4). 2.3

Composition of Building Blocks

Given the diversity in memory hardware, we designed a methodology of basic building blocks and composition rules from which we compose specifications hierarchically. This modular approach makes synthesis easier and more amenable to optimization [32]. After analyzing more than 12 different memory hardware units, we were pleasantly surprised that we identified only one basic building block and two composition rules from which we could specify all of them.

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands

2.3.1 The Basic Building Block. The basic building block is a segment that maps a contiguous input address range to a contiguous output address range. The output address range might be the ultimate result of a map or it might be an intermediate result, providing the address of the next unit in a structure such as the x86 tree-based page table. The segment has both a state and a control interface. The input or output address range, i.e., the base address and size, may be either fixed (i.e., hardwired to a certain value) or configurable (e.g., computed from the state). For example, the Xeon Phi entry system memory page table [36] maps a fixed input address range of 16 GB. In contrast, the x86 segment descriptor [37] allows mappings of different sizes, and x86 page directory entries may map to the next-level page table encoding the tree structure. 2.3.2 Combining Basic Building Blocks. Developers combine segments using the composition rules. Each rule has well-defined semantics and dictates constraints on the composite state arising from the combined states of the basic building blocks. Rules do not have state or control interfaces. Enumeration. Enumerations provide a way to create a structure akin to a C union from two or more segments. Each variant of the enumeration is a segment that has the same state bits, but it may interpret those state bits differently. For example, a page directory entry can map a large frame or a page table, depending on whether the page-size bit is set. Variants must be non-conflicting, i.e., the state must unambiguously identify which segment description provides the right interpretation of the state. StaticMap. A static map defines a table-like construct composed of a collection of entries, each of which covers an independent, non-overlapping, and contiguous address range. Each entry in a static map may be either a segment or an enumeration, but not another static map. In principle, Velosiraptor supports entries of different types, but we have not encountered this in the mapping units we analyzed. Some part of the input address must specify which table entry contains the mapping for the input address. Like the enumeration, the map links the state of the referenced segments together, adding constraints on the combined state. 2.3.3 Composition Example. We use a simplified representation of the four-level x86_64 virtual address translation as an illustrative example (we exclude segmentation and the TLB for simplicity). From the manual [37], we learn that address mapping accesses a four-level radix tree of in-memory descriptor tables, a translation base register (CR3), and registers that control translation features such as physical address extension and whether the MMU is enabled (omitted in Figure 2). The OS configures the mapping behavior by writing specific bit patterns into the registers or page table entries. Figure 2 shows the decomposition of the x86_64 address translation into Velosiraptor building blocks with the page directory shown in detail. We describe the behavior of these

Reto Achermann, Em Chu, Ryan Mehri, Ilias Karimalis, and Margo Seltzer CR3

PML4

48

page directory 0 21 frame frame

30

PDir

511

39 21

table

... table

PDirEntry frame

table

frame

table

PDPT

Huge Frame

30

output address

PDirEntryTable

PDirEntryFrame

Base Frame

entry.pagesize=0 PDirEntryTable

Page Table

...

PDirEntryFrame entry.pagesize=1

Page Table Level

12 21

Building Blocks segment Composition Rules static map Enumeration

Large Frame

PDirEntryTable -> PageTable; PDirEntryFrame -> LargeFrame; PDirEntry = [ PDirEntryTable | PDirEntryFrame ]; PDir = [ PDirEntry; 512 ];

Figure 2. Decomposition of the four-level x86_64 page table into basic building blocks and composition rules.

components by following a page table walk. A walk begins with access to the base register (CR3) and then traverses through a four-level radix tree (PML4, PDPT, PDIR, PTable) as indicated by the dotted boxes of Figure 2. Having identified the structures we need, we next recursively decompose the components into building blocks: CR3 cannot be split up further, so we model it as a segment unit. Each level in the tree is an array of entries each mapping a fixed, nonoverlapping part of the input address range. The page directory allows the mapping of either a page table or a large page (differentiated by the page size bit). Therefore, we use the enumeration rule to combine two segments – one mapping a frame (PDirEntryFrame) and the other mapping the page table (PDirEntryTable) – to form a page directory entry (PDirEntry). Finally, the enumerations are then combined using the static map composition rule to form the table. 2.4

Mapping Unit Type Hierarchy

From the composition example above, we see that expressing the mapping unit as a combination of segment units and composition rules is similar to a type or class hierarchy. Indeed, each of the defined segment units and rule applications defines a type. The specification defines how the types are instantiated and how they are referenced by the units. Thus, from the specification of the mapping unit, we can obtain the type hierarchy. Further, by knowing the type hierarchy, we can extract the structure of in-memory data structures such as the two descriptor tables used in the example. Finally, using the types we can reuse the basic building blocks in other mapping unit descriptions.

3

Specification Language

Developers write two specifications in the Velosiraptor Specification Language: The first specification describes the mapping behavior of the hardware using intuitive language constructs for the concepts outlined in the previous section. The second specification describes the runtime environment provided by the OS, e.g., memory allocation functions. We explain the language constructs and how they relate to the behavioral model using the X86_64 page directory from

Velosiraptor : Code Synthesis for Memory Translation // PDir table as static map

2 staticmap PDir ( base : paddr )

{

4 6 8 10 12 14 16 18 20 22 24 26 28 30 32

maps [ PDirEntry ( base + i * PTABLE_ENTRY_SIZE ) for i in 0.. PTABLE_NUM_ENTRIES ]; } // PDirEntry with two variants enum PDirEntry ( base : paddr ) { PDirEntryTable ( base ) , PDirEntryFrame ( base ) } // PDir entry mapping a page table ( derived ) segment PDirEntryTable ( base : paddr ) : PTableDesc { synth fn addmap ( va : vaddr , sz : size , flgs : flags , pa : PTable ) requires pa & ( BASE_PAGE_SIZE - 1) // ... } // PDir entry mapping a large frame segment PDirEntryFrame ( base : paddr ) { state ( base : paddr ) { mem entry [ base , 0 , 8] { 0 .. 1 present , 1 .. 2 writable , // bits 2..7 removed for space 7 .. 8 pagesize , // bits 8..21 removed for space 21 .. 48 address , } } interface ( base : paddr ) { mem entry [ base , 0 , 8 ] { Layout { /* same as state */ } WriteActions { interface . entry -> state . entry ; } ReadActions { state . entry -> interface . entry ; } } } #[ pred ] fn valid () -> bool { state . entry . present == 1 } #[ pred ] fn is_writable ( flgs : flags ) -> bool { flgs . writable == > state . entry . writable }

34 36

fn translate ( va : vaddr ) -> paddr requires state . entry . pagesize == 1 { va + ( state . entry . address << LARGE_PAGE_BITS ) }

38

synth fn addmap ( va : vaddr , sz : size , flgs : flags , pa : paddr ) requires va == 0 && sz == LARGE_PAGE_SIZE requires pa & ( LARGE_PAGE_SIZE - 1) == 0 42 } // end of PDirEntryFrame 40

Listing 2. Simplified x86_64 Page Directory Specification

Figure 2 and show the slightly simplified specification in Listing 2. We omit parts of the state and interface description and setperms and delmap for readability. 3.1

Language Overview

Listing 2 shows the definition of two basic building blocks and two composition rules that correspond to the x86_64 page directory shown in Figure 2. Line 2 defines the page directory (PDir) as a static map. The base parameter is the address where the PDir is allocated in memory. We use listcomprehension notation to express that the PDir is a table of PTABLE_NUM_ENTRIES=512 entries. We instantiate each entry at an address relative to the base parameter to associate individual entries with the full table. An entry in the PDir has two variants, so we use the enum keyword to define an enumeration (PDirEntry) on line 6. The enumeration lists the variants and constrains the variant’s parameters by binding them to the corresponding parameter of the enumeration (base parameter). The first variant maps

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands

a page table that we express as a configurable segment. In x86, table entries mapping other tables have similar representations. To avoid duplication, Velosiraptor provides a notion of inheritance. On line 9, we specify the PDirEntryTable by deriving it from the generic page table descriptor PTableDesc (omitted) and specialize the addmap function (Line 10). Note the type of the pa parameter here defines the type of the next unit, i.e., PTable, effectively encoding the page table tree structure. The second variant maps a large frame. Thus, on line 14 we declare a segment unit (PDirEntryTable). 3.2

Specification Details

The Velosiraptor language has specific constructs to express the concepts of the operational model (Section 2) and allows developers to intuitively specify the mapping behavior. 3.2.1 State Definitions. Recall, that the state is just a sequence of bits in the operational model. The state definition (line 15) assigns names to specific groups of bits of the state. The state definition can be interpreted as declaring private data members of a class. Logically, the state is divided into a set of fields that correspond to individual registers or words in memory. Register fields (declared with the reg keyword) have just a size, while in-memory fields (mem keyword) also have an address parameter and an offset. For example, line 16 defines an 8-byte in-memory location, named entry, at offset 0 from base. Registers or memory words may further contain groups of bits with specific semantic meanings. Developers can define bit slices a..b, which assign names to consecutive ranges of bits from a to b (exclusive). Line 17 assigns bit slice 0..1 (i.e., bit 0) the name present, so it can be referenced by a semantically meaningful name. 3.2.2 Interface Definitions. The control interface definition (line 22) specifies the software-visible API and follows a similar pattern to the state definition by assigning names to parts of the interface. Recall, that the operational model does not permit directly accessing the state of the unit. The interface is divided into a set of fields each of which may have a layout (i.e., bit slices) and a set of actions (i.e., ReadActions and WriteActions) that specify how the state is updated. Each field is either: 1) an in-memory location (mem) that is an overlay of an in-memory state field, 2) a memorymapped register (mmio), 3) a non-memory-mapped register (reg), or 4) an instruction (instr). Action blocks contain a list of data transfer actions that atomically execute whenever the interface field is accessed. Lines 25 and 26 show the data transfer between the interface and the state where the state and interface variables refer to the current unit instance. Note that for fields defined with mem, the actions are restricted to the corresponding mem state fields. Register-backed interface fields may trigger multiple non-conflicting updates to the entire state As an optimization, developers may omit the layout and action blocks if there is a state field with the same name and

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands

Reto Achermann, Em Chu, Ryan Mehri, Ilias Karimalis, and Margo Seltzer OS Spec

kind. In that case, the interface field acts as an overlay and inherits the same layout as the state field and the default actions will simply pass through all reads and writes. 3.2.3 Methods. Methods, defined with the keyword fn, contain expressions to compute a value and specify the mapping behavior. They can access the state directly through the state variable referring to the state of the current unit instance (such as the this pointer). Methods can further specify requires clauses that express pre-conditions of the method, which serve as constraints in the synthesis process. Methods effectively create named expressions that can call each other (we disallow loops and recursion). There are three special method classes. mapping Predicates. As outlined in the behavioral model, the mapping function is defined only if all conjuncts are true. Developers define such conjuncts by tagging a function returning a boolean value with the #[pred] decorator. This explicitly names the conjuncts: e.g., valid on line 29 states that the entry is valid if the present bit is set. Translation Function. The translate() function on line 35 defines how the output address is computed. The requires clauses further establish the condition for the variant (i.e., the page size bit must be one). Synthesis Target Functions. Only the synthesis targets of Listing 1 are declared as synth fn. They define additional constraints on the synthesis target through pre-conditions, and have the implicit post-conditions shown in Listing 1. Line 39 shows addmap with the pre-conditions that establish constraints on the alignment of the frame and the unit’s supported mapping range, i.e., the mapping is a large frame. 3.3

Environment Specification

Operating systems have different personalities, so the runtime environments (e.g., functions for allocating and freeing memory, types, and means to access registers) vary. For example, Linux allocates memory for the translation descriptors using page_alloc, whereas on capability-based systems (e.g., seL4 [39] or Barrelfish [16]), applications perform allocations through a sequence of capability operations, but the kernel still needs to format the translation descriptors correctly. The description language allows developers to specify the runtime environment by declaring external types and function signatures that the OS provides. If changes can be applied only indirectly (e.g., through capability operations) the developer provides the corresponding invocation to the addmap, setperms, and delmap .

4

Program Synthesis Methodology

Velosiraptor uses hierarchical software synthesis to automatically generate correct implementations for the addmap, setperms and delmap functions (our synthesis targets). The

SMT Model

Unit Spec

Feasibility Query

1

Solution Exists?

parser

3

Parse Tree

Type checker Velosiraptor

Operational Model 2

Query Cache

Feasibility Check

Code Generator

Hardware Module

sat?

sat?

6

Verify Query

Correct?

SMT Solvers

Yes!

Program Next 5 Program Candidate Generator Program 4

Verifier

Extract Goal Conditions

Predicates

Optimizer

Interface Bindings addmap/setperms/delmap

Figure 3. Synthesis Oveview

resulting programs are correct, because Velosiraptor verifies the synthesized programs against the model and their specification, i.e., the post-conditions stated in Listing 1. We start by defining our synthesis problem, followed by an overview of the synthesis process. We then describe the generation of candidate programs and the grammar that we use to construct them. Finally, we present techniques to reduce the search space and handle caches, maintenance operations, and barriers. 4.1

Formulating the Synthesis Problem

Velosiraptor solves the synthesis problem of finding a sequence of control interface invocations that move the state machine from an arbitrary start state into an end state that has the desired mapping behavior, i.e., satisfies the postcondition of the synthesis target (Listing 1). Synthesis Problem: Let 𝑠 0 represent an arbitrary starting state and 𝑎𝑟𝑔𝑠 represent the arguments to the higherlevel function. Further, let assms be the constraints on valid states, and goal be the post-condition of the current synthesis target. Find a sequence of state transitions 𝑜𝑝 that satisfies the following predicate. ∀𝑠 0, 𝑎𝑟𝑔𝑠 :: assms(𝑠 0, 𝑎𝑟𝑔𝑠) ⇒ goal(op(𝑠 0, 𝑎𝑟𝑔𝑠), 𝑎𝑟𝑔𝑠) In other words, for any valid starting state and input arguments, applying the state transitions of the candidate program results in a state that has the desired mapping behavior. The assms define assumptions on the initial state and the input arguments, e.g., the bit widths and alignments of addresses, and goal are the post-conditions stated in Listing 1. 4.2

Synthesis Overview

Figure 3 shows the overview of the synthesis process. 1 The input to the synthesis process is a specification of the mapping unit in the Velosiraptor specification language (Section 3). 2 From the specification, we create the operational model of the mapping unit including its state and control interface. 3 We encode the operational model in smtlib2 [14] using bit vector logic and perform a feasibility check using the SMT solver. 4 The program generator starts constructing candidate programs, following a grammar derived from the control interface. 5 We iterate through the candidate

Velosiraptor : Code Synthesis for Memory Translation

programs until we find one that satisfies the goal or we exhaust the search space. 6 The verifier encodes the candidate program into an SMT query and uses an SMT solver to check whether it satisfies the goal conditions derived from the postconditions. For efficiency, we apply various domain-specific optimizations that we describe in Section 4.4. 4.3

Generating Candidate Programs

From the specifications of addmap, setperms, and delmap, Velosiraptor automatically generates possible implementations called candidate programs. With no constraints, this quickly leads to an explosion in the size of the search space. We use a domain-specific property that lets us constrain the search space. Recall, that the control interface of the mapping unit defines the software-visible API (i.e., the interface fields as the function calls, and the bit slices are the argument values). Thus, the control interface defines the grammar that generates the candidate programs. Grammar Description. At the top level, a candidate program is a sequence of one or more atomic API invocations chosen from the defined control interface fields. Each API invocation is either a read or a write that will trigger the corresponding ReadActions or WriteActions. The API invocation consists of three parts: 1) initialize the argument value with zero, or read the current value from the control interface. 2) update the argument value by setting the values of the corresponding bit slices. 3) perform a read or write with the constructed argument value. The values of the bit slices are set based on an expression that may involve the high-level function parameters (e.g., address or size), binary operators, masks, or symbolic values. Program Generation. Intuitively, the program generator starts by iterating over possible distinct combinations of API invocations starting with the smallest possible candidate programs and then recursively expanding them. For example, assuming a mapping unit with two registers interface fields 𝐴 and 𝐵, the program generator starts considering programs of the form [A,B], [AA,AB,BA,BB], ... For each of the API interactions, the program generator constructs all possible expressions that update the argument value, initializations, and invocation type. The number of possible programs grows factorially in the size of the interface. 4.4

Search Space Reduction

Simply generating all possible programs is impractical, so we introduce domain-specific search space reduction techniques to make the synthesis process tractable. State Reduction Through Decomposition. As outlined in Section 2.3, we decompose complex mapping units into basic building blocks and composition rules. This reduces the state and the interface by splitting the mapping unit into smaller pieces. For example, instead of considering an MMU with its multi-level page tables and registers in its entirety, we can focus on a single page-table entry at a time.

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands

Program Structure. The grammar that we use to construct candidate programs already constrains what programs we can consider. This not only reduces the search space but also enables the possibility of merging two programs, a property that we leverage in the following technique. Divide-and-Conquer Synthesis Goal. We leverage the definition of a successful map to split up the goal predicate, solve for each subgoal independently, and merge the partial programs. In Section 2, we defined a successful map operation as correctly calculating the address and satisfying a conjunction of predicates. The specification language (Listing 2) already follows this division. We further rewrite all predicates into conjunctive normal form to enable further predicate splitting. We generate partial candidate programs and check whether they satisfy the subgoals. Finally, we merge the partial candidate programs to obtain the candidate program and verify it against the original goal. API Reduction. The subgoal predicates may not use all bits of the state. For example, the valid predicate of Listing 2 depends only on the present bit. Thus, instead of taking the entire control interface as the API, we reduce it to include only the relevant parts by performing the following steps. First, we create the subset of the state that is relevant to the current goal (i.e., parts of the state that are referenced in the goal predicate). Then we identify the parts of the interface that can change any of the relevant parts by looking at the ReadActions and WriteActions blocks. This is a form of backprojection of the bit slices of the interface onto the state. This drastically reduces the grammar of the candidate programs to only 10-100 candidate programs per subgoal. Expression Reduction. The divide-and-conquer approach produces a set of subgoals that may have simple boolean expressions such as 𝑒𝑛𝑡𝑟𝑦.𝑝𝑟𝑒𝑠𝑒𝑛𝑡 == 1. From the expression, we can extract various properties such as whether the returned value is a boolean or address, whether any parameters of the synthesis target are accessed, the size of the bit slice in bits, or whether the comparison is a constant expression. This lets us reduce the possible expressions. For example, if the expression does not refer to any of the arguments, we can exclude those from the list of possible expressions. 4.5

Tree-Based Divide-and-Conquer

Instead of simply combining all partial programs of the conjuncts, we construct a balanced binary tree structure. The idea behind this is to filter wrong partial programs early to reduce the number of possible combinations. Consider an example with four conjuncts 𝐴, 𝐵, 𝐶, 𝐷 with 10 candidate programs each, and 50% of the possible programs for each subgoal satisfy the subgoal. Combining all of them in one step (𝐴 ∧ 𝐵 ∧ 𝐶 ∧ 𝐷) produces 4 × 10 + 54 = 665 programs to check. However, with the tree structure (𝐴 ∧ 𝐵) ∧ (𝐶 ∧ 𝐷), the number of programs drops to 2 × (4 × 10 + 52 ) = 94 for the leaf level, plus another 132 = 169 candidate programs on the middle level (with 50% satisfiability). This results in only

2 4 6 8 10 12 14

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands

Reto Achermann, Em Chu, Ryan Mehri, Ilias Karimalis, and Margo Seltzer

size_t PDirEntryFrame_do_map ( PDirEntryFrame_t * unit , vaddr_t va , size_t sz , flags_t flgs , paddr_t pa ) { // pre - condition check : ( pa & 0 x1fffff ) == 0 x0 if (!((( pa & 0 x1fffff ) == 0 x0 ) ) ) { return 0 x0 ; } // configuration sequence PDirEntryFrame_entry_t v = PDirEntryFrame_entry_new (0) ; v = PDirEntryFrame_entry_address_set (v , (( pa >> 0 x15 ) & 0 x7ffffff ) ) ; v = PDirEntryFrame_entry_ps_set (v , 0 x1 ) ; v = PDirEntryFrame_entry_present_set (v , 0 x1 ) ; v = PDirEntryFrame_entry_rw_set (v , flgs . writable ) ; // write the entry PDirEntryFrame_entry__wr ( unit , v ) ; return LARGE_PAGE_SIZE ; }

generate a type with functions to set and extract bit slice values (e.g., PDirEntryFrame_entry_present_set). The synthesized program then prepares the argument value v and then invokes the control interface (e.g., PDirEntryFrame_entry__wr). From the instantiated composition rules, the code generator emits the corresponding code following a template. Finally, the output is adapted to the OS environment. The code generator finds the functions in the OS environment using the corresponding type signature. The generated code follows a similar pattern to that found in Linux, seKVM [42], seL4 [39], and Barrelfish [16]. For example, Velosiraptor generates functions that walk the page tables, allocate and free memory for page tables, and write the corresponding page table entries as shown in Listing 3. Similarly, Velosiraptor-generated code also includes types for the different unit types as seL4 and Barrelfish do with its capability types or Linux and seKVM with their pmd_t, pud_t, etc, respectively.

Listing 3. Velosiraptor-generated Code for Mapping a Frame in the simplified x86 Page Directory from Listing 2. 263 programs to check compared to the 665 programs that arise from brute force search 4.6

Caches and Barriers

So far, we have assumed that interface interactions immediately update the state and become visible to the mapping function. Unfortunately, this is not always true. Stores may end up in write-buffers, caches, or even get reordered delaying the effect of the interface interaction. Multi-Phase Synthesis. Velosiraptor handles cached or delayed updates by extending the mapping unit model and the program generator to express write buffers and caches. However, instead of directly including cache operations and barriers in the synthesis process, we pursue a multi-phase approach. The first phase operates as explained before and produces a program that satisfies the goal under the assumption that updates become visible immediately. The second phase takes the output program as a starting point and starts inserting barriers and cache operations. The new candidate programs are then verified against the extended model. Modeling Cache Operations. Instead of applying the updates directly to the state, the extended model maintains a list of outstanding write operations on the interface fields. Read operations bypass this list and still return the current interface value directly. We add additional operations for cache maintenance and barriers to the set of possible API interactions that make sure all previous API interactions have been successfully executed. 4.7

Code Generation

The code generator takes the mapping unit specification, the synthesized sequences of interface interactions, the OS environment specification, and produces the corresponding C or Rust source code that implements the addmap, setperms, and delmap functions. Listing 3 shows the generated code for setting up a frame mapping for the simplified x86 page directory from Listing 2. For each of the defined building blocks and composition rules, the code generator declares a type (e.g., PDirEntryFrame_t). For each field in the control interface, we

5

Implementation

We describe the details of the Velosiraptor implementation starting with an overview of the toolchain implementation and how we encode the SMT queries. We then explain our query scheduling and hardware generation backends, and show how Velosiraptor helps developers write specifications. 5.1 Toolchain Overview We implement Velosiraptor in Rust and use the Z3 SMT solver [25]. The main components are the specification parsing, the intermediate representation of the mapping modules, the synthesizer and the program generator, and backends for code generation for OS code and hardware components. We run the Z3 SMT solver as multiple standalone processes to leverage parallelism. Velosiraptor sends smtlib2 [14] formulas to the Z3 process and reads the results over a pipe. The toolchain currently supports generating OS code in C and Rust and generating hardware components for the Arm Fast Models Simulator. We leave the generation of Verilog or other hardware description languages for future work. 5.2

Encoding the Mapping Unit Model in SMT

Velosiraptor converts the mapping unit specification into SMT formulas (smtlib2 [14]) that can be evaluated by an SMT solver. The generated formulas can be divided into 1) a prelude that defines types, 2) a representation of the mapping unit model including its state and interface, and 3) queries that verify the candidate programs against the current goal. Type Encoding. Each mapping unit has a specified input and output bit width it supports. These bit widths define the maximum values for the vaddr, paddr, and size types of the specification language. We declare a new typed term containing a bit vector of length 64 and a boolean function constraining the supported range of the values.

Velosiraptor : Code Synthesis for Memory Translation

Mapping Unit Encoding. The encoding of a mapping unit model closely follows the language constructs (Listing 2) and the model outlined in Section 2. We assert the model only once once for each solver instance. We declare a new type containing a bit vector for each of the state and interface fields and functions providing accessors to insert or extract the bit slices. Then we combine the field definitions into data types for the interface and state, and combine the interface and state datatypes into the model. For the ReadActions and WriteActions we define a function with the corresponding state updates. We declare functions for predicates defined on the state, including the defined methods in the mapping unit specification, pre-conditions, and other assumptions such as type constraints. Write Buffers. To model caches and write buffers, we use Z3’s internal list theory. This adds a list of interface invocations with the corresponding arguments to the model state. Executing the WriteActions block just adds the operation to the list. Cache maintenance operations or barriers will then trigger the execution of the corresponding WriteActions block of the operations in the list. 5.3

Verifying Candidate Programs

To verify the candidate programs, we create a new assertion set and reuse the base model stated above. This enables checking the satisfiability of the current goal without reinstantiating the model again. Listing 4 shows this query. First, we convert the implementation of the current candidate program into an SMT function (Line 4) that takes the initial model state plus arguments and produces a new model state. The body performs the sequence interface actions to update the model. Secondly, we assert (Line 10) that for all possible initial states and arguments, the candidate program satisfies the goal condition for the end state. We chose to use the forall-style instead of the negated exists, because it allows us to directly obtain the value of symbolic variables. Finally, we check whether the assertion holds (Line 15). 5.4

Use of SMT Output during Synthesis

Velosiraptor uses the output of the SMT solver in three ways. As described before, we use it to check whether a program satisfies the goal. In addition, we use it for obtaining scalar values and detecting conflicting conditions. Obtaining Scalar Values. During synthesis, we encounter expressions with unknown constants (e.g., addr << ?). We declare a symbolic variable for it (Line 2). The SMT solver then tries to find a satisfying assignment to all variables including unknown constants. If the SMT solver succeeds, we can extract the assigned value from the SMT output (Line 16) and replace the unknown constant in the expression with the concrete value (e.g., addr << 12). Conflicting Conditions. As part of the synthesis process, we check whether the model itself is satisfiable, i.e., there is a state that satisfies all mapping predicates. We define

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands ( push )

; new assertion set

2 ( declare-const svar !0 Num_t ) ; define symbolic variable

; current candidate program for map

4 ( define-fun map (( st0 Model_t ) ( va VAddr_t ) ( sz Size_t ) 6 8 10 12 14 16

( flgs Flags_t ) ( pa PAddr_t ) ) Model_t ( let ( st1 ( Model.IFace.pte.set ! st0 ZERO ) ) ( let ( st2 ( Model.IFace.pte.present.set ! st1 symvar !0) ) ( let ( st3 ( Model.IFace.pte.wr ! st2 ) ) st3 ) ) ) ) ; assert post-condition of map ( assert ( forall (( st !0 Model_t ) ( va VAddr_t ) ( pa PAddr_t ) ( sz Size_t ) ( flgs Flags_t ) ) (= > ( map.assms st !0 va sz flgs pa ) ( translate.result ( map st !0 va sz flgs pa ) va sz flgs pa )))) ( check-sat ) ; check satisfiability ( get-value ( svar !0) ) ; obtain value of symbolic variable ( pop ) ; drop the current assertion set

Listing 4. SMT query to verify candidate programs a variable for the state, assert all mapping predicates, and then ask the SMT solver to check satisfiability. If it is not, we extract the unsat-core from the SMT output, which shows which mapping predicates are conflicting. 5.5

Query Scheduling and Caching

Velosiraptor leverages caching and scheduling techniques to reduce the number of queries executed, thus decreasing synthesis time. We execute queries asynchronously to give more flexibility in scheduling them. Query execution stops as soon as we find a program that satisfies the goal. Query Caching. Before sending a query to the SMT solver, Velosiraptor checks whether it already exists in the query cache. If it does not, we add the query to the cache, mark the entry as pending, register the query, execute it, and update the entry once the query is finished. If the query is in the cache, we either return the cached result or register the query if the entry was pending. This avoids evaluating duplicate queries during the synthesis process. Prioritizing Queries. We organize the execution of the SMT queries for the candidate programs as a tree (see Section 4.4). The query scheduler assigns priorities to the SMT queries based on their position in the tree. The root has the highest priority, and the leaves have the lowest priority. The intuition behind this strategy is to prioritize the verification of more complete programs and thus quickly bubble up candidate programs in the tree. Ideally, this means that not all queries of the lower levels have to be executed. 5.6

Hardware Generation

Velosiraptor features a proof-of-concept hardware generation backend that produces a simulated mapping unit that runs on the Arm Fast Models platform. This platform allows for functional, but not cycle-accurate, simulation of a hardware platform. In the Arm Fast Models, a platform is composed of multiple modules that are instantiated and their ports (e.g., memory buses or interrupt lines) connected. Each module is described as a LISA+ [9] file, a domain-specific language

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands

built on top of C++. The Arm Fast Models toolchain then processes all LISA+ components and dependencies to build an executable simulator binary. Velosiraptor generates a LISA+ file for the mapping unit and a C++ implementation of the behavior for each unit defined in the specification file. The mapping unit module has two upstream and downstream ports: two for the data plane (memory accesses), one for the control interface (registers), and one for emitting memory accesses when the unit reads in-memory descriptors. The C++ implementation of each building block and composition rule is generated directly from its specification; there is no synthesis required. The generated LISA+ registers the map() function of the top-level unit as the handler for incoming memory accesses. During the mapping process, the code path follows the type hierarchy of the specification, evaluating and calling the map() function of the next unit, if permitted, or returning an error. Ultimately, the output address is returned to the caller, and the incoming memory access is updated. On error, the simulator raises an exception at the originating CPU core. When describing a platform, the developer instantiates the mapping unit module and connects its ports to the memory bus of a processor core and a memory module simulating RAM. Multiple mapping unit modules can be connected serially, or different address ranges can be translated by different mapping unit modules. This enables the developer to set up complex memory hierarchies and translation schemes.

6

Evaluation

We evaluate Velosiraptor using quantitative and qualitative scenarios to answer the following questions: • How quickly does Velosiraptor synthesize code, and how well does synthesis scale? (Section 6.2) • How much does each optimization improve runtime? (Section 6.3) • How well does the hardware software co-generation work? (Section 6.4) • How easily can Velosiraptor be integrated into operating systems? (Section 6.5) • How does the performance of the generated code compare to hand-written code (Section 6.6). 6.1

Evaluation Setup

We run our evaluation on an Intel Xeon W-2275 processor with 14 cores with two hyperthreads each. The host OS is Ubuntu 24.04 LTS with Linux kernel 6.5.0, and we use Z3 version 4.10.2 as the SMT solver. We set the number of workers equal to the number of cores. 6.2

Velosiraptor generates code quickly

We evaluate Velosiraptor synthesis and code generation performance showing that its runtime is sufficiently small to be practically incorporated into kernel compilation.

Reto Achermann, Em Chu, Ryan Mehri, Ilias Karimalis, and Margo Seltzer Configurations Results [ms] Programs Time P50 Time P95 Name # Units Simple Page Table 3U+ 2F+ 7S 9M+ 4P+ 3U 151ms 163ms x86_32 Page Table 7U+ 5F+38S 39M+16P+ 9U 561ms 582ms x86_64 Page Table 13U+ 8F+91S 72M+32P+18U 1,137ms 1,171ms Arm MPU 1U+ 7F+22S 9M+ 7P+ 3U 750ms 1,129ms Xeon Phi SMPT 2U+ 1F+ 3S 4M+ 3P+ 0U 99ms 112ms 32ms 37ms Simple Segment 1U+ 1F+ 2S 4M+ 0P+ 3U Variable Segment 1U+ 2F+ 5S 9M+ 4P+ 3U 453ms 525ms 824ms 1,024ms Medium Segment 1U+ 4F+18S 15M+ 5P+ 3U Assoc Segment 1U+ 4F+ 6S 14M+ 4P+ 3U 1,058ms 4,475ms x86 Segmentation 1U+ 2F+16S 17M+ 5P+ 3U 12,445ms 12,683ms R4700 TLB 3U+ 8F+13S 17M+ 0P+ 7U 2,249ms 2,433ms Linux Ubuntu – – 153,831ms 154,352ms

Table 1. Synthesis Times and Complexities. The unit column shows the size of the specification in terms of basic building blocks and composition rules (U), the total size of the interface (F), and the number of bit slices (S). The program column shows the length of the synthesized programs for the addmap (M), setperms (P), and delmap (U) functions. Methodology. We measure the runtime of the synthesis and code generation for the translation hardware descriptions shown in Table 1. The units column shows the complexity of the description. This has a direct correlation with the size of the grammar for the synthesized programs, larger numbers indicate a bigger search space. We also measure the compilation time of the Ubuntu Linux kernel v6.2.0 (default Ubuntu configuration, no modules, using 28 hardware threads). Results. Table 1 shows the median and 95th percentile runtimes over 100 runs. Some of the hardware (e.g., Xeon Phi SMPT) does not support unmapping and/or access control so no program is generated. The measurements show that Velosiraptor runtime is negligible relative to the kernel compilation. For example, code synthesis for the x86_64 page tables takes about one second, whereas the entire kernel build takes more than 154 seconds. We see that x86 segmentation has a significantly higher runtime compared to the x86_64 page tables, despite similar search space size (Section 6.3). The page tables are very amenable to our divide-and-conquer approach resulting in many small subproblems, whereas the x86 segmentation has a complex expression for the output address and limit calculations that cannot be further split. We see higher variability in the runtime for specifications that involve variable mapping ranges (i.e., Arm MPU, Variable, Medium and Assoc Segments). Upon further examination, we observe a bimodal runtime distribution for these specifications. Investigation of the generated SMT queries reveals a nested forall quantifier involving symbolic variables. Solving these queries may take a few milliseconds or can take several seconds to solve, contributing to runtime variability and comprising almost half of the total runtime. Discussion. Velosiraptor provides a viable approach for automatically generating low-level OS code without significantly affecting kernel build time.

Velosiraptor : Code Synthesis for Memory Translation Spec No Opts +IfaceOpt +StateOpt +ExprOpt +Tree Simple Page Table 23 23 5 3 3 x86_32 Page Table 37 37 18 10 10 x86_64 Page Table 38 38 21 13 13 Arm MPU 38 38 7 5 5 Xeon Phi SMPT 7 7 2 1 1 Simple Segment 4 4 2 1 1 Variable Segment 33 33 7 5 5 Medium Segment 37 37 13 10 10 Assoc Segment 38 38 12 9 9 x86 Segmentation 38 38 18 13 13 R4700 TLB 38 37 11 9 9

Table 2. Calculated search space sizes (log10) with cumulative optimizations.

6.3

Ablation Study of Optimizations

We now evaluate how effectively each optimization reduces the search space size. Methodology. We run Velosiraptor on the descriptions shown in Table 1 and selectively turn on the optimizations outlined in Section 4.4 and calculate the search space of possible candidate programs. Due to the search space size, we are unable to run synthesis without certain optimizations and therefore do not measure synthesis time. Results. Table 2 shows the calculated search space sizes (in base-10 logarithm) for the different, cumulative optimization levels. Enabling interface and state reduction optimizations together has the most significant effect on the search space size, because it effectively reduces the size of the grammar with which we generate programs. Moreover, optimizing the possible set of expressions further reduces the search space significantly. The tree-based structure does not reduce the maximum number of candidate programs, but instead, quickly eliminates programs that do not satisfy the goal. Discussion. This evaluation shows that domain-specific optimization techniques reduce the search space significantly, making the synthesis process tractable for modern machines. 6.4

Hardware/Software Co-Design with Velosiraptor

We demonstrate Velosiraptor’s ability to generate translation hardware components and the corresponding code that configures it from the same description, using a qualitative study targeting the Arm Fast Models platform simulator. Methodology. We generate an emulated hardware component for the Arm Fast Models and instantiate it in the platform description file by placing it between the main system bus and a DRAM region. Memory accesses to a distinct, contiguous memory address range on the system bus will be forwarded to the generated translation hardware component. The hardware component maps or rejects the memory accesses based on the behavioral description and its current state. In case of a translation fault, a synchronous exception is raised to enable integration with the OS as with MMUbased translation faults. Velosiraptor generates the hardware

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands

component and the corresponding OS code. We boot our own simple, firmware-like image containing the Velosiraptor-generated code on the simulated hardware platform. We then perform a sequence of loads and stores to the region translated by the generated hardware component. We reconfigure the memory hardware and repeat the test while checking whether we observe the expected behavior. Results and Discussion. All cases booted successfully and we observed the expected behavior. Velosiraptor is capable of generating both a simulated hardware component and OS code from the same description. This is a promising result as it enables further research in mapping hardware and may reduce the effort of FPGA developers to use mapping hardware in their FPGA-accelerated applications. 6.5

Velosiraptor can be used in a real OS

We demonstrate that Velosiraptor can be used in an existing OS code base by integrating the generated code into the Barrelfish OS [16], including a monolithic setting. Methodology. We take the x86_64 page table specification and generate code for three OS environments: 1) Monolithic: The code can directly access the registers and in-memory data structures that define the translation behavior. It also allocates and frees memory for the page tables. 2) uKernel supervisor: The generated code can also directly access the registers and in-memory data structures, but it cannot allocate memory for the page tables. 3) uKernel userspace: The generated code cannot access the registers or in-memory data structures directly, instead, invoking operations through system calls. It performs the required memory allocations for the translation descriptors. We chose Barrelfish, a capability-based uKernel, as capability operations provide a nice separation of tasks for managing page tables. We add a mmap-like system call to the kernel to test the monolithic scenario. For all three cases, we replace the existing code with the generated code. We boot the system on x86_64 Qemu with KVM acceleration such that the hardware performs the page table walk where the guest page tables are set up by Velosiraptor-generated code. We then perform a sequence of memory mappings and accesses to the mapped regions to test whether the memory hardware has been configured correctly. Results and Discussion. We observed that the generated code correctly programs the translation hardware, the system booted, and ran the tests successfully. The OS environment specification can adapt the code generation of Velosiraptor to handle a diverse set of environments. 6.6

Performance of Generated Code

We evaluate the performance of the generated code by comparing the runtime performance against hand-written code of other operating systems. Methodology. We run the evaluation entirely in userspace on Linux to avoid the overheads of system calls and rule

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands Operation Map Protect Unmap Structure Code P50 P95 P50 P95 P50 P95 x86_64 Linux 13ns 13ns 13ns 13ns 12ns 12ns x86_64 Velosiraptor 13ns 13ns 12ns 12ns 11ns 12ns PTable Barrelfish 8ns 8ns 8ns 9ns 7ns 8ns PTable Velosiraptor 8ns 8ns 8ns 8ns 8ns 8ns

Table 3. Performance comparison of Velosiraptor-generated code with hand-written code from Linux and Barrelfish.

out possible differences in the OS environment. The pagetable structures are allocated on the heap. We extract the hand-written x86_64 page table code from the Barrelfish OS and the Linux kernel v6.8 and compare it against the Velosiraptor-generated code. We measure the latency of the addmap, setperms, and delmap over 200 iterations. Results and Discussion. Table 3 shows the median and 95th percentile latencies of the three functions. The x86_64 structure sets up the full four-level page table structure in memory, whereas PTable only configures the leaf level of the page table. We observe that there is no significant difference between Velosiraptor and the hand-written code. 6.7

Discussion

We demonstrated that Velosiraptor produces performant code that configures the memory hardware in a wide range of settings Potential barriers to integrating the Velosiraptorgenerated code into a larger OS are replacing existing, possibly tightly integrated data structures, e.g., Linux’s paging data types being passed around in the kernel instead of using high-level functions. The OS may make use of non-present translation table entries to store information on swapped-out pages, or during NUMA-balancing operations. The high-level functions generated by Velosiraptor do not expose functionality for these use cases, but the enumeration construct could be used to express OS-specific use cases (e.g., swap entries).

7

Related Work

MMU Configurations. Achermann et al. [1] present a toolchain for automatically generating a static initial page table for x86 and Arm-based systems based on a formal description of the memory topology [3, 4]. Their work focused on calculating the right address mappings to install into the page table. Fiedler et al. [27, 28] define trust boundaries based on the accessibility of control registers and translation tables. Dörr et al. [26] focus on access permissions and the generation of static configurations. In contrast, Velosiraptor provides functions to dynamically change the configuration of memory hardware at runtime and supports memory hardware besides translation tables. Memory hardware management can also be split between user-space and kernel. For example, Barrelfish [16], seL4 [39] and mmapx [2], allow userspace to safely manage translation tables by separating the construction from writing the actual bit patterns into

Reto Achermann, Em Chu, Ryan Mehri, Ilias Karimalis, and Margo Seltzer

the translation tables. Velosiraptor can handle generating the code for both the system call or capability invocations and the kernel’s updating of translation table entries (Section 6.5). Device Driver Synthesis. Termite [59, 60] synthesizes device drivers using a game-theoretic approach. It expresses what happens when the OS interacts with device registers (e.g., the character sent event), whereas Velosiraptor focuses on the resulting mapping, independent of the register interactions. Termite has no support for in-memory data structures and cannot generate corresponding hardware. GhostWriter [66] uses behavior trees to synthesize device drivers by specifying the corresponding device behavior but it neither generates hardware nor expresses mapping behavior. Porting. Porting an OS to new platforms requires significant effort [54]. Chen et al. [18] show a signification reduction in developer time by generating 70% of device driver code utilizing domain-specific aspects such as device classes and features. Velosiraptor follows a similar approach by synthesizing the memory management code. Hu et al. [32] present a system for automated porting of an OS to new platforms using a machine-independent OS specification and a machinedependent language describing the instruction set. Their work targets assembly code resulting in a huge search space, whereas Velosiraptor operates on a higher-level abstraction, i.e., API requests with a more manageable search space. Hardware Description. Describing the hardware interface using a specification language allows for the generation of OS bindings. For example, the Mackerel language [58] and Ghostwriter’s register definition file [66] are domain-specific languages for describing registers and data structures used by devices. Neither includes the hardware behavior so cannot generate the hardware itself. The Arm architecture is specified in ASL [55] that serves as the basis for generating the documentation, instruction interpreters [57], simulators for processors, and test suites for chip designers [56]. MMU Virtualization. Several works virtualize the MMU to provide isolation of system components and to enforce security policies through intercepting and restricting access to the MMU configuration to validate configuration updates. Para-virtualization used in Xen [13] and Linux’s PV-Ops interface [65] intercepts updates to the page tables. SecPod [67] isolates page-table management through paging delegation and execution trapping to enforce auditing the kernel’s page-table modifications by leveraging the PVOps interface. SecVisor [61] virtualizes the MMU by controlling all modifications to the page tables using nested paging and enforces policies on the execute permissions. Hypervision [11] validates page table updates in the secure monitor. Nested kernel [24] separates the kernel into a trusted, nested kernel that has control over the MMU, and an untrusted outer kernel that has no direct control over the MMU. Similarly, Nexen [62] uses the nested kernel architecture to introduce a secure monitor into Xen by enforcing read-only page tables. SVA [22] prevents the OS from mapping frames used

Velosiraptor : Code Synthesis for Memory Translation

by the ghost memory partition or SVA VM internal memory as ordinary memory. Inktag [31] divides physical memory into secure and non-secure frames where secure frames can only be mapped by the trusted extended page table in a nested paging setup. Overshadow [19] protects applications from the OS by leveraging context-dependent one-to-many mappings through the use of multiple shadow page tables. Mondrix [69] overlays the address space with protection domains assigning permissions to specific memory regions. Enforcing the security policies is orthogonal to Velosiraptor. Those systems could use Velosiraptor-generated code in the “bottom half” of the virtualized MMU, i.e., the trusted component that directly interacts with the physical MMU. Moreover, by tailoring the generated code with the OS specification, Velosiraptor can provide the corresponding paravirtualized interface that intercepts page table updates and invokes the trusted component instead – similar to the approach taken with Barrelfish in Section 6.5. Hardware Mechanisms. Several systems use hardware extensions to enforce isolation and protection. Hardwareassisted kernel compartmentalization (HAKCs) [47] partitions the code and data of a monolithic kernel and defines access policy for each partition using Arm’s PAC [7] and MTE [8] extensions. xMP [53] uses Intel’s VMFunc [37] to quickly switch the extended page tables to accelerate protection domain switching. vTZ [33] virtualizes Arm’s secure world before hardware support has been introduced [44] by leveraging the secure/non-secure modes and restricting second-stage translation configuration to the secure world. HDFI [64] and CHERI [68] use tag-based memory protection to perform an additional, hardware-accelerated permission check on every load/store instruction. ACES [20] uses a compiler-based approach to compartmentalize and isolate components through binary instrumentation and uses memory protection units to enforce access control. SKEE [12] creates an isolated environment by disallowing the kernel from managing its own translation tables, and forcing updates through a well-defined switch gate. EC [38] uses a 𝜇Kernel-design to isolate components using a memory protection unit and hardware watchpoints to monitor its configuration. Kenali [63] maintains a shadow address space with different access permissions and enforces MMU integrity by restricting access to the MMU-related data and registers. Leveraging hardware features such as Intel’s VMFfunc, memory tagging or watchpoints, or maintaining multiple page tables and shadow mappings is orthogonal to Velosiraptor. However, the Velosiraptor-generated code could be used to set up the MMU-based address translation, MPU-based memory protection, or create fat-pointers (e.g., CHERI [68]). We leave encryption-based approaches, e.g., pointer signatures, as future work. Formal Modeling and Verification. KCoFI [21] provides an interface to safely manage the page tables for an SVA VM [22]

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands

by assigning types to pages and then using this type information when constructing page tables (similar to the typed capabilities in seL4 [39] and Barrelfish [16]). Velosiraptor defines a type per page table node to ensure correct construction. Moreover, through OS specification the generated code can be tailored to API functions (e.g., sva.update.lN.mapping) or the corresponding handler code in the kernel. seKVM [42] provides a model and a verified implementation for the ARMv8 virtual memory system, including a proof that the resulting data structure is indeed a tree – a property that follows by construction from Velosiraptor’s specification language. Moreover, seKVM has layers for allocation, walking, and constructing the page table, similar to the generated functions of Velosiraptor. However, seKVM targets the ARMv8 architecture whereas Velosiraptor allows generating the corresponding functions for any given specification. Li et al. [43] verified a concurrent implementation of multi-level realm translation tables for the Arm architecture using their VIA framework. The proof is tied to the Arm architecture and leverages the CertiKOS [30] methodology. CertiKOS itself uses a two-level page map that follows the x86_32 page table structure. Velosiraptor could be used to generate code for other page tables and the corresponding proofs in the VIA framework. HyperKernel [52] ensures ownership properties of the root-level page table to ensure safety and security guarantees. With Velosiraptor, porting Hyperkernel to other architectures could be simplified by generating the code that configures the page tables. Dai et al. [23] verified the second stage translation setup of HyperEnclave, focusing on a framework to verify the correctness using a deep embedding of Rust’s MIR in Coq. Brun et al. [17] and Lattuada et al. [41] verify the correctness of a Rust implementation of the x86_64 page table in Verus with focus on hardware concurrency, an aspect which we plan to integrate in the future.

8

Conclusion

Correctly configuring the memory hardware of a platform is of paramount importance for the system integrity. Hardware is becoming more diverse and complex, and OS developers must adapt their code to the hardware they run on – a manual process that takes time and requires developers to deal with subtle, low-level hardware details. Velosiraptor is a methodology and system that uses software synthesis to automatically and efficiently generate correct implementations for addmap, setperms, and delmap to change the mapping behavior of memory hardware. Velosiraptor lets developers generate the corresponding memory hardware itself, enabling research into new mapping schemes that precisely have the features the developer wants.

Acknowledgments This work was supported by the Natural Sciences and Engineering Research Council of Canada (NSERC).

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands

Reto Achermann, Em Chu, Ryan Mehri, Ilias Karimalis, and Margo Seltzer

A

Artifact

A.1

Abstract

conditions. Arm-based machines are not tested and only support a subset of the experiments and are thus not recommended. If a virtual machine is used, please ensure an x86_64 host and appropriate configuration of hardware acceleration (e.g., KVM) when running the performance benchmarks.

The artifact consists of • the Velosiraptor toolchain, • a set of mapping specifications, • a set of benchmarks / tests to reproduce the results in the paper, and • and a modified version of the Barrelfish OS that uses the Velosiraptor-generated code. The following contains dependencies and instructions to reproduce the results presented in the evaluation Section 6 of the paper. A.2

Artifact check-list (meta-information)

• Algorithm: Yes. • Compilation: Rust 1.79 and GCC 13.2.0 • Binary: requires Z3 SMT Solver, Arm FastModels, and Qemu • Run-time environment: Linux (Ubuntu 24.04) • Hardware: x86_64 machine with a minimum of 8 cores and 32GB of RAM, either baremetal or a virtual machine • Run-time state: clean OS installation. • Execution: cargo / bash scripts. • Metrics: quantitative: performance (latency). Qualitative: functionality. • Output: Latex tables 1, 2, and 3, code and OS logs. • Experiments: a total of five experiments each corresponding to a subsection in Section 6. • How much disk space required?: 10GB. • How much time is needed to prepare workflow?: One hour. • How much time is needed to complete experiments?: Six hours. • Publicly available?: Yes, https://github.com/ubc-systopia/ velosiraptor-asplos25-artifact • Code licenses?: MIT. • Data licenses?: None. • Workflow automation framework used?: No. • Archived (provide DOI)?: 10.5281/zenodo.14752297 or on GitHub repository.

A.3

Description

A.3.1 How to access. Clone the git repository at https:// github.com/ubc-systopia/velosiraptor-asplos25-artifact and follow the instructions in the README.md file. Alternatively, download the artifact from DOI: 10.5281/zenodo.14752297 Ensure to initialize the submodules recursively. The respository contains all the code and data sets, and instructions to install dependencies that are required to reproduce the results on the machine. A.3.2 Hardware dependencies. The artifact requires one x86_64 machine (either baremetal or a virtual machine) with at least eight cores and 32GB of RAM. Smaller machines may also work, but can lead to longer runtimes or out-of-memory

A.3.3 Software dependencies. The artifact is tested on x86_64 Ubuntu 24.04 server – other operating systems, e.g., other Linux distributions and Windows Subsystem for Linux, may work too, but are not tested. The README.md file provides a detailed list of software packages and other software dependencies that can be installed using Ubuntu’s package manager. Additional dependencies are: Rust 1.79, Z3 4.10.2, Docker, and Arm Fast Models 11.15. A.4

Installation and Basic Test

Follow the instructions in the Preparation section of the README.md file in the repository to setup the build and run environment of the artifact. Beyond the dependencies, there is no installation necessary and the artifact builds and runs out of the repository. Basic Test: To test the artifact run the smoke test from section 6.2 and/or run the test Section 6.3. This exercises the synthesis workflow, SMT solver, optimizations, and code compilation. A.5

Experiment workflow

Most of the experiments are run through cargo commands or bash scripts as described in the README.md file of the artifact repository. The workflow consists of two phases: 1. running the respective commands to execute the experiment, and 2. inspecting the output to verify and compare the results. The README.md contains detailed descriptions of the commands and the expected output. A.6

Evaluation and expected results

The artifact is expected to 1. closely reproduce Tables 1, 2, and 3 in the evaluation Section 6 of the paper (quantitative benchmarks), and 2. emit similar output as described in the README.md file for the remaining experiments of Sections 6.4 and 6.5 in the paper (qualitative benchmarks). A.7

Experiment customization

Most experiments run within a few minutes in the current configuration. For the longer-running synthesis experiment (Table 1), we provide a smoke test that runs a smaller version of the experiment. Moreover, experiments can also be customized by changing the set of specifications that are evaluated, or the number of iterations executed. This requires modifying the respective benchmarking code in the repository.

Velosiraptor : Code Synthesis for Memory Translation

A.8

Notes

Arm Fast Models Licenses. The emulated hardware platforms require the Arm Fast Models to build and run the simulators. The Arm Fast Models require licenses. To download the Arm Fast Models and and obtaining the corresponding licenses, visit the Arm website: https://www.arm.com/ products/development-tools/simulation/fast-models. The artifact assumes that the user has access to 1. the Arm Fast Models and its third-party IP, 2. license for generating the simulation platform, 3. license to run the base platform, and 4. license to run the Arm Cortex A57 processor IP.

References [1] Reto Achermann, David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe, and Daniel Schwyn. 2021. Generating Correct Initial Page Tables from Formal Hardware Descriptions. In Proceedings of the 11th Workshop on Programming Languages and Operating Systems (Virtual Event, Germany, 2021) (PLOS ’21). Association for Computing Machinery, New York, NY, USA, 69–75. doi:10.1145/3477113.3487270 [2] Reto Achermann, David Cock, Roni Haecki, Nora Hossle, Lukas Humbel, Timothy Roscoe, and Daniel Schwyn. 2021. mmapx: uniform memory protection in a heterogeneous world. In Proceedings of the Workshop on Hot Topics in Operating Systems (Ann Arbor, Michigan, 2021) (HotOS ’21). Association for Computing Machinery, New York, NY, USA, 159–166. doi:10.1145/3458336.3465273 [3] Reto Achermann, Lukas Humbel, David Cock, and Timothy Roscoe. 2017. Formalizing Memory Accesses and Interrupts. In Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems, MARS at ETAPS 2017, Uppsala, Sweden, 29th April 2017. (2017) (MARS’17). 66–116. doi:10.4204/EPTCS.244.4 [4] Reto Achermann, Lukas Humbel, David Cock, and Timothy Roscoe. 2018. Physical Addressing on Real Hardware in Isabelle/HOL. In Proceedings of the 9th International Conference on Interactive Theorem Proving, 2018, Held as Part of the Federated Logic Conference, FloC 2018 (Oxford, UK, 2018) (ITP’18). 1–19. doi:10.1007/978-3-319-94821-8_1 [5] Reto Achermann, Ilias Karimalis, and Margo Seltzer. 2023. Why write address translation OS code yourself when you can synthesize it?. In Proceedings of the 19th Workshop on Hot Topics in Operating Systems (Providence, RI, USA) (HOTOS ’23). Association for Computing Machinery, New York, NY, USA, 174–180. doi:10.1145/3593856.3595895 [6] Hanna Alam, Tianhao Zhang, Mattan Erez, and Yoav Etsion. 2017. Do-It-Yourself Virtual Memory Translation. In Proceedings of the 44th Annual International Symposium on Computer Architecture (Toronto, ON, Canada) (ISCA ’17). Association for Computing Machinery, New York, NY, USA, 457–468. doi:10.1145/3079856.3080209 [7] Arm Ltd. 2016. Introduction to PAC. Online. https: //developer.arm.com/documentation/109576/0100/PointerAuthentication-Code/Introduction-to-PAC. [8] Arm Ltd. 2019. Armv8.5-A – Memory Tagging Extension. White Paper. [9] Arm Ltd. 2023. LISA+ Language for Fast Models Reference Manual. https://developer.arm.com/documentation/101092/0100 Version 1.0.. [10] Arm Ltd. 2024. Fast Models: SoC Verification Without Hardware. Online. https://www.arm.com/products/development-tools/simulation/ fast-models. [11] Ahmed M. Azab, Peng Ning, Jitesh Shah, Quan Chen, Rohan Bhutkar, Guruprasad Ganesh, Jia Ma, and Wenbo Shen. 2014. Hypervision Across Worlds: Real-time Kernel Protection from the ARM TrustZone Secure World. In Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security (Scottsdale, Arizona, USA)

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands (CCS ’14). Association for Computing Machinery, New York, NY, USA, 90–102. doi:10.1145/2660267.2660350 [12] Ahmed M. Azab, Kirk Swidowski, Rohan Bhutkar, Jia Ma, Wenbo Shen, Ruowen Wang, and Peng Ning. 2016. SKEE: A lightweight Secure Kernel-level Execution Environment for ARM. In Network and Distributed System Security Symposium (San Diego, California, USA) (NDSS’16). The Internet Society. doi:10.14722/ndss.2016.23009 [13] Paul Barham, Boris Dragovic, Keir Fraser, Steven Hand, Tim Harris, Alex Ho, Rolf Neugebauer, Ian Pratt, and Andrew Warfield. 2003. Xen and the art of virtualization. In Proceedings of the Nineteenth ACM Symposium on Operating Systems Principles (Bolton Landing, NY, USA) (SOSP ’03). Association for Computing Machinery, New York, NY, USA, 164–177. doi:10.1145/945445.945462 [14] Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2021. The SMT-LIB Standard. https://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-0512.pdf Version 2.6. [15] Arkaprava Basu, Jayneel Gandhi, Jichuan Chang, Mark D. Hill, and Michael M. Swift. 2013. Efficient virtual memory for big memory servers. SIGARCH Comput. Archit. News 41, 3 (jun 2013), 237–248. doi:10.1145/2508148.2485943 [16] Andrew Baumann, Paul Barham, Pierre-Evariste Dagand, Tim Harris, Rebecca Isaacs, Simon Peter, Timothy Roscoe, Adrian Schüpbach, and Akhilesh Singhania. 2009. The multikernel: a new OS architecture for scalable multicore systems. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (Big Sky, Montana, USA) (SOSP ’09). Association for Computing Machinery, New York, NY, USA, 29–44. doi:10.1145/1629575.1629579 [17] Matthias Brun, Reto Achermann, Tej Chajed, Jon Howell, Gerd Zellweger, and Andrea Lattuada. 2023. Beyond isolation: OS verification as a foundation for correct applications. In Proceedings of the 19th Workshop on Hot Topics in Operating Systems (Providence, Rhode Island, USA) (HotOS’23). Association for Computing Machinery, 158–165. doi:10.1145/3593856.3595899 [18] H. Chen, G. Godet-Bar, F. Rousseau, and F. Petrot. 2014. Device driver generation targeting multiple operating systems using a model-driven methodology. In 2014 25nd IEEE International Symposium on Rapid System Prototyping. 30–36. doi:10.1109/RSP.2014.6966689 [19] Xiaoxin Chen, Tal Garfinkel, E. Christopher Lewis, Pratap Subrahmanyam, Carl A. Waldspurger, Dan Boneh, Jeffrey Dwoskin, and Dan R.K. Ports. 2008. Overshadow: a virtualization-based approach to retrofitting protection in commodity operating systems. In Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems (Seattle, WA, USA) (ASPLOS XIII). Association for Computing Machinery, New York, NY, USA, 2–13. doi:10.1145/1346281.1346284 [20] Abraham A. Clements, Naif Saleh Almakhdhub, Saurabh Bagchi, and Mathias Payer. 2018. ACES: automatic compartments for embedded systems. In Proceedings of the 27th USENIX Conference on Security Symposium (Baltimore, MD, USA) (SEC’18). USENIX Association, USA, 65–82. [21] John Criswell, Nathan Dautenhahn, and Vikram Adve. 2014. KCoFI: Complete Control-Flow Integrity for Commodity Operating System Kernels. In Proceedings of the 2014 IEEE Symposium on Security and Privacy (SP ’14). IEEE Computer Society, USA, 292–307. doi:10.1109/ SP.2014.26 [22] John Criswell, Andrew Lenharth, Dinakar Dhurjati, and Vikram Adve. 2007. Secure virtual architecture: a safe execution environment for commodity operating systems. In Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles (Stevenson, Washington, USA) (SOSP ’07). Association for Computing Machinery, New York, NY, USA, 351–366. doi:10.1145/1294261.1294295 [23] Zhenyang Dai, Shuang Liu, Vilhelm Sjoberg, Xupeng Li, Yu Chen, Wenhao Wang, Yuekai Jia, Sean Noble Anderson, Laila Elbeheiry, Shubham Sondhi, Yu Zhang, Zhaozhong Ni, Shoumeng Yan, Ronghui Gu, and Zhengyu He. 2024. Verifying Rust Implementation of Page Tables in a

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands

Reto Achermann, Em Chu, Ryan Mehri, Ilias Karimalis, and Margo Seltzer

Software Enclave Hypervisor. In Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2 (La Jolla, CA, USA) (ASPLOS ’24). Association for Computing Machinery, New York, NY, USA, 1218–1232. doi:10.1145/3620665.3640398 [24] Nathan Dautenhahn, Theodoros Kasampalis, Will Dietz, John Criswell, and Vikram Adve. 2015. Nested Kernel: An Operating System Architecture for Intra-Kernel Privilege Separation. In Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems (Istanbul, Turkey) (ASPLOS ’15). Association for Computing Machinery, New York, NY, USA, 191–206. doi:10.1145/2694344.2694386 [25] Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: an efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Hungary) (TACAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg, 337–340. [26] Tobias Dörr, Timo Sandmann, and Jürgen Becker. 2021. Model-based configuration of access protection units for multicore processors in embedded systems. Microprocess. Microsyst. 87, C (nov 2021), 17 pages. doi:10.1016/j.micpro.2021.104377 [27] Ben Fiedler, Roman Meier, Jasmin Schult, Daniel Schwyn, and Timothy Roscoe. 2023. Specifying the de-facto OS of a production SoC. In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification (Koblenz, Germany) (KISV ’23). Association for Computing Machinery, New York, NY, USA, 18–25. doi:10.1145/3625275.3625400 [28] Ben Fiedler, Daniel Schwyn, Constantin Gierczak-Galle, David Cock, and Timothy Roscoe. 2023. Putting out the hardware dumpster fire. In Proceedings of the 19th Workshop on Hot Topics in Operating Systems (Providence, RI, USA) (HOTOS ’23). Association for Computing Machinery, New York, NY, USA, 46–52. doi:10.1145/3593856.3595903 [29] Krishnan Gosakan, Jaehyun Han, William Kuszmaul, Ibrahim N. Mubarek, Nirjhar Mukherjee, Karthik Sriram, Guido Tagliavini, Evan West, Michael A. Bender, Abhishek Bhattacharjee, Alex Conway, Martin Farach-Colton, Jayneel Gandhi, Rob Johnson, Sudarsun Kannan, and Donald E. Porter. 2023. Mosaic Pages: Big TLB Reach with Small Pages. In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3 (Vancouver, BC, Canada) (ASPLOS 2023). Association for Computing Machinery, New York, NY, USA, 433–448. doi:10.1145/3582016.3582021 [30] Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). USENIX Association, Savannah, GA, 653– 669. https://www.usenix.org/conference/osdi16/technical-sessions/ presentation/gu [31] Owen S. Hofmann, Sangman Kim, Alan M. Dunn, Michael Z. Lee, and Emmett Witchel. 2013. InkTag: secure applications on an untrusted operating system. In Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems (Houston, Texas, USA) (ASPLOS ’13). Association for Computing Machinery, New York, NY, USA, 265–278. doi:10.1145/2451116.2451146 [32] Jingmei Hu, Eric Lu, David A. Holland, Ming Kawaguchi, Stephen Chong, and Margo Seltzer. 2023. Towards Porting Operating Systems with Program Synthesis. ACM Trans. Program. Lang. Syst. 45, 1, Article 2 (mar 2023), 70 pages. doi:10.1145/3563943 [33] Zhichao Hua, Jinyu Gu, Yubin Xia, Haibo Chen, Binyu Zang, and Haibing Guan. 2017. vTZ: Virtualizing ARM TrustZone. In 26th USENIX Security Symposium (USENIX Security 17). USENIX Association, Vancouver, BC, 541–556. https://www.usenix.org/conference/ usenixsecurity17/technical-sessions/presentation/hua

[34] Jian Huang, Moinuddin K. Qureshi, and Karsten Schwan. 2016. An Evolutionary Study of Linux Memory Management for Fun and Profit. In Proceedings of the 2016 USENIX Conference on Usenix Annual Technical Conference (Denver, CO, USA) (USENIX ATC ’16). USENIX Association, Berkeley, CA, USA, 465–478. http://dl.acm.org/citation.cfm?id= 3026959.3027002 [35] Integrated Device Technology, Inc. 1995. IDT79R4600 TM and IDT79R4700 TM RISC Processor Hardware User’s Manual (revision 2.0 ed.). https://docslib.org/doc/718203/idt79r4600-and-idt79r4700-riscprocessor-hardware-users-manual [36] Intel Corp. 2013. Intel Xeon Phi Coprocessor Developer’s Quick Start Guide. https://www.intel.com/content/dam/develop/external/us/ en/documents/intel-xeon-phi-coprocessor-quick-start-developersguide.pdf Version 1.8. [37] Intel Corp. 2023. Intel 64 and IA-32 Architectures Software Developer’s Manual. https://www.intel.com/content/www/us/en/developer/ articles/technical/intel-sdm.html December 2023. [38] Arslan Khan, Dongyan Xu, and Dave Jing Tian. 2023. EC: Embedded Systems Compartmentalization via Intra-Kernel Isolation. In 2023 IEEE Symposium on Security and Privacy (SP). 2990–3007. doi:10.1109/SP46215.2023.10179285 [39] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (Big Sky, Montana, USA) (SOSP ’09). Association for Computing Machinery, New York, NY, USA, 207–220. doi:10.1145/1629575.1629596 [40] Joshua Landgraf, Matthew Giordano, Esther Yoon, and Christopher J. Rossbach. 2023. Reconfigurable Virtual Memory for FPGA-Driven I/O. In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3 (Vancouver, BC, Canada) (ASPLOS 2023). Association for Computing Machinery, New York, NY, USA, 556–571. doi:10.1145/3582016.3582048 [41] Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno. 2024. Verus: A Practical Foundation for Systems Verification. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles (Austin, TX, USA) (SOSP ’24). Association for Computing Machinery, New York, NY, USA, 438–454. doi:10.1145/3694715.3695952 [42] Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. 2021. Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association, 3953–3970. https://www.usenix. org/conference/usenixsecurity21/presentation/li-shih-wei [43] Xupeng Li, Xuheng Li, Christoffer Dall, Ronghui Gu, Jason Nieh, Yousuf Sait, and Gareth Stockwell. 2022. Design and Verification of the Arm Confidential Compute Architecture. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). USENIX Association, Carlsbad, CA, 465–484. https://www.usenix.org/ conference/osdi22/presentation/li [44] Berenice Mann. 2018. New Secure world architecture in Armv8.4. Online. https://community.arm.com/arm-communityblogs/b/architectures-and-processors-blog/posts/architecting-moresecure-world-with-isolation-and-virtualization. [45] A Theodore Markettos, Colin Rothwell, Brett F Gutstein, Allison Pearce, Peter G Neumann, Simon W Moore, and Robert NM Watson. 2019. Thunderclap: Exploring Vulnerabilities in Operating System IOMMU Protection via DMA from Untrustworthy Peripherals. In NDSS. [46] Alex Markuze, Adam Morrison, and Dan Tsafrir. 2016. True IOMMU Protection from DMA Attacks: When Copy is Faster Than Zero Copy. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems

Velosiraptor : Code Synthesis for Memory Translation (Atlanta, Georgia, USA) (ASPLOS ’16). ACM, New York, NY, USA, 249– 262. doi:10.1145/2872362.2872379 [47] Derrick McKee, Yianni Giannaris, Carolina Ortega, Howard Shrobe, Mathias Payer, Hamed Okhravi, and Nathan Burow. 2022. Preventing Kernel Hacks with HAKCs. In 29th Annual Network and Distributed System Security Symposium (San Diego, California, USA) (NDSS’22). The Internet Society. doi:10.14722/ndss.2022.24026 [48] Benot Morgan, Eric Alata, Vincent Nicomette, and Mohamed Kaaniche. 2016. Bypassing IOMMU Protection against I/O Attacks. In 2016 Seventh Latin-American Symposium on Dependable Computing (LADC). 145–150. doi:10.1109/LADC.2016.31 [49] Benot Morgan, Eric Alata, Vincent Nicomette, and Mohamed Kaaniche. 2018. IOMMU Protection Against I/O Attacks: A Vulnerability and a Proof of Concept. Journal of the Brazilian Computer Society 24, 1 (09 Jan 2018), 2. doi:10.1186/s13173-017-0066-7 [50] National Vulnerability Database. 2014. CVE-2014-9888. Online.https: //nvd.nist.gov/vuln/detail/CVE-2014-9888. [51] National Vulnerability Database. 2017. CVE-2017-16994. Online. https: //nvd.nist.gov/vuln/detail/CVE-2017-16994. [52] Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. 2017. Hyperkernel: PushButton Verification of an OS Kernel. In Proceedings of the 26th Symposium on Operating Systems Principles (Shanghai, China) (SOSP ’17). Association for Computing Machinery, New York, NY, USA, 252–269. doi:10.1145/3132747.3132748 [53] Sergej Proskurin, Marius Momeu, Seyedhamed Ghavamnia, Vasileios P. Kemerlis, and Michalis Polychronakis. 2020. xMP: Selective Memory Protection for Kernel and User Space. In 2020 IEEE Symposium on Security and Privacy (SP). 563–577. doi:10.1109/SP40000.2020.00041 [54] Richard Rashid, Avadis Tevanian, Michael Young, David Golub, Robert Baron, David Black, William Bolosky, and Jonathan Chew. 1987. Machine-independent virtual memory management for paged uniprocessor and multiprocessor architectures. In Proceedings of the Second International Conference on Architectual Support for Programming Languages and Operating Systems (Palo Alto, California, USA) (ASPLOS II). Association for Computing Machinery, New York, NY, USA, 31–39. doi:10.1145/36206.36181 [55] Alastair Reid. 2016. ARM’s Architecture Specification Language. Online. https://alastairreid.github.io/specification_languages/. [56] Alastair Reid. 2016. Trustworthy Specifications of ARM v8-A and v8-M System Level Architecture. In Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design (Mountain View, California) (FMCAD ’16). FMCAD Inc, Austin, Texas, 161–168. [57] Alastair Reid. 2020. Using ASLi with Arm’s v8.6-A ISA specification. Online. https://alastairreid.github.io/using-asli/. [58] Timothy Roscoe and Barrelfish Projec. [n. d.]. Mackerel User Guide – Barrelfish Technical Note 2. [59] Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur, and Gernot Heiser. 2009. Automatic Device Driver Synthesis with Termite. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (Big Sky, Montana, USA) (SOSP ’09). Association for Computing Machinery, New York, NY, USA, 73–86.

ASPLOS ’25, March 30-April 3, 2025, Rotterdam, Netherlands doi:10.1145/1629575.1629583 [60] Leonid Ryzhyk, Adam Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm, and Mona Vij. 2014. User-Guided Device Driver Synthesis. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (Broomfield, CO) (OSDI’14). USENIX Association, USA, 661–676. [61] Arvind Seshadri, Mark Luk, Ning Qu, and Adrian Perrig. 2007. SecVisor: a tiny hypervisor to provide lifetime kernel code integrity for commodity OSes. In Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles (Stevenson, Washington, USA) (SOSP ’07). Association for Computing Machinery, New York, NY, USA, 335–350. doi:10.1145/1294261.1294294 [62] Lei Shi, Yuming Wu, Yubin Xia, Nathan Dautenhahn, Haibo Chen, Binyu Zang, Haibing Guan, and Jinming Li. 2017. Deconstructing Xen. In Proceedings 2017 Network and Distributed System Security Symposium (NDSS’17). Internet Society. doi:10.14722/ndss.2017.23455 [63] Chengyu Song, Byoungyoung Lee, Kangjie Lu, William Harris, Taesoo Kim, and Wenke Lee. 2016. Enforcing Kernel Security Invariants with Data Flow Integrity. In 23rd Annual Network and Distributed System Security Symposium (San Diego, California, USA) (NDSS’16). The Internet Society. doi:10.14722/ndss.2016.23218 [64] Chengyu Song, Hyungon Moon, Monjur Alam, Insu Yun, Byoungyoung Lee, Taesoo Kim, Wenke Lee, and Yunheung Paek. 2016. HDFI: Hardware-Assisted Data-Flow Isolation. In 2016 IEEE Symposium on Security and Privacy (SP’16). 1–17. doi:10.1109/SP.2016.9 [65] The kernel development community. 2024. Paravirt_ops. The Linux Kernel Organization. https://www.kernel.org/doc/html/latest/virt/ paravirt_ops.html [66] Bingyao Wang, Sepehr Noorafshan, Reto Achermann, and Margo Seltzer. 2023. Synthesizing Device Drivers with Ghost Writer. In Proceedings of the 12th Workshop on Programming Languages and Operating Systems (Koblenz, Germany) (PLOS ’23). Association for Computing Machinery, New York, NY, USA, 10–17. doi:10.1145/3623759.3624545 [67] Xiaoguang Wang, Yue Chen, Zhi Wang, Yong Qi, and Yajin Zhou. 2015. SecPod: a framework for virtualization-based security systems. In Proceedings of the 2015 USENIX Conference on Usenix Annual Technical Conference (Santa Clara, CA) (USENIX ATC ’15). USENIX Association, USA, 347–360. [68] Robert N. M. Watson, Jonathan Woodruff, Peter G. Neumann, Simon W. Moore, Jonathan Anderson, David Chisnall, Nirav Dave, Brooks Davis, Khilan Gudka, Ben Laurie, Steven J. Murdoch, Robert Norton, Michael Roe, Stacey Son, and Munraj Vadera. 2015. CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization. In Proceedings of the 2015 IEEE Symposium on Security and Privacy (SP ’15). IEEE Computer Society, USA, 20–37. doi:10.1109/SP.2015.9 [69] Emmett Witchel, Junghwan Rhee, and Krste Asanović. 2005. Mondrix: memory isolation for linux using mondriaan memory protection. In Proceedings of the Twentieth ACM Symposium on Operating Systems Principles (Brighton, United Kingdom) (SOSP ’05). Association for Computing Machinery, New York, NY, USA, 31–44. doi:10.1145/1095810.1095814

Related documents

• Arancini: A Hybrid Binary Translator forWeak Memory Model Architectures / Sebastian Reimers, Dennis Sprokholt, Martin Fink, Theofilos Augoustis, Simon Kammermeier, Rodrigo C. O. Rocha, Tom Spink, Redha Gouicem, Soham Chakraborty, Pramod Bhatotia#780303
• ICOR: improving codon optimization with recurrent neural networks#19744
• Reprogramming the brain with synthetic neurobiology.#1107601
• Initialisation Determines the Basin: Efficient Codebook Optimisation for Extreme LLM Quantization#2622
• Language-machine for data reconfiguration#220759