La empresa Google ha presentado el sistema hardware y software Open Se Cura, diseñado para simplificar la creación de chipsets seguros destinados a resolver tareas relacionadas con el aprendizaje automático y la inteligencia artificial. El proyecto incluye un sistema operativo llamado CantripOS y hardware basado en la plataforma OpenTitan y un núcleo de procesador basado en la arquitectura RISC-V. Durante el desarrollo, Open Se Cura y CantripOS fueron conocidos como Sparrow y KataOS, pero para evitar confusiones con otros proyectos, los productos finales fueron renombrados. Los avances del proyecto, incluidos los códigos fuente de los servicios del sistema y los esquemas RTL (Register Transfer Level), se distribuyen bajo la licencia Apache 2.0.
El sistema operativo CantripOS se basa en el microkernel seL4, sobre el cual se ejecuta un entorno de sistema escrito en Rust. En sistemas RISC-V, para el microkernel seL4 se ha proporcionado una prueba matemática de fiabilidad, que demuestra la plena conformidad del código con las especificaciones establecidas en un lenguaje formal. La arquitectura seL4 es notable por la separación de partes para la gestión de recursos del núcleo en el espacio de usuario y la aplicación de los mismos mecanismos de control de acceso a esos recursos que para los recursos de usuario.
El microkernel no proporciona abstracciones de alto nivel listas para la gestión de archivos, procesos, conexiones de red, etc.; en su lugar, solo ofrece mecanismos mínimos para gestionar el acceso al espacio de direcciones físicas, interrupciones y recursos del procesador. Las abstracciones de alto nivel y los controladores para la interacción con el hardware se implementan por separado sobre el microkernel en forma de tareas que se ejecutan en el nivel de usuario. El acceso de tales tareas a los recursos del microkernel se organiza mediante la definición de reglas.
Todos los componentes del sistema operativo, excepto el microkernel, se han escrito inicialmente en Rust utilizando técnicas de programación seguras que minimizan los errores en el manejo de la memoria. En Rust, entre otras cosas, se escribieron el cargador de aplicaciones en el entorno seL4, los servicios del sistema, un marco para el desarrollo de aplicaciones, una API para acceder a las llamadas del sistema, un gestor de procesos y un mecanismo de distribución dinámica de memoria.
Para la construcción verificada se ha utilizado la herramienta CAmkES, desarrollada por el proyecto seL4. Para el desarrollo de aplicaciones finales que puedan ser cargadas dinámicamente por los servicios del sistema, se recomienda utilizar el SDK AmbiML, y para ejecutar modelos de aprendizaje automático, la herramienta IREE (Entorno de Ejecución de Representación Intermedia). Los componentes en Rust y los servicios del sistema se han desarrollado utilizando los marcos de Cantrip.
Entre las áreas de aplicación de la plataforma se mencionan los chips especializados que requieren un nivel particular de protección y confirmación de la ausencia de fallos. Por ejemplo, la plataforma puede aplicarse en productos de aprendizaje automático relacionados con el procesamiento de información confidencial, como sistemas de reconocimiento facial y procesamiento de grabaciones de voz. La combinación de un núcleo del sistema operativo lógicamente verificado con componentes de hardware confiables (RoT, Root of Trust) garantiza que en caso de un fallo en una parte del sistema, dicho fallo no se propagará al resto del sistema y, en particular, al núcleo y a las partes críticas.
Además de Google, en el desarrollo de la herramienta y los elementos de infraestructura participaron la organización sin fines de lucro lowRISC, que supervisa el desarrollo de un microprocesador libre basado en la arquitectura RISC-V, así como las empresas Antmicro y VeriSilicon. El procesador desarrollado por la organización lowRISC se utilizó como núcleo para construir componentes de hardware confiables (RoT, Root of Trust). La empresa Antmicro proporcionó al proyecto el simulador Renode, que permite probar CantripOS y el microkernel seL4 sin hardware real. La empresa VeriSilicon compartió su experiencia en la creación de chips y el desarrollo de BSP (Paquete de Soporte de Placa).
Fuente: opennet.ru
