Linux-based systems rely on large ecosystems of packaged binaries, many of which are implemented in C/C++. While these languages provide low-level memory control and high performance, they are also highly susceptible to memory-safety vulnerabilities, particularly buffer overflows (BOs). Traditional vulnerability discovery techniques, such as static and dynamic analysis, often struggle with scalability and precision when applied directly to binary code, which can thereby keep programs vulnerable. This work introduces BASICS, an approach and framework that combines model checking and bounded concolic execution to automatically verify security properties of stack memory in binary code, trampoline-based binary repair and crash-inducing inputs for bounded patch validation. BASICS constructs a Memory State Space -- MemStaCe -- from the binary program's control-flow graph and bounded concolic execution of C function calls and loops. Security properties, defined in Linear Temporal Logic, model vulnerable stack behaviours and allow the approach to identify violations in MemStaCe through counterexample traces. These vulnerabilities are then addressed using trampoline-based binary patching, and the resulting patches are validated using crash-inducing inputs extracted during concolic execution. We evaluated BASICS on the Juliet C/C++ and SARD benchmarks, as well as real open-source and Linux package binaries. BASICS achieved 86.4% precision and 87.4% accuracy on SARD, and 86.1% precision on Juliet, while also generating validated binary patches for supported vulnerable sinks. Compared with other evaluated tools, it provided the strongest overall balance between precision, analysis cost, and patching capability.

翻译：暂无翻译