Theseus: an Experiment in Operating System Structure and State Management
Kevin Boos, Namitha Liyanage, Ramla Ijaz, Lin Zhong
Abstract
This paper describes an operating system (OS) called Theseus. Theseus is the result of multi-year experimentation to redesign and improve OS modularity by reducing the states one component holds for another, and to leverage a safe programming language, namely Rust, to shift as many OS responsibilities as possible to the compiler.
Theseus embodies two primary contributions. First, an OS structure in which many tiny components with clearly-defined, runtime-persistent bounds interact without holding states for each other. Second, an intralingual approach that realizes the OS itself using language-level mechanisms such that the compiler can enforce invariants about OS semantics.
Theseus's structure, intralingual design, and state management realize live evolution and fault recovery for core OS components in ways beyond that of existing works.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 6b815ae3-59f5-4e20-8e5b-64adf3839809Cited by top-tier papers29
- Rudra: Finding Memory Safety Bugs in Rust at the Ecosystem ScaleYechan Bae, Youngsuk Kim, Ammar Askar, Jungwon Lim et al.SOSP 2021 · 61 citations
- RULF: Rust Library Fuzzing via API Dependency Graph TraversalJianfeng Jiang, Hui Xu, Yangfan ZhouASE 2021 · 44 citations
- FlexOS: towards flexible OS isolationHugo Lefeuvre, Vlad-Andrei Badoiu, Alexander Jung, Stefan Lucian Teodorescu et al.ASPLOS 2022 · 36 citations
- Lightweight Fault Isolation: Practical, Efficient, and Secure Software SandboxingZachary YedidiaASPLOS 2024 · 17 citations
- ASTERINAS: A Linux ABI-Compatible, Rust-Based Framekernel OS with a Small and Sound TCBYuke Peng, Hongliang Tian, Junyang Zhang, Ruihan Li et al.USENIX ATC 2025 · 16 citations
Builds on3
- Understanding memory and thread safety practices and issues in real-world Rust programsBoqin Qin, Yilun Chen, Zeming Yu, Linhai Song et al.PLDI 2020 · 112 citations
- Stacked borrows: an aliasing model for RustRalf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek DreyerPOPL 2020 · 67 citations
- Ginseng: Keeping Secrets in Registers When You Distrust the Operating SystemMin Hong Yun, Lin ZhongNDSS 2019 · 48 citations
Related papers
- RedLeaf: Isolation and Communication in a Safe Operating SystemVikram Narayanan, Tianjiao Huang, David Detweiler, Dan Appel et al.OSDI 2020 · 86 citations
- Tock: From Research To Securing 10 Million ComputersLeon Schuermann, Brad Campbell, Branden Ghena, Philip Alexander Levis et al.SOSP 2025
- SquirrelFS: using the Rust compiler to check file-system crash consistencyHayley LeBlanc, Nathan Taylor, James Bornholt, Vijay ChidambaramOSDI 2024 · 7 citations
- TRust: A Compilation Framework for In-process Isolation to Protect Safe Rust against Untrusted CodeInyoung Bang, Martin Kayondo, Hyungon Moon, Yunheung PaekUSENIX Security 2023
- TickTock: Verified Isolation in a Production Embedded OSVivien Rindisbacher, Evan Johnson, Nico Lehmann, Tyler Potyondy et al.SOSP 2025
