Formally Analyzing Software Vulnerability Based on Model Checking

This paper presents a study of the security vulnerability analysis based upon the formal methods and model checking tools. Through deeply exploring the characteristics of software vulnerabilities, we develop the FSM model to formalize and reason about security vulnerabilities. The vulnerability is modeled as a series of elementary FSMs (eFSMs), which specifies a derived predicate. We have proposed a fully automatic method for verifying that a particular program model (FSM) satisfies a given security property. Our work contributes to bridging the gap between abstract specifications of security properties and their actual implementations in program. The effectiveness and the practical usefulness of the approach are exemplified by an illustrative analysis of heap overflow vulnerability.