Google this week released KataOS as their latest operating system, which is geared towards embedded devices running machine learning applications. KataOS is a security-focused operating system that only employs its Rust programming language and is built on top of the seL4 microkernel to form its base.
KataOS is designed to be used with the growing variety of smart devices, focusing on embedded hardware running machine learning programs. With the industry’s increasing focus on RISC-V, this CPU architecture is the central area of support for KataOS. Here’s what Google want’s to say about KataOS:
“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.”