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.

• Type: Conference
• Year: 2008
• Where: PST
• Authors: Rachid Hadjidj, Xiaochun Yang, Syrine Tlili, Mourad Debbabi
• Keywords: Open Source, PST 2008, Security Privacy, Security Properties, Security Verification Framework