Formal verification to ensuring the memory safety of C++ Programs

• Ano de defesa: 2020
• Autor(a) principal: Sousa, Felipe Rodrigues Monteiro
• Outros Autores: http://lattes.cnpq.br/4475065926209027, https://orcid.org/0000-0001-9420-9056
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Instituição de defesa: Universidade Federal do Amazonas; Instituto de Computação; Brasil; UFAM; Programa de Pós-graduação em Informática
• Palavras-chave em Português: Engenharia de Software; Software Verification; Model Checking; Memory Safety; Segurança de Memória; CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO: METODOLOGIA E TÉCNICAS DA COMPUTAÇÃO: ENGENHARIA DE SOFTWARE; C++; Verificação Formal
• Link de acesso: https://tede.ufam.edu.br/handle/tede/7762

In the last three decades, memory safety issues in low-level 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. This work describes and evaluates a novel verification approach based on bounded model checking (BMC) and satisfiability modulo theories (SMT) to verify C++ programs formally. This verification approach analyzes bounded C++ programs by encoding various sophisticated features that the C++ programming language offers into SMT, such as templates, sequential and associative containers, inheritance, polymorphism, and exception handling. We formalize these sophisticated 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 this verification approach on top of the Efficient SMT-Based Context-Bounded Model Checker (ESBMC). We compare ESBMC to LLBMC and DIVINE, which are state-of-the-art verifiers to check C++ programs directly from LLVM bitcode. The experimental evaluation contains a set of over 1,500 benchmarks from several sources (e.g., Deitel & Deitel, NEC Corporation, and GCC test suite), which covers several C++ features. Experimental results show that ESBMC can handle a wide range of C++ programs, presenting a higher number of correct verification results, and at the same time, it reduces the verification time if compared to LLBMC and DIVINE tools.