Como resultado de una vulnerabilidad de software recientemente descubierta, señala a modo de ejemplo, "un coche puede ser controlado mediante un ataque a través de su sistema de música". Ella está tratando de reducir estos riesgos creando la parte más importante de un sistema operativo—el núcleo o ke el—de tal manera que pueda demostrar que no se cuelgue jamás.
El enfoque actual preferido para la creación de software fiable es probarlo bajo tantas condiciones como el tiempo y la imaginación permitan. En cambio, Andronick está adaptando una técnica conocida como verificación formal, que los diseñadores de microchips utilizan para comprobar sus diseños antes de hacer un circuito integrado: crean una representación matemática de los subsistemas del chip que se puede utilizar para demostrar que el chip se comportará según lo previsto en respuesta a todas las posibles entradas de órdenes. Hasta ahora, la verificación formal se consideraba no factible para programas de gran tamaño como los sistemas operativos, ya que el análisis de una representación del código del programa sería demasiado complicado. Sin embargo, en un tour de force computacional y matemático, Andronick y sus colegas del laboratorio de Gerwin Klein en NICTA, pudieron comprobar formalmente el código que compone la mayor parte del núcleo de un sistema operativo diseñado para procesadores que a menudo se encuentran incorporados a teléfonos inteligentes, automóviles y aparatos electrónicos, como los equipos médicos portátiles. Debido a que este código es lo que finalmente pasa las instrucciones de software de otras partes del sistema al hardware para su ejecución, su blindaje tiene un gran impacto sobre la fiabilidad de todo el sistema.
"El trabajo es muy significativo", afirma Lawrence Paulson, profesor de ciencias informáticas en la Universidad de Cambridge. Más allá de mostrar que no hay errores en el ke el que pudieran causar que se cuelgue, afirma, la verificación garantiza que el núcleo ejecutará, sin errores, cada función programada para llevarse a cabo.
La tarea se hizo un poco más fácil por la decisión de desarrollar un, así llamado, microke el. Los microke els delegan tantas funciones como sea posible—tales como el manejo de entradas y salidas—a los módulos de software fuera del núcleo. En consecuencia, son relativamente pequeños—en este caso, alrededor de 7.500 líneas de código C y 600 líneas de ensamblador. "Eso es realmente pequeño para un ke el, pero muy grande para la verificación formal", afirma Andronick. El análisis se ha dirigido a los miles de líneas de código C; tuvo que desarrollarse un nuevo software y nuevas herramientas matemáticas para la tarea. El ke el se lanzó en febrero, y el equipo está trabajando en otra versión diseñada para la popular línea de chips x86.
Andronick no espera que la técnica se amplíe a software mucho más grande, aunque no cree que tenga que hacerlo. El uso de código verificado en los subsistemas clave permitiría a los desarrolladores asegurarse de que los errores en programas examinados menos rigurosamente—como los que se utilizan para interactuar con un equipo estéreo del coche—no pueden afectar a los componentes críticos del hardware. También podría impedir que un equipo se bloquease si encontrase un problema. Andronick quiere que más desarrolladores de software usen la verificación formal "en campos donde la seguridad realmente importe", afirma. "Hemos demostrado que es posible".