seL4
Más información
- Creador
- NICTA (hoy CSIRO Data61)
- Año
- Tipo
- Micronúcleo
- Licencia
- GPLv2
- Sitio oficial
- sel4.systems
Un micronúcleo de la familia L4 con una prueba comprobada por máquina de que su código C hace exactamente lo que dice la especificación.
El equipo del NICTA australiano publicó la prueba en 2009: unas 8700 líneas de C verificadas con el asistente de demostración Isabelle/HOL frente a una especificación formal. Costó alrededor de 20 años-persona, unas veinte veces más que escribir el código. Pruebas posteriores demostraron que el binario compilado corresponde al código fuente y que el núcleo mantiene el aislamiento entre componentes.
El núcleo casi no hace nada por sí mismo —hilos, espacios de direcciones, IPC y capacidades— y todo lo demás corre como procesos aislados. Eso lo hace idóneo donde un fallo cuesta más que la verificación: en el programa HACMS de DARPA voló en un helicóptero no tripulado que un equipo rojo no logró secuestrar. El código se liberó como software libre en 2014.