| ???jsp.display-item.social.title??? |
|
???item.export.label???
Please use this identifier to cite or link to this item:
https://tede.ufam.edu.br/handle/tede/7762| ???metadata.dc.type???: | Dissertação |
| Title: | Formal verification to ensuring the memory safety of C++ Programs |
| Other Titles: | Verificação formal de programas C++ para garantir segurança de memória |
| ???metadata.dc.creator???: | Sousa, Felipe Rodrigues Monteiro  |
| ???metadata.dc.contributor.advisor1???: | Cordeiro, Lucas Carvalho |
| ???metadata.dc.contributor.referee1???: | Barreto, Raimundo da Silva |
| ???metadata.dc.contributor.referee2???: | Rocha, Herbert Oliveira |
| ???metadata.dc.description.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. |
| Keywords: | Engenharia de Software Software Verification Model Checking Memory Safety Segurança de Memória |
| ???metadata.dc.subject.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 |
| Language: | eng |
| ???metadata.dc.publisher.country???: | Brasil |
| Publisher: | Universidade Federal do Amazonas |
| ???metadata.dc.publisher.initials???: | UFAM |
| ???metadata.dc.publisher.department???: | Instituto de Computação |
| ???metadata.dc.publisher.program???: | Programa de Pós-graduação em Informática |
| Citation: | 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. |
| ???metadata.dc.rights???: | Acesso Aberto |
| ???metadata.dc.rights.uri???: | http://creativecommons.org/licenses/by/4.0/ |
| URI: | https://tede.ufam.edu.br/handle/tede/7762 |
| Issue Date: | 17-Jan-2020 |
| Appears in Collections: | Mestrado em Informática |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| Dissertação_FelipeRodriguesMonteiro_PPGI.pdf | Dissertação_FelipeRodriguesMonteiro_PPGI | 1.68 MB | Adobe PDF |  Download/Open Preview |
This item is licensed under a Creative Commons License
