Model checking C++ programs. (8th September 2021)

• Record Type: Journal Article
• Authors: Monteiro, Felipe R.; Gadelha, Mikhail R.; Cordeiro, Lucas C.
• Is Part Of: Software testing, verification & reliability. Volume 32:Number 1(2022)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2021-09-08
• Subjects: C++ -- memory safety -- model checking -- SMT -- software verification; Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1793
• Languages: English
• ISSNs: 0960-0833

Abstract

Summary: 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 analyses bounded C++ programs by encoding into SMT various sophisticated features that the C++ programming language offers, 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 efficiently 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. Abstract : ESBMC is a permissively licensed open‐source context‐bounded model checker for the verification of single‐ and multi‐threaded C and C++ programs. It can verify both predefined safety properties (e.g., bounds check, pointer safety, and arithmetic overflow) and user‐defined program assertions.