La organización RISC-V Foundation sobre la verificación del funcionamiento del microkernel en sistemas con arquitectura de conjunto de instrucciones RISC-V. La verificación consiste en de la fiabilidad del funcionamiento de seL4, que demuestra la conformidad total con las especificaciones formales establecidas. La prueba de fiabilidad seL4 en sistemas críticos basados en procesadores RISC-V RV64, que requieren un alto nivel de fiabilidad y garantizan la ausencia de fallos. Los desarrolladores de software que opera sobre el núcleo seL4 pueden estar completamente seguros de que, en caso de fallo en una parte del sistema, este fallo no se propagará al resto del sistema y, en particular, a sus partes críticas.
Originalmente, el microkernel seL4 fue verificado para procesadores ARM de 32 bits, y posteriormente para procesadores x86 de 64 bits. Se destaca que la combinación de la arquitectura de hardware abierto RISC-V con el microkernel abierto seL4 permitirá alcanzar un nuevo nivel de seguridad, ya que los componentes de hardware también pueden ser completamente verificados en el futuro, algo que no es posible lograr con arquitecturas de hardware propietarias.
Durante la verificación de seL4 se supone que el hardware funciona como se declara y que la especificación describe completamente el comportamiento del sistema, pero en realidad el hardware no está exento de errores, lo que se demuestra bien con los problemas recurrentes en el mecanismo de ejecución especulativa de instrucciones. Las plataformas de hardware abiertas facilitan la integración de cambios relacionados con la seguridad; por ejemplo, para bloquear todos los posibles canales de fuga a través de canales secundarios, es mucho más eficaz resolver el problema a nivel de hardware que tratar de encontrar soluciones a nivel de software.
Recordemos que la arquitectura seL4 la extracción de partes para la gestión de recursos del núcleo en el espacio del usuario y la aplicación de los mismos medios de control de acceso para estos recursos, como para los recursos del usuario. El micronúcleo no proporciona abstracciones de alto nivel listas para la gestión de archivos, procesos, conexiones de red, etc. En su lugar, proporciona 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 la interacción con el hardware se implementan por separado sobre el micronúcleo en forma de tareas que se ejecutan en el nivel del usuario. El acceso de estas tareas a los recursos del micronúcleo se organiza mediante la definición de reglas.
RISC-V proporciona un sistema de instrucciones de máquina abierto y flexible, que permite crear microprocesadores para diversas áreas de aplicación, sin requerir tasas de licencia ni imponer condiciones sobre su uso. RISC-V permite la creación de SoC y procesadores completamente abiertos. Actualmente, sobre la base de la especificación RISC-V, diferentes empresas y comunidades están desarrollando varias licencias libres (BSD, MIT, Apache 2.0) decenas de variantes de núcleos de microprocesadores, SoC y chips ya producidos. El soporte para RISC-V está presente desde las versiones Glibc 2.27, binutils 2.30, gcc 7 y el núcleo de Linux 4.15.
Fuente: opennet.ru
