Arch, David Daniel, 1990-

Verificación formal de código binario / David Daniel Arch. - [S.l. : s.n. ], 2015. - 146 p. : il. ; 30 cm.

Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2015.

Bibliografía : p. 145-146.

Los buffer overflow son una de las vulnerabilidades mas frecuentes que se encuentran en el software que utilizamos diariamente. El análisis de este tipo de vulnerabilidades se hace tedioso y complejo cuando solo se tiene acceso al código binario y no al código fuente del programa vulnerable debido al uso del lenguaje de bajo nivel ensamblador, la poca estructura que presenta este lenguaje, la ausencia de funciones bien definidas y de tipos de datos abstractos entre otros. Con el objetivo de facilitar el trabajo de los investigadores de seguridad presentamos una extensión para el framework BAP que agrega soporte para la verificación de buffer overflow en código binario mediante el uso de SMT solvers. Buffer overflows are one the most common vulnerabilites found on daily used software. This kind of vulnerability analysis is tedious and complex when researchers have access to binary code but don't have access to the source code of the program. This is due to the low level language assembler, the abscence of well defined functions and the absence of abstract data types among other factors. With the goal of making the job of security researchers easier is that we extended BAP to introduce a new feature that allows BAP to verify the presence of buffer overflow errors on binary code by using SMT solvers.




Licencia Creative Commons Atribución-NoComercial-CompartirIgual 2.5 Argentina.


Software--Program verification

Formal Methods Verificación de programas BAP SMT Código binario Buffer overflow