Google ha anunciado el descubrimiento de desarrollos relacionados con el proyecto KataOS, cuyo objetivo es crear un sistema operativo seguro para hardware integrado. Los componentes del sistema KataOS están escritos en Rust y se ejecutan sobre el microkernel seL4, para el cual se ha proporcionado una prueba matemática de confiabilidad en sistemas RISC-V, lo que indica que el código cumple completamente con las especificaciones especificadas en el lenguaje formal. El código del proyecto está abierto bajo la licencia Apache 2.0.
El sistema brinda soporte para plataformas basadas en arquitecturas RISC-V y ARM64. Para simular el funcionamiento de seL4 y el entorno KataOS sobre el hardware, se utiliza el marco Renode durante el proceso de desarrollo. Como implementación de referencia se propone el complejo de software y hardware Sparrow, que combina KataOS con chips seguros basados en la plataforma OpenTitan. La solución propuesta le permite combinar un kernel de sistema operativo verificado lógicamente con componentes de hardware confiables (RoT, Root of Trust), creados utilizando la plataforma OpenTitan y la arquitectura RISC-V. Además del código KataOS, en el futuro está previsto abrir todos los demás componentes de Sparrow, incluido el componente de hardware.
La plataforma se está desarrollando pensando en su aplicación 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 confirmación de la ausencia de fallas. Ejemplos de tales aplicaciones incluyen sistemas que manipulan imágenes de personas y grabaciones de voz. El uso de verificación de confiabilidad por parte de KataOS garantiza que si una parte del sistema falla, la falla no se extenderá al resto del sistema y, en particular, al núcleo y las partes críticas.
La arquitectura seL4 se destaca por mover partes para administrar los recursos del kernel al espacio del usuario y aplicar las mismas herramientas de control de acceso para dichos recursos que para los recursos del usuario. El microkernel no proporciona abstracciones de alto nivel listas para usar para administrar archivos, procesos, conexiones de red y similares; en cambio, proporciona sólo mecanismos mínimos para controlar el acceso al espacio de direcciones físicas, interrupciones y recursos del procesador. Las abstracciones de alto nivel y los controladores para interactuar con el hardware se implementan por separado en la parte superior del microkernel en forma de tareas a nivel de usuario. El acceso de dichas tareas a los recursos disponibles para el microkernel se organiza mediante la definición de reglas.
Para protección adicional, todos los componentes, excepto el microkernel, se desarrollan de forma nativa en Rust utilizando técnicas de programación seguras que minimizan los errores de memoria que provocan problemas como el acceso a la memoria después de la liberación, desreferencias de punteros nulos y desbordamientos del búfer. En Rust se escribieron un cargador de aplicaciones en el entorno seL4, servicios del sistema, un marco para el desarrollo de aplicaciones, una API para acceder a las llamadas del sistema, un administrador de procesos, un mecanismo para la asignación dinámica de memoria, etc. El ensamblaje verificado utiliza el kit de herramientas CAmkES, desarrollado por el proyecto seL4. Los componentes para CAmkES también se pueden crear en Rust.
Rust refuerza la seguridad de la memoria en tiempo de compilación mediante la verificación de referencias, la propiedad de los objetos y el seguimiento de la vida útil de los objetos (alcances), y mediante la evaluación de la exactitud de los accesos a la memoria en tiempo de ejecución. Rust también proporciona protección contra desbordamientos de enteros, requiere que los valores de las variables se inicialicen antes de su uso, utiliza el concepto de referencias y variables inmutables de forma predeterminada y ofrece tipos estáticos sólidos para minimizar los errores lógicos.
Fuente: opennet.ru