Google launches KataOS

Google has announcedthe existence of yet another new operating system, called KataOS, aimed atthe creation of secure embedded systems.

As the foundation for this new operating system, we chose seL4 asthe microkernel because it puts security front and center; it ismathematically proven secure, with guaranteed confidentiality,integrity, and availability. Through the seL4 CAmkES framework,we're also able to provide statically-defined and analyzable systemcomponents. KataOS provides a verifiably-secure platform thatprotects the user's privacy because it is logically impossible forapplications to breach the kernel's hardware security protectionsand the system components are verifiably secure. KataOS is alsoimplemented almost entirely in Rust, which provides a strongstarting point for software security, since it eliminates entireclasses of bugs, such as off-by-one errors and buffer overflows.