Abstract: In order to analyze vulnerabilities in executable programs, a vulnerability analysis framework for binaries based upon model checking was proposed. Firstly, the abstract model of binary was defined, and the formal models of vulnerabilities based upon finite state automaton and the representations of software security attributes based upon event system were described. Then, the model checking based vulnerability analysis process and algorithm were proposed with respect to the abstract models of binaries and the security attributes to be checked. After that, the prototype of vulnerability analysis tool was designed and implemented based upon the framework. I}he illustrative sample program was analyzed to show in detail the principles of the framework, and the experimental results show the effectiveness of the analysis method.

Key words: Model checking,Vulnerahility analysis,Formal method