BASICS: Binary Analysis and Stack Integrity Checker System for Buffer Overflow Mitigation

arXiv:2511.19670 · cs.CR · Submitted 2025-11-24 · Read on arXiv

Listen

Transcript

Introduction to the show: ident: Security Radio. Generated commentary on the latest security and cryptography papers.

Nadia: Today's paper: "BASICS: Binary Analysis and Stack Integrity Checker System for Buffer Overflow Mitigation".

Elias: This work introduces a novel approach to automatically detect and mitigate stack buffer overflow vulnerabilities in binary C programs by combining model checking with concolic execution and binary patching.

Nadia: First, who's behind it and why it matters.

Paper summary: Nadia: So, to wrap up this discussion on "BASICS: Binary Analysis and Stack Integrity Checker System for Buffer Overflow Mitigation," we've seen how this work aims to use model checking and concolic execution to build a Memory State Space, verify stack security properties with LTL, and then automatically patch vulnerabilities using crash-inducing inputs. Elias, what are your final thoughts on the title itself?

Elias: I think the title accurately reflects the combined nature of the work; it’s not just detection or just patching but an integrated system for binary analysis and stack integrity checking. I'm curious if we should consider how well this framework handles different types of memory corruption beyond simple buffer overflows, given its generic MemStaCe structure <ref:2511.19670#pg2>.

Priya: From a privacy researcher's standpoint, the focus on binary code analysis means this technique could be applied to proprietary software or even critical system binaries where source code isn't available for inspection. I wonder what kind of real-world security assurance this offers when dealing with compiled C programs.

Nadia: That’s the big implication, Priya; if we can reliably find and fix buffer overflows in compiled code automatically, it could significantly reduce the attack surface in many systems that rely heavily on C programming for performance and control <ref:2511.19670#pg2>. It moves beyond just finding bugs to actively fixing them.

Elias: And from a theoretical standpoint, the reliance on model checking to verify stack behavior through LTL provides a formal guarantee about the properties we specify, which is something that source-level symbolic execution often lacks in this direct binary context <ref:2511.19670#pg2>. I'm just thinking about the parameters that might break those assumptions if they are too restrictive.

Priya: The paper does flag a limitation regarding scalability, specifically mentioning state explosion issues when simulating deeply nested function calls or loops, which suggests that while the approach is powerful for specific cases, applying it universally across all complex binaries might require significant refinement <ref:2511.19670#pg2>.

Nadia: That limitation is important to remember; the authors acknowledge that state explosion is a challenge when dealing with very complex control flows, which means this system might be most effective for certain classes of software initially. However, they also show promising results against datasets like Juliet C/C++ and NIST SARD compared to tools like the CWE Checker <ref:2511.19670#pg0>.

Elias: It sounds like the authors are showing a solid performance metric when tested against those benchmark datasets, which gives us some concrete data on its effectiveness against known vulnerabilities <ref:2511.19670#pg0>. I'm still pondering how cheap it is to run this kind of deep analysis on a production system before we get into exploitation scenarios.

Priya: So, in summary, the work by Lu´ıs Ferreirinha and Iberia Medeiros presents BASICS as a way to systematically discover and automatically repair buffer overflows in binary C code using model checking and concolic execution <ref:2511.19670#pg1>. It offers a formal verification method for stack memory that is then paired with automated patching validated by crash-inducing inputs <ref:2511.19670#pg2>.

Nadia: That's the gist of it; the system is designed to bridge the gap between finding a vulnerability and fixing it automatically in compiled binaries. It’s a novel approach that integrates detection and mitigation into one pipeline using formal verification techniques <ref:2511.19670#pg2>. We should definitely keep an eye on how they address that state explosion issue as the research moves forward, because tackling that is key to making this system practical for wider use.

Conclusion: Nadia: So, we've covered how BASICS uses model checking and concolic execution to automatically find and fix stack overflows in binary C code. Now, let's talk about what that title actually means for the people who wrote it.

Elias: I think the title accurately reflects that this is a system for both analyzing binary data and actively fixing those kinds of security issues within the stack memory structure.

Priya: From my perspective, the authors are essentially proposing a way to get deep into compiled software—something usually reserved for source code analysis—to check its integrity without needing access to any original C files.

Nadia: Exactly, Priya; that's the core idea, and it’s pretty significant because it opens up a new way for security researchers to look at closed-source binaries.

Elias: And when you consider the authors who put this together, you see they brought together techniques from different areas of computer science—formal verification and practical binary analysis—to solve a very specific problem.

Priya: I'm curious about the impact here; if this method works reliably, it could drastically lower the barrier for finding vulnerabilities in complex systems that are hard to audit otherwise.

Nadia: That’s what we’re hoping to explore next, Priya; imagine the kind of security assurance you could get when you can systematically find and repair these kinds of bugs directly in compiled code.

VUSec, Vrije Universiteit Amsterdam · LASIGE, DI, Faculdade de Ciências, Universidade de Lisboa

cs.CR

Submitted: 2025-11-24

Updated: 2026-10-04

Comments: Accepted manuscript of the article published in Computers & Security. 23 pages

Journal ref: Computers & Security 172 (2027) 105165

DOI: 10.1016/j.cose.2026.105165

Code: https://github.com/Singularitty/BASICS

License: http://creativecommons.org/licenses/by-nc-nd/4.0/

Importance score: 73/100

The gist: This work introduces a novel approach to automatically detect and mitigate stack buffer overflow vulnerabilities in binary C programs by combining model checking with concolic execution and binary

Key concepts

Memory State Space (MemStaCe): This is a formal structure built from the program's control flow graph and simulations. Each transition represents an operation in the stack memory, allowing the system to model every possible arrangement of active stack frames during execution.
Linear Temporal Logic (LTL): LTL is a formal language used to define security properties for the program's memory. It allows developers to specify conditions that must hold true over time, such as ensuring critical memory regions always maintain a specific state.
Concolic Execution: This technique simulates the program's execution while actively exploring different paths and inputs. It is used to gather data on how the stack behaves during function calls and loops, which helps build the MemStaCe model.
Trampoline-based Binary Patching: This is a method for automatically fixing vulnerabilities by inserting extra binary code (a trampoline) instead of running the faulty instruction. This patch is then tested with crash-inducing inputs to confirm it successfully prevents the overflow.

Terminology

Verification — 29× in this paper · explained in 2 episodes
Trace — 20× in this paper · explained in 2 episodes
Accuracy — 13× in this paper · explained in 1 episode
Linear Temporal Logic — 9× in this paper
Nadia — 7× in this paper · explained in 2 episodes
Core — 6× in this paper · explained in 2 episodes
Elias — 6× in this paper · explained in 2 episodes
Formal Verification — 6× in this paper · explained in 2 episodes
Linear Temporal Logic (LTL) — 5× in this paper · explained in 4 episodes
Binary Analysis and Stack Integrity Checker System — 3× in this paper
Formal Methods — 3× in this paper · explained in 3 episodes
Frame Allocation — 3× in this paper
Arbiter — 2× in this paper · explained in 1 episode
Benchmark — 2× in this paper · explained in 2 episodes
Cyber-Physical Systems — 2× in this paper
Embeddings — 2× in this paper · explained in 2 episodes
Frame Extension — 2× in this paper
Labeled Transition System — 2× in this paper
Adaptation — 1× in this paper · explained in 1 episode
Common Weakness Enumeration — 1× in this paper
Fidelity — 1× in this paper · explained in 2 episodes
SMT solver — 1× in this paper · explained in 2 episodes
Satisfiability Modulo Theories — 1× in this paper

Summary

This work introduces a novel approach to automatically detect and mitigate stack buffer overflow vulnerabilities in binary C programs by combining model checking with concolic execution and binary patching. The core contribution is a framework that constructs a Memory State Space (MemStaCe) from the binary's control flow graph and simulations, uses Linear Temporal Logic (LTL) security properties to verify stack memory usage, and employs trampoline-based binary patching validated by crash-inducing inputs to eliminate identified vulnerabilities.

The gist

A novel approach is introduced that leverages 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.

Conceptual Foundation: Modeling Stack Memory

The approach constructs a Memory State Space – MemStaCe– from the binary program’s control flow graph and simulations of C library function calls and loops provided by concolic execution. In MemStaCe, each transition between memory states corresponds to an operation in the stack memory (e.g. pushing a register to the stack). A Memory State is formally defined as a Labeled Transition System (LTS) where each state corresponds to a collection of active stack frames, and transitions are governed by memory transition operators. These operators are categorized into Direct transitions (resulting from single assembly instructions) and Indirect transitions (arising from function calls), with indirect effects simulated through concolic execution.

Security Verification via Model Checking

The Model Checker module performs a comprehensive search within MemStaCe to identify any traces regarding the potential presence of buffer overflows based on the violation of predefined security properties. These properties are defined in Linear Temporal Logic (LTL) and translated into Omega-Automaton, which is then used by the model checker. For instance, one security property verifies that for every memory state M and every stack frame F in that state, the first 8 bytes should all have their state equal to Critical. When a guard fails to hold during the breadth-first search on the product of MemStaCe and the ω-automaton, a counterexample trace is produced, which consists of a list of "" tuples identifying the relevant steps leading to the violation.

Vulnerability Identification and Automated Repair

When a security property violation is detected, the Vulnerability Patcher and Validator performs a three-step pipeline:

Vulnerability Identification: A reverse flow analysis is performed, tracing the execution backwards to identify the assembly instruction that caused the violation. This process uses the counterexample trace and maps it back to an instruction in the bCFG.
Patch Generation: The system selects a patch template from the Patch Templates database corresponding to the identified C function and configures it using information from function call states collected during state space emulation.
Patch Application and Validation: The patch is applied using a trampoline-based binary patching method, which inserts extra binary code instead of executing the original instruction. The effectiveness is checked by testing the patch with crash-inducing inputs extracted during concolic execution, confirming that the program crashes on the original input but not on the patched one.

Evaluation and Tool Implementation

The approach is implemented in a tool called BASICS, which consists of four core modules: Binary Data Extractor, Model Checker, Security Property Converter, and Vulnerability Patcher and Validator. The evaluation involved testing against Juliet C/C++ and NIST SARD datasets compared against the CWE Checker. Results showed that BASICS achieved an accuracy of 84% in detection and a precision of 92%, outperforming CWE Checker in both metrics across the evaluated datasets. However, scalability was limited by state explosion issues inherent in model checking when simulating loops or deeply nested function calls, suggesting that rethinking the function call emulation approach could help circumvent this issue.

Extensibility and Future Work

BASICS is designed to be configurable, supporting user-provided security properties via LTL formulas and mapping them to CWE classes. Users can also expand the number of supported functions by providing their own patch templates written as small C code snippets. The MemStaCe structure is generic enough to support other types of security property verifications on the stack memory, such as return-oriented programming (ROP). Furthermore, users can modify the existing stack frame model to model the red zone of the stack by adding a 128-byte fixed-size region beyond the stack pointer. This allows for custom analysis and vulnerability mitigation.

Related Work Context

Existing research has focused primarily on source code-level detection (static analysis, symbolic execution) or functional correctness verification (Model Checking C Source Code). This work addresses the gap by employing formal verification to systematically discover stack BOs directly in binary code and combines this detection with an automated binary repair mechanism, integrating model checking with concolic execution for enhanced precision.

Improvements for AI systems

As a fastidious and diligent AI researcher, I have analyzed this paper, BASICS: Binary Analysis and Stack Integrity Checker System for Buffer Overflow Mitigation. The core innovation lies in combining Model Checking with Concolic Execution to perform formal verification of stack memory integrity in binary C programs, followed by automated binary patching.

Based on the proposed methodology and its demonstrated capabilities (detection accuracy >87%, precision >92%), here are specific improvements to AI systems that can be derived from this research:

The improved AI system, which we can call the Formal Binary Security Auditor (FBSA), will possess the following enhanced capabilities:

Enhanced Vulnerability Detection in Compiled Binaries (Superior to current static/dynamic tools):
Automated, Validated Binary Patch Generation:
Formal Verification of Code Integrity Post-Patching:
Scalable Security Analysis Across Diverse Software Repositories:

Specific improvements and what the improved FBSA system can do:

Enhanced Vulnerability Detection in Compiled Binaries (Superior to current static/dynamic tools):
The FBSA system will move beyond traditional static and dynamic analysis limitations by constructing a Memory State Space (MemStaCe) from the binary's Control Flow Graph (CFG). It will use LTL-specified security properties to formally verify the stack memory transitions.
It can precisely detect subtle, hard-to-find buffer overflows, such as those involving off-by-one errors or underflows caused by loop constructs and C library calls (as modeled in properties A.1.5 and A.1.6), which traditional tools often miss due to state space explosion or insufficient modeling of complex control flow interactions.
It can differentiate between genuine vulnerabilities and false positives by leveraging the concrete inputs gathered during concolic execution, leading to a high-precision detection rate (up to 92% precision reported).
Automated, Validated Binary Patch Generation:
Upon detecting a violation, the FBSA system will perform reverse flow analysis on the counterexample trace to pinpoint the exact assembly instruction causing the overflow. It will then use pre-defined patch templates (like those for functions such as strcpy) configured with real function call state data to generate precise binary patches (using trampoline techniques).
This generated patch is not just a guess; it is immediately validated by executing both the original and patched binaries using the concrete inputs extracted during concolic execution. This ensures that the fix successfully mitigates the BO without introducing new vulnerabilities or altering program functionality, achieving high correction success rates (reported at 78% F1-Score).
Formal Verification of Code Integrity Post-Patching:
The system will verify the effectiveness of its own patches by re-running crash-inducing inputs against the patched binary to confirm stability, providing a rigorous correctness proof that goes beyond simple functional testing.
Scalable Security Analysis Across Diverse Software Repositories:
The FBSA tool (BASICS) is designed to be configurable via user-provided security properties and CWE maps, allowing it to be adapted for detecting other vulnerability classes like Return-Oriented Programming (ROP) by simply defining new LTL properties.
It can integrate with existing binary analysis frameworks (like Angr) for CFG reconstruction, making it applicable across a wide range of compiled C binaries, from small test cases to large open-source applications, offering scalable security auditing capabilities despite the inherent state-space challenges.

Abstract

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.