A Parallel Vulnerability Detection Framework via MPI

Open source applications have flourished recent years. Meanwhile, security vulnerabilities in such applications have grown. Since manual code auditing is error-prone, time-consuming and costly, it is necessary to find automatic solutions. To address this problem we propose an approach that combines constraint-based analysis and model checking together. Model checking technology as a constraint solver can be employed to solve the constraint-based system. CodeAuditor, the prototype implementation of our methods, is targeted at detecting vulnerabilities in C source code. With this tool, 9 previously unknown vulnerabilities in two open source applications were discovered and the observed false positive rate was at around 29%.