Google announced the discovery of developments related to the KataOS project, aimed at creating a secure operating system for embedded hardware. KataOS system components are written in Rust and run on top of the seL4 microkernel, for which a mathematical proof of reliability is provided on RISC-V systems, indicating full compliance of the code with the specifications specified in the formal language. The project code is open under the Apache 2.0 license.
The system provides support for platforms based on RISC-V and ARM64 architectures. To simulate the operation of seL4 and the KataOS environment on top of the hardware, the Renode framework is used during development. As a reference implementation, the Sparrow hardware and software system is proposed, which combines KataOS with secure chips based on the OpenTitan platform. The proposed solution makes it possible to combine a logically verified operating system kernel with trustworthy hardware components (RoT, Root of Trust) built using the OpenTitan platform and the RISC-V architecture. In addition to the KataOS code, it is planned to open all other components of Sparrow, including the hardware component, in the future.
The platform is being developed with an eye on purpose-built chips designed to run machine learning and privacy applications that require a specific level of protection and assurance 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 verification 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 seL4 architecture is notable for moving parts for managing kernel resources into user space and applying the same access controls for such resources as for user resources. The microkernel does not provide out-of-the-box high-level abstractions for managing files, processes, network connections, and the like, instead it provides only minimal mechanisms for controlling access to the physical address space, interrupts, and processor resources. High-level abstractions and drivers for interacting with 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 additional 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 a memory area after it is freed, dereferencing null pointers, and buffer overruns. The application loader in the seL4 environment, system services, an application development framework, an API for accessing system calls, a process manager, a dynamic memory allocation mechanism, etc. 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 through reference checking, keeping track of object ownership and object lifetime (scope), as well as through evaluation of the correctness of memory access during code execution. Rust also provides protection against integer overflows, requires variables to be initialized before use, applies the concept of immutable references and variables by default, and offers strong static typing to minimize logical errors.
Source: opennet.ru