Tipo
Artigos em Conferência
Tipo de Documento
Artigo Completo
Título
On the Path to Buffer Overflow Detection by Model Checking the Stack of Binary Programs
Participantes na publicação
Luís Ferreirinha (Author)
LASIGE
Ibéria Medeiros (Author)
Dep. Informática
LASIGE
Resumo
The C programming language, prevalent in Cyber-Physical Systems, is crucial for system control where reliability is critical. However, it is notably susceptible to vulnerabilities, particularly buffer overflows that are ranked among the most dangerous due to their potential for catastrophic consequences. Traditional techniques, such as static analysis, often struggle with scalability and precision when detecting these vulnerabilities in the binary code of compiled C programs. This paper introduces a novel approach designed to overcome these limitations by leveraging model checking techniques to verify security properties within a program’s stack memory. To verify these properties, we propose the construction of a state space of the stack memory from a binary program’s control flow graph. Security properties, modelled for stack buffer overflow vulnerabilities and defined in Linear Temporal Logic, are verified against this state space. When violations are detected, counter-example traces are generated to undergo a reverse-flow analysis process to identify specific instances of stack buffer overflow vulnerabilities. This research aims to provide a scalable and precise approach to vulnerability detection in C binaries.
Instituição
FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA
Evento
19th International Conference on Evaluation of Novel Approaches to Software Engineering
Identificadores da Publicação
ISSN - 2184-4895
ISBN - 9789897586965
Local
Angers, France
Editora
SCITEPRESS - Science and Technology Publications
Identificadores do Documento
DOI -
https://doi.org/10.5220/0012732700003687
URL -
http://dx.doi.org/10.5220/0012732700003687
Identificadores de Qualidade
CORE B (2023) - - Software Engineering