Tu código apesta: vamos a ponernos formales

Jesús Marín (@_jesusmg), devsecops de Entelgy Innotec Security nos hablará de como empezar a usar TLA+. Gran parte de las vulnerabilidades conocidas en aplicaciones proceden de fallos en el diseño, casuísticas que no se tienen en cuenta a la hora de elaborar los requisitos técnicos o de implementar el código. Este tipo de errores son difíciles de detectar con técnicas clásicas, especialmente en arquitecturas complejas, como puede ser la de una aplicación con procesos concurrentes. La verificación formal de software permite determinar si el diseño de un algoritmo o sistema es lógicamente correcto, a través de la aplicación de diversas técnicas matemáticas, incluso antes de comenzar la implementación real. TLA+ es una pila tecnológica que permite la verificación formal, de licencia libre y cuya comunidad de desarrollo está liderada por Leslie Lamport. Gracias a PlusCal, el lenguaje de pseudocódigo de TLA+, se reduce la curva de aprendizaje permitiendo obtener rápidamente los beneficios de la verificación formal. En esta charla se explicarán las ventajas de la verificación formal, junto a una breve introducción a TLA+, e importantes casos de éxito.