Ya es bastante malo perder una hora de trabajo cuando su computadora falla, pero en entornos como la atención médica y la aviación, los fallos de software pueden tener consecuencias mucho más graves. En un caso notorio, un error informático provocó que los pacientes con cáncer recibieran sobredosis letales de una máquina de radioterapia; en titulares más recientes, Se culpó a un software defectuoso de los accidentes aéreos en Etiopía e Indonesia.

Ahora, investigadores del Instituto de Tecnología Stevens, en colaboración con la Universidad de Yale, están desarrollando herramientas que podrían hacer que los accidentes informáticos catastróficos sean mucho menos probables. Dirigido por Eric Koskinen, profesor asistente de informática en Stevens, El trabajo no solo tiene como objetivo garantizar que los programas se ejecuten correctamente en situaciones específicas, pero también utiliza algoritmos para determinar si es lógicamente posible, en cualquier circunstancia, para que el software produzca resultados no deseados.

"Lo que buscamos es una garantía del 100% de que nunca encontrará un error, "dijo Koskinen.

El equipo de Koskinen, respaldado por más de $ 2.5 millones de la Oficina de Investigación Naval, Modela las diferencias entre dos versiones de un programa. Eso es útil porque los programadores a menudo trabajan basándose en software existente, en lugar de escribir código desde cero, y se pueden introducir errores de una versión a la siguiente. Este enfoque es especialmente valioso para los militares, Dado que las agencias de defensa suelen comprar software a contratistas privados, luego, realice cambios internos antes de implementarlos en situaciones de misión crítica.

"Necesitan una forma de confirmar que han realizado los cambios correctamente internamente, y no ha presentado nuevos problemas, "Dijo Koskinen.

Para demostrar matemáticamente que un programa de computadora nunca podría tener ningún tipo de error, no importa las circunstancias, anticipado o inimaginado, El equipo de Koskinen usa una estrategia llamada lógica temporal. En lugar de escudriñar líneas individuales de código para buscar diferencias sintácticas, el equipo, incluido el profesor asistente Jun Xu, experto en análisis binario en Stevens, analiza cómo se comporta un programa a lo largo del tiempo. La idea es demostrar que no importa cuánto tiempo se ejecute el programa, no hay forma lógica de que alguna vez devuelva un resultado no deseado.

Modelar la estructura y el comportamiento de un programa, en lugar de estudiar detenidamente líneas de código individuales, es importante porque exactamente las mismas líneas de código pueden tener diferentes efectos en diferentes contextos, al igual que las líneas de código que parecen muy diferentes pueden lograr lo mismo. Es como estudiar un documento legal Koskinen explica:cambiar una sola palabra puede parecer trivial, pero puede cambiar todo el significado del documento. La lógica temporal ayuda a modelar el potencial de un programa, obteniendo información valiosa sobre las capacidades del programa en el mundo real.

El enfoque del equipo también permite eliminar errores en el software comercial estándar para el cual el código fuente no está disponible. Sin el código fuente, el equipo debe comparar los programas de computadora usando la versión binaria del código fuente. "Es difícil ver si la vulnerabilidad realmente se ha eliminado si no puede ver el código fuente, ", dijo." Las técnicas que estamos construyendo harán eso:si tiene una versión del software en la que confía, Nuestras técnicas podrán ayudarlo a detectar cambios (vulnerabilidades en las actualizaciones de software o malware insertado en programas ejecutables) y decidir si confiar en la nueva versión ".

El equipo de Koskinen también está desarrollando un conjunto de herramientas que otros investigadores y miembros del público podrán usar para probar software, y están ampliando su enfoque para trabajar con programas más grandes y fallas más complejas. "Estos son grandes problemas que afectan a los sistemas informáticos modernos, ", dijo Koskinen." Estos problemas solo se volverán más críticos, en campos como la atención médica, aviación, vehículos autónomos, y muchos más, por lo que es vital que desarrollemos técnicas prácticas para hacer que los sistemas controlados por computadora estén libres de errores y sean seguros de usar ".