La Fundación RISC-V anunció que ha verificado el funcionamiento del microkernel seL4 en sistemas con la arquitectura del conjunto de instrucciones RISC-V. En la cual el proceso de verificación se reduce a la prueba matemática de la fiabilidad de seL4, lo que indica el pleno cumplimiento de las especificaciones especificadas en un lenguaje formal.

La prueba de confiabilidad permite usar seL4 en sistemas de misión crítica basados ​​en procesadores RISC-V RV64, lo que requiere un mayor nivel de confiabilidad y no garantiza fallas.

Los desarrolladores de software que se ejecutan en la parte superior del núcleo seL4 pueden estar completamente seguros de que, en caso de una falla en una parte del sistema, esta falla no se extenderá al resto del sistema y, en particular, a sus partes críticas.

Sobre seL4

La arquitectura seL4 es notable por la eliminación de partes para administrar los recursos del kernel en el espacio del usuario y usar los mismos métodos de control de acceso para tales recursos como para los recursos del usuario.

El microkernel no proporciona abstracciones de alto nivel ya preparadas para administrar archivos, procesos, conexiones de red, etc., 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 equipo se implementan por separado en la parte superior del microkernel en forma de tareas realizadas a nivel de usuario.

El acceso de tales tareas a los recursos disponibles en el microkernel se organiza a través de la definición de reglas.

RISC-V proporciona un sistema abierto y flexible de instrucciones de máquina que permite crear microprocesadores para aplicaciones arbitrarias, sin requerir deducciones y sin imponer condiciones de uso.

RISC-V  permite crear SoCs y procesadores completamente abiertos. Actualmente, sobre la base de la especificación RISC-V, varias compañías y comunidades bajo varias licencias gratuitas (BSD, MIT, Apache 2.0) están desarrollando varias docenas de variantes de núcleos de microprocesador, SoC y chips ya producidos.

El soporte RISC-V ha estado presente desde el lanzamiento de Glibc 2.27, binutils 2.30, gcc 7 y el kernel Linux 4.15.

Sobre la pruebas del microkernel seL4

Inicialmente, el microkernel seL4 fue verificado para procesadores ARM de 32 bits, y más tarde para procesadores x86 de 64 bits.

Se observa que la combinación de la arquitectura de hardware abierto RISC-V con el microkernel abierto seL4 logrará un nuevo nivel de seguridad, ya que los componentes de hardware en el futuro también pueden verificarse completamente, lo que es imposible de lograr para las arquitecturas de hardware patentadas.

Cuando verificamos seL4, debemos suponer que el hardware funciona correctamente (es decir, como se especifica). Eso supone que hay una especificación inequívoca en primer lugar, que no es el caso para todo el hardware. 

Pero incluso cuando existe tal especificación, y es formal (es decir, ritten en un formalismo matemático que admite el razonamiento matemático sobre sus propiedades), ¿cómo sabemos que realmente captura el comportamiento del hardware? 

La realidad es que podemos estar bastante seguros de que no es así. El hardware no es diferente del software en que ambos tienen errores.

Pero tener un ISA abierto tiene ventajas que van más allá de estar libres de regalías. Una es que permite tener implementaciones de hardware de código abierto.

Al verificar seL4, se supone que el equipo funciona como se indica y la especificación describe completamente el comportamiento del sistema, pero de hecho el equipo no está libre de errores, lo cual está bien demostrado por problemas que surgen regularmente en el mecanismo de ejecución especulativa de instrucciones.

Las plataformas de hardware abiertas simplifican la integración de los cambios relacionados con la seguridad, por ejemplo, para bloquear todos los canales de fuga posibles a través de canales de terceros, en los que es mucho más eficiente deshacerse de un problema por hardware que tratar de encontrar soluciones por software.

Finalmente, si quieres conocer mas al respecto, puedes consultar la nota en el siguiente enlace.