计算机工程2012，Vol.38Issue(18)：107-110,4.DOI:10.3969/j.issn.1000-3428.2012.18.029
基于模型检测的程序恶意行为识别方法
Program Malicious Behavior Recognizing Method Based on Model Checking
摘要
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.关键词
模型检测/恶意行为/线性时序逻辑/控制流图/反汇编/Kripke结构Key words
model checking/ malicious behavior/ Linear Temporal Logic(LTL)/ Control Flow Graph(CFG)/ disassemble/ Kripke structure分类
信息技术与安全科学引用本文复制引用
张一弛,庞建民,范学斌,姚鑫磊..基于模型检测的程序恶意行为识别方法[J].计算机工程,2012,38(18):107-110,4.基金项目
国家“863”计划基金资助项目(2006AA01Z408,2009AA01Z434) （2006AA01Z408,2009AA01Z434）
河南省重大科技攻关计划基金资助项目(092101210500) （092101210500）
