Document type
Conference papers
Document subtype
Full paper
Title
On the Path to Buffer Overflow Detection by Model Checking the Stack of Binary Programs
Participants in the publication
Luís Ferreirinha (Author)
LASIGE
Ibéria Medeiros (Author)
Dep. Informática
LASIGE
Summary
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.
Institution
FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA
Event
19th International Conference on Evaluation of Novel Approaches to Software Engineering
Publication Identifiers
ISSN - 2184-4895
ISBN - 9789897586965
Address
Angers, France
Publisher
SCITEPRESS - Science and Technology Publications
Document Identifiers
DOI -
https://doi.org/10.5220/0012732700003687
URL -
http://dx.doi.org/10.5220/0012732700003687
Rankings
CORE B (2023) - - Software Engineering