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

In this paper we develop a security verification framework for open source software with a multi-language support. We base our approach on the GCC compiler which is considered as the defacto open source compiler for several languages including C, C++, JAVA, ADA, FORTRAN,etc. To achieve our goal we 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. We also allow programmers to define a wide range of temporal security properties using an automata-based specification approach. As a result, our approach can model-check large scale software against system-specific security properties.