Formally analyzing software vulnerability based on model checking Conference

Chunlei, W, Minhuan, H, Ronghui, H. (2009). Formally analyzing software vulnerability based on model checking . 1 615-618. 10.1109/NSWCTC.2009.104

cited authors

  • Chunlei, W; Minhuan, H; Ronghui, H

fiu authors

abstract

  • 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. © 2009 IEEE.

publication date

  • July 20, 2009

Digital Object Identifier (DOI)

International Standard Book Number (ISBN) 13

  • 9780769536101

start page

  • 615

end page

  • 618

volume

  • 1