关键词: 静态分析, 模型检查, 反汇编, 恶意代码, 自动机

Abstract: Introduce model checking method to built model for binary executable，develop a useful model checker.This paper produces a finite state machine，which is used to model a normal malicious binary executable，then make use of model checker to check obfuscated binary executable.If obfuscated binary executable can be identified by finite state machine，this binary executable is malicious executable.The experiment result shows model checking for obfuscated binary executable is an effective static analysis method and can check out some obfuscated binary executable.

Key words: static analysis, model checking, disassembly, malicious code, automata