模型检测迷惑二进制恶意代码

对二进制恶意代码进行形式化建模，开发了一个检查迷惑恶意代码的模型检查器。生成迷惑前的二进制恶意代码的有限状态机模型，再使用模型检查器检测迷惑二进制恶意代码，如果迷惑二进制恶意代码能被有限状态机模型识别，可判定其为恶意代码。实验结果表明模型检查迷惑二进制恶意代码是一种有效的静态分析方法，可以检测出一些常用的迷惑恶意代码。

Model checking obfuscated binary malicious code

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.