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

Hoy 29 de Julio, es un día para la historia de la informática. La empresa General Dynamics C4 Systems y el NICTA (Centro de Excelencia Australiano) han publicado bajo licencia de software libre el primer kernel de un sistema operativo conjunto con pruebas matemáticas “punto a punto” que demuestra su corrección y seguridad. Se llama seL4 y tiene pinta que va a dar mucho que hablar.