safeL4: Rethinking Safe-Language-Based Single Address Space Microkernels

1 Introduction

• Microkernels pair a small trusted base and capability-based least-privilege access with security, safety, flexibility, and a basis for formal verification.Their protection domains can be updated or replaced independently.Source: §1 · p. 2
• Emerging security-sensitive platforms favor microkernels but run general-purpose applications, while hardware isolation adds IPC-related switching and data-transfer overhead.Prior mitigations either move critical servers or drivers into the kernel, conflicting with minimality, or duplicate state and require synchronization.Source: §1 · p. 2
• Safe-language kernels avoid some hardware-isolation overhead but lack capability control over all resources, and their trusted bases can include substantial linked code.The paper evaluates functionality and linked code size; it notes that Tock's smaller linked code size reflects its lightweight microcontroller scope.Source: §1 · pp. 2–3
• safeL4 builds capabilities from Rust object capabilities, uses low-level hardware and communication abstractions, and encapsulates essential unsafe operations.A capability derivation tree and Rust visibility controls address derivation tracking and revocation limitations of native object capabilities.Source: §1 · p. 3
• 1.91× average performance over seL4, with IDC performance improving 7.8× to 22.3×.The prototype implements core OS services and supports applications written in unsafe languages in user space.Source: §1 · p. 3

2.1 seL4 Capability System

• seL4 capabilities encapsulate an object reference and rights, and applications invoke kernel objects through unique capability indices in their CSpace.The kernel stores capabilities against user-level tampering and manages authority propagation with a variant of the take-grant model.Source: §2.1 · p. 3

2.2 Object-Capability System

• Object-capability systems treat objects as resources, methods as access interfaces, and object references as capabilities.Rust references and smart pointers can serve this role.Source: §2.2 · p. 3
• Rust's object-capability model requires safe code because unsafe raw-pointer manipulation can bypass reference unforgeability.safeL4 therefore requires code within isolated domains to use only safe Rust.Source: §2.2 · pp. 3–4

3.1 Safe Language-Based OSes

• Safe-language isolation keeps domains in one address space and turns cross-domain communication into function calls, but trusts the compiler, libraries, and sometimes runtime.This enlarges the OS TCB compared with relying on CPU hardware isolation.Source: §3.1 · p. 4
• Earlier systems used safe-language object capabilities and domain isolation, while garbage-collected languages could introduce latency that conflicts with some real-time services.SPIN and Singularity are examples; Rust-based systems avoid garbage collection but must carefully manage unsafe code in the TCB.Source: §3.1 · p. 4

3.2 Heavy Overhead of Current Microkernel Capability Systems

• Conventional microkernel capabilities incur system-call and, in multi-server scenarios, address-space switching costs; avoiding that model weakens least-privilege control.Safe-language object capabilities and a single-address-space design offer a route to lower-cost typed invocation without raw-byte capability decoding.Source: §3.2 · pp. 4–5

3.3 New Minimality Requirement for Safe Language-Based OSes

• Safe-language microkernel minimality must minimize unsafe code as well as kernel functionality, while providing rich safe abstractions for hardware resources.These abstractions can let protection-domain services such as file systems and drivers be implemented entirely in safe Rust.Source: §3.3 · p. 5
• The proposed direction centralizes unsafe hardware operations in a minimal kernel and exposes resources through safe interfaces; Asterinas is described as retaining some OS functions in its TCB and lacking unified capabilities.The paper notes that expressive safe abstractions and strict minimality can coexist in microkernels.Source: §3.3 · pp. 5–6

4.1 Overview

• Protection domains run as safe Rust crates in the microkernel’s address space and privilege level, accessing hardware resources and inter-domain communication through capabilities.User-level tasks instead run in user space with hardware isolation, supporting legacy applications written in unsafe languages.Source: §4.1 · p. 6

4.2 Trusted Computing Base and Safety Guarantees

• safeL4 guarantees protection domains language-level memory and type safety and capability safety, but not general safety or correct device programming.Its TCB includes trusted compiler, libraries, kernel, initialization components, and hardware assumptions; DMA-capable devices and drivers remain trusted because IOMMU isolation is unsupported.Source: §4.2 · pp. 6–7

4.3 Capability System

• Arc/Weak alone cannot support revocation or track multilevel derivation, so safeL4 combines them with a private capability derivation tree (CDTree).Each tree node corresponds to a RawCap and Cap; domains receive only a Cap, not the RawCap directly.Source: §4.3.1 · p. 7
• The CDTree retains RawCap ownership and records derivation, allowing revocation to drop a derived node so the descendant’s Weak upgrade fails.The microkernel restricts Weak upgrades to a proxy function, controlling how long resource access remains active.Source: §4.3.1 · pp. 7–8

4.3.2 Security Analysis of the Capability System.

• The system enforces capability unforgeability and non-bypassability, tracks provenance to boot-created roots, and keeps derived rights within parent rights.The procedural macro is the only interface for invoking kernel-object operations from protection domains.Source: §4.3.2 · p. 8

4.4 The Minimality Design

• safeL4 preserves minimality by providing safe interfaces for hardware resources, privileged operations, non-privileged instructions, and basic data structures.Kernel objects abstract CPU, memory, I/O, and communication resources; implementations may use unsafe Rust behind strictly safe method signatures.Source: §4.4 · p. 9
• These abstractions confine rather than eliminate unsafe code, so undefined behavior or arbitrary memory corruption inside them can still violate safety guarantees.The trusted implementation also includes internal unsafe code for panic unwinding, trap entry and return, and procedural-macro dependencies.Source: §4.4 · p. 9

4.5 Fault Isolation

• Because a panic in a protection domain can crash the shared-address-space OS, safeL4 catches callee panics during synchronous IDC and returns an error to the caller.The mechanism unwinds the callee’s stack and cleans up associated resources.Source: §4.5 · p. 9

5.1 The safeL4 Microkernel

• The microkernel implements TCB, memory, device, interrupt, notification, and endpoint objects, accessed through capabilities, alongside safe interfaces for non-privileged instructions and basic data structures.Source: §5.1 · p. 9

5.2 Inter-Domain Communication

• Asynchronous IDC uses Notification objects and adds message passing through zero-copy ownership transfer; synchronous IDC invokes registered callee interfaces through Endpoint objects.Source: §5.2 · p. 10
• Callee crates register exported interfaces at link time, and the microkernel loads their function pointers for later invocation using a unique crate-and-signature key.Source: §5.2.1 · p. 10
• Runtime IDC invocation checks parameter types, locates the callee interface, and wraps execution in catch_unwind to handle potential panics.The implementation also uses a custom compilation target to generate exception-handling information for stack unwinding.Source: §5.2.2 · p. 10

5.3 Capability Invocation

• Capability invocation uses a proxy that checks authority, temporarily upgrades the Cap’s Weak reference, locks the kernel object, runs its method, then releases the lock and upgraded reference.Source: §5.3 · p. 10

5.4 OS Services in Protection Domains

• Implemented services include process and memory management, a file system, and peripheral drivers; RedoxFS runs in a protection domain with its interfaces registered for IDC.Source: §5.4 · p. 10, §5.4.2 · p. 11

5.4.1 Process Management and Memory Management.

• Process management schedules threads using TCB objects, while memory management allocates from Untyped objects through buddy and slab systems.The process manager also obtains multicore hardware-core IDs through an MPI capability.Source: §5.4.1 · pp. 10–11
• Drivers access MMIO through DeviceMemory capabilities, and safeL4 ports Redox’s SD card driver alongside UART, timer, and DMA drivers.The implementation also ports musl libc and implements 50 system calls for unsafe-language user applications.Source: §5.4.3 · p. 11, §5.4.4 · p. 11

6.1 Experiment Setup

• Experiments ran on a Raspberry Pi 3B+ and compared safeL4 with seL4 LibOS, Redox, and Ubuntu Linux with ZFS across the specified workloads.The evaluation covers low-level operations, SQLite3/YCSB workloads, and filesystem-related microbenchmarks.Source: §6.1 · pp. 11–12, §6 · p. 11

6.2 Source Code and Linked Code Size Evaluation

• safeL4 comprises 22,018 LoC, including an 11,688-LoC microkernel with 15.1% unsafe code; its other trusted linked code for system-resource abstraction is smallest among compared Rust OSes.Architecture support requires 462 LoC of unsafe code for AArch64 and 349 LoC for RISC-V64.Source: §6.2 · p. 12, Table 4 · p. 12, Table 5 · p. 12

6.3 Microbenchmark Comparison with seL4

• safeL4 is 1.91× faster than seL4 on average in seL4bench, with IDC 7.8× to 22.3× faster.Synchronization benchmarks avoid CPU-mode and address-space switches. Frame allocation is a counterpoint: safeL4's fine-grained locking adds overhead, with RwLock/Arc capability initialization averaging 656.11 CPU cycles.Source: §6.3 · pp. 12–13, Table 6 · p. 13

6.4 Macrobenchmark Comparison with seL4 and Linux

• safeL4 outperforms seL4 by 14.3% and Linux by 23.2% on average in the SQLite3 YCSB benchmark.Four system calls account for more than 70% of execution time; safeL4's implementations are simpler than Linux's, with less locking logic, fewer system states, and no access-control checks.Source: Figure 3 · p. 12, §6.4 · p. 13

6.5 Microbenchmark Comparison with Redox

• safeL4 outperforms Redox in all filesystem-related microbenchmarks, with a geometric-mean speedup of 1.47×.The experiment uses ported RedoxFS and an SD-card driver, maintaining source-code consistency.Source: Table 7 · p. 13, §6.5 · p. 14

6.6 Case Study: MMIO Abstraction and Capability-Protected Device Access

• DeviceMemory uses bounds-checked volatile MMIO reads and writes, while capabilities restrict drivers to authorized objects and remove the confused-deputy issue.These guarantees do not establish driver functional correctness: logic errors or violations of device-specific state-machine protocols remain possible.Source: §6.6 · p. 14

• safeL4’s primitives achieve 1.91× the performance of seL4 on average.Source: §7 · p. 14
• The design combines low-overhead capability invocation in a single address space with safe language-enforced capability unforgeability.Source: §7 · p. 14
• Although the Rust toolchain accounts for a notable portion of the TCB, the kernel itself remains compact.Source: §7 · p. 14

• The artifact includes a pre-built safeL4 image and source code and pre-built images for seL4, Redox, and Linux.Source: §A.1 · p. 15
• It supports reproducing microbenchmark comparisons with seL4 and Redox and a SQLite3/YCSB macrobenchmark comparison with seL4 and Linux.Source: §A.1 · p. 15
• Detailed instructions for running each experiment are included in the artifact repository.Source: §A.1 · p. 15

• The evaluation uses pre-built images, so compilation is not required for the main experiments.Source: §A.2 · p. 15
• Experiments compare microbenchmarks with seL4 and Redox and macrobenchmarks with seL4 and Linux on a bare-metal Raspberry Pi 3 Model B+.Source: §A.2 · p. 15
• The software set includes Ubuntu Linux with ZFS, YCSB on SQLite3, and a filesystem-related subset of LMbench.Source: §A.2 · p. 15
• Runs produce UART logs and parsed numerical summaries, require under 15 GB of disk space, and take 10–12 hours.Source: §A.2 · p. 15

• The artifact and its README are available at the stated DOI and include images, checksums, and documentation for building, running, and extracting results.Source: §A.3.1 · p. 15
• The evaluation hardware requires a Raspberry Pi 3 Model B+ with a microSD card, Linux host, and USB-to-TTL UART adapter.Source: §A.3.1 · p. 15
• The host should run a 64-bit Debian-based Linux distribution, tested with Ubuntu 22.04, and provide tools for image writing, UART capture, and result parsing.Source: §A.3.3 · p. 15

A.4 Installation

• Pre-built images let evaluators run the operating systems without installing their build environments; optional build instructions are in the README.Source: §A.4 · p. 15

A.5 Experiment workflow

• To run an experiment, flash its Raspberry Pi 3B+ firmware and OS images to an SD card, capture UART output, and follow its README to collect and process results.Source: §A.5 · p. 15

A.6 Evaluation and expected results

• Exact evaluation results may differ across machines because hardware and execution environments vary, although the authors expect relative trends and conclusions to hold.Source: §A.6 · p. 15
• safeL4 is expected to achieve better geometric-mean performance than seL4 across microbenchmarks of IPC, interrupt handling, signaling, and scheduling.The stated advantage primarily comes from avoiding privilege-level and address-space switches.Source: §A.6.1 · p. 15
• Under YCSB on SQLite3, safeL4 is expected to outperform both seL4 and Linux in the macrobenchmark comparison.The results correspond to Figure 3.Source: §A.6.1 · p. 16
• In file-system microbenchmarks, safeL4 is expected to outperform Redox after porting RedoxFS and the SD driver into kernel-mode protection domains.This arrangement reduces IPC overhead and eliminates privilege-level and address-space switch costs.Source: §A.6.3 · p. 16