Post Syndicated from original https://lwn.net/Articles/911332/

Google has announced
the existence of yet another new operating system, called KataOS, aimed at
the creation of secure embedded systems.

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.