Se ha terminado el trabajo en la verificación formal matemática de la confiabilidad y seguridad del microkernel seL4 en sistemas con arquitectura del conjunto de instrucciones AArch64. La verificación se reduce a una prueba matemática de la corrección del funcionamiento de seL4, lo que indica que cumple completamente con las especificaciones establecidas en un lenguaje formal. La prueba de confiabilidad permite usar seL4 en sistemas críticos basados en procesadores ARM64, que requieren un alto nivel de seguridad y garantizan la ausencia de fallos.
Inicialmente, el microkernel seL4 fue verificado para procesadores ARM de 32 bits, y más tarde para procesadores de 64 bits x86 y RISC-V. La verificación garantiza que en caso de fallo en una parte del sistema, se evitará que este fallo se propague al resto del sistema y a sus partes críticas. En el contexto de la seguridad, la verificación confirma que el núcleo proporciona el nivel adecuado de aislamiento de las aplicaciones, evita que accedan a información sin autorización y asegura que en caso de compromiso de aplicaciones secundarias, el ataque no se propagará a aplicaciones críticas.
La arquitectura del microkernel seL4 es notable por la delegación de partes de la gestión de recursos del núcleo al espacio del usuario y por el uso de los mismos mecanismos de control de acceso para estos recursos que para los recursos de usuario. El microkernel no proporciona abstracciones de alto nivel listas para gestionar archivos, procesos, conexiones de red, etc. En su lugar, ofrece solo 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 interactuar 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 estas tareas a los recursos disponibles en el microkernel se organiza mediante la definición de reglas.
Fuente: opennet.ru
