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

Sousa, Janislley Oliveira de

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

dc.contributor.advisor-co1	Lima Filho, Eddie Batista de
dc.contributor.advisor-co1Lattes	http://lattes.cnpq.br/7827981023232761	eng
dc.contributor.advisor1	Cordeiro, Lucas Carvalho
dc.contributor.advisor1Lattes	http://lattes.cnpq.br/5005832876603012	eng
dc.contributor.advisor1orcid	https://orcid.org/0000-0002-6235-4272	eng
dc.contributor.referee1	Becker, Leandro Buss
dc.contributor.referee2	Barreto, Raimundo da Silva
dc.creator	Sousa, Janislley Oliveira de
dc.creator.Lattes	http://lattes.cnpq.br/2630113981577092	eng
dc.creator.orcid	https://orcid.org/0009-0002-9242-7345	eng
dc.date.issued	2023-12-20
dc.description.abstract	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.	por
dc.description.resumo	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.	eng
dc.format	application/pdf	*
dc.identifier.citation	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.	eng
dc.identifier.uri	https://tede.ufam.edu.br/handle/tede/10010
dc.language	eng	eng
dc.publisher	Universidade Federal do Amazonas	eng
dc.publisher.country	Brasil	eng
dc.publisher.department	Faculdade de Tecnologia	eng
dc.publisher.initials	UFAM	eng
dc.publisher.program	Programa de Pós-graduação em Engenharia Elétrica	eng
dc.rights	Acesso Aberto
dc.rights.uri	https://creativecommons.org/licenses/by-nc-nd/4.0/
dc.subject	Software gratuito	por
dc.subject	Software - Proteção	por
dc.subject.cnpq	ENGENHARIAS: ENGENHARIA ELETRICA	eng
dc.subject.user	Bounded model checking	eng
dc.subject.user	Software verification	eng
dc.subject.user	Security vulnerabilities	eng
dc.subject.user	Open-source software	eng
dc.subject.user	Large systems	eng
dc.subject.user	Bounded model checking	por
dc.subject.user	Verificação de software	por
dc.subject.user	Vulnerabilidades de segurança	por
dc.subject.user	Software de código aberto	por
dc.subject.user	Sistemas de grande escala	por
dc.thumbnail.url	https://tede.ufam.edu.br/retrieve/72974/DISS_JanislleySousa_PPGEE.pdf.jpg	*
dc.title	LSVerifier: a BMC approach to identify security vulnerabilities in C open-source software projects	eng
dc.type	Dissertação	eng