Google Announces KataOS As Security-Focused OS, Leveraging Rust & seL4 Microkernel

Google this week has announced the release of KataOS as their newest operating system effort focused on embedded devices running ambient machine learning workloads. KataOS is security-minded, exclusively uses the Rust programming language, and is built atop the seL4 microkernel as its foundation.

KataOS is intended for use with the ever-growing number of smart devices with a particular emphasis on embedded hardware running machine learning applications. Given the increasing industry focus of RISC-V, that CPU architecture is a primary support focus for KataOS. Google's Open-Source Blog announced:

"As the foundation for this new operating system, we chose seL4 as the microkernel because it puts security front and center; it is mathematically proven secure, with guaranteed confidentiality, integrity, and availability. Through the seL4 CAmkES framework, we're also able to provide statically-defined and analyzable system components. KataOS provides a verifiably-secure platform that protects the user's privacy because it is logically impossible for applications to breach the kernel's hardware security protections and the system components are verifiably secure. KataOS is also implemented almost entirely in Rust, which provides a strong starting point for software security, since it eliminates entire classes of bugs, such as off-by-one errors and buffer overflows.

The current GitHub release includes most of the KataOS core pieces, including the frameworks we use for Rust (such as the sel4-sys crate, which provides seL4 syscall APIs), an alternate rootserver written in Rust (needed for dynamic system-wide memory management), and the kernel modifications to seL4 that can reclaim the memory used by the rootserver."

Learn more about this Google effort via their Open-Source Blog. KataOS code is being worked on via GitHub under the AmbiML umbrella.