Finding Software Vulnerabilities in Open-Source C Projects via Bounded Model Checking

TL;DR

This paper presents a scalable methodology using bounded model checking to detect vulnerabilities in large open-source C projects, effectively verifying extensive codebases with low memory usage.

Contribution

The authors developed a source-code pre-processing and prioritization approach that enables bounded model checkers to efficiently verify large software systems.

Findings

Successfully verified 12 open-source C projects

Detected real vulnerabilities confirmed by developers

Achieved low peak memory usage during verification

Abstract

Computer-based systems have solved several domain problems, including industrial, military, education, and wearable. Nevertheless, such arrangements need high-quality software to guarantee security and safety as both are mandatory for modern software products. We advocate that bounded model-checking techniques can efficiently detect vulnerabilities in general software systems. However, such an approach struggles to scale up and verify extensive code bases. Consequently, we have developed and evaluated a methodology to verify large software systems using a state-of-the-art bounded model checker. In particular, we pre-process input source-code files and guide the respective model checker to explore them systematically. Moreover, the proposed scheme includes a function-wise prioritization strategy, which readily provides results for code entities according to a scale of importance. Experimental results using a real implementation of the proposed methodology show that it can efficiently verify large software systems. Besides, it presented low peak memory allocation when executed. We have evaluated our approach by verifying twelve popular open-source C projects, where we have found real software vulnerabilities that their developers confirmed.