Fundación RISC-V sobre verificar el funcionamiento del microkernel en sistemas con arquitectura de conjunto de instrucciones RISC-V. La verificación se reduce a confiabilidad del funcionamiento de seL4, lo que indica el pleno cumplimiento de las especificaciones especificadas en el lenguaje formal. Prueba de confiabilidad seL4 en sistemas de misión crítica basados en procesadores RISC-V RV64 que requieren un mayor nivel de confiabilidad y garantizar la ausencia de fallas. Los desarrolladores de software que se ejecutan sobre el kernel seL4 pueden estar completamente seguros de que si hay una falla en una parte del sistema, esta falla no se extenderá al resto del sistema y, en particular, a sus partes críticas.
El microkernel seL4 se verificó inicialmente para procesadores ARM de 32 bits y luego para procesadores x64 de 86 bits. Cabe señalar que la combinación de la arquitectura de hardware abierta RISC-V con el microkernel abierto seL4 logrará un nuevo nivel de seguridad, ya que los componentes de hardware también podrán verificarse completamente en el futuro, lo que es imposible de lograr para arquitecturas de hardware propietarias.
Al verificar seL4, se supone que el equipo funciona como se indica y la especificación describe completamente el comportamiento del sistema, pero en realidad el equipo no está libre de errores, lo que se demuestra claramente por los problemas que surgen periódicamente 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 todas las posibles fugas de canales laterales, donde es mucho más eficiente deshacerse del problema en el hardware que tratar de encontrar soluciones en el software.
Recordemos que la arquitectura seL4 mover partes para administrar los recursos del kernel en el espacio del usuario y aplicar los mismos medios 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.
RISC-V proporciona un sistema de instrucción de máquina abierto y flexible que permite construir microprocesadores para aplicaciones arbitrarias sin requerir regalías ni condiciones para su uso. RISC-V le permite crear procesadores y SoC completamente abiertos. Actualmente basado en la especificación RISC-V por diferentes empresas y comunidades bajo diversas licencias libres (BSD, MIT, Apache 2.0) varias docenas de variantes de núcleos de microprocesadores, SoC y chips ya producidos. La compatibilidad con RISC-V ha estado presente desde los lanzamientos de Glibc 2.27, binutils 2.30, gcc 7 y el kernel de Linux 4.15.
Fuente: opennet.ru