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.

Y no es para menos. Hasta ahora, pocas piezas de software habían publicado pruebas matemáticas verificables acerca de sus propiedades de seguridad. Esto se considera muy complejo poder realizar afirmaciones de forma matemáticamente verificable acerca de la seguridad de todas las casuísticas a las que se debe enfrentar un programa de ordenador.

E incluso si se pueden hacer afirmaciones sobre un programa concreto, hay que tener en cuenta que hasta el programa más sencillo tiene muchas dependencias del entorno en el que se ejecuta. Hasta un programa que sólo imprime un «hola mundo!» depende de un compilador o intérprete, que ya de por si suele tener millones de líneas de código, y del sistema operativo y las librerías para por ejemplo pintar en pantalla, que tienen en su conjunto normalmente otros tantos millones de líneas de código.

Y es por eso que resulta novedoso y relevante que el kernel de un sistema operativo sea verificable: ahora será posible verificar matemáticamente en su conjunto no sólo ciertos programas de ordenador, sino incluso el sistema operativo donde se ejecutan dichos programas. Pensad esto por un momento: cuando normalmente los informáticos hablamos de la seguridad de un sistema, hacemos afirmaciones del tipo «se han hecho 3 auditorías del código y no han encontrado ninguna vulnerabilidad». Es decir, son opiniones. Pero cuando hablamos de pruebas matemáticamente verificables, ya dejan de ser opiniones, son hechos contrastables e incontestables. Es un nivel de seguridad mucho mayor. Es comparable a pasar de la alquimia y las brujas al método científico.

Es mucho aventurarse y puede que sea más las ganas que la realidad, pero este hito puede aportar cierta relevancia pública sobre los programas matemáticamente verificables, y marcar una tendencia en cuestiones de seguridad, hacia un camino donde cada vez más librerías y programas sean verificables.

Es importante destacar que pese a que haya una serie de pruebas matemáticas e incontestables sobre la seguridad de un software, eso no significa que sea 100% seguro. La razón es sencilla: esas pruebas demuestran ciertas afirmaciones acerca de la seguridad del sistema. Por ejemplo, afirman cosas como «no se puede hacer un ataque de buffer overflow». Pero continuamente se están descubriendo nuevas técnicas de ataque. Incluso si se tomasen en cuenta todos los vectores de ataque conocidos hasta el momento y fuesen capaces de aportar pruebas matemáticamente verificables de que cierto software no es vulnerable a ninguna de ellas, mañana podría descubrirse un nuevo vector de ataque, desconocido hasta la fecha.

Además, un sistema operativo y en general cualquier programa de ordenador necesitan un soporte material donde grabarse y ejecutarse: un disco duro, una placa base, una CPU. El hardware es y será siempre otro vector de ataque del que ninguna prueba matemática sobre el software podrá zafarse. El firmware, la BIOS, etc son también piezas de software, que convendría que viniesen con pruebas matemáticas verificables de buen funcionamiento, pero que por ahora pueden ser altamente inseguras.

En criptografía, otro vector de ataque muy importante son los Side channel attacks (ataques de canal secundario/alternativo). Un algoritmo como por ejemplo AES puede ser muy seguro. Puedes incluso tener pruebas matemáticas acerca de su seguridad, pero es posible que un atacante pueda obtener información que no debiera por un canal alternativo, de una forma que no esperas. Por ejemplo, quizás si pongo un micrófono al lado de tu teclado, puedo escuchar cómo tecleas, y según el sonido de cada tecla, averiguar tu contraseña. El algoritmo de cifrado quizás sea muy bueno, pero de nada te va a servir si tengo acceso al secreto (la contraseña) en base al cual se supone que es seguro.