LSVerifier: a BMC approach to identify security vulnerabilities in C open-source software projects

• Ano de defesa: 2023
• Autor(a) principal: Sousa, Janislley Oliveira de
• Outros Autores: http://lattes.cnpq.br/2630113981577092, https://orcid.org/0009-0002-9242-7345
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Instituição de defesa: Universidade Federal do Amazonas; Faculdade de Tecnologia; Brasil; UFAM; Programa de Pós-graduação em Engenharia Elétrica
• Palavras-chave em Português: Software gratuito; Software - Proteção; ENGENHARIAS: ENGENHARIA ELETRICA; Bounded model checking; Software verification; Security vulnerabilities; Open-source software; Large systems; Verificação de software; Vulnerabilidades de segurança; Software de código aberto; Sistemas de grande escala
• Link de acesso: https://tede.ufam.edu.br/handle/tede/10010

This research advances the field of software vulnerability analysis by highlighting the critical role of software validation and formal verification techniques in developing systems with high dependability and reliability. A particular focus is placed on addressing the prevalent issue of memory safety properties in C software. We introduce LSVerifier, an innovative tool that utilizes the Bounded Model Checking (BMC) technique to uncover security vulnerabilities within C open-source software efficiently. LSVerifier stands out by not only identifying vulnerabilities but also producing a comprehensive report that outlines detected software weaknesses, thereby serving as a resource for developers aiming to enhance software security. Our experimental evaluation showcases the tool's effectiveness in scrutinizing large software systems while maintaining low peak memory usage. We applied LSVerifier to twelve open-source C projects, successfully detecting real software vulnerabilities that were later acknowledged and confirmed by the developers. The results of this study highlight the potential of LSVerifier as a crucial tool in the ongoing efforts to protect open-source software from vulnerabilities.