Abstract: By using the same or similar behavior characteristics of malicious codes, this paper proposes a method based on model checking technology to recognize malicious behaviors in binary files. It extracts Control Flow Graph(CFG) from disassembled binary executable and builds program model with Kripke structure, then produces Linear Temporal Logic formula to describe malware specification. The model checker recognizes malicious behavior and denotes detected behavior in the CFG. Experimental result shows that compared with common antivirus software, the proposed method is more effectively in recognizing malicious behaviors.

Key words: model checking, malicious behavior, Linear Temporal Logic(LTL), Control Flow Graph(CFG), disassemble, Kripke structure

摘要： 利用恶意代码所具有的相同或相似的行为特征，提出一种基于模型检测技术的程序恶意行为识别方法。通过对二进制可执行文件进行反汇编，构建程序控制流图，使用Kripke结构对程序建模，利用线性时序逻辑描述典型的恶意行为，采用模型检测器识别程序是否具有恶意行为，并在程序控制流图上对该恶意行为进行标注。实验结果表明，与常用的杀毒软件相比，该方法能更有效地发现程序中的恶意行为。

关键词: 模型检测, 恶意行为, 线性时序逻辑, 控制流图, 反汇编, Kripke结构

CLC Number: 

• TP393