Model Checking C++ Programs

Felipe R. Monteiro, Mikhail R Gadelha, Lucas Cordeiro

Research output: Contribution to journalArticlepeer-review

Abstract

In the last three decades, memory safety issues in system programming languages such as C or C++ have been one of the most significant sources of security vulnerabilities. However, there exist only a few attempts with limited success to cope with the complexity of C++ program verification. We describe and evaluate a novel verification approach based on bounded model checking (BMC) and satisfiability modulo theories (SMT) to verify C++ programs. Our verification approach analyzes bounded C++ programs by encoding into SMT various sophisticated features that the C++ programming language oers, such as templates, inheritance, polymorphism, exception handling, and the Standard Template Libraries. We formalize these features within our formal verification framework using a decidable fragment of first-order logic and then show how state-of-the-art SMT solvers can eciently handle that. We implemented our verification approach on top of ESBMC. We compare ESBMC to LLBMC and DIVINE, which are state-of-the-art verifiers to check C++ programs directly from the LLVM bitcode. Experimental results show that ESBMC can handle a wide range of C++ programs, presenting a higher number of correct verification results. Additionally, ESBMC has been applied to a commercial C++ application in the telecommunication domain and successfully detected arithmetic-overflow errors, which could potentially lead to security vulnerabilities.
Original languageEnglish
JournalSoftware Testing, Verification and Reliability
Publication statusAccepted/In press - 4 Aug 2021

Fingerprint

Dive into the research topics of 'Model Checking C++ Programs'. Together they form a unique fingerprint.

Cite this