LSVerifier: A BMC Approach to Identify Security Vulnerabilities in C Open-Source Software Projects
Janislley Oliveira de Sousa, Bruno Farias, Thales Araujo da Silva, Eddie B. de Lima Filho, Lucas Carvalho Cordeiro · 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.