KataOS, un sistema operativo orientado a la seguridad de hardware embebido.

Se dio a conocer la noticia de que Google anunció la liberación del código fuente de los desarrollos relacionados con el proyecto KataOS, cuyo objetivo es crear un sistema operativo seguro para hardware embebido.

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 durante el desarrollo, se utiliza el marco Renode.

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 hace posible combinar un kernel de sistema operativo verificado lógicamente con componentes de hardware confiables (RoT, Root of Trust) construidos utilizando la plataforma OpenTitan y la arquitectura RISC-V.

Además del código de KataOS, está previsto abrir todos los demás componentes de Sparrow, incluido el componente de hardware, en el futuro.

Como base para este nuevo sistema operativo, elegimos seL4 como el microkernel porque pone la seguridad al frente y al centro; está matemáticamente probado como seguro, con confidencialidad, integridad y disponibilidad garantizadas. A través del marco seL4 CAmkES, también podemos proporcionar componentes del sistema analizables y definidos estáticamente. KataOS proporciona una plataforma segura verificable que protege la privacidad del usuario porque es lógicamente imposible que las aplicaciones violen las protecciones de seguridad del hardware del kernel y los componentes del sistema son seguros verificables.

La plataforma se está desarrollando teniendo en cuenta los chips especialmente diseñados para ejecutar aplicaciones de privacidad y aprendizaje automático que requieren un nivel específico de protección y garantía de que no hay fallas. Los sistemas que manipulan imágenes de personas y grabaciones de voz se dan como ejemplo de dichas aplicaciones. El uso de la verificación de confiabilidad en KataOS garantiza que, en caso de falla en una parte del sistema, esta falla no se extienda al resto del sistema y, en particular, al kernel y las partes críticas.

La arquitectura seL4 se destaca por mover partes para administrar los recursos del kernel en el espacio del usuario y aplicar los mismos controles 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, sino que solo proporciona mecanismos mínimos para controlar el acceso al espacio de direcciones físicas, las interrupciones y los 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 tales tareas a los recursos disponibles para el microkernel se organiza a través de la definición de reglas.

Para una protección adicional, todos los componentes, excepto el microkernel, se desarrollan inicialmente en Rust utilizando técnicas de programación seguras que minimizan los errores cuando se trabaja con la memoria, lo que genera problemas como el acceso a un área de la memoria después de liberarla, la desreferenciación de punteros nulos y el desbordamiento del búfer.

El cargador de aplicaciones en el entorno seL4, los servicios del sistema, un marco de desarrollo de aplicaciones, una API para acceder a las llamadas del sistema, un administrador de procesos, un mecanismo de asignación de memoria dinámica, etc. están escritos en Rust. Para el montaje verificado se utiliza el toolkit CAmkES desarrollado por el proyecto seL4. Los componentes para CAmkES también se pueden crear en Rust.

La seguridad de la memoria se proporciona en Rust en tiempo de compilación mediante la verificación de referencias, el seguimiento de la propiedad del objeto y la vida útil del objeto (alcance), 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 brinda protección contra desbordamientos de enteros, requiere que las variables se inicialicen antes de su uso, aplica el concepto de referencias y variables inmutables de forma predeterminada y ofrece tipado estático fuerte para minimizar los errores lógicos.

Finalmente para los interesados, deben saber que los componentes del sistema KataOS están escritos en Rust y se ejecutan sobre el microkernel seL4, para el cual se proporciona una prueba matemática de confiabilidad en los 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, puedes consultar más detalles al respecto en el siguiente enlace.