代码迷惑及其语义研究

移动代码是计算机网络和Internet技术中广泛应用的一种计算模式,而且也被应用在许多新的技术中,如移动代理、主动网络等。但是,移动代码也带来了单机环境中不存在的安全威胁。这种威胁来自两个方面:一方面,当移动代码被下载到主机,恶意主机将可能会逆向工程这些代码,从而窃取代码中包含的关键算法或数据。在一些特殊的场合,如在移动代理中,代表计算主体完成计算的移动代理程序及其数据状态对于执行这些程序的主机是开放的。如果该主机是恶意主机,它就有可能对移动代理程序及其数据状态进行篡改,以达到攻击其它主机的目的。另一方面,网络的发展使得我们可以越来越方便地下载并执行一段代码,但是如果这段代码是具有恶意行为的,就有可能会破坏主机系统的资源,威胁到主机机密信息的安全。这两方面问题就称为是恶意主机问题和恶意客户问题。 代码迷惑是为解决恶意主机问题提出的一种自动程序变换技术,在恶意主机问题和恶意客户问题两个方面,代码迷惑扮演着不同的角色,这分别带来了需要研究的问题: 在恶意主机问题中,代码迷惑是一种有效的软件保护机制,但是,代码迷惑以前的研究主要集中在如何构造代码迷惑算法,而对于构造的代码迷惑算法是否有效,这些研究都没有提供严格证明,代码迷惑算法的构造缺乏有效性证明的理论支持。 在恶意客户问题中,代码迷惑被广泛地用来构造恶意软件变体,这给现存的恶意软件判定技术带来了新的问题。采用代码迷惑构造的多态病毒、变体病毒,使得现在已有的恶意软件判定器对主机的保护效果大大降低。 本文研究的思路是建立代码迷惑与语义理论的联系,从而可以利用已有的形式语义方面的研究解决代码迷惑研究中现存的问题。针对上述代码迷惑应用于移动代码安全时分别存在和导致的问题,本文研究分为两个方面: (1)在恶意主机问题中,代码迷惑是一种保护客户代码的重要的安全性技术,但是目前缺乏代码迷惑作为安全性方法的理论基础。本文研究了从语义角度为代码迷惑建立统一的有效性比较方法: ◇建立代码迷惑有效性比较框架,包括两个部分:形式化代码迷惑空间,形式地定义代码迷惑有效性度量。在该框架中,采用语义信息的变化来刻画有效性,允许定义更加细化的有效性度量,也能将传统的基于语法的有效性度量纳入这个比较系统。 ◇压平算法是一种重要的迷惑算法,本文给出了压平算法的形式描述,并基于代码迷惑有效性比较框架证明了其有效性。 我们发现基于偏序的代码迷惑有效性比较框架在表达力方面具有一定的局限性,无法为各种代码迷惑算法都建立有效性比较。 ◇本文研究了概率化抽象解释框架,通过建立程序不确定性的量化比较关系,从而达到量化比较代码迷惑有效性的目的。针对目前概率化抽象解释只能适用于有限维状态空间的问题,提出使用紧空间来刻画无限维状态空间的方法,扩展了概率化抽象解释的应用范围。这样,将状态空间提升到可度量的矢量空间上,就可以通过在矢量空间中定义距离来作为迷惑算法的有效性度量。 (2)在恶意客户问题中,代码迷惑技术是一种重要的攻击手段,为构造恶意软件变体提供了一种有效的方法,这使得传统病毒发现技术受到了挑战。本文从语义角度研究了恶意软件的变体判定技术: ◇本文建立了一种新的基于语义的恶意软件判定框架(MOM)。代码迷惑是一种保语义的程序变换技术,可以使用这种程序之间的语义相关性来作为识别一个程序是否是某恶意程序变体的标准。对于属于同一变体的恶意程序,MOM无需更新病毒库就能实现对恶意程序的识别。 ◇改进并设计了基于验证的恶意软件判定方法。该方法将恶意软件判定问题转化为证明验证条件正确性问题,并且通过输入迷惑算法规范来指导验证条件的产生和证明。 ◇MOM的验证条件产生是采用符号执行技术,因此如何高效地求解符号状态也是需要研究的问题。本文提出了一种不同于传统符号执行的方式,针对传统符号执行中状态替换时效率低下的问题,以静态单赋值形式作为中间表示,以基于支配树作为程序符号状态的收集策略,从而实现了高效地收集符号状态。 ◇本文基于编译框架LLVM,实现了一个MOM的原型系统。实验过程说明了基于语义恶意软件判定框架的有效性。