LSVerifier: a BMC approach to identify security vulnerabilities in C open-source software projects
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 safe...
| Autor principal: | Sousa, Janislley Oliveira de |
|---|---|
| Outros Autores: | http://lattes.cnpq.br/2630113981577092, https://orcid.org/0009-0002-9242-7345 |
| Grau: | Dissertação |
| Idioma: | eng |
| Publicado em: |
Universidade Federal do Amazonas
2024
|
| Assuntos: | |
| Acesso em linha: |
https://tede.ufam.edu.br/handle/tede/10010 |
| id |
oai:https:--tede.ufam.edu.br-handle-:tede-10010 |
|---|---|
| recordtype |
dspace |
| spelling |
oai:https:--tede.ufam.edu.br-handle-:tede-100102024-02-22T05:03:46Z LSVerifier: a BMC approach to identify security vulnerabilities in C open-source software projects Sousa, Janislley Oliveira de Cordeiro, Lucas Carvalho http://lattes.cnpq.br/2630113981577092 http://lattes.cnpq.br/5005832876603012 Becker, Leandro Buss Barreto, Raimundo da Silva https://orcid.org/0009-0002-9242-7345 Software gratuito Software - Proteção ENGENHARIAS: ENGENHARIA ELETRICA Bounded model checking Software verification Security vulnerabilities Open-source software Large systems Bounded model checking Verificação de software Vulnerabilidades de segurança Software de código aberto Sistemas de grande escala 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. Esta pesquisa avança o campo da análise de vulnerabilidades de software, destacando o papel crítico das técnicas de validação e verificação formal de software no desenvolvimento de sistemas com alta dependabilidade e confiabilidade. O estudo enfoca nas propriedades de segurança da memória em software C. Introduzimos o LSVerifier, uma ferramenta inovadora que utiliza a técnica de Bounded Model Checking (BMC) para identificar vulnerabilidades de segurança em software de código aberto em C. O LSVerifier destaca-se não apenas por identificar vulnerabilidades, mas também gera um relatório detalhado das potenciais vulnerabilidades detectadas. Nossa avaliação experimental demonstra a eficácia da ferramenta na inspeção de grandes sistemas de software enquanto mantém um uso baixo de memória. Aplicamos o LSVerifier a doze projetos de C de código aberto, detectando com sucesso vulnerabilidades reais de software que foram posteriormente reconhecidas e confirmadas pelos desenvolvedores. Os resultados deste estudo destacam o potencial do LSVerifier como uma ferramenta chave no esforço contínuo para proteger o software de código aberto contra vulnerabilidades. 2024-02-21T19:38:07Z 2023-12-20 Dissertação SOUSA, Janislley Oliveira de. LSVerifier: a BMC approach to identify security vulnerabilities in C open-source software projects. 2023. 95 f. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Manaus (AM), 2023. https://tede.ufam.edu.br/handle/tede/10010 eng Acesso Aberto https://creativecommons.org/licenses/by-nc-nd/4.0/ application/pdf Universidade Federal do Amazonas Faculdade de Tecnologia Brasil UFAM Programa de Pós-graduação em Engenharia Elétrica |
| institution |
TEDE - Universidade Federal do Amazonas |
| collection |
TEDE-UFAM |
| language |
eng |
| topic |
Software gratuito Software - Proteção ENGENHARIAS: ENGENHARIA ELETRICA Bounded model checking Software verification Security vulnerabilities Open-source software Large systems Bounded model checking Verificação de software Vulnerabilidades de segurança Software de código aberto Sistemas de grande escala |
| spellingShingle |
Software gratuito Software - Proteção ENGENHARIAS: ENGENHARIA ELETRICA Bounded model checking Software verification Security vulnerabilities Open-source software Large systems Bounded model checking Verificação de software Vulnerabilidades de segurança Software de código aberto Sistemas de grande escala Sousa, Janislley Oliveira de LSVerifier: a BMC approach to identify security vulnerabilities in C open-source software projects |
| topic_facet |
Software gratuito Software - Proteção ENGENHARIAS: ENGENHARIA ELETRICA Bounded model checking Software verification Security vulnerabilities Open-source software Large systems Bounded model checking Verificação de software Vulnerabilidades de segurança Software de código aberto Sistemas de grande escala |
| description |
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. |
| author_additional |
Cordeiro, Lucas Carvalho |
| author_additionalStr |
Cordeiro, Lucas Carvalho |
| format |
Dissertação |
| author |
Sousa, Janislley Oliveira de |
| author2 |
http://lattes.cnpq.br/2630113981577092 https://orcid.org/0009-0002-9242-7345 |
| author2Str |
http://lattes.cnpq.br/2630113981577092 https://orcid.org/0009-0002-9242-7345 |
| title |
LSVerifier: a BMC approach to identify security vulnerabilities in C open-source software projects |
| title_short |
LSVerifier: a BMC approach to identify security vulnerabilities in C open-source software projects |
| title_full |
LSVerifier: a BMC approach to identify security vulnerabilities in C open-source software projects |
| title_fullStr |
LSVerifier: a BMC approach to identify security vulnerabilities in C open-source software projects |
| title_full_unstemmed |
LSVerifier: a BMC approach to identify security vulnerabilities in C open-source software projects |
| title_sort |
lsverifier: a bmc approach to identify security vulnerabilities in c open-source software projects |
| publisher |
Universidade Federal do Amazonas |
| publishDate |
2024 |
| url |
https://tede.ufam.edu.br/handle/tede/10010 |
| _version_ |
1831970239196168192 |
| score |
11.753896 |