Inicio > Computación Teórica, Sistemas Operativos > seL4: Primer Sistema Operativo Formalmente Probado?

seL4: Primer Sistema Operativo Formalmente Probado?

13 agosto 2009

La tecnología de la información ha permeado todos los sectores de nuestra sociedad, economía, transporte, comunicaciones, salud, etc. Sin embargo toda nueva tecnología conlleva nuevos riesgos. Y en la industria del software todavía hay muchos problemas por resolver.

Hasta hoy en día nadie sabe como crear un programa que no contenga errores o agujeros de seguridad.

Esto significa que al implementar una solución de software debemos ser cuidadosos y estar bien preparados para esperar lo peor. Es decir debemos de manejar los riesgos.

Pero ¿que pasaría si pudiéramos crear software sin errores, sin agujeros de seguridad, que realice exactamente aquello para lo que fue programado? Tal vez esto pueda ser una utopía pero al menos el equipo NICTA ha logrado un gran avance en la dirección de la verificación del software.

NICTA ha logrado probar matemáticamente que su sistema operativo seL4 es correcto. Es decir que no contiene errores, agujeros de seguridad o comportamientos indeseados.

Para lograr esto tuvieron que realizar una demostración automática, mediante el software Isabelle, de más de 10 mil teoremas, lo que lo convierte en una de las demostraciones computarizadas más largas que se han realizado.

A pesar de este gran logro, la demostración tiene sus limitaciones, pues al parecer no es una demostración directa, sobre el lenguaje C de la implementación final, sino sobre el lenguaje Haskell, el cual esta basado en Calculo Lambda (más información técnica aquí). Por otro lado seL4 es un sistema operativo micro-kernel de alto desempeño de tan solo 7500 lineas de código C que no cuenta con soporte para múltiples procesadores.

Y claro que hay muchos detalles en la demostración, como por ejemplo: ¿como sabes que el compilador, el hardware, el demostrador, etc, etc…  es matemáticamente correcto?.

A pesar de todos los detalles o posibles errores que puedan quedar, seL4 podría ser el sistema operativo más seguro y confiable del mundo. Y por otro lado el equipo NICTA a demostrado que se pueden llevar las herramientas de demostraciones formales al software que utilizamos todos los días.

Seguramente conforme estas herramientas vayan madurando podremos desarrollar software más confiable.

Anuncios
A %d blogueros les gusta esto: