KataOS, an embedded hardware security-oriented operating system.
The news was released that Google announced the release of the source code of developments related to the project Kata OS, whose goal is to create a secure operating system for embedded hardware.
The system provides support for platforms based on RISC-V and ARM64 architectures. To simulate the operation of seL4 and the KataOS environment on hardware during development, the Renode framework is used.
As a reference implementation, the Sparrow software and hardware complex is proposed, which combines KataOS with secure chips based on the OpenTitan platform. The proposed solution hIt is possible to combine a kernel logically verified operating system with Root of Trust (RoT) hardware components built using the OpenTitan platform and the RISC-V architecture.
In addition to the KataOS code, it is planned to open up all other Sparrow components, including the hardware component, in the future.
As the basis for this new operating system, we chose seL4 as the microkernel because it puts security front and center; it is mathematically proven to be secure, with guaranteed confidentiality, integrity, and availability. Through the seL4 CAmkES framework, we can also provide statically defined and parsable system components. KataOS provides a verifiable secure platform that protects user privacy because it is logically impossible for applications to violate kernel hardware security protections and verifiable secure system components.
The platform is being developed with chips in mind especially designed to run privacy and machine learning applications that require a specific level of protection and guarantee that there are no failures. Systems that manipulate images of people and voice recordings are given as an example of such applications. The use of reliability checking in KataOS ensures that in the event of a failure in one part of the system, this failure does not spread to the rest of the system and in particular to the kernel and critical parts.
The architecture seL4 excels at moving parts to manage kernel resources in user space and apply the same access controls for those resources as for user resources.
The microkernel does not provide high-level abstractions out-of-the-box to manage files, processes, network connections, and the like, but only provides minimal mechanisms for controlling access to physical address space, interrupts, and processor resources. High-level abstractions and drivers to interact with the hardware are implemented separately on top of the microkernel in the form of user-level tasks. The access of such tasks to the resources available to the microkernel is organized through the definition of rules.
For extra protection, all components except the microkernel are initially developed in Rust using safe programming techniques that minimize errors when working with memory, leading to problems such as accessing an area of memory after freeing it, dereferencing null pointers, and buffer overflow.
The application loader in the seL4 environment, system services, an application development framework, an API to access system calls, a process manager, a dynamic memory allocation mechanism, etc. they are written in Rust. For the verified assembly, the CAmkES toolkit developed by the seL4 project is used. Components for CAmkES can also be created in Rust.
Memory safety is provided in Rust at compile time by checking references, tracking object ownership, and object lifetime (scope), as well as by evaluating the correctness of memory access during code execution. Rust also provides integer overflow protection, requires variables to be initialized before use, enforces the concept of immutable variables and references by default, and provides strong static typing to minimize logic errors.
Finally for those interested, you should know that the components of the KataOS system are written in Rust and run on the seL4 microkernel, for which a mathematical proof of reliability in RISC-V systems is provided, indicating that the code fully complies with the specifications specified in the formal language.
The project code is open under the Apache 2.0 license, you can consult more details about it in the following link