Investigadores de Microsoft exploran una manera práctica de diseñar un software libre de fallas
El equipo de investigadores que trabaja en IronFleet incluye a, desde arriba a la izquierda a Chris Hawblitzel, Brian Zill, John Howell, Michael Lowell Roberts, Bryan Parno, Manos Kapritsos, Jay Lorch y Srinath Setty.
Investigadores de Microsoft han descubierto una manera de diseñar sistemas de software que abarcan muchas computadoras y que pueden ser probados sin fallas, una característica significativa en esta búsqueda, que ha durado décadas, por crear el software perfecto.
“El programa de verificación ha sido un Santo Grial para la ciencia de cómputo por 40 o 50 años”, dijo Bryan Parno, un investigador de Microsoft quien es uno de los co-autores de un próximo documento sobre este proyecto.
Los investigadores prevén que aún estamos lejos de un mundo en el que los grandes programas de computadora, tales como los sistemas operativos complejos, puedan ser diseñados de una manera en la cual se garantice que estén libre de fallas.
Pero, ellos dicen, que los avances recientes han hecho posible el diseñar software a escala pequeña que puede ser probada de manera matemática, que no tienen el tipo de imperfecciones que provocan que un programa se congele, o lo deje vulnerable a un ataque de seguridad.
“Estas herramientas han alcanzado el punto donde los desarrolladores pueden empezar a escribir códigos de esta manera” dijo Jay Lorch, un investigador senior quien es otro de los co-autores del documento.
El proyecto de investigación de Microsoft, llamado IronFleet, es uno de varios proyectos que han mostrado avances en la construcción de sistemas libres de fallas, el cual será presentado en el Simposio ACM 25 sobre los Principios de los Sistemas Operativos, el cual se llevará a cabo la próxima semana.
IronFLeet apunta a sistemas que abarcan diversas máquinas. Este tipo de sistemas pueden ser propensos a fallas, ya que los desarrolladores tienen que pensar en todas las maneras complejas en las que las máquinas tienen que interactuar.
Por ejemplo, tal vez un banco pueda tener un sistema distribuido que permita que sus múltiples servidores se coordinen entre ellos. No existe espacio para el error porque un titular de cuenta, tal vez tenga una petición de depósito que aparece en un servidor y una solicitud de retiro en otro, sin mencionar que el banco necesita estar seguro de manera absoluta que ambas transacciones serán registradas de manera consistente.
Los investigadores dijeron que eso es también un tipo de sistema en el cual la seguridad de estar libre de fallas es lo suficientemente importante para justificar la enorme inversión para producir este tipo de código probablemente correcto. Por ahora, ellos anotan, que sería impráctico y con un costo muy elevado, producir software a gran escala del tipo de sistemas operativos grandes, de esta forma, debido a que ese tipo de sistemas tienen millones de líneas de código, y por lo general es diseñado sobre un trabajo pasado.
“Al principio estaremos enfocados en pequeñas pero críticas piezas de software, donde la seguridad y la confiabilidad son muy importantes”, Parno dijo.
Lorch dijo que los investigadores también se han enfocado en sistemas que interactúan solo con otras computadoras, debido a que son más predecibles.
“Los humanos son muy complicados, así que tratar de especificar cómo un humano interactúa con un programa es bastante complejo” Lorch dijo.
Herramientas más rápidas e inteligentes
La capacidad de hacer este tipo de trabajo ha mejorado de manera reciente debido a mejores hardware y mejores herramientas, en las que se incluyen algoritmos más rápidos que han sido desarrollados en Microsoft Research, dijo Chris Hawblitzel, un investigador que también es co-autor del documento IronFleet, y quien antes creó un sistema operativo a menor escala, libre de fallas.
Hace una década, Hawblitzel dijo que tal vez le habría tomado toda su vida utilizar las herramientas de verificación necesarias para determinar que su sistema era correcto. Ahora, gracias a los algoritmos mejorados, podría tomar seis horas en una sola computadora.
Con un set de servidores basados en la nube, el sistema puede ser verificado en tan solo seis u ocho minutos.
El sistema de IronFleet es una salida del sistema más común para probar software de manera rigurosa para fallas antes de su lanzamiento, y también para reaccionar a cualquier falla que pudiera cortarse después de salir al público. Este sigue a otro proyecto por parte del mismo equipo de investigadores de Microsoft, Ironclad, el cual se enfocaba en crear sistemas que garanticen la seguridad de los datos personales.
Con estos proyectos, los investigadores dicen, existe el potencial para terminar el proceso de desarrollo de software de manera completa, al crear sistemas que han probado de manera matemática, ser perfectos para comenzar.
“Si tenemos éxito, en 10 o 15 años, las personas mirarán atrás y dirán, ‘No puedo creer que solían escribir código de esa forma”, comentó Parno. “Es como si los doctores hicieran cirugías sin anestesia o equipo esterilizado”.
Relacionados:
IronFleet: Probando los Sistemas Distribuidos Prácticos de manera Correcta
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty and Brian Zill (Microsoft Research)