Pith. sign in

REVIEW 3 major objections 7 minor 63 references

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

T0 review · 3 major / 7 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A Linux-compatible operating system kernel written almost entirely in safe Rust can match Linux's performance while confining all unsafe code to a 14% trusted framework.

desk verdict A substantial engineering result — a Linux-ABI-compatible kernel with a 14% unsafe-Rust TCB and roughly Linux-parity benchmarks — where the architecture is the contribution and the 'sound' claim in the abstract is ahead of the KERNMIRI evidence. read the letter →

arxiv 2506.03876 v1 pith:4O5H6ZKU submitted 2025-06-04 cs.OS

Yuke Peng , Hongliang Tian , Zhang Junyang , Ruihan Li , Chengjun Chen , Jianfeng Jiang , Jinyi Xian , Xiaolin Wang
show 5 more authors
Chenren Xu Diyu Zhou Yingwei Luo Shoumeng Yan Yinqian Zhang
This is my paper
classification cs.OS
keywords framekernelsafeRustintra-kernelprivilegeseparationuntypedmemorymemory-safetyTCBLinuxABIcompatibilitypolicyinjectionundefinedbehaviordetection
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper asks whether a feature-rich, general-purpose operating system can be built almost entirely in safe Rust, and it answers yes with a new architecture called framekernel. In a framekernel the whole OS runs in a single address space, but a language-enforced boundary splits it: a small privileged framework (OSTD) is the only place unsafe Rust is allowed, and every OS service — virtual memory, scheduling, file systems, sockets, and device drivers — is written in safe Rust against OSTD's safe APIs. The authors' OS, Asterinas, supports over 210 Linux system calls, reports a mean normalized LMbench score of 1.08 relative to Linux, and puts the code that must be trusted for memory safety (the TCB) at only 14.0% of the codebase, versus 43.8% to 66.1% in comparable Rust-based OSes. A checker called KERNMIRI, built by extending Rust's Miri interpreter with physical memory and paging, exercises every unsafe line in OSTD's memory module and has already caught real undefined behavior there. If the claims hold, memory safety in an OS kernel does not have to be bought at the price of performance or of abandoning the Linux software ecosystem.

What carries the argument

The load-bearing mechanism is OSTD's safe-API layer, organized by the framekernel principle that sensitive resources stay inside the privileged framework while insensitive resources are delegated to safe services. The central abstraction is untyped memory (UFrame and USegment), which handles externally modifiable memory such as MMIO, DMA buffers, and user pages by exposing only a read-write interface that copies plain old data, never forming Rust references into memory that hardware or user code can change. Around this sit ten safety invariants (Inv. 1–10) that define what the framework guarantees, plus safe policy injection, a technique that lets complex policies — task schedulers, frame allocators, slab allocators — be written in safe Rust outside the TCB while the framework still enforces the load-bearing rule, for example that a task runs on at most one CPU. The validation machinery is KERNMIRI, a Miri-based interpreter extended with physical memory simulation and a paging system, used to check OSTD's unsafe code for undefined behavior.

What would settle it

Exhibit a safe-Rust Asterinas service that corrupts kernel memory through an OSTD API, or run KERNMIRI over OSTD's untested modules (task switching, trap and interrupt delivery, IOMMU setup) and find any undefined behavior — either outcome would disprove the soundness claim. A weaker but decisive check is to rebuild the TCB measurement independently and show that the 14.0% figure omits unsafe code that is actually linked into the running kernel.

Watch

Extended reading notes

Core claim

The central claim is that a framekernel — a single-address-space OS whose privilege separation is enforced by Rust's safe/unsafe language boundary rather than by hardware isolation — combines the throughput of a monolithic kernel with a small and sound memory-safety TCB. To make this work, the paper contributes OSTD, a privileged framework that hides all hardware-sensitive operations behind safe APIs and states ten invariants (Inv. 1–10) that collectively define the framework's soundness, and Asterinas, a Linux ABI-compatible OS whose over 210 system calls and all subsystems are implemented entirely in safe Rust on top of OSTD. The paper reports that Asterinas performs on par with Linux (LMbench geometric mean 1.08; normalized application scores 1.17 for Nginx, 1.31 for Redis, 0.85 for SQLite), that its memory-safety TCB is 14.0% of the codebase, and that KERNMIRI, a Miri extension simulating physical memory and paging, covers 100% of unsafe lines in OSTD's memory-management module and has already surfaced a data race and a mutability violation, both of which were fixed.

Load-bearing premise

The memory-safety guarantee rests on the assumption that every unsafe operation inside the OSTD framework is correctly encapsulated by its safe APIs — a claim backed by the paper's ten stated invariants and by complete unsafe-line testing of the memory module, while unsafe code in other framework modules is not yet verified to the same standard.

Editorial extensions

If this is right

  • Linux applications run unmodified: because Asterinas implements the Linux ABI with over 210 system calls, stock Nginx, Redis, and SQLite binaries boot and run without porting, so a safe-Rust kernel does not wall itself off from the existing ecosystem.
  • Safety checks are cheap: the per-operation overhead of OSTD's checks is at most 6.7% (frame allocation) and mostly below 3%, so the small TCB is not paid for with a per-call performance tax.
  • Device drivers can be written in safe Rust: the largest unsafe surface in earlier Rust OSes is moved into safe code, which is what lets the TCB stay small even though drivers dominate a mature OS codebase.
  • TCB growth is contained: because schedulers and allocators are injectable safe-Rust policies, added sophistication in these components grows the non-TCB code rather than the trusted framework.
  • UB checking becomes practical for OS kernels: KERNMIRI found a data race in frame reference-count handling and a mutability violation in heap initialization that ordinary testing missed, and it can be rerun as the framework evolves.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The 14.0% figure is a relative, runtime-code measurement; the paper itself lists the Rust toolchain, core library, bootloader, and firmware as part of the full TCB, so the headline number is best read as a comparison across Rust-based OSes rather than an absolute trusted-surface size.
  • KERNMIRI's complete unsafe-line coverage is confined to the memory-management module; running it over task switching, trap and interrupt delivery, and IOMMU setup is the direct next test of the soundness claim, since those modules also contain unsafe code.
  • The evaluation is single-core; multi-core behavior — preemption, per-CPU run queues, lock contention — is the setting most likely to strain the claim that language-level isolation is free.
  • Part of the networking edge over Linux (in Nginx and TCP microbenchmarks) is attributed by the paper to the smoltcp stack lacking congestion control, so the fairness of the parity claim is best judged on the system-call and memory benchmarks rather than the networking wins.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 7 minor

Summary. The paper proposes the framekernel architecture, in which a kernel is split into a privileged OS framework (OSTD) that contains all unsafe Rust code and exposes safe APIs, and de-privileged services written entirely in safe Rust. The authors present Asterinas, a Linux-ABI-compatible OS built on OSTD that supports over 210 system calls and is implemented in safe Rust. The main claims are (1) a small memory-safety TCB of about 14.0% of the codebase, (2) performance on par with Linux in micro- and macro-benchmarks, and (3) soundness of the privileged framework, evidenced by a custom Miri-based tool, KERNMIRI, that detects undefined behavior in OSTD's memory-management module.

Significance. If the claims hold, this is a significant contribution to Rust-based OS research: it demonstrates that a feature-rich, general-purpose OS can be built almost entirely in safe Rust, with unsafe code confined to a small framework, and that the resulting system can be competitive with Linux. The work is also careful in several respects: the performance evaluation is detailed and the authors acknowledge many caveats; the TCB comparison uses a defined metric applied consistently across OSes; and KERNMIRI provides a concrete, reproducible mechanism for detecting UB in at least part of OSTD. The open-source repository and artifact links are positive factors for reproducibility. The central concern is that the strength of the soundness claim exceeds the verification evidence, which affects the headline contribution rather than the overall architectural idea.

major comments (3)
  1. [§6.3 (Table 10) and §3] The paper's central claim of a 'sound TCB' is not supported by the evidence presented. Section 3 defines soundness as 'the absence of UBs under all circumstances, irrespective of interactions with OS services, user code, or peripheral devices.' The only verification evidence, KERNMIRI, is described in §6.3 and covers just the mm submodules listed in Table 10 (dma, frame, heap, kspace, page_table, io, vm_space); §6.3.1 states this module 'contains the majority of unsafe code in OSTD.' Unsafe code in trap handling, context switching, interrupt and IOMMU setup, and the enforcement of Inv. 2, 3, 8, 9, 10 lies outside the tested set. A single UB in any of those locations would break memory safety for the entire system. Furthermore, KERNMIRI is a dynamic testing tool, not a proof; even 100% unsafe-line coverage within mm cannot establish 'absence of UBs under all circumstances.' I recommend either extending KERNMIRI coverage to all unsafe code in OSTD or reformulating the title/abstract to claim soundness for the memory-management core, with the remaining framework verified by audit. This is a load-bearing issue for the paper's headline contribution.
  2. [§6.1, Table 7] The performance parity claim is overstated because a substantial part of the advantage comes from an unfair TCP comparison. Table 7 reports lat_tcp 1.95, lat_udp 1.57, and other network entries with large normalized gains; §6.1.1 explicitly attributes these to the smoltcp stack's lack of congestion control, which lets TCP operate at full speed. Since the overall geometric mean of 1.08 in Table 7 includes these network benchmarks, the headline 'performance on par with Linux' is not a like-for-like comparison. In addition, Linux is run with mitigations=off and hugepages=0, and both kernels run in single-CPU QEMU. I ask the authors to report the geometric mean with network benchmarks excluded, to add a comparison that controls for the TCP congestion-control difference, and to state clearly in the abstract/conclusions that the parity claim holds only under these conditions.
  3. [§6.2.1 (Rules 1–3)] The TCB size metric is self-referential in a way that weakens the 'small TCB' contribution. Rule 2 defines TCB membership as 'crates containing unsafe code,' so the 14.0% figure is largely an arithmetic consequence of confining unsafe code to OSTD; it does not measure whether a crate is actually required for soundness, as the Section 3 Minimality principle demands. A crate may contain a single `unsafe` block that is unrelated to memory safety, and it is counted as fully in the TCB; conversely, safe crates that are critical to the framework's invariants are counted as non-TCB unless they are dependencies of a TCB crate (Rule 3). I recommend reporting a complementary metric, such as the number of `unsafe` lines per crate, and discussing how the framework's sensitive-resource classification (Figure 2) maps onto the crate-level rule. This would turn the TCB claim from a definitional observation into an architectural one.
minor comments (7)
  1. [Figure 7] The x-axis extends to 2027, but the paper is dated 2025; please clarify whether this is a projection or a typographical error.
  2. [Table 9] The numeric columns appear to run together in the manuscript (e.g., '662875285' and '290310571'); please fix the formatting and verify the totals against the paper's statement of over 100K lines of Rust.
  3. [§6.2.1] The LCS metric needs a more precise definition of how source lines are mapped from LLVM IR after LTO; without this, the TCB-size comparison is not reproducible.
  4. [§6.1.1] Report confidence intervals or statistical tests for the reported geometric mean; Table 7 shows standard deviations only for some entries and no aggregate uncertainty.
  5. [Figure 5 caption] The caption contains a typo: 'Ngnix' should be 'Nginx.'
  6. [Appendix C and Figure 5(c)] 'V ACUUM' should be 'VACUUM' in the test description.
  7. [§4.4.1] The description of Inv. 8 says the is_running flag is 'checked and set prior to a context switch,' but does not specify the atomicity or ordering guarantees that make this check safe under interrupts and preemption; please clarify.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper's central claims are empirical measurements and an architectural design, and the apparent weaknesses are evidence-completeness concerns rather than circular derivations.

full rationale

After tracing the claimed derivation chain, I find no circular step. The paper's headline claims are empirical: the 1.08 LMbench normalized score, the Nginx/Redis/SQLite results, and the 14.0% TCB figure are measurements, not consequences of the paper's definitions. The TCB classification rule ('Crates containing unsafe code... are considered part of the TCB') is a standard trust-boundary modeling choice; it does not by itself produce the 14.0% number, which comes from an LLVM-based LCS measurement applied uniformly to Asterinas, RedLeaf, Theseus, and Tock. The performance evaluation compares Asterinas against Linux 5.15 under the same QEMU configuration, so no fitted input is relabeled as a prediction. The soundness section relies on KERNMIRI, a tool built by the authors, but KERNMIRI is an extension of Miri's UB checker and is used as dynamic testing; the paper's own scoping statement that the mm module 'contains the majority of unsafe code in OSTD' is a limitation on verification coverage rather than a circular justification. The safety invariants (Inv. 1-10) are design requirements enforced by runtime checks and API design, not conclusions derived from the claim of soundness. Citations to the authors' own repositories and sample projects are for artifact availability, not load-bearing support for the architecture's correctness. The weakest point of the paper is the gap between the strong 'sound TCB' claim and the partial KERNMIRI coverage of unsafe code outside the mm module, but that is an evidence-strength or verification-completeness concern, not circularity. Accordingly, the circularity score is 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The central claims rely on the correctness of the OSTD framework and the resource classification, both of which are assumptions or partially tested design assertions. No free parameters are fitted to data, and no new physical entities are postulated. The trust in the Rust compiler and hardware are standard domain assumptions, while the invariants and resource classification are specific to this paper's architecture.

assumptions (5)
  • domain assumption Rust's type system and borrow checker guarantee memory safety for all safe Rust code in the non-TCB components.
    Invoked throughout, e.g., Section 4.3, where the safety of OSTD clients relies on the compiler enforcing memory safety for safe Rust.
  • domain assumption The Rust toolchain, including core and alloc crates, is trusted and does not introduce memory safety violations.
    Explicitly stated in Section 6.2.1, Rule 1: crates provided by the Rust toolchain are not part of the run-time TCB, assuming they are correct.
  • domain assumption The CPU, IOMMU, and other core hardware behave as specified, e.g., IOMMU interrupt remapping prevents device spoofing.
    Required for Inv. 3 and Inv. 6 in Section 4.3, where protection against peripheral devices relies on hardware features.
  • ad hoc to paper The classification of OS resources into sensitive and insensitive (Figure 2) is complete and correct.
    This classification underpins the entire privilege separation. If a sensitive resource is misclassified as insensitive and exposed to non-TCB code, the TCB soundness would be compromised.
  • ad hoc to paper The ten safety invariants (Inv. 1 through Inv. 10) are sufficient to ensure the absence of undefined behavior in OSTD.
    Invariants are stated in Sections 4.2, 4.3, and 4.4 but are not formally proven; they are design assertions validated only by tests and KERNMIRI.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Asterinas: A Linux ABI-Compatible, Rust-Based Framekernel OS with a Small and Sound TCB." pith.science (2026). https://pith.science/paper/4O5H6ZKU

@misc{pith2026250603876,
  author       = {Pith},
  title        = {Pith review of: Asterinas: A Linux ABI-Compatible, Rust-Based Framekernel OS with a Small and Sound TCB},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4O5H6ZKU}},
  note         = {Machine review of arXiv:2506.03876}
}
read the original abstract

How can one build a feature-rich, general-purpose, Rust-based operating system (OS) with a minimal and sound Trusted Computing Base (TCB) for memory safety? Existing Rust-based OSes fall short due to their improper use of unsafe Rust in kernel development. To address this challenge, we propose a novel OS architecture called framekernel that realizes Rust's full potential to achieve intra-kernel privilege separation, ensuring TCB minimality and soundness. We present OSTD, a streamlined framework for safe Rust OS development, and Asterinas, a Linux ABI-compatible framekernel OS implemented entirely in safe Rust using OSTD. Supporting over 210 Linux system calls, Asterinas delivers performance on par with Linux, while maintaining a minimized, memory-safety TCB of only about 14.0% of the codebase. These results underscore the practicality and benefits of the framekernel architecture in building safe and efficient OSes.

Figures

Figures reproduced from arXiv: 2506.03876 by the authors.

Figure 1
Figure 1. A framekernel combines the speed of a monolithic [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 3
Figure 3. An example of OSTD APIs: system call handling work or encapsulated into high-level, insensitive ones. The net result is that the privileged OS framework only exposes to the de-privileged OS services a small set of insensitive resources that is sufficient to support the three primary needs of safe OS development: (1) safe user-kernel interactions, (2) safe kernel logic, and (3) safe kernel-peripheral interactions. Th… view at source ↗
Figure 4
Figure 4. An overview of Asterinas. Inv. 9: A HeapSlot or any object derived from it must not outlive its parent Slab. Additionally, when HeapSlot::into_box is called, the method checks cheaply whether the slot’s address and size can fit a requested object of type T: Inv. 10: An object is created from a HeapSlot only if the slot meets the object’s size and alignment requirements. In practice, many kernel components rely on a … view at source ↗
Figures from the paper (5 more)
Figure 5
Figure 5. Figure 5: I/O-intensive application benchmarks with Ngnix, Redis, and SQLite. [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]
Figure 6
Figure 6. Figure 6: IOMMU overhead with different mechanism 6.1.3 Overhead due to Safety Checks The overhead introduced by the OSTD’s safety mechanisms does not prevent ASTERINAS’s performance from being com￾parable to a monolithic kernel. ASTERINAS has integrated several safety mechanism…
Figure 8
Figure 8. Figure 8: KERNMIRI, a UB detection tool for Rust OSes [PITH_FULL_IMAGE:figures/full_fig_p012_8.png]
Figure 9
Figure 9. Figure 9: UB cases detected by KERNMIRI. proves the soundness of our implementation of OSTD. We outline two representative UB cases in OSTD detected by KERNMIRI, as illustrated in [PITH_FULL_IMAGE:figures/full_fig_p013_9.png]
Figure 10
Figure 10. Figure 10: An example of OSTD API usage: request data from a device. B Complete results for Redis benchmark [PITH_FULL_IMAGE:figures/full_fig_p016_10.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

63 extracted references · 63 canonical work pages

  1. [1]

    https://github

    The Asterinas Github repository. https://github. com/asterinas/asterinas

    work page

  2. [2]

    https://github.com/asterinas/ atc25-artifact-evaluation/

    The ATC’25 artifact evaluation reposi- tory. https://github.com/asterinas/ atc25-artifact-evaluation/

    work page

  3. [3]

    https://en.wikipedia

    Rust for linux on wikipedia. https://en.wikipedia. org/wiki/Rust_for_Linux, 2024

    work page 2024

  4. [4]

    C++ named requirements: POD- Type (deprecated in C++20) - cppreference.com

    cppreference . C++ named requirements: POD- Type (deprecated in C++20) - cppreference.com. https://en.cppreference.com/w/cpp/named_ req/PODType

    work page

  5. [5]

    CFS Scheduler — The Linux Kernel documenta- tion

    Linux . CFS Scheduler — The Linux Kernel documenta- tion. https://www.kernel.org/doc/html/latest/ scheduler/sched-design-CFS.html

    work page

  6. [6]

    Behavior con- sidered undefined - The Rust Reference

    The Rust Project Developers . Behavior con- sidered undefined - The Rust Reference. https: //doc.rust-lang.org/nightly/reference/ behavior-considered-undefined.html

    work page

  7. [7]

    The borrow checker - Rust Compiler Development Guide

    The Rust Project Developers . The borrow checker - Rust Compiler Development Guide. https://rustc-dev-guide.rust-lang.org/ borrow_check.html

    work page

  8. [8]

    How Safe and Unsafe In- teract - The Rustonomicon

    The Rust Project Developers . How Safe and Unsafe In- teract - The Rustonomicon. https://doc.rust-lang. org/nomicon/safe-unsafe-meaning.html

    work page

Show all 63 references
  1. [9]

    Type check- ing - Rust Compiler Development Guide

    The Rust Project Developers . Type check- ing - Rust Compiler Development Guide. https://rustc-dev-guide.rust-lang.org/ type-checking.html

  2. [10]

    What is Ownership? - The Rust Programming Lan- guage

    The Rust Project Developers . What is Ownership? - The Rust Programming Lan- guage. https://doc.rust-lang.org/book/ ch04-01-what-is-ownership.html

  3. [11]

    Widespread IT Outage Due to CrowdStrike Update

    America’s Cyber Defense Agency. Widespread IT Outage Due to CrowdStrike Update. https:// www.cisa.gov/news-events/alerts/2024/07/19/ widespread-it-outage-due-crowdstrike-update , 2024

    2024

  4. [12]

    Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, and Alexander J. Summers. How do pro- grammers use unsafe rust?Proc. ACM Program. Lang., 4(OOPSLA):136:1–136:27, 2020

    2020

  5. [13]

    Flexible I/O Tester

    Jens Axboe. Flexible I/O Tester. https://github. com/axboe/fio, 2022

    2022

  6. [14]

    The Slab Allocator: An Object-Caching Kernel Memory Allocator

    Jeff Bonwick. The Slab Allocator: An Object-Caching Kernel Memory Allocator. InUSENIX Summer

  7. [15]

    Magazines and Vmem: Extending the Slab Allocator to Many CPUs and Arbitrary Resources

    Jeff Bonwick and Jonathan Adams. Magazines and Vmem: Extending the Slab Allocator to Many CPUs and Arbitrary Resources. InUSENIX ATC, General Track

  8. [16]

    Theseus: an experiment in operating system structure and state management

    Kevin Boos, Namitha Liyanage, Ramla Ijaz, and Lin Zhong. Theseus: an experiment in operating system structure and state management. In14th USENIX Sym- posium on Operating Systems Design and Implemen- tation (OSDI 20), pages 1–19. USENIX Association, November 2020

    2020

  9. [17]

    An empirical study of operating systems errors.SIGOPS Oper

    Andy Chou, Junfeng Yang, Benjamin Chelf, Seth Hallem, and Dawson Engler. An empirical study of operating systems errors.SIGOPS Oper. Syst. Rev., 35(5):73–88, October 2001

    2001

  10. [18]

    A first look at Rust in the 6.1 kernel

    Jonathan Corbet. A first look at Rust in the 6.1 kernel. https://lwn.net/Articles/910762/, 2022

    2022

  11. [19]

    Frans Kaashoek, and Robert T

    Cody Cutler, M. Frans Kaashoek, and Robert T. Morris. The benefits and costs of writing a POSIX kernel in a high-level language. In13th USENIX Symposium on Op- erating Systems Design and Implementation (OSDI 18), pages 89–105, Carlsbad, CA, October 2018. USENIX Association

    2018

  12. [20]

    Nested kernel: An op- erating system architecture for intra-kernel privilege sep- aration

    Nathan Dautenhahn, Theodoros Kasampalis, Will Dietz, John Criswell, and Vikram Adve. Nested kernel: An op- erating system architecture for intra-kernel privilege sep- aration. InProceedings of the Twentieth International Conference on Architectural Support for Programming Lang...

    2015

  13. [21]

    Redox - your next(gen) os

    Redox Developers. Redox - your next(gen) os. https: //www.redox-os.org/, 2024

    2024

  14. [22]

    Smoltcp: TCP/IP Stack for Embed- ded Rust.https://github.com/smoltcp-rs, 2025

    Smoltcp Developers. Smoltcp: TCP/IP Stack for Embed- ded Rust.https://github.com/smoltcp-rs, 2025

    2025

  15. [23]

    Example: Writing a Kernel in 100 Lines of Safe Rust - The Asterinas Book

    The Asterinas developers. Example: Writing a Kernel in 100 Lines of Safe Rust - The Asterinas Book. https: //github.com/asterinas/asterinas/blob/ dec7ac1346649a0ef1a1256da258cd2f9f11ac4b/ docs/src/ostd/a-100-line-kernel.md

  16. [24]

    The reader- writer interface of untyped memory

    The Asterinas developers. The reader- writer interface of untyped memory. https: //github.com/asterinas/asterinas/blob/ main/ostd/src/mm/frame/untyped.rs#L73

  17. [25]

    The Rustonomicon

    The Rust Project Developers. The Rustonomicon. https://github.com/rust-lang/nomicon, 2024. 14

    2024

  18. [26]

    ab - apache http server benchmarking tool

    The Apache Software Foundation. ab - apache http server benchmarking tool. https://httpd.apache. org/docs/2.4/programs/ab.html, 2024

    2024

  19. [27]

    Growth, evolution, and structural change in open source software

    Michael Godfrey and Qiang Tu. Growth, evolution, and structural change in open source software. InProceed- ings of the 4th International Workshop on Principles of Software Evolution, IWPSE ’01, page 103–106, New York, NY , USA, 2001. Association for Computing Ma- chinery

    2001

  20. [28]

    The JX operating system

    Michael Golm, Meik Felser, Christian Wawersich, and Jürgen Kleinoeder. The JX operating system. In2002 USENIX Annual Technical Conference (USENIX ATC 02), Monterey, CA, June 2002. USENIX Association

    2002

  21. [29]

    Android rust introduction

    Google. Android rust introduction. https: //source.android.com/docs/setup/build/ rust/building-rust-modules/overview

  22. [30]

    What is mem- ory safety and why does it matter? https://www

    Internet Security Research Group. What is mem- ory safety and why does it matter? https://www. memorysafety.org/docs/memory-safety/, 2025

    2025

  23. [31]

    Klint: Compile-time detection of atomic context violations for kernel rust code

    Gary Guo. Klint: Compile-time detection of atomic context violations for kernel rust code. https://www.memorysafety.org/blog/ gary-guo-klint-rust-tools/, 2023

    2023

  24. [32]

    ghost: Fast & flexible user-space delegation of linux schedul- ing

    Jack Tigar Humphries, Neel Natu, Ashwin Chaugule, Ofir Weisse, Barret Rhoden, Josh Don, Luigi Rizzo, Oleg Rombakh, Paul Turner, and Christos Kozyrakis. ghost: Fast & flexible user-space delegation of linux schedul- ing. InProceedings of the ACM SIGOPS 28th Sympo- sium on Opera...

    2021

  25. [33]

    Singularity: Rethinking the software stack.ACM SIGOPS Operating Systems Review, 41(2):37–49, April 2007

    Galen Hunt and Jim Larus. Singularity: Rethinking the software stack.ACM SIGOPS Operating Systems Review, 41(2):37–49, April 2007

    2007

  26. [34]

    The evolution of freebsd and linux

    Clemente Izurieta and James Bieman. The evolution of freebsd and linux. InProceedings of the 2006 ACM/IEEE International Symposium on Empirical Soft- ware Engineering, ISESE ’06, page 204–211, New York, NY , USA, 2006. Association for Computing Machinery

    2006

  27. [35]

    A simple cor- rectness proof of the MCS contention-free lock.Infor- mation Processing Letters, 48(5):215–220

    Theodore Johnson and Krishna Harathi. A simple cor- rectness proof of the MCS contention-free lock.Infor- mation Processing Letters, 48(5):215–220

  28. [36]

    Kdpm: Kernel data protection mechanism using a memory protection key

    Hiroki Kuzuno and Toshihiro Yamauchi. Kdpm: Kernel data protection mechanism using a memory protection key. InAdvances in Information and Computer Security: 17th International Workshop on Security, IWSEC 2022, Tokyo, Japan, August 31 – September 2, 2022, Proceed- ings, page 66...

    2022

  29. [37]

    Ex- ploring rust for unikernel development

    Stefan Lankes, Jens Breitbart, and Simon Pickartz. Ex- ploring rust for unikernel development. InProceedings of the 10th Workshop on Programming Languages and Operating Systems, PLOS ’19, page 8–15, New York, NY , USA, 2019. Association for Computing Machinery

    2019

  30. [38]

    Giffin, Pat Pannuto, Prabal Dutta, and Philip Levis

    Amit Levy, Bradford Campbell, Branden Ghena, Daniel B. Giffin, Pat Pannuto, Prabal Dutta, and Philip Levis. Multiprogramming a 64kb computer safely and efficiently. InProceedings of the 26th Symposium on Operating Systems Principles, SOSP ’17, page 234–251, New York, NY , USA,...

    2017

  31. [39]

    An Empirical Study of {Rust- for-Linux}: The Success, Dissatisfaction, and Compro- mise

    Hongyu Li, Liwei Guo, Yexuan Yang, Shangguang Wang, and Mengwei Xu. An Empirical Study of {Rust- for-Linux}: The Success, Dissatisfaction, and Compro- mise. pages 425–443

  32. [40]

    An empirical study of rust- for-linux: The success, dissatisfaction, and compromise

    Hongyu Li, Liwei Guo, Yexuan Yang, Shangguang Wang, and Mengwei Xu. An empirical study of rust- for-linux: The success, dissatisfaction, and compromise. In Saurabh Bagchi and Yiying Zhang, editors,Proceed- ings of the 2024 USENIX Annual Technical Conference, USENIX ATC 2024, S...

    2024

  33. [41]

    Rust — The Linux Kernel documen- tation

    Linux. Rust — The Linux Kernel documen- tation. https://docs.kernel.org/rust/index. html, 2024

    2024

  34. [42]

    Llvm tools

    LLVM Project. Llvm tools. https://llvm.org/ docs/CommandGuide/, 2025. Accessed: 2025-01-14

    2025

  35. [43]

    Anil Madhavapeddy and David J. Scott. Unikernels: Rise of the virtual library operating system: What if all the software layers in a virtual appliance were compiled within the same safe, high-level language framework? Queue, 11(11):30–44, December 2013

    2013

  36. [44]

    Theodore Markettos, Colin Rothwell, Brett F

    A. Theodore Markettos, Colin Rothwell, Brett F. Gut- stein, Allison Pearce, Peter G. Neumann, Simon W. Moore, and Robert N. M. Watson. Thunderclap: Ex- ploring Vulnerabilities in Operating System IOMMU Protection via DMA from Untrustworthy Peripherals. InProceedings 2019 Netwo...

    2019

  37. [45]

    McKenney, Joel Fernandes, Silas Boyd- Wickizer, and Jonathan Walpole

    Paul E. McKenney, Joel Fernandes, Silas Boyd- Wickizer, and Jonathan Walpole. RCU usage in the Linux kernel: Eighteen years later.SIGOPS Oper. Syst. Rev., 54(1):47–63, August 2020

    2020

  38. [46]

    Lmbench: Portable tools for performance analysis

    Larry W McV oy, Carl Staelin, et al. Lmbench: Portable tools for performance analysis. InUSENIX annual tech- nical conference, pages 279–294. San Diego, CA, USA, 1996. 15

    1996

  39. [47]

    Enoki: High velocity linux kernel scheduler development

    Samantha Miller, Anirudh Kumar, Tanay Vakharia, Ang Chen, Danyang Zhuo, and Thomas Anderson. Enoki: High velocity linux kernel scheduler development. In Proceedings of the Nineteenth European Conference on Computer Systems, EuroSys ’24, page 962–980, New York, NY , USA, 2024. ...

    2024

  40. [48]

    Miri - an interpreter for rust’s mid-level in- termediate representation

    Miri. Miri - an interpreter for rust’s mid-level in- termediate representation. https://github.com/ rust-lang/miri, 2024

    2024

  41. [49]

    RedLeaf: Isolation and communication in a safe operating system

    Vikram Narayanan, Tianjiao Huang, David Detweiler, Dan Appel, Zhaofeng Li, Gerd Zellweger, and Anton Burtsev. RedLeaf: Isolation and communication in a safe operating system. In14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20), pages 21–39. USENIX ...

    2020

  42. [50]

    Lightweight kernel isolation with virtualization and vm functions

    Vikram Narayanan, Yongzhe Huang, Gang Tan, Trent Jaeger, and Anton Burtsev. Lightweight kernel isolation with virtualization and vm functions. InProceedings of the 16th ACM SIGPLAN/SIGOPS International Confer- ence on Virtual Execution Environments, VEE ’20, page 157–171, New ...

    2020

  43. [51]

    Measuring and reducing cpu usage in sqlite.https://sqlite.org/cpu.html, 2024

    SQLite organization. Measuring and reducing cpu usage in sqlite.https://sqlite.org/cpu.html, 2024

    2024

  44. [52]

    rcore os. rcore. https://github.com/rcore-os/ rCore, 2023

    2023

  45. [53]

    Redis benchmark

    Redis. Redis benchmark. https://redis.io/docs/ latest/operate/oss_and_stack/management/ optimization/benchmarks/, 2024

    2024

  46. [54]

    Microsoft is busy rewrit- ing core windows code in memory-safe rust

    The Register. Microsoft is busy rewrit- ing core windows code in memory-safe rust. https://www.theregister.com/2023/04/27/ microsoft_windows_rust/

    2023

  47. [55]

    Mutex::lock_noguard() may be unsafe · Issue #862 · Rust-for-Linux/linux

    Rust for Linux. Mutex::lock_noguard() may be unsafe · Issue #862 · Rust-for-Linux/linux. https://github. com/Rust-for-Linux/linux/issues/862

  48. [56]

    Sartakov, Lluís Vilanova, and Peter Pietzuch

    Vasily A. Sartakov, Lluís Vilanova, and Peter Pietzuch. Cubicleos: a library os with software componentisation for practical isolation. InProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, AS- PLOS ’21...

    2021

  49. [57]

    Understanding open source software evolution.Software Evolution and Feedback: Theory and Practice, 9:181–205, 2006

    Walt Scacchi. Understanding open source software evolution.Software Evolution and Feedback: Theory and Practice, 9:181–205, 2006

    2006

  50. [58]

    Strace linux syscall tracer

    Strace. Strace linux syscall tracer. https://strace. io/, 2024

    2024

  51. [59]

    Intra-unikernel isolation with intel mem- ory protection keys

    Mincheol Sung, Pierre Olivier, Stefan Lankes, and Bi- noy Ravindran. Intra-unikernel isolation with intel mem- ory protection keys. InProceedings of the 16th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments, VEE ’20, page 143–156, New York, NY , US...

    2020

  52. [60]

    RustSec Advisory Database

    Rust Secure Code WG. RustSec Advisory Database. https://github.com/RustSec/advisory-db, 2024

    2024

  53. [61]

    Paul Willmann, Scott Rixner, and Alan L. Cox. Pro- tection strategies for direct access to virtualized I/O devices. In2008 USENIX Annual Technical Conference (USENIX ATC 08), Boston, MA, June 2008. USENIX Association

    2008

  54. [62]

    Safe to the last instruc- tion: Automated verification of a type-safe operating system

    Jean Yang and Chris Hawblitzel. Safe to the last instruc- tion: Automated verification of a type-safe operating system. InPLDI. Association for Computing Machin- ery, Inc., June 2010

    2010

  55. [63]

    Gligor, James Newsome, and Jonathan M

    Zongwei Zhou, Virgil D. Gligor, James Newsome, and Jonathan M. McCune. Building verifiable trusted path on commodity x86 computers. In2012 IEEE Sympo- sium on Security and Privacy, pages 616–630, 2012. A Another Example for OSTDAPIs Task Context Request data from device Create...

    2012

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.