Google announces KataOS as a security focused OS, using Rust & seL4 Microkernel

This week, Google announced the release of KataOS as their latest operating system focused on embedded devices running on ambient machine learning. KataOS is security-oriented, uses the Rust programming language exclusively, and is built on the seL4 microkernel as its foundation.

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

“As the foundation for this new operating system, we chose seL4 as a microkernel because it puts security first and center; it is mathematically proven to be secure, with guaranteed confidentiality, integrity and availability. Through the seL4 CAmkES framework, we are also able to provide statically defined and analyzed system components. KataOS provides a verifiably secure platform that protects user privacy because it is logically impossible for applications to break through the kernel’s hardware security protections, and 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 errors, such as point-to-point errors and buffer overflows.

The current GitHub release includes most of the core parts of KataOS, including the frameworks we use for Rust (such as the sel4-sys crate, which provides the seL4 syscall APIs), an alternative root server written in Rust (required for dynamic memory management across system ), and kernel modifications to seL4 that can reclaim memory used by the root server.”

Learn more about this Google effort via their An open source blog. The KataOS code is hosted on GitHub under AmbiML umbrella.