Detección de errores en software mediante verificación de modelos

Resumen

La introducción del ordenador e Internet en nuestras vidas ha hecho que muchos procesos que antes costaban horas, días, incluso meses, ahora puedan ser llevadas a cabo en mucho menos tiempo, mejorando nuestras vidas en numerosos aspectos. Como ha sucedido tantas veces en la historia, cualquier invento puede acabar siendo utilizado con fines maliciosos. En Internet también se llevan a cabo ataques a estados, espionaje, invasiones, y otros aspectos tan característicos de cualquier guerra. Muchos de estos ataques están dirigidos a programas conocidos que presentan algún tipo de vulnerabilidad, haciendo que éstos sean la puerta de entrada a cualquier sistema o red. A causa de esto, la búsqueda de vulnerabilidades se está convirtiendo en una nueva profesión, muy bien pagada y valorada tanto por naciones y empresas, por un lado, como por mafias y un gran mercado negro, por el otro. Por esta razón, la presente tesis doctoral busca mejorar los procesos de encontrar errores en el software, y por esta razón se formula la siguiente hipótesis: «Existe un método de representación de la memoria que es capaz de detectar errores conocidos, tanto en el heap como en la pila». En este contexto, nos centramos en crear un nuevo algoritmo para buscar vulnerabilidades utilizando model checking para el análisis de binarios. Nuestra notación, facilita la creación de fórmulas que representen errores y el algoritmo devuelve los posibles flujos de ejecución que provocarían que una vulnerabilidad se llevase a cabo. Además, la programación de nuestro algoritmo se ha realizado en un lenguaje que valida el código generado, Coq, asegurando de esta forma que el propio código que busca errores no contenga ninguno en sí mismo. La validación del algoritmo y del código ha sido corroborada de dos modos: i) encontrando nuevas vulnerabili- dades que no habían sido descubiertas y ii) comprobando código inseguro que ya ha sido publicado por otros expertos en seguridad. Finalmente, tras este estudio, se ha liberado una plataforma para la búsqueda de vulnerabilidades que puede ayudar a la comunidad a realizar un software más seguro.