Abstract
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.
Original language | English |
---|---|
Title of host publication | Proceedings of the 19th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2024 |
Editors | Hermann Kaindl, Hermann Kaindl, Hermann Kaindl, Mike Mannion, Leszek Maciaszek, Leszek Maciaszek |
Publisher | Science and Technology Publications, Lda |
Pages | 719-726 |
Number of pages | 8 |
ISBN (Electronic) | 9789897586965 |
DOIs | |
Publication status | Published - 2024 |
Externally published | Yes |
Event | 19th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2024 - Angers, France Duration: 28 Apr 2024 → 29 Apr 2024 |
Publication series
Name | International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE - Proceedings |
---|---|
ISSN (Electronic) | 2184-4895 |
Conference
Conference | 19th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2024 |
---|---|
Country/Territory | France |
City | Angers |
Period | 28/04/24 → 29/04/24 |
Bibliographical note
Publisher Copyright:© 2024 by SCITEPRESS – Science and Technology Publications, Lda.
Keywords
- Assembly
- Linear Temporal Logic
- Model Checking
- Software Security
- Stack Buffer Overflow
- Static Analysis