How Google’s KataOS Uses Rust and seL4 to Build a Verified Secure OS

Google announced the launch of KataOS, a secure operating system aimed at embedded devices that run machine‑learning workloads. Prioritising security, KataOS is written almost entirely in Rust and is built on the formally verified seL4 microkernel.

Through the seL4 CAmkES framework we can provide statically defined and analytically verifiable system components. KataOS offers a verifiable secure platform to protect user privacy because applications cannot logically violate the kernel’s hardware security protections, and system components are provably safe. Being almost completely implemented in Rust gives a strong foundation for software security by eliminating whole classes of bugs such as off‑by‑one errors and buffer overflows.

Google has open‑sourced most of KataOS’s core on GitHub, including a Rust framework (e.g., the sel4‑sys crate that provides the seL4 system‑call API), a Rust‑written backup rootserver for dynamic system‑wide memory management, and kernel modifications that reclaim memory used by the rootserver.

Internally, KataOS can dynamically load and run third‑party applications built outside the CAmkES framework, though the necessary components are not yet open‑sourced; Google plans to release them soon. To fully demonstrate a secure environment, Google built a reference implementation called Sparrow, which combines KataOS with a secure hardware platform. Besides the logically secure OS kernel, Sparrow includes a logically secure root of trust built with OpenTitan on RISC‑V, while the initial version targets running a standard 64‑bit ARM platform in QEMU simulation. Google’s goal is to open‑source all of Sparrow, including hardware and software designs; the currently released early version of KataOS is just the beginning.

Google Blog Announcement

Sparrow Manifest Repository