The goal is to create verifiable secure systems for embedded hardware or peripheral devices
Google recently released via a blog post to KataOS, an operating system focused on embedded devices running machine learning workloads. KataOS is designed to be focused on security, since it uses the Rust programming language and is based on the seL4 microkernel as a base.
KataOS is designed for use with the ever-increasing number of connected devices, with a particular focus on embedded hardware that runs machine learning applications. Given the growing industrial focus of RISC-V, this processor architecture is a primary support focus for KataOS.
About KataOS
Google presented its operating system KataOS, still in development, whose objective is to provide a security system for embedded devices.
He mentions that it was born from an observation, due to the need to work on a project of this type, «more and more connected devices are being marketed that collect and process environmental information«. Nevertheless, According to Google, these devices are more susceptible to security problems. The company points out, for example, that the data these devices collect can be vulnerable to external attackers. This means that viruses can steal photos, audio recordings, and other data.
To start collaborating with others, we've open sourced several components for our secure operating system, called KataOS, on GitHub, as well as partnerships with Antmicro on their Renode simulator and related frameworks. As the basis for this new operating system, we have chosen seL4 as the microkernel because it prioritizes security; it is mathematically proven to be secure, with guaranteed confidentiality, integrity, and availability.
For Google, a simple solution to deal with this would be a verifiable secure system for onboard hardware. Because ? System security is often treated as a software feature that can be added to existing systems or solved with an additional piece of ASIC hardware, which is usually not enough. It is in this context that KataOS was born.
Google is also collaborating with Antmicro. The asociación will emulate and debug GDB on target devices using Renode. Internally, KataOS has the ability to dynamically load and run third party programs. Even programs created outside of the CAmkES framework can run there. The components required to run these applications are not yet present in the Github source. However, Google intends to make these operations available soon.
Thanks to the seL4 CAmkES framework, we can also provide statically defined and parsable system components. KataOS provides a verifiably secure platform that protects user privacy because it is logically impossible for applications to violate kernel hardware security protections and system components are verifiably secure. KataOS is also almost entirely implemented in Rust, which provides a solid starting point for software security by eliminating entire classes of bugs, such as single errors and buffer overflows.
Google has also created a reference implementation for KataOS called Sparrow. Sparrow's reason is to fully expose the safe environment system.
Use KataOS with a secure hardware platform, as sparrow includes a clearly secure root of trust built with OpenTitan on the RISC-V architecture. This adds to the core of the secure operating system. However, for the initial release of KataOS, Google aims to use QEMU emulation. You will use this emulation to run the more standard 64-bit ARM system.
Finally For those interested, they should know that the project is housed in GitHub and currently the repository includes most major parts of KataOS, including the frameworks we use for Rust (such as sel4-sys, which provides the seL4 system call APIs), an alternate root server written in Rust (needed for system-wide dynamic memory management), and the kernel modifications to seL4 that can reclaim memory used by the root server.
You can visit the project repository at the following link.