La división de Investigación y Desarrollo de Microsoft, Microsoft Research, anuncia que un grupo de sus científicos ha alcanzado un importante hito, que consiste en el desarrollo de un método que hace posible crear sistemas de software distribuido, con la capacidad de verificar y garantizar su infalibilidad.
“La verificación de software ha sido un Santo Grial para la informática durante 40 o 50 años”, escribe Brian Parno, uno de los científicos de Microsoft participantes en el proyecto, y coautor de un artículo científico presentado la víspera en la conferencia 25° simposio de ACM sobre principios de sistemas operativos en Monterrey, California.
IronFleet
El proyecto es denominado IronFleet, y está concebido para sistemas multiplataforma, susceptibles de errores cuando los desarrolladores descuidan la compleja forma en que los distintos sistemas operativos interactúan entre sí.
Como ejemplo de lo anterior, los científicos mencionan un banco con un sistema distribuido que permite a los numerosos servidores de la entidad coordinarse entre sí. Un sistema bancario no admite margen de error, debido a que la transacción de un cliente puede ingresar mediante un servidor, mientras que otra transacción hecha posteriormente puede ser recibida mediante otro servidor. Para el banco es imprescindible saber que ambas transacciones han sido registradas de manera consistente.
Los científicos de Microsoft explican que el mundo actual dista mucho de estar en una situación donde, de manera realista, sea posible desarrollar programas grandes y complejos, como por ejemplo sistemas operativos, cuya infalibilidad pueda ser garantizada.
Según Microsoft Research, aunque el desarrollo de código infalible será costoso, de todas formas se trata de un proyecto viable para sistemas donde las garantías de funcionamiento son fundamentales, como por ejemplo, el citado sistema bancario.
“Al comienzo nos concentraremos en porciones pequeñas, aunque de rango crítico, de software, donde la seguridad y la confiabilidad sean imprescindibles”, declaró Parno.
Por su parte, su colega Jay Lorch agrega que el grupo de investigadores trabaja únicamente con sistemas que interactúan con otros. La razón de esto sería lo imprevisibles que son los seres humanos. “Las personas somos muy complejas, razón por la que es aventurado siquiera intentar especificar la forma en que un ser humano interactúa con un programa informático” explicó Lorch.
Velocidad multiplicada
Según otro científico participante en la iniciativa, Chris Hawblitzel, el proyecto ha sido posible mediante la combinación de hardware y software mejorado, como asimismo algoritmos más veloces, desarrollados por Microsoft Research. Hawblitzel agrega que los nuevos sistemas permiten acercarse aún más al momento en que los desarrolladores podrán comenzar a escribir código infalible. “Si tenemos éxito, la gente dentro de 15 años podrá mirar el retrospectiva y decir “es increíble que antes escribían código de esa forma”.