Last Friday, Google announced the release of KataOS, a security-oriented operating system. The new OS focuses on embedded devices running machine learning workloads.
According to Phoronix, it uses the Rust programming language and is "built on the seL4 microkernel that it uses as its base".
From Google's open source blog:
“As the basis for this new operating system, we chose the seL4 microkernel because it focuses on security. It is mathematically proven secure, with guaranteed privacy, integrity and availability. Through the seL4 CAmkES framework, we are also able to provide statically defined and analyzable system components.”
“KataOS provides a verifiably secure platform that protects user privacy because it is logically impossible for applications to breach the kernel's hardware security protections and system components are verifiably secure. KataOS is developed almost entirely with Rust, which provides a strong starting point for software security by eliminating entire classes of bugs, such as off-by-one bugs and buffer overflows.”
The current GitHub release contains most of the core pieces of working KataOS, including the frameworks we use for Rust (such as the sel4-sys crate, which also provides the seL4 syscall APIs), an alternative rootserver written in Rust (required for dynamic system-wide memory management), and kernel modifications to seL4 that can reclaim memory used by the rootserver.
The KataOS code is maintained via GitHub under the umbrella of AmbiML.
