"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," explains Google's open-source team, which is building intelligent ambient machine-learning (AmbiML) systems.
The project's GitHub page emphasizes that KataOS and its umbrella project name, Sparrow, "are definitely a work in progress". Sparrow is a reference implementation of KataOS.
"Our team in Google Research has set out to solve this problem by building a provably secure platform that's optimized for embedded devices that run ML applications. This is an ongoing project with plenty left to do, but we're excited to share some early details and invite others to collaborate on the platform so we can all build intelligent ambient systems that have security built-in by default," Google said.
The OS is not for desktops or smartphones but the Internet of Things, possibly for smart homes.
The goal is to build verifiably secure systems for embedded hardware or edge devices like network-connected cameras used to capture images that are processed on-device or in the cloud for machine learning.
"If the devices around us can't be mathematically proven to keep data secure, then the personally-identifiable data they collect – such as images of people and recordings of their voices – could be accessible to malicious software," note the AmbiML team, who adds that security is often tacked on at the end.
The OS is being built with the new sel4 "security-first" microkernel. It's open source but is not based on Linux and has no relation to Google's Fuchsia OS.
Data61, the digital arm of Australia's research agency CSIRO, announced sel4 in 2020 as a mathematically proven correct, bug-free kernel. The Linux Foundation hosts the selL4 Foundation.
"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," Google explains.
"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."
While it is an early-stage project, the GitHub repository features Rust-based sel4-sys Crate add-ons, which provide seL4 syscall application programming interfaces. It's also got a rootserver written in Rust – for dynamic system-wide memory management – and customizations to seL4 to reclaim memory used by the rootserver. It also enabled debugging.
The aim is to support RISC-V architecture chips, which are receiving early interest from NASA, Intel and others.
"Sparrow includes a logically-secure root of trust built with OpenTitan on a RISC-V architecture. However, for our initial release, we're targeting a more standard 64-bit ARM platform running in simulation with QEMU," Google notes.
What happens to KataOS remains to be seen. Google launched its Fuchsia OS a few years ago and it too was aimed for the IoT. It was running on Made by Google devices like the Nest Hub but, as 9to5Google notes, the latest developments in Fuchsia suggest Google wants to expand it from smarthome devices to a more general-purpose OS.