Google has introduced the Open Se Cura software-hardware complex aimed at simplifying the creation of secure chips designed to tackle challenges related to machine learning and artificial intelligence. The project includes the CantripOS operating system and hardware based on the OpenTitan platform and a processor core built on the RISC-V architecture. During the development of Open Se Cura and CantripOS, they were initially known as Sparrow and KataOS, but to avoid overlap with other projects, the final products were renamed. The project's developments, including the source code of system services and RTL (Register Transfer Level) schematics, are distributed under the Apache 2.0 license.
The CantripOS operating system is based on the seL4 microkernel, on top of which a system environment is executed, written in Rust. A mathematical proof of reliability has been provided for the seL4 microkernel on RISC-V systems, demonstrating full compliance of the code with the specifications defined in a formal language. The seL4 architecture is notable for relocating components for managing core resources into user space and applying the same access control mechanisms for those resources as for user resources.
The microkernel does not provide ready-made high-level abstractions for managing files, processes, network connections, etc.; instead, it only offers minimal mechanisms for controlling access to 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 tasks executed at the user level. Access of these tasks to the resources available to the microkernel is organized through the definition of rules.
All components of the OS, except for the microkernel, are originally written in Rust using safe programming practices that minimize errors related to memory handling. In Rust, among other things, the application loader in the seL4 environment, system services, a framework for application development, an API for accessing system calls, a process manager, and a dynamic memory allocation mechanism are written.
For the verified build, the CAmkES toolkit developed by the seL4 project is used. To create end applications that can be dynamically loaded by system services, it is recommended to utilize the AmbiML SDK, and for executing machine learning models, the IREE (Intermediate Representation Execution Environment) toolkit should be employed. Components written in Rust and system services have been developed using the Cantrip framework.
The platform is applicable in specialized chip areas where a special level of protection and confirmed failure absence is required. For example, it can be utilized in machine learning products that process sensitive information, such as facial recognition systems and voice recording processing. The combination of a logically verified operating system kernel with trusted hardware components (RoT, Root of Trust) ensures that if one part of the system fails, that failure will not propagate to the rest of the system, particularly to the kernel and critical components.
In addition to Google, the development of tools and infrastructure elements has involved the nonprofit organization lowRISC, which oversees the development of an open microprocessor based on RISC-V architecture, along with companies Antmicro and VeriSilicon. The processor developed by lowRISC has been used as the core for building trusted hardware components (RoT, Root of Trust). Antmicro provided the project with the Renode simulator, enabling testing of CantripOS and the seL4 microkernel without physical hardware. VeriSilicon shared its expertise in chip creation and the development of BSP (Board Support Package).
Source: opennet.ru
