恶意代码分析是提取恶意代码特征进而对恶意代码进行检测的基础和前提，因此它是当前信息安全领域所关注的一个重要课题。对于恶意代码分析，当前大多数的反病毒厂商还主要依赖于病毒分析师的手工分析，这种人工方法虽然分析较为深入和准确，但存在响应时间长、过程繁琐和成本过高等缺点；而在理论研究领域，由于现有工作在对程序的状态空间建模、处理路径爆炸或刻画数据传播行为上有较大不足，它们在漏报率和执行效率上存在诸多缺点。　　 针对现有工作的不足，本文基于模型检验提出了若干对恶意行为进行自动分析的关键技术。基本的出发点是，用状态迁移系统表示程序路径，用有穷状态机或者信息流刻画恶意行为，然后计算程序可能到达的状态，并且验证程序的每条路径是否包含恶意行为。本文的创新性工作包括：用有穷状态机刻画时序型恶意行为并用下推自动机为程序路径建模，进而能够分析过程间的恶意行为；用加权下推自动机表示程序路径并用信息流中的污点分析来刻画数据传播型恶意行为，从而部分解决了路径爆炸问题；用静态隐式流敏感的方法分析隐式流型恶意行为，进而降低分析恶意行为时的漏报率。　　 本文的工作主要围绕如何改进恶意代码分析的漏报率和执行效率而进行，可以分为以下四个方面：　　 (一)时序型恶意行为分析方法研究　　 当前的恶意代码分析方法对时序型恶意行为只能进行过程内分析，无法处理恶意行为与控制结构相关的情形，并且它们能够对抗的混淆方法有限。为了解决这些问题，本文对时序型的恶意行为进行分析时，使用有穷状态自动机刻画恶意行为，使用下推自动机为程序的路径空间建模，使用模型检验方法验证恶意行为是否存在。因此，它能够描述恶意行为的复杂上下文环境和控制流信息，并支持对恶意代码的流敏感、上下文敏感和路径敏感的过程间分析，具有较高的分析精度，同时可以对抗更多的混淆技术。在实现中，本文根据对实际的恶意代码的分析和总结，给出了多种恶意行为模型。实验结果表明，该方法能够发现过程间的恶意行为和依赖于控制结构的恶意行为，并且能够发现不同种类的恶意代码中的相似恶意行为。　　 (二)数据传播型恶意行为分析方法研究　　 针对现有恶意代码分析方法在分析数据传播型恶意行为时效率较低的问题，本文根据污点数据在程序中的可达性来消减需要精确执行的路径数，从而部分解决了路径爆炸问题。现有方法对恶意代码中污点数据进行跟踪时往往需要精确执行所有的路径，导致在静态执行中，待分析的路径数量呈现指数级的增长，引起严重的效率问题。本文发现污点分析中的数据流转换方程能够构成一个有界幂等半环，从而将加权下推自动机理论引入到恶意代码分析中，并将污点分析问题转换为加权下推自动机的一个可达性问题。它用加权下推自动机表示程序路径，并用信息流中的污点分析来刻画恶意行为。这种转换使得恶意行为分析能够做上下文敏感和路径敏感的污点传播分析，并能在多项式时间内求解。实验结果表明，与经典的路径遍历方法和逐点展开方法相比，本文的方法可以更有效地对具有较多分支的程序进行过程间数据流分析，且具有较小的时间代价和空间代价。　　 (三)隐式流型恶意行为分析方法研究　　 当前仅有动态方法支持对隐式流型恶意行为进行分析，而且它们具有较低的路径覆盖率。为了解决这个不足，本文扩展了现有的静态污点分析方法，提出了隐式流敏感的污点分析方法，以刻画条件语句和循环语句对类型环境的影响，从而改善分析的漏报率并能达到较高的路径覆盖率。该方法结合程序切片技术和模拟执行技术，对可执行程序中的间接跳转语句的目标地址进行计算，提高了分支结构识别的准确性。基于分支条件的操作语义，提出了一个改进的污点标记规则，能够区分木马间谍程序和合法软件中的隐式流。实验结果表明，该方法能够跟踪采用隐式流进行的数据传播，在进行木马间谍软件分析时比显式流敏感的方法具有较低的漏报率，并且能够有效地发现需要特定条件触发的信息窃取行为；同时该方法能够消减对合法软件中的隐式流跟踪的数量。　　 (四)基于模型检验的恶意行为分析系统的设计和实现　　 基于模型检验理论，本文实现了一个恶意代码自动分析的系统，它包含预处理器、路径求解器前端、模型检验器以及路径验证器等多个模块。该系统能对恶意行为进行多粒度的刻画，并提供了一种易于扩展的恶意行为描述方式，能够对抗恶意代码的不同层次的变形和多态，具有较高的执行效率，特别适合对木马等实现复杂的恶意代码进行分析和检验。在该系统的设计与开发中，本文开展了一系列具有创新性的研究，包括研究和开发上述三个不同方面的恶意行为分析方法、可执行程序的归一化技术和路径验证技术等。该系统被多次成功应用于X86可执行文件中恶意行为的分析，包括拒绝服务攻击行为分析和击键信息窃取行为分析等。该研究已经被成功应用于恶意代码自动分析平台课题(国家242信息安全计划项目，项目编号2006A30)中，与动态分析方法并列成为两个重要基础模块。