Automated detection of code vulnerabilities based on program analysis and model checking

Ensuring the correctness and reliability of software systems is one of the main problems in software development. Model checking, a static analysis method, is preponderant in improving the precision of vulnerabilities detection. However, when applied to buffer overflow and other bugs, it is hard to automatically construct the model for detecting the vulnerabilities. To address this problem we propose an approach that combines constraint based analysis and model checking together. We trace the memory size of buffer-related variables and instrument the code with corresponding constraint assertions before the potential vulnerable points by constraint based analysis. Then the problem of detecting vulnerabilities is converted into the problem of detecting vulnerabilities to verifying the reach ability of these assertions by model checking. In order to reduce the cost of model checking, program slicing is introduced to reduce the code size. CodeAuditor is a prototype implementation of our approach. With CodeAuditor, several yet unreported vulnerabilities are discovered in several open source software, and the performance is shown to be improved significantly with the help of program slicing.