计算机工程 ›› 2012, Vol. 38 ›› Issue (18): 107-110.doi: 10.3969/j.issn.1000-3428.2012.18.029

• 安全技术 • 上一篇    下一篇

基于模型检测的程序恶意行为识别方法

张一弛,庞建民,范学斌,姚鑫磊   

  1. (国家数字交换系统工程技术研究中心,郑州 450002)
  • 收稿日期:2011-09-08 修回日期:2011-12-14 出版日期:2012-09-20 发布日期:2012-09-18
  • 作者简介:张一弛(1983-),男,博士研究生,主研方向:信息安全,逆向工程;庞建民,教授、博士生导师;范学斌、姚鑫磊,硕士研究生
  • 基金项目:
    国家“863”计划基金资助项目(2006AA01Z408, 2009AA01Z434);河南省重大科技攻关计划基金资助项目(092101210500)

Program Malicious Behavior Recognizing Method Based on Model Checking

ZHANG Yi-chi, PANG Jian-min, FAN Xue-bin, YAO Xin-lei   

  1. (National Digital Switching System Engineering & Technological R&D Center, Zhengzhou 450002, China)
  • Received:2011-09-08 Revised:2011-12-14 Online:2012-09-20 Published:2012-09-18

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

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

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

中图分类号: