LSVerifier: A BMC Approach to Identify Security Vulnerabilities in C Open-Source Software Projects - Sousa, Janislley Oliveira de; Farias, Bruno Carvalho de; Silva, Thales Araujo da; Lima Filho, Eddie Batista de; Cordeiro, Lucas Carvalho (Anais Estendidos do Simpósio Brasileiro de Cibersegurança (SBSeg); 2023: Anais Estendidos do XXIII Simpósio Brasileiro de Segurança da Informação e de Sistemas Computacionais, 2023)
Researchers continue to advance the state-of-the-art of software vulnerability analysis. Software validation and verification techniques are indispensable tools for cultivating robust systems characterized by high levels of dependability and reliability. Remarkably, the pressing concern of memory errors in C software looms large in the landscape of systems security. This paper introduces the innovative tool called LSVerifier, leveraging the bounded model checking technique to effectively detect security vulnerabilities in C open-source software. The proposed tool emerges as a pivotal asset for identifying vulnerabilities and generating an output report summarizing the software weaknesses found. The method’s efficacy was validated through real-world applications. The results show that LSVerifier was able to check complex open-source software, identifying software issues that could potentially result in vulnerabilities.