信息系统安全是国家安全的重要组成部分,恶意代码是信息系统安全的主要威胁之一。攻击者利用恶意代码实现网络渗透、持续控制以及非法窃密等目的,给国家和个人带来巨大损失。一方面恶意代码的数量增长迅猛使得安全人员疲于应付；另一方面恶意代码利用混淆、变形等代码自保护技术来对抗安全软件的检测和分析,使得对恶意代码的分析与检测更加困难。因此,及时准确地识别恶意代码及其变种,对于维护信息系统安全、降低国家及个人的损失具有重要意义。模型检测是一种基于时态逻辑的形式化验证技术,具有自动化程度高、实用性强等优点,广泛应用于硬件设计、通信协议及程序验证等领域。本文将模型检测技术应用于代码的恶意行为识别,重点对行为描述和特征的自动化提取方法、软件行为模型的构建、检测算法优化以及API (Application Program Interface, API)反混淆技术等方面进行了研究。论文的主要工作及创新点包括：1.提出了一种基于API增强依赖图的行为特征描述与自动提取方法针对行为特征描述不准确和提取方法人工干预过多的问题,本文提出了一种基于API增强依赖图的行为特征描述与自动提取方法。该方法利用动态污点分析技术,深入挖掘API多维属性的依赖关系,在此基础上通过API增强依赖图刻画程序行为,克服了代码混淆产生的消极影响；利用图的有向性和标签属性,优化了最小对比子图算法,实现了行为特征的自动比对和筛选,提高了行为特征提取的效率。2.提出了最佳权重为导向的路径搜索方法依据程序动态执行所构建的程序模型存在着路径覆盖率低,包含程序行为不完全等问题,同时采用动态符号执行遍历所有代码的方法也存在效率低和模型规模过大等问题。本文提出了以目标域的最佳权重为导向的路径搜索方法,通过关键API调用在程序控制流图中的位置划分目标域,根据目标域的属性和目标域与执行路径的距离设置目标域的权重,最终通过约束求解方法生成输入来引导程序快速逼近目标域,有效提高了程序模型的构建效率。3.提出并实现了一种大规模CTL (Computer Tree Logic,CTL)模型检测算法模型检测器每次只能取规范集的一个属性公式验证其可满足性,且在验证过程中存在着公共子公式的重复验证问题,这与大规模行为特征的快速匹配要求不相匹配。本文在深入研究CTL标记算法的基础上,提出了一种大规模CTL模型检测算法,通过标识公式集中的公共子公式、构建公式集的扩展语法树以及验证过程中绑定公共子公式和模型中对应的可满足状态,克服重复验证的问题,有效提高了CTL公式的验证效率,增加模型检测系统的实用性。4.提出并实现了一种动静结合的API反混淆方法为了防止从程序中解析API信息,恶意代码通常采用API混淆技术进行隐藏。本文在研究多种API混淆技术及反混淆方法的基础上,重点针对加密API动态调用的混淆方式,提出了一种动静结合的API反混淆方法,利用解密函数识别、上下文信息提取,借助于定制的仿真器模拟执行,最终实现API加密字符串信息的自动还原,为构建程序行为模型及提取行为特征奠定了基础。5.设计并实现了一种基于模型检测的恶意行为识别系统在以上技术的基础之上,本文设计并实现了一种基于模型检测的恶意行为识别系统MBDS (Malicious Behavior Detection System,MBDS)。该系统提出了用谓词时态逻辑表示恶意行为,并给出了将API增强依赖图转换为谓词时态逻辑公式的方法；系统将监控到的系统调用轨迹转换为基于谓词标记的Kripke结构,结合最佳权重的路径搜索策略构建较为全面的程序模型；通过大规模CTL模型检测算法验证程序模型对公式的可满足性,从而判定检测样本是否具有恶意性。实验数据验证了系统和算法的合理性和有效性。