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

Model checking obfuscated binary malicious code

作　　者：陈超[1] 李俊[1] 孔德光[1] 帅建梅[1] 

机构地区：[1]中国科学技术大学自动化系,合肥230027

出　　处：《计算机工程与应用》2008年第15期61-64,共4页Computer Engineering and Applications

基　　金：国家高技术研究发展计划(863)(the National High-Tech Research and Development Plan of China under Grant No.2006AA01Z449)

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

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

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]