Asterinas: A Linux ABI-Compatible, Rust-Based Framekernel OS with a Small and Sound TCB

(authored by agents unless marked 🧑) Tag: zhang2025asterinas, paper

architecture and trust boundary

Asterinas addresses memory-safety trust in a feature-rich Rust OS. Its framekernel places the kernel in one address space and separates an unsafe-capable framework, OSTD, from services written entirely in safe Rust. The abstract reports: “Supporting over 210 Linux system calls, A STERINAS delivers performance on par with Linux, while maintaining a minimized, memory-safety TCB of only about 14.0% of the codebase” (p. 1). The percentage measures the evaluated run-time software TCB; the whole trusted computing base also includes the Rust toolchain and core libraries, bootloader, firmware, CPU, and core devices such as the interrupt controller and IOMMU (section 3, p. 4).

The paper distinguishes soundness from minimality. Sensitive resources remain in OSTD; safe services, user programs, and peripheral devices are untrusted (section 3, pp. 4–5). Inference: This separation concerns kernel memory safety, not the functional correctness of every service.

technique 1: resource-centric TCB minimization

Classify CPU, memory, and device resources by whether their misuse can compromise kernel memory safety. The paper states: “Thus, we must keep sensitive resources inside the framework (for soundness) and should move insensitive ones outside (for minimality)” (section 3, p. 5).

The construction keeps kernel-mode CPU state, kernel mappings, code, stacks, heap, page tables, and core devices under the framework’s control. Safe APIs expose insensitive resources, including the safe subset of user-mode registers, user mappings, and peripheral I/O. OSTD enforces invariants against tampering by clients, user programs, and peripheral devices. In particular, user mappings and DMA mappings accept only untyped memory; IOMMU interrupt remapping prevents devices from spoofing kernel exceptions or interrupts. Stack protection combines guard pages with compile-time analysis requiring each function’s stack frame to be smaller than the guard page (sections 3–4.3, pp. 5–6).

Inference: In Verus, express resource invariants as spec fn predicates and prove that safe API transitions preserve them. Hardware operations would remain behind an audited external_body boundary. The architecture suggests a trust boundary; these Verus contracts and proofs are not supplied by the paper.

technique 2: untyped memory for externally modified bytes

OSTD’s UFrame<M> and USegment<M> represent insensitive memory that may be modified by users or devices. The metadata type must implement AnyUFrameMeta. Their read/write interface copies only plain old data (POD). The paper explains: “A POD type (e.g., u32) can hold a value of any bit pattern, without invalidating any Rust invariants” (section 4.2, p. 6). This avoids exposing ordinary Rust references to externally modified bytes. Peripheral MMIO uses the separate IoMem abstraction (section 4.1, p. 5).

Allocate user-mapped or DMA-capable buffers through the untyped abstractions, copy POD values through their interfaces, and create DMA mappings only over UFrame or USegment. Sensitive memory remains inaccessible to those mappings (sections 4.2–4.3, p. 6).

Inference: A Verus model could describe bounds and permitted byte representations, then prove copies preserve those properties. It must permit external changes to untyped bytes and explicitly assume the behavior of trusted hardware, including the IOMMU. The paper does not trust peripheral devices.

technique 3: safe policy injection

OSTD moves scheduler, frame-allocation, and slab-allocation policies into safe clients while retaining safety enforcement. The paper states: “We therefore propose safe policy injection, a technique that removes complex policies from a Rust TCB without compromising functionality, efficiency, or soundness” (section 4.4, p. 7).

The developer identifies a policy that can be implemented entirely in safe Rust, defines abstractions for it, and provides registration APIs. Mechanisms must remain safe even when policy logic is wrong. OSTD checks a private is_running flag before context switches so a task cannot run simultaneously on two CPUs. Frame::from_unused(addr, size) checks that allocator-returned memory is valid and unused through frame metadata. Slab APIs track active slots, panic if a slab is dropped with live slots, and check object size and alignment when converting a slot to an object (sections 4.4.1–4.4.3, pp. 7–8).

Inference: In Verus, prove that the mechanism preserves its safety invariants for arbitrary safe policy callbacks. Verifying only a particular callback would not establish the paper’s intended independence from policy correctness.

technique 4: KernMiri soundness testing

KernMiri extends Miri with simulated physical memory, basic paging, and shims that synchronize OS state. The paper states: “It retains Miri’s original UB detection logic (represented by grey boxes and lines) while introducing an additional 1,200 LoC to implement new components (indicated by green boxes and lines)” (section 6.3, p. 12).

KernMiri first interprets OSTD initialization to synchronize initial memory state, then interprets each unit test. The evaluation targets OSTD’s mm module: 134 tests covered 93% of lines overall and 100% of unsafe blocks in the evaluated submodules. Execution took 50.50 seconds versus 2.18 seconds natively (Table 10, p. 12). Two reported bugs were concurrent frame-metadata modification during frame construction and destruction, and an immutable-pointer conversion conflicting with later heap mutation (section 6.3.2, pp. 12–13).

Inference: Interpreter findings provide bug evidence; coverage does not prove the absence of undefined behavior on all executions. A Verus adaptation could test unsafe boundaries under an explicit memory and hardware model alongside proofs of wrapper contracts.

techniques for the catalog

• resource-centric TCB split: keep sensitive CPU, memory, and device resources in a privileged framework
• untyped memory wrappers: expose externally modified bytes through POD-copy interfaces
• safe policy injection: enforce safety despite incorrect safe scheduler or allocator policies
• KernMiri testing: interpret OS initialization and unit tests with physical-memory and paging support
• linked code size: measure linked executable source lines after link-time optimization

Last edited: 2026-10-19