LSVerifier: A BMC Approach to Identify Security Vulnerabilities in C Open-Source Software Projects

• Janislley Oliveira de Sousa Sidia Institute of Science and Technology / UFAM
• Bruno Carvalho de Farias University of Manchester
• Thales Araujo da Silva UFAM
• Eddie Batista de Lima Filho UFAM / TPV Technology
• Lucas Carvalho Cordeiro UFAM / University of Manchester

DOI: https://doi.org/10.5753/sbseg_estendido.2023.235802

Resumo

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.

Referências

Clarke, E., Kroening, D., and Lerda, F. (2004). A tool for checking ansi-c programs. Lecture Notes in Computer Science, 2988:168–176.

Cordeiro, L. C. and de Lima Filho, E. B. (2016). Smt-based context-bounded model checking for embedded systems: Challenges and future trends. ACM SIGSOFT Software Engineering Notes, 41(3):1–6.

for Standardization, I. O. (2012). Iso/iec 9899-2011: Programming languages – c. ISO Working Group, Geneva, Switzerland.

Gadelha, M., Monteiro, F., Cordeiro, L., and Nicole, D. (2019). ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference. In Tools and Algorithms for the Construction and Analysis of Systems.

Gadelha, M. R., Menezes, R. S., and Cordeiro, L. C. (2021). Esbmc 6.1: automated test case generation using bounded model checking. International Journal on Software Tools for Technology Transfer, 23(6):857–861.

Guardian, T. (2015). Airbus issues software bug alert after fatal plane crash. Available at: [link]. Accessed on 2023-07-25.

Ivancic, F., Shlyakhter, I., Gupta, A., Ganai, M. K., Kahlon, V., Wang, C., and Yang, Z. (2005). Model Checking C Programs Using F-SOFT. volume 2005, pages 297 – 308.

Merz, F., Falke, S., and Sinz, C. (2012). LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. In Proceedings of the 4th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE’12, page 146–161.

MITRE (2023). 2023 cwe top 25 most dangerous software weaknesses. Accessed: 2023-07-10.

Rodriguez, M., Piattini, M., and Ebert, C. (2019). Software verification and validation technologies and tools. IEEE Software, 36(2):13–24.

van Oorschot, P. C. (2023). Memory errors and memory safety: C as a case study. IEEE Security & Privacy, 21(2):70–76.

Wired (2015). Hackers remotely kill a jeep on the highway—with me in it. Available at: [link]. Accessed on 2023-07-25.