On the Path to Buffer Overflow Detection by Model Checking the Stack of Binary Programs

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.