CodeAuditor: A vulnerability detection framework based on constraint analysis and model checking

Open source applications have flourished over recent years. Meanwhile security vulnerabilities in such applications have grown. Since manual code auditing is error-prone, time-consuming and costly, automatic solutions have become necessary. In this paper we address program vulnerabilities by static code analysis. First, we use flow-insensitive and interprocedural constraint-based analysis to extract the vulnerability detection model from the source code. Second, we employ model checking to solve the model. In addition, we do alias analysis to improve the correctness and precision of the detection model. The presented concepts are targeted at the general class of buffer-related vulnerabilities and can be applied to the detection of vulnerability types such as buffer overflow, format string attack, and code injection. CodeAuditor, the prototype implementation of our methods, is targeted at detecting buffer overflow vulnerabilities in C source code. It can be regarded as a vulnerability framework in which a variety of analysis and model checking tools can be incorporated. With this tool, 18 previously unknown vulnerabilities in six open source applications were discovered and the observed false positive rate was at around 23%.