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

• URL: http://arxiv.org/abs/2511.19670v1
• Date: Mon, 24 Nov 2025 20:11:41 GMT
• Title: BASICS: Binary Analysis and Stack Integrity Checker System for Buffer Overflow Mitigation
• Authors: Luis Ferreirinha, Iberia Medeiros,
• Abstract summary: Cyber-Physical Systems have played an essential role in our daily lives, providing critical services such as power and water.<n>Traditional vulnerability discovery techniques struggle with scalability and precision when applied directly to the binary code of C programs.<n>This work introduces a novel approach designed to overcome these limitations by leveraging model checking and concolic execution techniques.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• CARE: Decoding Time Safety Alignment via Rollback and Introspection Intervention [68.95008546581339]
  Existing decoding-time interventions, such as Contrastive Decoding, often force a severe trade-off between safety and response quality.<n>We propose CARE, a novel framework for decoding-time safety alignment that integrates three key components.<n>The framework achieves a superior balance of safety, quality, and efficiency, attaining a low harmful response rate and minimal disruption to the user experience.
  arXiv  Detail & Related papers  (2025-09-01T04:50:02Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• VulBinLLM: LLM-powered Vulnerability Detection for Stripped Binaries [4.1417640577742425]
  Vul-BinLLM is a framework for binary vulnerability detection using Large Language Models.<n>Vul-BinLLM mirrors traditional binary analysis with fine-grained optimizations in decompilation and vulnerability reasoning with an extended context.<n>Our evaluations show that Vul-BinLLM is highly effective in detecting vulnerabilities on the compiled Juliet dataset.
  arXiv  Detail & Related papers  (2025-05-28T06:17:56Z)
• CRAFT: Characterizing and Root-Causing Fault Injection Threats at Pre-Silicon [3.6158033114580674]
  Fault injection attacks pose significant security threats to embedded systems.<n>Early detection and understanding of how physical faults propagate to system-level behavior are essential to safeguarding cyberinfrastructure.<n>This work introduces CRAFT, a framework that combines pre-silicon analysis with post-silicon validation to systematically uncover and analyze fault injection vulnerabilities.
  arXiv  Detail & Related papers  (2025-03-05T20:17:46Z)
• Improving Discovery of Known Software Vulnerability For Enhanced Cybersecurity [0.0]
  Vulnerability detection relies on standardized identifiers such as Common Platformion (CPE) strings.<n>Non-standardized CPE strings issued by software vendors create a significant challenge.<n>Inconsistent naming conventions, and versioning practices lead to mismatches when querying databases.
  arXiv  Detail & Related papers  (2024-12-21T12:43:52Z)
• Assessing the Effectiveness of Binary-Level CFI Techniques [0.0]
  Flow Control Integrity (CFI) provides protection against control flow hijacking attacks. binary-level type recovery is inherently speculative, which motivates the need for an evaluation framework.
  arXiv  Detail & Related papers  (2024-01-13T19:38:15Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
  This paper addresses learning safe output feedback control laws from partial observations of expert demonstrations. We first propose robust output control barrier functions (ROCBFs) as a means to guarantee safety. We then formulate an optimization problem to learn ROCBFs from expert demonstrations that exhibit safe system behavior.
  arXiv  Detail & Related papers  (2021-11-18T23:21:00Z)
• Pointwise Feasibility of Gaussian Process-based Safety-Critical Control under Model Uncertainty [77.18483084440182]
  Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs) are popular tools for enforcing safety and stability of a controlled system, respectively. We present a Gaussian Process (GP)-based approach to tackle the problem of model uncertainty in safety-critical controllers that use CBFs and CLFs.
  arXiv  Detail & Related papers  (2021-06-13T23:08:49Z)
• V2W-BERT: A Framework for Effective Hierarchical Multiclass Classification of Software Vulnerabilities [7.906207218788341]
  We present a novel Transformer-based learning framework (V2W-BERT) in this paper. By using ideas from natural language processing, link prediction and transfer learning, our method outperforms previous approaches. We achieve up to 97% prediction accuracy for randomly partitioned data and up to 94% prediction accuracy in temporally partitioned data.
  arXiv  Detail & Related papers  (2021-02-23T05:16:57Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.