Un modelo que permite mejorar la verificación de errores en programas computacionales mientras estos se ejecutan. Esta fue una de las diez propuestas ganadoras del concurso sobre testeo y verificación de software lanzado por Facebook Research a nivel global, iniciativa impulsada por el gigante de las redes sociales que busca entregar soluciones a los grandes desafíos en informática para mantener la seguridad, corrección y estabilidad de los sistemas de información digital en todo el mundo.
De casi 150 propuestas recibidas, diez resultaron ganadoras de este concurso, entre ellas la presentada por Éric Tanter, académico del Departamento de Ciencias de la Computación (DCC) de la Facultad de Ciencias Físicas y Matemáticas de la Universidad de Chile e investigador del Instituto Milenio Fundamentos de los Datos, junto a Jonathan Aldrich y Joshua Sunshine, ambos de la Carnegie Mellon University de Estados Unidos. De acuerdo al profesor Tanter, la propuesta se enmarca en la investigación que ha venido realizando durante la última década, que busca hacer más accesible las técnicas de verificación de software para fomentar su adopción progresiva en el desarrollo de sistemas informáticos de los que cada día dependemos más como sociedad y que abarcan al universo de servicios que se ofrecen a través de internet, desde sistemas bancarios hasta redes sociales.
Muchos de estos sistemas generan y procesan gigantescos volúmenes de datos, por lo que garantizar su operación óptima y segura para todos los usuarios se torna aún más complejo. De esta forma, según explica, existen herramientas que permiten analizar el comportamiento de programas antes de ejecutarlos para asegurar que no tengan errores cuando se van a ejecutar. Estas hacen lo que se llama “verificación de programas”, una de las cuales es Infer, que ha sido creada por Facebook y es capaz de analizar programas en varios lenguajes para detectar errores comunes.
“Un problema de estas herramientas es que necesariamente son conservadoras y a veces van a rechazar programas que en realidad se comportarían bien. En consecuencia, trabajar con una herramienta de verificación tiende a ser complejo y tedioso”, señaló. El tema de los actuales modelos de verificación, además, es que son costosos, “por ende uno quiere poder hacerlo de manera selectiva (solo en algunas partes), incremental (aumentar lo verificado componentes por componentes), y gradual (combinando lo estático y dinámico)”, agregó el académico del DCC.
En este sentido, la propuesta busca avanzar en una técnica de verificación gradual para Infer, “que permite aflojar la verificación estática cuando sea necesario, complementándola con verificación dinámica, es decir, en tiempo de ejecución. Así, los programadores pueden elegir el nivel de rigidez estática al cual se someten en función del avance del proyecto de software y el nivel de sensibilidad de cada componente del sistema informático".
Código abierto
Facebook Research entregará US$ 50 mil a cada equipo de investigación ganador. Según Mark Harman, Engineering Manager en Facebook Infrastructure, el propósito del concurso era encontrar propuestas que fuesen “desafiantes y excelentes a nivel científico, pero que también tenga el potencial de ser utilizado en la escala que solemos ver en el sector tecnológico en general”.
La idea de los desafíos que plantea Facebook Research -indica Éric Tanter- es que las propuestas y sus avances sean de código abierto, es decir, que estén disponibles para todo el ecosistema de desarrolladores, desde organizaciones a individuos, para que puedan usarlos para mejorar la robustez de sus propios sistemas.
