???item.export.label??? ???item.export.type.endnote??? ???item.export.type.bibtex???

Please use this identifier to cite or link to this item: https://tede.ufam.edu.br/handle/tede/7762
Tipo do documento: Dissertação
Título: Formal verification to ensuring the memory safety of C++ Programs
Título(s) alternativo(s): Verificação formal de programas C++ para garantir segurança de memória
Autor: Sousa, Felipe Rodrigues Monteiro 
Primeiro orientador: Cordeiro, Lucas Carvalho
Primeiro membro da banca: Barreto, Raimundo da Silva
Segundo membro da banca: Rocha, Herbert Oliveira
Resumo: 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.
Abstract: Este trabalho descreve e avalia o Efficient SMT-Based Context-Bounded Model Checker (ESBMC) para verificar formalmente programas C++. O ESBMC implementa a técnica de verificação de modelos limitados (do inglês, bounded model checking -- BMC) com base em teorias do módulo da satisfabilidade (do inglês, satisfiability modulo theories -- SMT) para lidar com recursos complexos que a linguagem de programação C++ oferece, tais como templates, contêineres sequenciais e associativos, herança, polimorfismo e manipulação de exceções. ESBMC é comparado as ferramentas LLBMC e DIVINE, as quais verificam os programas C++ diretamente a nível de bitcode do LLVM. Resultados experimentais mostram que o ESBMC pode lidar com uma ampla gama de estruturas do C++, apresentando uma taxa de aproximadamente 85% de verificações corretas e, ao mesmo tempo, reduzindo o tempo de verificação se comparado as ferramentas LLBMC e DIVINE.
Palavras-chave: Engenharia de Software
Software Verification
Model Checking
Memory Safety
Segurança de Memória
Área(s) do CNPq: CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO: METODOLOGIA E TÉCNICAS DA COMPUTAÇÃO: ENGENHARIA DE SOFTWARE
???metadata.dc.subject.user???: Software Verification
Model Checking
C++
Memory Safety
Engenharia de Software
Verificação Formal
Segurança de Memória
Idioma: eng
País: Brasil
Instituição: Universidade Federal do Amazonas
Sigla da instituição: UFAM
Departamento: Instituto de Computação
Programa: Programa de Pós-graduação em Informática
Citação: MONTEIRO, Felipe Rodrigues Monteiro. Formal verification to ensuring the memory safety of C++ Programs. 2020. 71 f. Dissertação (Mestrado em Informática) - Universidade Federal do Amazonas, Manaus, 2020.
Tipo de acesso: Acesso Aberto
Endereço da licença: http://creativecommons.org/licenses/by/4.0/
URI: https://tede.ufam.edu.br/handle/tede/7762
Data de defesa: 17-Jan-2020
Appears in Collections:Mestrado em Informática

Files in This Item:
File Description SizeFormat 
Dissertação_FelipeRodriguesMonteiro_PPGI.pdfDissertação_FelipeRodriguesMonteiro_PPGI1,68 MBAdobe PDFThumbnail

Download/Open Preview


This item is licensed under a Creative Commons License Creative Commons