Model-Checking for Software Vulnerabilities Detection With Multi-Language Support

In this paper, the authors develop a security verification framework for open source software with a multi-language support. They base their approach on the GCC compiler which is considered as the de facto open source compiler for several languages including C, C++, JAVA, ADA, FORTRAN, etc. To achieve their goal they use a conventional push down system model-checker for reachability properties, and turn it into a fully fledged verification tool for both low and high level software security properties. They also allow programmers to define a wide range of temporal security properties using an automata-based specification approach. As a result, their approaches can model-check large scale software against system-specific security properties.