一类恶意代码检测算法可靠性与完备性证明  

Soundness and Completeness Proof of a Class of Malware Detection Algorithms

作　　者：曾颖[1] 刘粉林[1] 

机构地区：[1]信息工程大学信息工程学院,河南郑州450002

出　　处：《小型微型计算机系统》2011年第1期85-90,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(60970141;60902102)资助;河南省科技创新杰出人才基金项目(094200510008)

摘　　要：代码迷惑可以使恶意代码绕过基于特征匹配的恶意代码检测器的检测.本文利用抽象解释理论,从程序语义的角度对高鹰等人提出的基于语义的恶意代码检测算法处理代码迷惑的能力进行了分析.在对该算法形式化描述的基础上,建立了一个与其等价的基于迹语义的检测器,并通过证明基于迹语义的检测器对于保持变体关系的代码迷惑算法的谕示可靠性和谕示完备性,从理论上阐述了高鹰等人的恶意代码检测算法的谕示可靠性和谕示完备性.Code obfuscation can alter the syntactic properties of the malware byte sequences without significantly affecting their execution behaviors.Thus it can easily foil signature-based detections.In this paper,the ability to handle obfuscating transformations of the semantics-based malware detection algorithm proposed by Gao et al.is discussed by the abstract interpretation theory from a semantic point of view.First,a formal description of the algorithm is proposed.Then an equivalent trace-based detector is developed.After that,the oracle-soundness and oracle-completeness of the semantics-based malware detection algorithm proposed by Gao et al.for a restricted class of obfuscating transformations which preserve variation relationships is proved by showing that the equivalent trace-based detector is oracle-sound and oracle-complete for the obfuscating transformations which preserve variation relationships.

关 键 词：恶意代码检测 抽象解释 代码迷惑 可靠性 完备性 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]