Identifying security vulnerabilities in source code with safety verification

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.