Formal verification to ensuring the memory safety of C++ Programs
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 d...
| Autor principal: | Sousa, Felipe Rodrigues Monteiro |
|---|---|
| Outros Autores: | http://lattes.cnpq.br/4475065926209027, https://orcid.org/0000-0001-9420-9056 |
| Grau: | Dissertação |
| Idioma: | eng |
| Publicado em: |
Universidade Federal do Amazonas
2020
|
| Assuntos: | |
| Acesso em linha: |
https://tede.ufam.edu.br/handle/tede/7762 |
| id |
oai:https:--tede.ufam.edu.br-handle-:tede-7762 |
|---|---|
| recordtype |
dspace |
| spelling |
oai:https:--tede.ufam.edu.br-handle-:tede-77622020-04-07T05:03:48Z Formal verification to ensuring the memory safety of C++ Programs Verificação formal de programas C++ para garantir segurança de memória Sousa, Felipe Rodrigues Monteiro Cordeiro, Lucas Carvalho http://lattes.cnpq.br/4475065926209027 http://lattes.cnpq.br/5005832876603012 Barreto, Raimundo da Silva http://lattes.cnpq.br/1132672107627968 Rocha, Herbert Oliveira http://lattes.cnpq.br/2284500318304899 https://orcid.org/0000-0001-9420-9056 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 Software Verification Model Checking C++ Memory Safety Engenharia de Software Verificação Formal Segurança de Memória 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. 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. 2020-04-07T03:16:45Z 2020-01-17 Dissertaçã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. https://tede.ufam.edu.br/handle/tede/7762 eng Acesso Aberto http://creativecommons.org/licenses/by/4.0/ application/pdf Universidade Federal do Amazonas Instituto de Computação Brasil UFAM Programa de Pós-graduação em Informática |
| institution |
TEDE - Universidade Federal do Amazonas |
| collection |
TEDE-UFAM |
| language |
eng |
| topic |
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 Software Verification Model Checking C++ Memory Safety Engenharia de Software Verificação Formal Segurança de Memória |
| spellingShingle |
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 Software Verification Model Checking C++ Memory Safety Engenharia de Software Verificação Formal Segurança de Memória Sousa, Felipe Rodrigues Monteiro Formal verification to ensuring the memory safety of C++ Programs |
| topic_facet |
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 Software Verification Model Checking C++ Memory Safety Engenharia de Software Verificação Formal Segurança de Memória |
| description |
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. |
| author_additional |
Cordeiro, Lucas Carvalho |
| author_additionalStr |
Cordeiro, Lucas Carvalho |
| format |
Dissertação |
| author |
Sousa, Felipe Rodrigues Monteiro |
| author2 |
http://lattes.cnpq.br/4475065926209027 https://orcid.org/0000-0001-9420-9056 |
| author2Str |
http://lattes.cnpq.br/4475065926209027 https://orcid.org/0000-0001-9420-9056 |
| title |
Formal verification to ensuring the memory safety of C++ Programs |
| title_short |
Formal verification to ensuring the memory safety of C++ Programs |
| title_full |
Formal verification to ensuring the memory safety of C++ Programs |
| title_fullStr |
Formal verification to ensuring the memory safety of C++ Programs |
| title_full_unstemmed |
Formal verification to ensuring the memory safety of C++ Programs |
| title_sort |
formal verification to ensuring the memory safety of c++ programs |
| publisher |
Universidade Federal do Amazonas |
| publishDate |
2020 |
| url |
https://tede.ufam.edu.br/handle/tede/7762 |
| _version_ |
1831969867329175552 |
| score |
11.753735 |