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

Sousa, Felipe Rodrigues Monteiro

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

dc.contributor.advisor1	Cordeiro, Lucas Carvalho
dc.contributor.advisor1Lattes	http://lattes.cnpq.br/5005832876603012	por
dc.contributor.advisor1orcid	https://orcid.org/0000-0002-6235-4272	por
dc.contributor.referee1	Barreto, Raimundo da Silva
dc.contributor.referee1Lattes	http://lattes.cnpq.br/1132672107627968	por
dc.contributor.referee2	Rocha, Herbert Oliveira
dc.contributor.referee2Lattes	http://lattes.cnpq.br/2284500318304899	por
dc.contributor.referee2orcid	https://orcid.org/0000-0002-2648-8468	por
dc.creator	Sousa, Felipe Rodrigues Monteiro
dc.creator.Lattes	http://lattes.cnpq.br/4475065926209027	por
dc.creator.orcid	https://orcid.org/0000-0001-9420-9056	por
dc.date.issued	2020-01-17
dc.description.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.	por
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.	por
dc.format	application/pdf	*
dc.identifier.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.	por
dc.identifier.uri	https://tede.ufam.edu.br/handle/tede/7762
dc.language	eng	por
dc.publisher	Universidade Federal do Amazonas	por
dc.publisher.country	Brasil	por
dc.publisher.department	Instituto de Computação	por
dc.publisher.initials	UFAM	por
dc.publisher.program	Programa de Pós-graduação em Informática	por
dc.rights	Acesso Aberto	por
dc.rights.uri	http://creativecommons.org/licenses/by/4.0/
dc.subject	Engenharia de Software	por
dc.subject	Software Verification	por
dc.subject	Model Checking	por
dc.subject	Memory Safety	por
dc.subject	Segurança de Memória	por
dc.subject.cnpq	CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO: METODOLOGIA E TÉCNICAS DA COMPUTAÇÃO: ENGENHARIA DE SOFTWARE	por
dc.subject.user	Software Verification	eng
dc.subject.user	Model Checking	eng
dc.subject.user	C++	eng
dc.subject.user	Memory Safety	eng
dc.subject.user	Engenharia de Software	por
dc.subject.user	Verificação Formal	por
dc.subject.user	Segurança de Memória	por
dc.thumbnail.url	https://tede.ufam.edu.br//retrieve/38459/Disserta%c3%a7%c3%a3o_FelipeRodriguesMonteiro_PPGI.pdf.jpg	*
dc.title	Formal verification to ensuring the memory safety of C++ Programs	por
dc.title.alternative	Verificação formal de programas C++ para garantir segurança de memória	por
dc.type	Dissertação	por