Google has announced the release of its work related to the KataOS project, aimed at creating a secure operating system for embedded devices. The system components of KataOS are written in Rust and run on top of the seL4 microkernel, for which a mathematical proof of reliability has been provided on RISC-V systems, confirming that the code meets the specifications outlined in formal language. The project's code is open under the Apache 2.0 license.
The system supports 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. The Sparrow software-hardware complex is proposed as a reference implementation, combining KataOS with secure chips built on the OpenTitan platform. This solution allows for the integration of a logically verified operating system core with trusted hardware components (RoT, Root of Trust) built using the OpenTitan platform and RISC-V architecture. In addition to the KataOS code, there are plans to open all other components of Sparrow, including the hardware aspect.
The platform is being developed with a focus on use in specialized chips designed for running applications for machine learning and processing sensitive information, which require a special level of protection and confirmation of faultlessness. Examples of such applications include systems that manipulate images of people and voice recordings. The implementation of reliability verification in KataOS ensures that if a failure occurs in one part of the system, this failure will not propagate to the rest of the system and, in particular, to the core and critical parts.
The architecture of seL4 is noteworthy for transferring parts of core resource management into user space and applying the same access control mechanisms for these resources as for user resources. The microkernel does not provide ready-to-use high-level abstractions for managing files, processes, network connections, etc.; instead, it merely offers minimal mechanisms for managing access to physical address space, interrupts, and CPU resources. High-level abstractions and drivers for hardware interaction are implemented separately on top of the microkernel in the form of user-level tasks. Access of these tasks to the resources available to the microkernel is organized through defining rules.
For added security, all components except the microkernel are initially developed in Rust using safe programming practices that minimize memory-related errors, which can lead to issues such as accessing memory areas after they have been freed, dereferencing null pointers, and buffer overflows. The application loader in the seL4 environment, system services, framework for application development, API for accessing system calls, process manager, dynamic memory allocation mechanism, etc., are all written in Rust. The CAmkES toolkit, developed by the seL4 project, is used for verified builds. Components for CAmkES can also be created in Rust.
Safe memory operations in Rust are ensured at compile time through reference checks, ownership tracking of objects, and consideration of object lifetimes (scope), as well as through the evaluation of the correctness of memory access during code execution. Rust also provides means to protect against integer overflows, requires mandatory initialization of variable values before use, applies the concept of immutability (immutable) for references and variables by default, and offers strong static typing to minimize logical errors.
Source: opennet.ru
