Model Checking C++ Programs

TL;DR

This paper presents a formal verification approach for C++ programs using bounded model checking and SMT solving, effectively handling complex language features and outperforming existing tools in accuracy and efficiency.

Contribution

It introduces a novel SMT-based verification framework for C++, formalizing complex features and implementing it in ESBMC, demonstrating improved verification results over state-of-the-art tools.

Findings

ESBMC handles a wide range of C++ features effectively.

ESBMC achieves higher correctness in verification results.

ESBMC reduces verification time compared to LLBMC and DIVINE.

Abstract

In the last three decades, memory safety issues in system programming languages such as C or C++ have been one of the significant sources of security vulnerabilities. However, there exist only a few attempts with limited success to cope with the complexity of C++ program verification. Here we describe and evaluate a novel verification approach based on bounded model checking (BMC) and satisfiability modulo theories (SMT) to verify C++ programs formally. Our verification approach analyzes 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 C++ 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. At the same time, it reduces the verification time if compared to LLBMC and DIVINE tools. Additionally, ESBMC has been applied to a commercial C++ application in the telecommunication domain and successfully detected arithmetic overflow errors, potentially leading to security vulnerabilities.