Author: Thom Holwerda
Source
To begin collaborating with others, we’ve open sourced several components for our secure operating system, called KataOS, on GitHub, as well as partnered with Antmicro on their Renode simulator and related frameworks. 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. 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. 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. Another new open source operating system by Google. This time, it seems almost entirely focused on embedded machine learning applications, so it’s definitely a bit outside of my wheel house.