La empresa Google ha anunciado la apertura de los desarrollos relacionados con el proyecto KataOS, destinado a crear un sistema operativo seguro para equipos embebidos. Los componentes del sistema KataOS están escritos en el lenguaje Rust y se ejecutan sobre el microkernel seL4, para el cual en sistemas RISC-V se ha proporcionado una prueba matemática de fiabilidad, que demuestra la completa conformidad del código con las especificaciones dadas en el lenguaje formal. El código del proyecto está abierto bajo la licencia Apache 2.0.
El sistema asegura soporte para plataformas basadas en arquitecturas RISC-V y ARM64. Para simular el funcionamiento de seL4 y el entorno de KataOS sobre el hardware, durante el desarrollo se utiliza el marco Renode. Como implementación de referencia, se propone un complejo de hardware y software llamado Sparrow, que combina KataOS con chips seguros basados en la plataforma OpenTitan. La solución propuesta permite combinar un núcleo del sistema operativo lógicamente verificado con componentes de hardware de confianza (RoT, Root of Trust), construidos utilizando la plataforma OpenTitan y la arquitectura RISC-V. Además del código de KataOS, se planea abrir en el futuro todos los demás componentes de Sparrow, incluyendo la parte de hardware.
La plataforma se desarrolla con miras a su uso en chips especializados, diseñados para ejecutar aplicaciones de aprendizaje automático y procesamiento de información confidencial, que requieren un nivel especial de protección y verificación de la ausencia de fallos. Como ejemplo de tales aplicaciones, se citan sistemas que manipulan imágenes de personas y grabaciones de voz. El uso de la verificación de fiabilidad en KataOS garantiza que, en caso de falla en una parte del sistema, esta falla no se propagará al resto del sistema y, en particular, al núcleo y las partes críticas.
La arquitectura de seL4 destaca por la separación de partes para la gestión de recursos del núcleo en el espacio de usuario, utilizando los mismos mecanismos de control de acceso que para los recursos de usuario. El microkernel no proporciona abstracciones de alto nivel predefinidas para la gestión de archivos, procesos, conexiones de red, etc., sino que solo ofrece mecanismos mínimos para gestionar el acceso al espacio de direcciones físicas, interrupciones y recursos de la CPU. 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 a nivel de usuario. El acceso de estas tareas a los recursos del microkernel se organiza a través de la definición de reglas.
Para una mayor protección, todos los componentes, excepto el microkernel, se desarrollan inicialmente en el lenguaje Rust utilizando prácticas de programación seguras que minimizan los errores relacionados con la memoria, como el acceso a áreas de memoria después de que han sido liberadas, la desreferenciación de punteros nulos y los desbordamientos de búfer. En Rust se han escrito, entre otras cosas, el cargador de aplicaciones en el entorno de seL4, servicios del sistema, un marco para el desarrollo de aplicaciones, una API para acceder a llamadas del sistema, un gestor de procesos y un mecanismo de distribución dinámica de memoria. Para una construcción verificada se utiliza la herramienta CAmkES, desarrollada por el proyecto seL4. Los componentes para CAmkES también pueden ser creados en el lenguaje Rust.
La gestión segura de la memoria en Rust se garantiza durante la compilación mediante la verificación de referencias, el seguimiento de la propiedad de los objetos y la consideración de la duración de vida de los objetos (área de visibilidad), así como mediante la evaluación de la corrección del acceso a la memoria durante la ejecución del código. Rust también proporciona herramientas para proteger contra desbordamientos enteros, requiere la inicialización obligatoria de los valores de las variables antes de su uso, aplica el concepto de inmutabilidad (immutable) de referencias y variables por defecto, y ofrece una fuerte tipificación estática para minimizar errores lógicos.
Fuente: opennet.ru
