Asterinas: a new Linux-compatible kernel project

What's a framekernel?

The framekernel concept is explained in the September 2024 paper "Framekernel: A Safe and Efficient Kernel Architecture via Rust-based Intra-kernel Privilege Separation" by Yuke Peng et al. A fuller version of the paper was published in early June.

Traditionally, monolithic kernels lump everything into one kernel-mode address space, whereas microkernels only implement a minimal trusted computing base (TCB) in kernel space and rely on user-mode services for much of the operating system's functionality. This separation implies the use of interprocess communication (IPC) between the microkernel and those services. This IPC often has a performance impact, which is a big part of why microkernels have remained relatively unpopular.

The core of Asterinas's "framekernel" design is the encapsulation of all code that needs Rust's unsafe features inside a library, enabling the rest of the kernel (the services) to be developed using safe abstractions. Those services remain within the kernel's address space, but only have access to the resources that the core library gives to them. This design is meant to improve the safety of the system while retaining the simple and performant shared-memory architecture of monolithic kernels. The Asterinas book on the project's website provides a nice architectural mission statement and overview.

The aptness of the "framekernel" nomenclature can perhaps be debated. The frame part refers to the development framework wrapping the unsafe parts behind a memory-safe API. The concept of the TCB is, of course, not exclusive to microkernel architectures but, because there are strong incentives to strictly scrutinize and, in some contexts, even formally verify the TCB of a system, keeping the TCB as small as possible is a central aspect of microkernel designs.

An update on the project is available on the Asterinas blog in the June 4 post titled "Kernel Memory Safety: Mission Accomplished". The post explains the team's motivations and the need for the industry to address memory-safety problems; it provides some illustrations that explain how the framekernel is different from monolithic kernels and microkernels. It also takes a moment to emphasize that the benefits of Rust don't stop with memory safety; there are improvements to soundness as well. Perhaps most importantly, the post highlights the upcoming Asterinas presentation at the 2025 USENIX Annual Technical Conference.

Related work

In their paper, the authors compare Asterinas to some prior Rust-based operating-system work, exploring the benefits of the language's memory-safety features and explain how Asterinas differs from that previous work. Specifically, the paper contrasts Asterinas with RedLeaf, an operating system written in Rust and presented at the 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20) in 2020. Asterinas uses hardware isolation to permit running user-space programs written in any programming language, aims to be general-purpose, and provides a Linux-compatible ABI, while RedLeaf is a microkernel that is designed not to use the hardware's isolation features, and the project focuses on different things.

Another project of interest is Tock, an embedded system that targets SoCs with limited hardware protection functionality. Like Asterinas, Tock also divides the kernel into a trusted core allowed to use unsafe and untrusted "capsules" that are not. As mentioned, Asterinas does rely on hardware protection and isn't intended for strictly embedded use, which differentiates it from Tock.

It bears mentioning that the Rust for Linux project, which is introducing Rust code into the upstream Linux kernel, has similar goals as Asterinas. It also aims to encapsulate kernel interfaces with safe abstractions in such a way that drivers can be written in Rust without any need for unsafe.

Work toward formal verification

One goal of shrinking the TCB of an operating system is to make it feasible to have it formally verified. In February 2025, the Asterinas blog featured a post detailing plans to do just that. The best known formally verified kernel is seL4, an L4-family microkernel.

Asterinas aims to use the framekernel approach to achieve a system that has a small, formally verified TCB akin to a lean microkernel, but also a simple shared-memory architecture with Linux ABI compatibility, all at the same time. This is a radical departure from any previously formally verified kernel; the blog post describes those kernels as deliberately small and limited compared to "full-fledged, UNIX-style OSes".

The Asterinas project is collaborating with a security-auditing company called CertiK to use Verus to formally verify the kernel. There is an extensive report available from CertiK on how Asterinas was audited and the issues that were found.

Libraries and tools

The Asterinas kernel is only one result of the project. The other two are OSTD, described as "a Rust OS framework that facilitates the development of and innovation in OS kernels written in Rust", and OSDK, a Cargo addon to assist with the development, building, and testing of kernels based on OSTD.

There are four stated goals for OSTD as a separate crate. One is to lower the entry bar for operating-system innovation and to lay the groundwork for newcomers to operating-system development. The second is to enhance memory safety for operating systems written in Rust; other projects can benefit from its encapsulation and abstraction of low-level operations. The third is to promote code reuse across Rust-based operating-system projects. The fourth is to boost productivity by enabling testing of new code in user mode, allowing developers to iterate without having to reboot.

It is worth emphasizing that the kernels that can be written with OSTD do not have to be Linux-compatible or, in any way, Unix-like. The APIs provided are more generic than that; they are memory-safe abstractions for functionality like x86 hardware management, booting, virtual memory, SMP, tasks, users, and timers. Like most Rust crates, OSTD is documented on docs.rs.

Asterinas reports Intel, among others, as a sponsor of the project. Intel's interest is likely related to its Trust Domain Extensions (TDX) feature, which provides hardware modes and features to facilitate isolation of virtual machines, and memory encryption. The Asterinas book has a brief section on TDX, and the OSDK supports it.

The OSTD, or at least the parts that Asterinas ends up using, seems to essentially be the restricted TCB that allows unsafe. For an illustrative example, we could take a look at the network kernel component's source code and see that the buffer code uses DMA, locking, allocation, and virtual-memory code from the OSTD through memory-safe APIs.

Current state

Asterinas was first released under the Mozilla Public License in early 2024; it has undergone rapid development over the past year. GitHub lists 45 individual committers, but the majority of the commits are from a handful of PhD students from the Southern University of Science and Technology, Peking University, and Fudan University, as well as a Chinese company called Ant Group, which is a sponsor of Asterinas.

At the time of writing, Asterinas supports two architectures, x86 and RISC-V. In the January blog post linked above, it was reported that Asterinas supported 180 Linux system calls, but the number has since grown to 206 on x86. As of version 6.7, Linux has 368 system calls in total, so there is some way to go yet.

Overall, Asterinas is in early development. There have been no releases, release announcements, changelogs, or much of anything other than Git tags and a short installation guide in the documentation. The Dependents tab of the OSTD crate on crates.io shows that no unrelated, published crate yet uses OSTD.

It does not seem like Asterinas is able to run any applications yet. Issue #1868 in Asterinas's repository outlines preliminary plans toward a first distribution. The initial focus on a custom initramfs and some rudimentary user-space applications, followed by being able to run Docker. There are initial plans to bootstrap a distribution based on Nix. Notably (but unsurprisingly), this issue mentions that Asterinas doesn't support loading Linux kernel modules, nor does it ever plan to.

Near-future goals

The Roadmap section of the Asterinas book says that the near-term goals are to expand the support for CPU architectures and hardware, as well as to focus on real-world usability in the cloud by providing a host OS for virtual machines. Apparently, the support for Linux virtio devices is already there, so a major hurdle has already been cleared. In particular, the Chinese cloud market, in the form of Aliyun (also known as Alibaba Cloud) is a focus. The primary plans involve creating a container host OS with a tight, formally verified TCB and support for some trusted-computing features in Intel hardware, for the Chinese cloud service.

While both Rust for Linux and Asterinas have similar goals (providing a safer kernel by relying on Rust's memory safety), their scopes and approaches are different. Rust for Linux focuses on safe abstractions strictly for new device drivers to be written in safe Rust, but this leaves the rest of the kernel untouched. Asterinas, on the other hand, aims to build a whole new kernel from the ground up, restricting the unsafe-permitting core to the absolute minimum, which can then be formally verified. Asterinas also focuses on containers and cloud computing, at least for now, while Rust for Linux looks to benefit the whole of the Linux ecosystem.

Despite the stated cloud focus, there is more going on, for example building support for X11 and Xfce. Also, the OSTD could, of course, prove interesting for OS development enthusiasts irrespective of the Asterinas project, but so far it remains unknown and untested by a wider audience.

Asterinas is certainly a refreshingly innovative take on principles for operating-system development, leaning on the safety and soundness foundations provided by the Rust language and compiler. So far it is at an early exploratory stage driven by enthusiastic Chinese researchers and doesn't see any serious practical use, but it is worth keeping an eye on. It will be interesting to see the reception it will get from the Rust for Linux team and the Linux community at large.