Google announced that it open-sourced several components for its secure operating system called KataOS as part of an effort to build verifiably secure systems for embedded hardware.
Google Research aims to solve this problem by providing a secure platform optimized for embedded devices running ML applications.
SeL4 is the microkernel for the project because it prioritizes security and the seL4 CAmkES framework provides statically-defined and analyzable system components.
With KataOS, it’s impossible for applications to breach the kernel’s hardware security protections and the system components are verifiably secure.
The GitHub release includes many of the KataOS core pieces such as the frameworks used for Rust, an alternate rootserver, and kernel modifications to seL4 that can reclaim memory used by the rootserver.
Google stated that currently KataOS can’t run applications built outside of the CAmkES framework, but that it is working on incorporating it in the near future. Also, Google is building a reference implementation for KataOS called Sparrow that combines KataOS with a secured hardware platform.
Google also partnered with Antmicro, a software-driven tech company providing development services, platforms, know-how and guidance to customers, on their Renode simulator and related frameworks.
