BASICS: Binary Analysis and Stack Integrity Checker System for Buffer Overflow Mitigation
Luis Ferreirinha, Iberia Medeiros
TL;DR
The paper tackles stack-based buffer overflow vulnerabilities in binary C programs, particularly within cyber-physical systems, and identifies scalability and precision gaps in binary-level vulnerability detection. It introduces BASICS, a framework that builds a Memory State Space (MemStaCe) of the binary stack, employs model checking against LTL-defined security properties, uses concolic execution to enhance emulation of library calls and loops, and patches vulnerabilities via trampoline-based binary patches with rigorous validation. Key contributions include a formal MemStaCe model, LTL-based vulnerability properties, a patching workflow with patch templates, and an open-source BASICS prototype that demonstrates detection and repair capabilities on Juliet, SARD, and real open-source applications. Results show meaningful gains in precision and practical patching capability, though state-space explosion remains a challenge for larger binaries, suggesting future work in scalability and broader vulnerability coverage.
Abstract
Cyber-Physical Systems have played an essential role in our daily lives, providing critical services such as power and water, whose operability, availability, and reliability must be ensured. The C programming language, prevalent in CPS development, is crucial for system control where reliability is critical. However, it is also commonly susceptible to vulnerabilities, particularly buffer overflows. Traditional vulnerability discovery techniques often struggle with scalability and precision when applied directly to the binary code of C programs, which can thereby keep programs vulnerable. This work introduces a novel approach designed to overcome these limitations by leveraging model checking and concolic execution techniques to automatically verify security properties of a program's stack memory in binary code, trampoline techniques to perform automated repair of the issues, and crash-inducing inputs to verify if they were successfully removed. The approach constructs a Memory State Space -- MemStaCe -- from the binary program's control flow graph and simulations, provided by concolic execution, of C function calls and loop constructs. The security properties, defined in LTL, model the correct behaviour of functions associated with vulnerabilities and allow the approach to identify vulnerabilities in MemStaCe by analysing counterexample traces that are generated when a security property is violated. These vulnerabilities are then addressed with a trampoline-based binary patching method, and the effectiveness of the patches is checked with crash-inducing inputs extracted during concolic execution. We implemented the approach in the BASICS tool for BO mitigation and evaluated using the Juliet C/C++ and SARD datasets and real applications, achieving an accuracy and precision above 87%, both in detection and correction. Also, we compared it with CWE Checker, outperforming it.