可信计算经过长期发展, 取得了令人瞩目的成果^[1-24].随着可信计算成为高价值体系结构(如可信云等)的关键安全支撑技术之一, 其自身安全性面临着更高的挑战.在这些挑战中, 本文关注于如下3个问题.

(1) 第1个问题是:当前可信计算缺少理论支撑, 且理论研究与实践应用部分脱节.

可信计算在诞生之初即面临着“实践超前于理论”的情况^[1], 经过近20年的发展, 仍然没有从数学上建立一个较为完善的可信计算模型.理论上, 可信计算首先要明确定义“可信”.当前主流的定义包括“完整性”^[3]、“行为符合预期”^[3]和“可靠+安全”^[1]等几种不同形式.已有的工作大多从单一的角度研究可信^[4-24], 而并没有考虑建立一个统一的、涵盖以上3种不同定义的模型.另一方面, 即便理论上取得了一些成果, 这些成果也难以应用到实践当中.以国内广受关注的无干扰模型在可信计算领域的研究为例^[22-24], 由于几乎没有工作解决无干扰属性自动化验证的难题^[25-27], 使得大多理论成果并不能实际应用于实时信息系统, 如进程信任链传递^[22]、可信度量^[23]等当中.理论成果和实践应用之间仍然存在着较大差距.

(2) 第2个问题是:当前的可信度量属于“被动发现”机制, 缺少“主动防御”能力.

根据可信计算标准, 可信计算有三大核心功能:度量、存储和报告, 三者协同运作确保了第三方能够可靠地判定本机的可信性.其基本过程是:本机在运行的过程中不断度量自身的可信性, 并将度量结果存储到专用安全芯片TPM(trusted platform module)和内存log当中.当其他机器想与本机通信时, 由本机将存储的度量结果报告给对方, 并由对方来判定本机的可信性.上述过程是一种“事后被动发现”机制, 换句话说, 这种机制只能确保其他机器可靠地判定本机是否被攻击而处于不可信状态, 但却无法及时检测到机器被攻击的情况.事实上, “事前防御、事中审计、事后发现”应当作为环环相扣的整体.然而, 现有的可信度量侧重于“事后被动发现”、而缺少“事前主动防御”的研究工作.

(3) 第3个问题是:可信计算如何在层出不穷的攻击手段下可靠地实现可信度量.

可信计算“度量、存储和报告”三大核心功能中, 度量居于基础地位, 存储和报告的内容均来自于度量的结果.随着新型攻击方法(如ROP^[28]等)层出不穷、传统攻击不断应用包括多态/混淆/变形/编码等在内的多种对抗手段以及未公开攻击机理的威胁等, 使得度量信息系统的可信性变得日益复杂和困难.特别地, 运行时(runtime)度量才能真正反映系统行为的可信性^[1], 但这对度量的实时性提出了很高的要求.

针对上述问题, 本文提出了一种基于无干扰理论的软件实时可信度量与防护方法, 主要贡献如下:

(1) 针对问题(1)和问题(2), 首先, 利用无干扰模型解释了主流可信定义——即“完整性”“行为符合预期”和“可靠+安全”——的数学涵义(参见第2.2节的定义9);其次, 通过将系统调用看做原子动作, 提出了基于无干扰的实时可信度量与防护方法, 其基本思想是:根据不同系统调用所属安全域之间的无干扰关系, 建立软件预期行为EB(expected behavior), 并利用无干扰模型判定软件真实行为与预期行为之间的一致性, 从而实现对软件的实时可信度量与主动防护(参见第3节); 最后, 给出了实时可信性判定算法(参见第3.5节的算法1), 算法的时间复杂性为O(1).

(2) 针对问题3, 本文基于如下观察:绝大多数攻击都需要前后相继的两个步骤, 即首先定位可利用的漏洞, 然后通过漏洞执行攻击代码(shellcode).打断以上环环相扣的任何一步, 就可以有效地防御攻击.本文从第2步入手, 注意到攻击代码几乎都需要系统调用的支持, 因而不论是何种类型的攻击, 我们只需要利用系统调用序列构建代码的真实行为, 利用系统调用安全域之间的无干扰关系刻画软件的预期行为EB, 即可以通过判定当前代码的真实行为与预期行为EB之间是否存在偏差来度量是否发生了攻击.实验结果表明:方法是有效的, 其不仅能够实时度量到新型攻击如ROP等, 而且可以有效地发现多态、混淆、变形和编码等多种传统对抗方法所生成的攻击代码, 理论上也可以防御未知机理攻击(只要其利用系统调用实现攻击).

(3) 所提出的方法无需任何学习训练过程, 无需任何先验知识.使用者亦不必关心底层理论机制, 只要给出安全策略即可, 具体来说, 只需要根据实际安全需求, 依照预期行为规范EBS(expected behavior specification)语法编写EBS(参见第3.3节和附录), 系统即可实现实时可信度量与防护.

1 相关研究工作 1.1 可信度量相关研究工作

国际上第一个基于TCG(trusted computing group)标准的完整性度量架构是IMA^[4].IMA是一种“加载时度量”, 这种度量方式只能说明软件没有被篡改(哈希不变), 并不能说明软件运行时的动态行为是否可信.随后, 卡内基梅隆大学的Shi等人提出了为分布式系统建立可信环境的BIND框架^[5].BIND把完整性度量对象的范围缩小到关键代码段, 并对关键代码段的每一组数据生成一个认证器, 实现了细粒度的动态度量验证.但BIND需要事先确定关键代码段, 并建立关键代码段和输入数据/输出数据之间的绑定关系.这种绑定与本文是有差别的:本文对进程所绑定的是基于系统调用描述的预期行为EB, 同时, 绑定过程也无需确定关键代码段.在IMA的基础上, Jaeger等人通过引入CW-Lite模型设计了PRIMA架构^[6], 实现了运行时度量.但PRIMA所基于的CW- Lite模型缺少形式化验证能力, 因而无法形式化地对系统设计进行可信验证.从内核完整的角度, Loscocco等人^[7]提出了Linux内核完整性监视器LKIM, 用以监控Linux内核运行时关键数据结构的动态完整性; Carbone等人^[8]实现了KOP系统, 用以监控内核指针对象的动态完整性.LKIM和KOP的贡献在于它们对于可信计算平台的关键基础软件(操作系统)的动态完整性度量具有重要的意义, 不足之处在于它们无法扩展到一般应用程序.针对云计算环境下的动态完整性度量问题, Schiffman等人^[9]实现了VMV(virtual machine verifier).VMV能够对虚拟机及其内部的应用程序进行动态完整性度量, 以确保云端计算的可信性.不过, VMV构建的基础仍然是PRIMA^[6], 从而缺少形式化验证能力.从软件运行时的局部结构化约束完整性和全局不变式完整性入手, Kil等人^[10]提出了一种基于完整性动态属性的远程证明系统ReDAS.ReDAS需要一个学习训练过程, 这使得它只能局限于度量经过训练的软件.Xu等人^[11]通过将系统的可信性归结为系统状态变化的可信性, 提出了一个远程证明框架DR@FT.但DR@FT只能适用于基于Clark-Wilson或CW-Lite模型的完整性度量框架, 因而也无法验证自身设计架构的可信性.John等人^[12]发现:在Dell Latitude E6400 Laptop上, 可信度量根核CRTM(core root of trust measurement)的实现没有满足TPM PC规范和NIST 800-155指导规范, 这使得攻击者可以回放伪造的度量结果给TPM, 从而导致证明方错误地认为本机被攻击过的BIOS仍然处于“干净可信”的状态.该方法侧重于解决CRTM和信任链传递的安全性问题, 而并非针对软件行为的实时度量.针对动态度量时动态可信度量根DRTM(dynamic root of trust for measurement)的存在性(activated/enabled)攻击问题, Zhang等人^[13]提出了一种强制性、最小化、用户参与的解决方案.但该方案只确保DRTM确实存在(activated), 同样不涉及软件行为的实时度量.Abera等人^[14]设计并实现了控制流证明C-FLAT(control flow attestation)架构, 通过软件的控制流路径, 而不是源码, 来证明软件的可信性, 尝试为物联网设备上的远程证明提供一种解决方案.针对越来越深入的硬件可信度量和防护方法, Zhang等人^[15]提出了一种化整为零的攻击技术, 以绕过现有的硬件检查措施, 其基本思想是:将整体的、恶意的硬件功能分解成零散的、正常的子模块, 在子模块通过可信验证之后再将其组合成整体, 以实现恶意硬件功能.由于硬件层位于系统调用层之下, 因而本文无法对这种攻击进行检测和防御.Matetic等人^[16]提出了一种称为ROTE的分布式回滚保护机制, 攻击者若要利用恶意回归攻击破坏Intel SGX等安全机制下的信息完整性, 就必须将ROTE分布式平台中的所有参与者同时回滚到初始状态, 这大大增加了攻击的难度.

国内对于可信度量相关问题也展开了深入的研究.为了解决可信平台模块TPM在云计算、网络功能虚拟化等场景下低成本可信扩展和前向安全问题, 余发江等人^[17]提出了一种动态信任扩展方法, 有效保证了虚拟可信平台模块vTPM的可信性, 为虚拟环境下的度量、存储、报告、密码、证书等功能构建了可靠的硬件基础.邓良等人^{[18, 19]}用ring 0层的内可信基(inner TCB)替代传统的虚拟机监视器, 实现对内核代码和控制流的完整性度量以及对硬件操作和软件行为的验证, 有效保证了上层应用的安全, 且开销很小.林杰等人^[20]针对虚拟机软件的完整性问题, 提出了一种利用关键数据结构内存映射和地址动态转换技术, 实现对上层应用运行时完整性度量的方法.与本文工作相比, 上述完整性度量方法^[18-20]的共有问题在于其无法回答软件(即便代码和数据被度量是完整的)在运行过程中是否会出现不可信的行为.陈志锋等人^[21]基于内存取证技术提出了一种内核实时完整性度量方法.与本文相比, 本文针对上层软件, 陈志锋等人^[21]针对的内核, 两者的研究对象并不一致.另一方面, 若将文献[21]的技术应用于上层应用, 其需要“完整性基准库”, 换句话说, 文献[21]需要一个学习训练的过程, 对于未经学习的软件可能无法准确实施度量.相反, 本文的方法无需学习训练, 只要编写好软件预期行为规范, 即可以度量任何软件的实时行为.理论上, 甚至还可以发现未知攻击.张兴等人^{[22, 23]}利用无干扰模型, 对信任链传递^[22]以及进程^[23]的可信性度量问题进行了研究.他们工作的重要性在于首次将无干扰模型应用于可信计算领域, 但不足之处是没有给出可实践的方法, 而如何将无干扰模型应用于实践, 一直是无干扰研究的一个关键所在.

1.2 无干扰及其应用相关研究工作

Goguen等人^[29]以状态机的形式首先引入了传递无干扰的概念, 随后, Rushby建立了标准的非传递无干扰模型^[25].Rushby的研究表明, 传递无干扰只是非传递无干扰的一个特例.因此, 如果没有特殊说明, “无干扰”一般都特指“非传递无干扰”.在Rushby的模型中, 仅仅考虑了观察者是否能够区分状态变迁所导致的状态差异, 而并不关心观察者是否能够同时观察到所执行的不同动作的差异.Meyden注意到了这个问题, 由此定义了安全约束更强的TA-Security和TO-Security^[30].随后, Eggert等人研究了经典的传递无干扰和非传递无干扰以及TA-Security和TO-Security这4种无干扰属性验证的时间和空间复杂度^[26].需要指出的是, Eggert等人仅仅给出了时空复杂度推演结果, 但没有给出具体的属性验证算法.事实上, 到目前为止, 状态机形式的无干扰模型属性验证仍然是一个难题^[25-27], 当前最好的工作是Hadj-Alouane等人给出的验证算法^[27], 其不仅支持任意多个安全域, 而且支持无干扰属性的可靠性和完备性条件, 然而其时间复杂性却高达双指数$O({2^{|X||{2^D}|}})$, 无法实用.

除了状态机以外, 进程代数的互模拟特性使得它成为描述无干扰的另一个有力工具^{[31, 32]}.特别地, 利用进程代数的验证工具, 可以很容易地对基于进程代数描述的无干扰属性进行验证.然而需要指出的是, 3种不同的无干扰模型, 即Rushby建立的无干扰模型^[25]、Meyden和Eggert等人建立的无干扰模型^{[26, 30]}以及Ryan和Focardi等人建立的无干扰模型^{[31, 32]}, 三者之间两两语义不等价.这意味着基于进程代数^{[31, 32]}的无干扰属性验证算法和工具对于状态机形式^{[25, 26, 30]}的无干扰属性验证并无任何帮助.

在国内, 无干扰模型在可信计算领域受到了广泛关注, 应用在包括可信测评^[33]、信任链可信^{[22, 34]}、进程可信^[23]和终端隔离^[24]等在内的众多领域.但是如前所述, 由于没有有效的无干扰属性验证算法, 上述工作中采用状态机作为工具的工作几乎都只能停留在理论分析层面而难以实用^[22-24].为了解决可实践的验证问题, 当前国际上的主流方法^{[35, 36]}是基于Rushby的展开定理(unwinding theorem)^[25], 利用公理语义, 结合定理证明器进行属性验证.但定理证明器的证明时间相对于实时要求而言并不可控, 并且有可能无法给出证明, 因而这类方法也无法应用在实时可信防护领域.

1.3 基于系统调用的安全防护

系统调用在检测异常行为方面具有较好的特异性, 早期的系统调用主要应用在入侵检测领域, 研究人员通过考察系统调用序列切片(不考虑参数)或者系统调用参数集合关系(不考虑系统调用自身)与预期标准的差异来判定一个进程是否被入侵, 代表性方法如文献[37]等.这类方法在早期开启了系统调用在入侵检测领域的新应用, 但这些方法大多只考虑了系统调用的语法特征, 而并未考虑其语义规律, 因而有较大的局限性.之后, 研究人员尝试综合考虑系统调用或者API的语法和语义, 以图、状态机、马尔科夫链、机器学习等作为工具对进程行为进行研究, 取得了较为丰硕的成果^[38-43].现阶段, 采用系统调用方法的研究困难和热点在于, 底层系统调用与上层应用之间存在着语义断层(semantic gap), 仅仅从系统调用本身无法与上层应用行为之间建立映射, 从而必须具体问题具体分析, 尚没有一种较为通用的方法或者框架解决这个问题^{[38, 41]}.

系统调用与无干扰模型的结合很少见, 主流工作中相近的是Calvin等人^[44]基于无干扰实时检测和防御TOCTTOU(time-of-check-to-time-of-use)竞争条件攻击, 其核心思想在于构建语义等价、但执行顺序不同的系统调用序列以消除竞争条件.多数情况下, 这种构建是困难的, 文献[44]也未提及构建方法(算法), 因此, 我们认为更多的是理论意义^[44].不同于文献[44], 由于前期我们找到了无干扰属性基于状态等价的充要条件^[45], 因而为系统调用与无干扰模型相结合、对软件行为进行实时无干扰属性验证探索了一条可能的道路.

1.4 携带证明的代码

携带证明的代码PCC(proof carrying code)亦可以对代码可信性进行验证.PCC框架^[46]由代码提供者CP (code producer)和代码使用者CC(code consumer)两部分构成.其中, CP必须为其提供的代码提供一个安全证明(safety proof), 该安全证明实质上是CP对CC所规定的安全策略(safety policy)的形式化描述.CC在运行CP所提供的代码之前, 会先用证明验证器对CP提供的安全证明进行验证:如果验证通过, 则说明安全策略得到了遵守, 从而CP所提供的代码是可信的, 可以安全地在CC上执行; 否则, 代码不可信, CC拒绝代码的执行.

PCC为代码的可信执行建立坚实理论基础, 但应用到实时可信度量领域还存在如下难点需要解决.

(1) PCC破坏了已部署代码的兼容性.PCC框架中, CP在根据安全策略编写了形式化规范之后, 需要将原应用和形式化规范一起重新打包编译生成新的、包含形式化规范的二进制代码^[47], 我们称其为PCC风格的二进制代码.显然, 若采用PCC架构进行软件实时可信度量, 则度量平台上所有的应用(即代码)都必须重新编译以形成PCC风格的二进制代码, 否则, 应用无法通过平台验证, 进而无法运行.这意味着如果采用PCC架构, 则必然会破坏已部署应用的兼容性.

(2) PCC安全策略编写代价较大.由于不同应用所使用的编程语言以及语言的安全特性等存在差异, 使得难以构造一个统一、标准的形式化规范.换句话说, 每一个应用的CP都需要单独提供其应用所对应的形式化规范.当安全策略发生变化, 例如当发生网络安全事件进行应急响应时, 每个应用的形式化规范必须要对应更新, 并重新编译生成新的PCC代码.这大大增加了安全策略规范编写、维护和更新的代价.

与PCC相反, 本文的方法不存在上述问题:(1)从兼容性的角度, 由于本文的方法不需要代码自身携带安全证明, 因而无需对应用做任何改动, 从而对已部署应用的兼容性没有任何影响; (2)从安全策略规范角度, 本文的方法以所有应用所共用的系统调用为对象来构造安全策略.通用情况下, 使用者可以基于系统调用建立适用于所有应用的统一、标准的安全策略规范; 在此基础上, 对于特定应用的特定需求, 亦可以建立与其一一对应的特殊的安全策略规范.当安全策略发生变化时(如前述网络安全事件应急响应时), 只需要更新适用于所有应用的统一、标准的安全策略规范即可.与PCC相比, 本文的方法大大减小了安全策略规范编写、维护和更新的代价.然而, PCC方法也有其优势, 例如PCC的度量粒度可以更细, 且已发展出坚实的理论基础和较多的工具, 如何尝试解决PCC的前述两大难题, 以结合PCC和本文的方法进一步提升本文方法的理论基础和可实践性, 是一个值得研究的工作, 但这超出了本文的研究范围.

2 理论基础 2.1 无干扰模型定义

无干扰的思想最早由Goguen和Meseguer^[29]提出, 其基本思想是:一组用户G_A, 使用一组命令集合C操作之后, 如果对另一组用户G_B所能观察到的结果没有影响, 则称用户组G_A对用户组G_B是无干扰的.既然G_B无法感知G_A的操作, 那么也就无法从G_A的操作中逆推出任何信息, 从而也就防止了G_A和G_B之间的隐通道信息流传输.文献[29]解决了困扰BLP的隐通道问题, 但只能处理传递信息流, 对于非传递信息流是无法处理的.例如, 不失一般性, 假设某个涉密系统中划分有文件域u_f、加密机域u_e和网络域u_n这3个安全域.如果我们用$ \rightsquigarrow $和$\not \rightsquigarrow $分别表示允许和不允许信息在安全域之间的流动, 则此涉密系统中机密文件的传输方式可以表示为$({u_f}\not \rightsquigarrow {u_n}) \wedge $ (u_f$ \rightsquigarrow $u_e$ \rightsquigarrow $u_n).其含义是:机密信息不能直接传输到网络${u_f}\not \rightsquigarrow {u_n}$, 而必须首先流经加密机加密u_f$ \rightsquigarrow $u_e、再由加密机将加密后的密文发送到网络进行传输u_e$ \rightsquigarrow $u_n.换句话说, u_f只能通过加密机中介u_e间接地将信息传递到u_n.直觉地, 对于这种信息流非直接(间接)流动的情形, 我们称其为非传递信息流, 文献[29]无法对其进行处理

随后, 众多研究人员对非传递信息流情况下的无干扰模型进行了深入研究, 但是直到Rushby才首次提出完全正确的非传递无干扰模型^[25].由于传递无干扰只是非传递无干扰的一个特例^[25], 因而本文中我们以一般性的非传递无干扰模型为基础, 研究如何构建可实践的软件实时度量和防护方法.以下若没有特殊说明, 则文中的无干扰模型均特指非传递无干扰模型, 且文中所有的定义均特指在非传递安全策略前提下.

定义1. 无干扰模型定义.一个系统M可以用一个状态机表示, 其包含如下元素.

(1) 状态机S, 其中包含一个唯一的初始状态s₀.

(2) 一个原子动作集A, 其中包含了所有的原子动作.

(3) 一个行为集B, 其中包含了所有由原子动作的连接所构成的行为.如果用∘表示原子动作的连接, 则一个行为的示例是α=a₀∘a₁∘…∘a_n, 其中, $ {a_i}_{(0 \le i \le n)} \in A $.

(4) 一个输出集O, 其中包含了所有利用原子动作所观察到的输出结果.

(5) 一个安全域集D, 其中包含了系统中所有的安全域.

(6) 干扰关系$ \rightsquigarrow $和无干扰关系$\not \rightsquigarrow $, 分别表示信息授权/禁止在两个安全域之间流动, 两者互为补集.

(7) 动作-安全域映射函数dom:A→D.返回每一个原子动作a∈A所属的安全域dom(a).

(8) 单步状态变迁函数:step:S×A→S, 描述了系统M的单步状态变迁.

(9) 多步状态变迁函数:multisteps:S×B→S.如果用Λ表示空动作, 则multisteps可以右递归表示为

$\left\{ {\begin{array}{*{20}{l}} {multisteps(s, \varLambda )\; = \;s} \\ {multisteps(s, a \circ \alpha ) = \;multisteps(step(s, a), \alpha )} \end{array}} \right., $

其描述了系统M从状态s∈S执行行为(即多个原子动作序列)α=a₀∘…∘a_m∈β之后所到达的新状态.

(10) 行为结果函数(behavior consequence):behcon:S×A→O, 给出了系统M在某个状态s∈S, 外界利用动作a∈A所能观察到的结果o∈O.

约定使用…, s, t, …表示系统状态, 约定使用α, β, …表示行为(原子动作序列), 使用u, v, …表示安全域.

定义2. 结构化机器M.结构化机器M包含如下部分.

(1) 存储单元集N.机器的每一个存储单元都有一个独一无二的名字, 所有这些名字的集合构成存储单元集N, 又叫名字集N.存储单元包含寄存器单元、内存单元、外存单元、缓存等.

(2) 值集V.当状态一定的时候, 每一个存储单元都有一个具体的值v.所有存储单元值的集合构成值集V.

(3) 内容函数contents:S×N→V.内容函数返回在状态s∈S, 名字n∈N的值v∈V.

(4) 观察函数observe:D→${\mathcal{P}}$(N).观察函数给出安全域u∈D所能观察的名字集合.这里, ${\mathcal{P}}$是幂集计算.

(5) 修改函数alter:D→${\mathcal{P}}$(N).修改函数给出安全域u∈D所能修改的名字集合.这里, ${\mathcal{P}}$是幂集计算.

定义1中的原子动作粒度可大可小, 可以是输入(input)、函数调用(API或者syscall)、命令(command)或者机器指令(instruction)等^[25].当执行原子动作之后, 机器从一个状态变迁到里另外一个状态.根据结构化机器假设, 机器M的状态由M中的所有存储单元取值构成.存储单元包括寄存器(registers)、内存单元(memory)或者磁盘扇区(disk)等.上述存储单元有一些是不可观察的(如内部存储单元), 有一些是暴露给观察者的; 有一些是只读的, 有一些是可读可写的; 有一些是遗失性的, 有一些是非遗失性的, 等等, 所有这些存储单元的取值情况决定了机器M的当前状态.在实践中, 用户可以根据实际需要, 基于定义1、定义2, 将实际系统与机器M一一对应起来.

定义3. $\mathop \sim \limits^u $是等价关系, 当且仅当同时满足输出一致性和弱单步一致性.

(1) 输出一致性:$s\mathop \sim \limits^u t \supset behcon(s, a) = behcon(t, a)$.

(2) 弱单步一致性:$dom(a) \rightsquigarrow u \wedge s\mathop \sim \limits^{dom(a)} t \wedge s\mathop \sim \limits^u t \supset step(s, a)\mathop \sim \limits^u step(t, a)$.

本文全文遵从文献[25], 约定使用⊃表示蕴含关系, 使用→定义函数.

定义4. 引用监视器假设RMA(reference monitor assumption).RMA由如下3条假设构成.

(1) 假设1:$s\mathop \sim \limits^u t\;{\bf{iff}}\;\forall n \in observe(u).contents(s, n) = contents(t, n)$.其含义是:两个状态等价$s\mathop \sim \limits^u t$, 当且仅当它们的存储单元都具有相同的值.假设1保证了定义3中的输出一致性.

(2) 假设2:$s\mathop \sim \limits^u t$∧[contents(step(s, a), n)≠contents(s, n)∨contents(step(t, a), n)≠contents(t, n)]⊃contents(step(s, a), n)=contents(step(t, a), n).其含义是:如果两个状态等价$s\mathop \sim \limits^u t$, 则当它们使用相同的动作修改某个存储单元时, 必须保证该存储单元被修改为同样的值.

(3) 假设3:contents(step(s, a), n)≠contents(s, n)⊃n$ \rightsquigarrow $alter(dom(a)).其含义是:若动作修改了某a个存储单元的值, 则安全域dom(a)必须拥有对该存储单元修改授权.

定义5. 干扰源集interfsrcs:B×D→${\mathcal{P}}$(D).干扰源集的递归定义为interfsrcs(Λ, u)={u}, 且

$interfsrcs(a \circ \alpha , u) = \left\{ {\begin{array}{*{20}{l}} {\{ dom(a)\} \cup interfsrcs(\alpha , u), {\rm{ if }}\;\exists v.v \in interfsrcs(a, u) \supset dom(a) \rightsquigarrow v} \\ {interfsrcs(\alpha , u), {\rm{ }}{\rm{otherwise}}} \end{array}} \right..$

干扰源集的含义是:抽取所有对u有(直接或间接)干扰关系的安全域形成(干扰源)集合.

定义6. 弱预期函数wexpected:B×D→B.其递归定义为wexpected(Λ, u)=Λ, 且

$wexpected(a \circ \alpha , u) = \left\{ {\begin{array}{*{20}{l}} {a \circ wexpected(\alpha , u), {\rm{ if }}\;dom(a) \in interfsrcs{\rm{(}}a \circ \alpha , u{\rm{)}}} \\ {\varLambda \circ wexpected(\alpha , w), {\rm{ otherwise}}} \end{array}} \right..$

弱预期函数的含义是:将所有对u有(直接或间接)干扰关系的动作保留, 并将除此以外的所有动作删除, 从而得到在非传递无干扰安全策略控制下的预期行为.

定义7. 域集等价关系$\mathop \approx \limits^C :s\mathop \approx \limits^C t{\rm{ }}\;{\bf{iff}}\;{\rm{ }}\forall u \in C.s\mathop \sim \limits^u t.$

定义8. 局部无干扰属性:$dom(a)\not \rightsquigarrow u \supset s\mathop \sim \limits^u step(s, a).$

2.2 基于无干扰的可信性判定

根据文献[25], 一个信息系统满足无干扰, 当且仅当如下判定等式(1)成立.

定义9. 无干扰判定等式:

$ \forall \alpha \forall a.behcon(exec({s_0}, \alpha ), a) = behcon(exec({s_0}, wexpected(\alpha , dom(a))), a) $

(1)

关于什么是“可信”, 国际上可信计算组织TCG将其定义为:(1)完整性; 或(2)行为符合预期; 国内有专家指出:(3)可信≈可靠+安全.形式上, 等式(1)对这些“可信”的定义均可以进行解释.

(1) “完整性”的定义

等式(1)的左边表示行为α的实际执行结果, 右边表示在完整性策略控制下, 行为wexpected(α, dom(a))的理论执行结果.如果等式成立, 则表明真实执行结果与完整性策略控制下的执行结果一致, 换句话说, 当前的执行是符合完整性策略的.因而完整性没有遭到破坏.

事实上, 利用无干扰研究和解释完整性是完全可行的.我们曾询问文献[31]的作者Ryan是否可以利用无干扰研究完整性, Ryan回复指出:“利用无干扰研究完整性是完全可行的.唯一的细微差别在于, 完整性无干扰模型可能需要一个更弱一点的形式化:对于安全性/机密性必须确保低(low)安全等级观察者不能够推断出任何高(high)安全等级的信息; 而对于完整性很可能不需要担心高(high)完整性等级能够推断出低(low)完整性等级的信息, 只要低完整性等级信息不能干扰高完整性等级信息即可”.

(2) “行为符合预期”的定义

类似的, 等式(1)的左边表示行为α的实际执行结果, 右边表示在安全策略控制下, 行为wexpected(α, dom(a))的理论执行结果(预期执行结果).如果等式成立, 则表示真实执行结果与预期执行结果一致.换句话说, 机器M是以预期的方式朝着预期的目标在执行, 因而是可信的.

(3) “安全性(机密性)”的定义

这是无干扰模型提出的本义, 因而自然成立.

综上所述, 对于“可信”的几种主流定义, 等式(1)均可以给予解释.我们认为, 无干扰模型是研究可信的一个非常合适的数学工具.

接下来的困难在于如何将无干扰模型应用于实时动态系统.Rushby曾明确指出了无干扰模型所面临的挑战^[25]:一是寻求有效(efficient and effective)的无干扰属性自动化验证算法, 二是探索无干扰模型的实际应用.本质上, 这两个问题可以归结为第1个问题.因此, 虽然无干扰模型非常适用于可信研究, 但是要真正应用于实时动态度量和防护, 就必须解决无干扰属性的自动化验证问题.幸运的是, 我们在文献[45]中找到了一种与等式(1)等价、以状态递归形式表达、可靠且完备的无干扰表达形式(参见如下定理2)解决了这个问题.详细说明如下.

定理1(无干扰属性验证展开定理^[25]). 如果机器M满足如下属性, 则机器M是满足无干扰的, 或者说可信的.

(1) 输出一致属性:$s\mathop \sim \limits^{dom(a)} t \supset behcon(s, a) = behcon(t, a){\rm{.}}$

(2) 弱单步一致属性:$s\mathop \sim \limits^{dom(a)} t \wedge s\mathop \sim \limits^u t \wedge dom(a) \rightsquigarrow u \supset step(s, a)\mathop \sim \limits^u step(t, a){\rm{.}}$

(3) 局部无干扰属性:$dom(a)\not \rightsquigarrow u \supset s\mathop \sim \limits^u step(s, a), $

证明:参见文献[25]定理7.

Rushby将等式(1)看作一个状态机, 利用归纳法证明了定理1所示的展开定理.在文献[45]中, 我们将等式(1)的左右两边看作两个状态机, 分别称为等价自动机EMA(equivalent machine’s automaton)和弱预期等价自动机WEMA(weakly equivalent machine’s automaton).不失一般性, 假设左右两个状态机的状态集分别是S和T, 则等式(1)中的EMA和WEMA将从相同的初始状态s₀=t₀(s₀∈S∧t₀∈T)出发, 分别执行行为α以及安全策略控制下的行为β=wexpected(α, dom(a)).利用EMA和WEMA, 可以证明定理1的3条属性的数学本质是:EMA和WEMA在同步执行的过程中, 总是保持状态等价的^[45].该数学本质可以形式地表达为定理2.

定理2(无干扰(或者说可信)的状态递归定义^[45]). 机器M是满足无干扰的, 或者说可信的, 当且仅当:

$\forall {i_{(0 \leqslant i \leqslant N)}}.{s_i}\mathop \approx \limits^{I{S_{{\gamma _i}}}} {t_i} \supset {s_{i + 1}}\mathop \approx \limits^{I{S_{{\gamma _{i + 1}}}}} {t_{i + 1}}$

(2)

证明:参见文献[45]的定理3.

定理2中的符号含义如下.

(1) N:对于任意行为γ, N是γ中原子动作的个数.例如, 不失一般性, 设α=a₀∘a₁∘…∘a_m, 则γ中共有m个原子动作, 故N=m.

(2) γ_i(0≤i≤N):对于任意行为γ, 随着机器M对γ中原子动作的不断执行, 用γ_i表示剩下的行为, 称为“执行子行为串”(参见文献[45]的定义16), 并令γ₀=γ, γ_N=Λ.例如, 不失一般性, 设α=a₀∘a₁∘…∘a_m, 则有:初始时, γ₀=γ=a₀∘a₁∘…∘a_m; 当机器M执行原子动作a₁后, 有γ₁=a₂∘…∘a_m; …; 当机器M执行a_m-1后, 有γ_m-1=a_m; 当机器M执行a_m后, 有γ_m=γ_N=Λ.

(3) $I{S_{{\gamma _i}}}$:如果用w表示等式(1)中的dom(a), 即w=dom(a), 则为了书写简单起见, 文献[45]中约定$I{S_{{\gamma _i}}} = interfsrcs({\gamma _i}, w)$, 即$I{S_{{\gamma _i}}}$的含义是:所有对w=dom(a)有直接或者间接干扰的安全域构成的集合.

(4) s_i和s_i+1:s_i表示EMA的当前状态, s_i+1表示EMA从当前状态s_i执行γ_i=a_i+1∘…∘a_m中的第1个原子动作a_i+1之后到达的新状态, s_i+1=step(s_i, a_i+1).

(5) t_i和t_i+1:t_i表示WEMA的当前状态, t_i+1表示WEMA从当前状态t_i执行β_i=wexpected(γ_i, w)中的第1个原子动作之后到达的新状态t_i+1.由公式(4)中的γ_i=a_i+1∘…∘a_m, 根据定义6, 当dom(a_i+1)$ \rightsquigarrow $interfsrcs(γ_i, w), 即dom(a_i+1)对w=dom(a)有直接或者间接干扰时, β_i=wexpected(γ_i, w)的第1个原子动作为a_i+1, 此时t_i+1=step(t_i, a_i+1); 否则, 若dom(a_i+1)∉interfsrcs(γ_i, w), 即dom(a_i+1)对w=dom(a)没有任何干扰时, β_i= wexpected(γ_i, w)的第1个原子动作为Λ, 此时t_i+1=step(t_i, Λ)=t_i.

综上, 定理2(公式(2))的含义是:机器M是无干扰的, 或者说可信的, 当且仅当EMA和WEMA两个状态机在同步运行的过程中, 总是在对w=dom(a)(参见等式(1))有直接或者间接干扰的安全域上保持状态等价的.

定理2是无干扰成立的可靠和完备性条件.限于篇幅, 其证明思想简单说明如下.

(1) 可靠性证明

递归展开公式(2), 有:${s_0}\mathop \approx \limits^{I{S_{{\gamma _0}}}} {t_0} \supset \;...\; \supset {s_n}\mathop \approx \limits^{IS{\gamma _n}} {t_n} \supset {s_{n + 1}}\mathop \approx \limits^{I{S_{{\gamma _{n + 1}}}}} {t_{n + 1}}$.既然${s_{n + 1}}\mathop \approx \limits^{I{S_{{\gamma _{n + 1}}}}} {t_{n + 1}}$成立, 由IS(文献[45]的定义14)和执行子行为串定义(文献[45]的定义16)立即可得:${s_{n + 1}}\mathop \sim \limits^w {t_{n + 1}}$.对${s_{n + 1}}\mathop \sim \limits^w {t_{n + 1}}$利用输出一致性有:behcon(s_n+1, a)=behcon(t_n+1, a)(dom(a)=w).再根据EMA和WEMA的定义代入s_n+1和t_n+1, 有公式(1)成立, 故M满足无干扰.可靠性得证.

(2) 完备性证明

完备性证明采用反证法.根据引用监视器假设, 机器M的状态具体表现为其名字集的取值.因此, EMA和WEMA状态等价, 本质上等价于EMA和WEMA对应名字集的取值相同.再注意到某个名字的值发生变化时, 是由该名字当前本身的值加上当前对其进行干扰的名字的值共同决定的.综合以上两点, 要保证EMA和WEMA在w上的状态等价关系, 就必须要保证EMA和WEMA在同步运行的过程中, 在所有那些对w有直接或者间接干扰的安全域上总是保持状态等价的, 亦即当EMA和WEMA到达任意状态对(s_i, t_i)时, 必须在$I{S_{{\gamma _i}}}$上是保持状态等价的, 此即公式(2).否则, 就一定可以构造一个恶意子行为${\gamma '_i}$, 使得当M从状态s_i出发执行${\gamma '_i}$后, EMA和WEMA最终在w上不等价, 从而导致公式(1)不成立, M不满足无干扰属性, 矛盾!完备性得证.

更详细的证明请参见[45]的定理3.

接下来以一个例子说明定理2的含义及应用.假设某个涉密系统中划分有输入域u_i(input)、过滤域u_f (filter)、加密机域u_e(encryption)和网络域u_n(network)共4个安全域.系统安全策略是:从输入域u_i接收所有的输入, 经过滤域u_f过滤识别出敏感信息, 再经加密域u_e的加密机加密, 最后将加密后的密文经网络域u_n传出, 输入域u_i和过滤域u_f禁止直接向网络传输信息.安全策略可以表达为:${u_i} \rightsquigarrow {u_f} \rightsquigarrow {u_e} \rightsquigarrow {u_n} \wedge {u_i}\not \rightsquigarrow {u_n} \wedge {u_f}\not \rightsquigarrow {u_n}.$

再令安全域u_i, u_f, u_e和u_n中发出的动作分别用a_i, a_f, a_e和a_n表示.不失一般性, 假设有如下动作序列(即行为):α=a_i1∘a_f1∘a_i2∘a_e∘a_f2, 则根据安全策略计算WEMA中的对应行为β=wexpected(α, u_n), 由定义6可得:β=a_i1∘a_f1∘Λ∘a_e∘Λ.根据定理2, 行为α是否可信的自动化验证过程如图 1所示.图 1中的圆圈表示状态, 圆圈之间的箭头表示引发状态变迁的动作, 圆圈之间的虚线表示EMA和WEMA同步执行的过程.

对α=a_i1∘a_f1∘a_i2∘a_e∘a_f2的可信性验证过程如下.

(1) 首先, EMA和WEMA两者从相同的初始状态s₀=t₀出发同步运行.

根据定理2的符号解释:

● 对EMA:此时, α₀=α=a_i1∘a_f1∘a_i2∘a_e∘a_f2.EMA执行首个动作a_i1之后, 从状态s₀变迁到状态s₁, 并将继续执行子行为α₁=a_f1∘a_i2∘a_e∘a_f2.

● 对WEMA:此时, β₀=β=a_i1∘a_f1∘Λ∘a_e∘Λ.WEMA执行首个动作a_i1之后, 从状态t₀=s₀变迁到状态t₁, 并将继续执行子行为β₁=a_f1∘Λ∘a_e∘Λ.

计算$I{S_{{\alpha _0}}} = interfsrc({\alpha _0}, {u_n}) = \{ {u_n}, {u_e}, {u_f}, {u_i}\} , I{S_{{\alpha _1}}} = interfsrc({\alpha _1}, {u_n}) = \{ {u_n}, {u_e}, {u_f}\} $.将$({s_0}, I{S_{{\alpha _0}}}, {t_0})$和$({s_1}, I{S_{{\alpha _1}}}, {t_1})$分别代入公式(2)的左边和右边, 如果公式(2)的前件和后件均成立(事实上, 只需要代入$({s_1}, I{S_{{\alpha _1}}}, {t_1})$验证后件即可, 因为s₀=t₀故前件总是成立), 则转到步骤(2)继续递归验证; 否则, 如果公式(2)不成立, 则说明行为不可信, 报警.

(2) 其次, 继续根据公式(2)递归验证行为是否可信.

● 对EMA:此时, α₁=a_f1∘a_i2∘a_e∘a_f2.EMA执行动作a_f1之后, 从状态s₁变迁到状态s₂, 并将继续执行子行为α₂=a_i2∘a_e∘a_f2.

● 对WEMA:此时, β₁=a_f1∘Λ∘a_e∘Λ.WEMA执行动作a_f1之后, 从状态t₁变迁到状态t₂, 并将继续执行子行为β₂=Λ∘a_e∘Λ.

计算$I{S_{{\alpha _2}}} = interfsrc({\alpha _1}, {u_n}) = \{ {u_n}, {u_e}\} $.将$({s_1}, I{S_{{\alpha _1}}}, {t_1})$和$({s_2}, I{S_{{\alpha _2}}}, {t_2})$代入公式(2)的两边, 如果公式(2)的前件和后件均成立(事实上, 只要代入$({s_2}, I{S_{{\alpha _2}}}, {t_2})$验证后件即可, 因为本次验证的前件即上一验证步骤的后件, 故而本次验证的前件一定是成立的), 则转到步骤(3)继续递归验证; 否则, 如果公式(2)不成立, 则行为不可信, 报警.

(3), (4)然后, 继续根据公式(2)验证行为是否可信.

在步骤(3)和步骤(4), 依次计算并代入“$({s_2}, I{S_{{\alpha _2}}}, {t_2})$和$({s_3}, I{S_{{\alpha _3}}}, {t_3})$”以及“$({s_3}, I{S_{{\alpha _3}}}, {t_3})$和$({s_4}, I{S_{{\alpha _4}}}, {t_4})$”到公式(2)进行验证即可.限于篇幅, 具体过程从略.

(5) 最后, 对于最后一个动作a_f2, 继续根据公式(2)验证其运行之后行为是否可信.

● 对EMA:此时, α₅=a_f2=a_f2∘Λ.EMA执行动作a_f2之后, 从状态s₄变迁到状态s₅, 并将继续执行子行为α₆=Λ.

● 对WEMA:此时, β₁=Λ=Λ∘Λ.WEMA执行空动作Λ, 状态保持不变s₄=s₅, 并将继续执行子行为β₆=Λ.

计算$I{S_{{\alpha _5}}} = interfsrc({\alpha _1}, {u_n}) = \{ {u_n}\} $.将$({s_4}, I{S_{{\alpha _4}}}, {t_4})$和$({s_5}, I{S_{{\alpha _5}}}, {t_5})$代入公式(2)的两边, 如果公式(2)的前件和后件均成立(事实上, 只需要代入$({s_5}, I{S_{{\alpha _5}}}, {t_5})$验证后件即可, 原因同上), 则EMA和WEMA在同步执行的过程中总是保持状态等价的, 因而可以立即判定行为α=a_i1∘a_f1∘a_i2∘a_e∘a_f2是可信的; 否则行为不可信, 报警.

示例结束.

由于传递无干扰是非传递无干扰的特例, 对于传递无干扰, 定理2可以简化为推论1.

推论1(传递无干扰的状态递归定义). 在传递无干扰安全策略下, 机器M是满足无干扰的, 或者说可信的, 当且仅当:

$\forall {i_{(1 \leqslant i \leqslant N + 1)}}.{s_i}\mathop \sim \limits^w {t_i}$

(3)

其中, w=dom(a)是定义9中观察动作a所属的安全域.

证明:根据传递无干扰安全策略定义, 所有对w发生干扰的安全域, 无需通过任何中间(intermediate)媒介安全域, 即可直接对w进行干扰.这意味着无需保证EMA和WEMA在中间安全域(公式(2)中$I{S_{{\gamma _i}}}$和$I{S_{{\gamma _{i + 1}}}}$)上的状态等价性, 只要确保两者总是在w上等价即可.故公式(2)可简化为$\forall {i_{(0 \leqslant i \leqslant N)}}.{s_i}\mathop \approx \limits^w {t_i} \supset {s_{i + 1}}\mathop \approx \limits^w {t_{i + 1}}$, 即

$\forall {i_{(0 \leqslant i \leqslant N)}}.{s_i}\mathop \sim \limits^w {t_i} \supset {s_{i + 1}}\mathop \sim \limits^w {t_{i + 1}}$

(4)

注意到, 如下公式(5)和公式(6)是公式(4)前后相继的两次验证, 且公式(6)的前件正好是公式(5)的后件.

${s_i}\mathop \sim \limits^w {t_i} \supset {s_{i + 1}}\mathop \sim \limits^w {t_{i + 1}}$

(5)

${s_{i + 1}}\mathop \sim \limits^w {t_{i + 1}} \supset {s_{i + 2}}\mathop \sim \limits^w {t_{i + 2}}$

(6)

再注意到, 只有公式(5)验证通过之后, 才会验证公式(6).这意味着当验证公式(6)时, 其前件必然成立, 故而对公式(6), 只需要验证后件即可.

考察公式(4), 令j=j+1, 其后件下标满足1≤j≤N+1, 故只需要验证${s_1}\mathop \sim \limits^w {t_1}, ..., {s_{(N + 1)}}\mathop \sim \limits^w {t_{(N + 1)}}$即可.

此即公式(3), 推论1得证.

3 方法及实现 3.1 基本思想

大多数攻击都需要两个步骤:首先, 定位可利用的漏洞; 其次, 通过漏洞执行攻击代码(称为shellcode).只要打断以上环环相扣的两个步骤中的任何一步, 即可以有效防御攻击.本文从第2步入手, 建立在如下观察之上:几乎所有的shellcode都必须通过系统调用达成攻击.由此, 一旦检测到系统调用序列的语义破坏了定义9的等式(1), 即可以认定破坏了系统的可信性.

图 2给出了基于无干扰理论的软件实时可信防护方法, 包括3部分.

(1) 预期行为规范EBS(expected behavior specification).

预期行为规范基于系统调用编写, 描述了进程的预期行为, 即进程预期可以可以做什么, 或者预期不可以做什么.EBS的说明和示例请分别参见第3.3节和附录.

(2) 每一个进程绑定一个预期行为规范EBS.

所绑定的EBS描述了该进程的预期行为, 并且EBS放置在内核中.注意:在原型实验中, 我们默认内核是可信的, 因而将EBS放置在内核中可以保护其完整性.

需要指出的是, 内核完全有可能是不可信的, 但如何确保内核可信超出了本文的研究范围.对于内核不可信情况下保证EBS完整性的可能方法有:采用现有的技术对内核进行加固^{[7, 8, 18-21]}, 从而增强内核中EBS的完整性; 或者将EBS放置在TPM安全协处理芯片、TrustZone的安全世界等类似硬软件安全架构中, 保证EBS的完整性.

(3) 安全增强的内核实时监测软件行为是否偏离预期.

安全增强后的内核, 对每个进程实时捕获其系统调用, 并依据定理2(推论1)实时判定进程的行为是否偏离了预期(即EBS), 由此发现各类复杂攻击(如新型的ROP攻击以及传统的多态、混淆、变形和编码攻击等), 理论上也可以识别未知攻击(因为即使是未知攻击, 绝大多数情况下也需要执行shellcode, 而只要shellcode的行为偏离了EBS, 即可以被捕获).

根据文献[25], 构成进程行为的原子动作可以是输入(input)、命令(command)、机器指令(instruction)等任意可以被机器所执行的内容.本文选择系统调用作为原子动作, 并以Linux操作系统作为原型环境.系统调用、EBS和机器M这三者之间的关系如下:系统调用作为原子动作, 其执行导致机器M发生状态变迁; EBS作为安全策略, 描述了系统调用所属安全域之间的干扰/无干扰关系; 在此基础上, 软件动态执行是可信的, 当且仅当在EBS的控制下, 其系统调用执行满足推论1所示的充要条件.

3.2 进程系统调用所属安全域之间的无干扰关系

根据根据Linux手册, 基于不同的功能, Linux系统调用可以分为如下8类^[48], 分别是:(1)进程控制类(u₀); (2)文件系统控制类(u₁); (3)系统控制类(u₂); (4)内存管理类(u₃); (5)网络管理类(u₄); (6)网络Socket控制类(u₅); (7)用户管理类(u₆); (8)进程间通信类(u₇).这8类系统调用可以看作8个不同的安全域, 分别用u₀~u₇表示.由于系统调用之间的功能隔离关系(操作系统内核设计决定了系统调用的功能划分不会存在耦合关系, 否则会导致非预期行为), 这8个安全域之间是互相无干扰的, 形式地:$\forall i\not = j.{u_i}\not \rightsquigarrow {u_j}_{(0 \leqslant i, j \leqslant 7)}$.这意味着安全策略由复杂的非传递安全策略退化为简单的传递安全策略, 因而在判定软件真实行为与EBS之间是否存在偏差时, 只需要使用推论1即可, 这大大简化了行为可信验证算法的时间复杂度(参见第3.5节).需要指出的是, 这种简化具有一般性, 因为其是由系统调用所属安全域之间的无干扰关系决定的.

3.3 基于系统调用的EBS编写

限于篇幅, 附录给出了本文所采用的一种EBS编写形式作为示例.事实上, 如何编写和对应解析EBS, 并不限于示例1所示的方法, 可以由使用者自己决定, 只要基于系统调用刻画软件预期行为即可.

EBS具有如下特点.

(1) EBS可以采用无干扰信息流安全策略$\not \rightsquigarrow $, 也可以采用干扰信息流安全策略$ \rightsquigarrow $.由无干扰模型定义可知, 两种安全策略本质上是等价的.经验表明:一般情况下, 推荐使用$\not \rightsquigarrow $安全策略, 因为这可以得到复杂度更低的EBS.

(2) EBS描述了软件预期的行为, 与具体攻击行为无关.因此, 任何攻击, 包括Zero-Day攻击在内, 理论上只要导致软件行为偏离了预期, 仍然可以被本文方法度量到.

(3) EBS有两种类型:一是适用于平台所有软件的通用EBS; 二是绑定于特定软件、满足特定安全需求的特殊EBS.两种EBS可以同时使用.当两种EBS同时存在的情况下, 特殊EBS优先级高于通用EBS优先级, 增加了灵活性.

3.4 系统调用实时获取

接下来, 需要实时捕获被监控进程的系统调用(含参数)行为并与EBS进行对比, 以判定进程的运行是否偏离了预期行为.方便起见, 本文原型实验通过ptrace实现:将PTRACE_PEEKUSER作为ptrace的第1个参数进行调用, 即可以实时取得与待度量进程相关的系统调用信息.其中,

(1) EAX当中存储的是系统调用的索引号, 亦即指明了具体的系统调用.

(2) 在32位架构中, 当系统调用参数的个数小于5个时, EBX, ECX, EDX, ESI, EDI当中依次存储着系统调用所有的参数; 当系统调用参数的个数大于5个时(这种情况不多见), EBX指向一块内存区域, 这个区域中就依序存放着系统调用的所有参数.

(3) 在64位架构当中, %rdi, %rsi, %rdx, %r10, %r8, %r9依次存放着系统调用参数信息.

3.5 实时可信性验证

第3.2节说明, Linux系统调用的8个安全域之间互相无干扰, 即$\forall i\not = j.{u_i}\not \rightsquigarrow {u_j}_{(0 \leqslant i, j \leqslant 7)}$.因此任何两个安全域之间都无法利用第三安全域作为中间安全域(intermediate domain)来间接传递信息, 这本质上退化为传递无干扰, 故使用推论1来对进程u_p的实时可信性进行验证.推论1可以表述为如下验证算法1.

算法1. 进程u_p实时可信度量(验证)算法.

1.任意时刻, 实时获取进程u_p的本次系统调用, 不失一般性, 假设为本次执行的系统调用为a.

2.遍历EBS, 计算原子动作a在EBS安全策略控制下的预期执行动作β=wexpected(a, w).根据wexpected(·)的定义, 最终有β=a(EBS安全策略预期允许执行a)或者β=Λ(EBS安全策略预期不允许执行a).

3.如果β=a, 则进程真实执行与预期执行一致(真实执行动作和预期执行动作都是a, 两者执行之后状态一致, 故在EBS关注的w上等价), 根据推论1, u_p执行a后可信, 转步骤1;如果β=Λ, 则进程真实执行与预期执行不一致(真实执行动作a, 预期执行空动作Λ, 两者执行之后导致状态空间不一致, 故在EBS所关注的w上不等价), u_p执行a后不可信, 报警.

算法1结束.算法1只需要在每次系统调用a执行时, 判定a是否被EBS安全策略所允许即可, 因而其时间复杂度为O(1).

4 实验评估

实验平台采用TOSHIBA笔记本电脑, CPU Intel i5 2.5G, 内存Samsung 8G.操作系统Linux Fedora, 内核版本2.6.43.8-1.fc15.i686.PAE.实验测试了在ROP攻击以及传统代码多态、代码混淆、代码变形和代码编码等对抗形式下对攻击行为的可信度量功能.表 1给出了实验结果.

表 1显示, 本文的方法可以检测到ROP(return-oriented programming)攻击.ROP代表了现代攻击的发展趋势, 其不寻求注入代码, 而是从已有的“干净代码”中寻找合适的“指令片段”(gadget), 通过“ret或者与ret语义等价的指令”将前述指令片段链接形成完整的攻击代码, 以达成攻击目的.ROP可以高度自动化地构造图灵完全的攻击, 危害巨大.为此, 研究人员提出了多种对抗方法^[49-53], 取得了长足的进展.早期的ROP防御侧重于检测可疑的ret指令, 但没有处理与ret语义等价的指令(如jmp/pop等)^[49], 对ROP的防御是不完全的.随后的工作实现了对各类ROP攻击的全覆盖, 其基本思想在于消除ROP指令片段, 或者检测并阻止(ROP指令片段所导致)的非法间接跳转.但这些方法均需要额外的条件, 如, 需要被保护应用的非直接跳转指令和地址^[50], 或者被保护应用的指令片段IG(instruction & gadget)信息^[51]; 需要硬件的特殊功能^[52]; 需要特殊的编译器^[53]; 需要对受保护应用进行重写^{[50, 53]}等等.不同于这些工作, 本文的方法基于如下观察:ROP是一种代码重用方法, 其本身并不能达成攻击, 而仍然要通过调用敏感系统调用来实现恶意功能.因此, 通过度量应用程序系统调用与EBS规范的偏离可以发现基于ROP技术所发起的攻击.严格来说, 本文方法并不能检测ROP攻击本身, 这是与文献[49-53]相比的不足之处.但从另外一个角度, 在面向大量商业应用和通用度量平台的一般情况下——此时可能难以进行预处理(因而难以获得应用本身的信息^{[50, 51]}), 不一定具备特殊硬件和软件(因而不一定满足特定功能的CPU^[52]和编译器^[53]要求), 且不一定能够进行代码重写(如开启了完整性度量架构IMA), 本文的方法可以作为上述方法的补充, 结合应用.

对于表 1中余下的4种经典攻击代码对抗方法, 实验结果表明亦可以有效度量.从实验结果还可以发现, 通过分析和抽取已有shellcode的特征, 利用较少的EBS规范(实验中采用了7条主要EBS规范), 就可以覆盖主要的攻击流程和大量的攻击代码, 实现对软件可信性的实时度量, 这表明方法是高效的.

表 2对实时度量的时间负载进行了分析.实时度量所引起的时间负载由两部分构成:一是捕获系统调用及其参数所花的时间t₁; 二是分析系统调用是否偏离了EBS安全策略所花的时间t₂.t₂主要是字符串比较等指针操作, 时间相对较快, 大致取t₂≈t₁.再假设在未进行实时度量时(no real-time measurement)软件的运行时间为T_NRM= t₀, 则进行实时度量时(real-time measurement)软件的运行时间为T_RM=t₀+t₁+t₂≈T_NRM+2×t₁, 此时, 可求时间负载ζ为如下等式(7), 故只要得到t₁/t₀即可.

$ \zeta=T_{R M} / T_{N R M}=1+2 \times t_{1} / t_{0} $

(7)

利用time命令和strace命令, 可以立即求出T₀=t₀以及T₁=t₀+t₁, 两者相比有:

$ t_{1} / t_{0}=T_{1} / T_{0}-1 $

(8)

将等式(8)代入等式(7), 即得ζ.

注意, time命令会给出3种时间.

(1) 真实时间(real):软件从开始执行到结束执行的时间.

(2) 用户CPU时间(user):软件在用户态花费的CPU时间.

(3) 系统CPU时间(sys):软件在内核态花费的CPU时间.

那么对应可以定义T_r0, T_r1; T_u0, T_u1; T_s0, T_s1.由于真实时间包含了软件由于等待如I/O等资源的挂起时间, 其意义不大, 一般关注后两者(后两者之和user+sys给出了软件运行的真实CPU时间), 则等式(7)和等式(8)可以对应改写如下.

$ \zeta = \left( {{\zeta _u} + {\zeta _s}} \right)/2, {\zeta _u} = 1 + 2 \times {t_{u1}}/{t_{u0}}, {\zeta _s} = 1 + 2 \times {t_{s1}}/{t_{s0}} $

(9)

$ {t_{u1}}/{t_{u0}} = {T_{u1}}/{T_{u0}} - 1, {t_{s1}}/{t_{s0}} = {T_{s1}}/{T_{s0}} - 1 $

(10)

表 2给出了T_u1/T_u0和T_s1/T_s0的实验结果.

取平均时间比, 将T_u1/T_u0=5.05和T_s1/T_s0=5.58代入等式(9), 有t_u1/t_u0=4.05以及t_s1/t_s0=4.58;再代入等式(8), 立即可得:ζ_u=9.1, ζ_s=10.16, ζ=9.63.因此在实时度量时, 一般情况下, 用户时间负载ζ_u约为9.10倍, 系统时间负载ζ_s约为10.16倍, 总体时间负载ζ_s约为9.63倍.

以上各类时间负载总体约为10倍, 但这已经本方法所能达到的接近最优结果, 且实际测试表明, 该负载并不影响用户的实际使用体验.原因如下.

(1) 实验所选取的测试数据是接近最坏情况下的测试数据.本文方法对系统调用进行捕获和度量, 对其他函数和指令则不做任何处理, 显然, 被测试代码中系统调用相关代码所占的比例越高, 则对时间负载影响越大.注意到shellcode正好满足上述特征:考虑到存储空间, shellcode会尽可能短小精干, 去除冗余指令以调用系统调用完成攻击功能.换句话说, 系统调用相关代码所占比例高.因此, 本文直接选择shellcode代码为测试对象, 所得的10x时间负载约为最坏情况下的结果.一般情况下, 测试结果表明, 时间负载会介于1.6x~10x之间.

(2) 前面已说明, 时间负载由两部分构成:捕获系统调用和参数的t₁以及分析系统调用是否偏离EBS的t₂, 且取t_2≈t₁.实验中, 为方便起见, 使用strace命令获取系统调用和参数信息(strace仍然基于ptrace实现).由于strace是Linux标准命令, 因此t₁可以认为是优化后的最优结果, 从而基于表 2所计算到的时间负载ζ_u, ζ_s和ζ也可以认为是接近最优的结果.

(3) 以用户交互性强的应用为测试对象表明, 本文方法所引起的时间负载并不影响用户使用感受.以Firefox为例, 利用“time strace firefox”命令启动火狐浏览器并浏览文本、图片和视频等各类网页, 统计时间信息并计算可得:若将real time视作1, 则user time约占23%, sys time约占8%, 即陷入内核CPU的运行时间(sys time)仅仅约占8%, 由于内核CPU时间(sys time)由系统调用和非系统调用时间两部分构成, 因而实际捕获系统调用和参数信息的时间不到8%.

根据测试结果, 上述时间占比不影响用户使用感受.

5 结论

运行时可信度量是可信计算有待解决的一个关键问题, 本文提出了一种基于无干扰的软件实时可信度量方法, 尝试为可信度量的理论构建和实践应用提供一种新的思路.选择无干扰模型是因为研究表明:无干扰模型可以以一种统一的形式描述“行为符合预期、完整性和机密性”等不同的主流“可信”定义, 从而可以在统一的框架下对不同内涵的可信性进行研究.在此基础上, 给出了行为可信性的实时判定算法(时间复杂度O(1)), 解决了无干扰模型难以应用于实时系统的难题.针对理论的实践应用问题, 根据无干扰模型的定义, 选择系统调用作为基本原子动作, 将软件真实行为定义为原子动作的序列, 并根据系统调用所属安全域之间的无干扰关系定义预期行为规范EBS.最后, 通过判定软件真实行为与预期行为之间是否存在偏差, 实现对软件行为的实时可信度量.原型实验证明了本文方法的有效性.

后续的研究拟从如下几个方面入手:一是探索如何结合人工智能技术自动抽取恶意代码样本特征并形成预期行为规范库; 二是研究适用于实时或者准实时环境的漏洞定位技术; 三是研究移动智能终端、物联网等环境下的实时可信度量和防护问题.

附录. EBS编写示例

攻击者在定位漏洞之后, 往往会执行一些通用攻击操作, 以达成进一步攻击目的, 这些通用攻击操作包括(但不限于)生成shell、开启反向连接、清空防火墙规则、关闭地址空间布局随机化ASLR等等.针对这些攻击, 这里给出部分EBS示例如下:

1. EBS规范1:预期不能生成shell.

FOR INDEX==2:{1==“bin/bash”∨1==“bin/sh”∨1==“bin/tcbash”∨1==“bin/csh”∨1==“bin/dash”∨}

u_[i][j]的下标分别是i, j, 其表明:i是安全域u_i的编号, j是u_i中子安全域编号.因此, 这里u_[i][j]=u_[0][0]的含义是u₀安全域中的第1个子安全域.类似的, 如果是u₁安全域中的第3个子安全域, 则表示为u_[1][2].

回到u_[0][0]={2}, 查阅[48]可知, u₀安全域为进程控制类系统调用, 其中, 编号2对应execve, 故u_[0][0]={2}= {execve}.再结合FOR INDEX==2:语句的参数安全策略, 由于execve的第1个参数是字符串类型, 指明了要运行的二进制文件名, 因此规范1的含义是:进程u_p预期不能运行/bin目录下的bash, sh, tcsh, csh和dash文件以开启shell.

解释:攻击者突破系统之后, 一般需要开启shell以进一步执行命令.规范1度量并禁止了这种行为.需要说明的是:Linux的shell并不只有上述5种类型(规范1是根据实验者机器的配置情况编写的), 使用者可以根据实际安全需求容易地更新规范1.

2.规范2:预期不能开启非法监听端口连接或者不能进行反向连接.

${u_p}\not \rightsquigarrow {u_{[5][0]}} = = \{ 2,3\} $

FOR INDEX==2:{2→sin_port!=PORT_LIST₁}

FOR INDEX==3:{2→sa_family==AF_INET, 2→sin_port==PORT_LIST₂, 2→sin_addr==IP_LIST}

规范2的含义是:进程u_p预期对子安全域u_[5][0]无干扰.查阅文献[48]可知, u₅中2和3号系统调用分别为bind和connect.进一步查阅bind和connect参数信息, 两者的第2个参数均是常量结构体指针const struct sockaddr*, 该结构体的内部元素sa_familiy指明了协议族; sin_port指明了端口号; sin_addr指明了远程连接的IP地址.结合FOR INDEX==2:语句的参数安全策略可知, 进程u_p预期对所有不在端口列表PORT_LIST₁当中的端口都不能开放监听.类似地, 结合FOR INDEX==3:语句的参数安全策略可知, 进程u_p预期不能对端口列表PORT_LIST₂和地址列表IP_LIST中的机器发起远程连接.

解释:攻击者突破系统之后, 往往会开启受害机器监听端口监听外部连接, 以方便进一步入侵.为此, 规范2的安全策略预期进程u_p不会开启必要端口(即PORT_LIST₁中列出的端口)之外的任何端口, 从而能够度量并禁止攻击者非法开启监听端口的行为.另一方面, 在内网中, 由于防火墙的存在, 外网机向内网机的连接会触发警报.此时, 攻击者往往会从受害的内网机向外网特定机器发起反向连接.规范2度量并禁止了这种反向连接(反弹端口)行为.

3.规范3:预期不能清空防火墙规则.

FOR INDEX==2:{1==/sbin/iptables}∧{2==[“/sbin/iptables”, “-F”]}

规范3的含义是:进程u_p预期对子安全域u_[0][1]无干扰.由于规则1中u_[0][0]和这里u_[0][1]均是来自于u₀的子安全域, 因此两者赋予不同的编号j=0和j=1.类似地, 查阅文献[48]可知:规范3表明, 进程u_p预期不能带参数“-F”执行/sbin/iptables文件以清空所有防火墙规则.

解释:规范3度量并禁止了清空防火墙规则行为.

限于篇幅, 这里给出3个EBS示例.

根据我们的分析结果, 大多shellcode的代码有很强的功能重合性.换句话说, 绝大多数shellcode的恶意功能都局限于生成shell、开启反向连接、清空防火墙规则、关闭地址空间布局随机化ASLR、修改/etc/passwd文件、提升权限和重启等, 只是其机器码形式或者对抗手段(多态、混淆、变形和编码)不一致.在我们的实验中, 通过提炼这些重合功能, 只需要不到10条通用EBS, 即可检测到大多数shellcode, 表明了方法的有效性.