El microkernel seL4 ha sido verificado formalmente para procesadores RISC-V [ENG]

El kernel de un sistema operativo es el software que funciona a más bajo nivel en un ordenador. Es el código que funciona en modo privilegiado (S-Mode en RISC-V), por lo que es el responsable principal y único de la seguridad del sistema. Que un kernel, en este caso seL4, esté formalmente verificado significa que su implementación en C es funcionalmente correcta, ya que ha sido matemáticamente verificada mediante software probando que está libre de errores.

[#2 Desactivado]

No sólo eso sino que además han modificado un núcleo RISC-V añadiéndole una instrucción (fence.t) que permite a seL4 bloquear cualquier tipo de ataque que utilice información de latencias. Esa instrucción permite al SO borrar el estado del procesador guardado en los componentes seleccionados. Es decir, un co-diseño software-hardware que da como resultado un sistema 100% seguro. Eso sí, con un coste en rendimiento nada despreciable.

Tal vez se pudiera combinar con un circuito que añada interferencias, impidiendo la detección de esa variación de tiempos que permite descubrir vectores de ataque sin necesidad de hacer flushes del pipeline, BHT, etc. https://www.tomshardware.com/news/georgia-tech-intel-circuit-mitigate-side-channel-attacks,38875.html

[#3 Desactivado]

#2 Uops, he patinado un poco. Son 320 ciclos. En un procesador de 4 GHz, 320 ciclos es insignificante. Aunque ellos hablan de insignificante para un circuito de cambio de partición (context switch) funcionando a 1 KHz, un 30%
No comprendo su concepto de «insignificante».

[#5 Desactivado]

#3
https://www.quora.com/How-long-does-a-context-switch-take
Un P4 con su pipeline super largo tarda 1348 ciclos según esa web. Así que sí, 320 ciclos es poco en comparación. Pero un Pentium 2 lo hace en 227 ciclos, así que este RISC-V de ejecución en orden tarda más pese a tener menos estado (no SIMD, no ROB, etc).

Bueh. No sé. Necesita más de los que emplearía sin necesidad de hacer todo eso. Pero tampoco supone un sobrecoste enorme como sí ocurre con las soluciones actuales basadas en software, como ésta:

[#1 mr_b]

Relacionada: seL4, el primer sistema operativo que demuestra matemáticamente su seguridad.

[#4 pakoloko]

¿Quién ha verificado que el software verificador esté libre de errores?

PD: Interesante noticia.