Title: Identifying security vulnerabilities in source code with safety verification

Authors: Salim Yahia Kissi; Rabéa Ameur-Boulifa; Yassamine Seladji

Addresses: LRIT, Department of Computer Science, University of Abou Bekr Belkaid, Tlemcen, Algeria ' LTCI, Télécom Paris, Institut Polytechnique de Paris, Paris, France ' LRIT, Department of Computer Science, University of Abou Bekr Belkaid, Tlemcen, Algeria

Abstract: Ensuring the security of modern software systems is critical due to increasing complexity and interconnectedness. While automated testing and bug-finding tools have made progress, detecting security flaws - especially those related to runtime behaviour - remains a significant challenge. Existing research in software security has concentrated on source code analysis and often ignores how the execution environment affects program semantics, leaving machine-dependent vulnerabilities undetected. To bridge this gap, our approach analyses source code with awareness of its execution environment, acknowledging that many flaws arise from subtle mismatches between the two. Our work targets arithmetic errors in C/C+ + programs by modelling how the execution context shapes program behaviour. This article presents the construction of our knowledge base and explains how it integrates with our algorithm to enable accurate, environment-aware vulnerability detection using precise logical formulas, enabling the reformulation of vulnerability detection as a satisfiability problem suitable for automated reasoning using formal methods.

Keywords: formal analysis; vulnerabilities detection; static analysis; runtime environment specifications.

DOI: 10.1504/IJCCBS.2026.153768

International Journal of Critical Computer-Based Systems, 2026 Vol.12 No.1, pp.45 - 70

Received: 28 Sep 2024
Accepted: 17 Nov 2025
Published online: 26 May 2026 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article