0 引言

云服务通过虚拟化技术^[1]对底层计算、网络、存储资源进行封装,在给远程租户提供各类资源、实现资源有效利用的同时也存在着巨大的安全威胁。云服务目前面临的安全威胁主要来自两个方面：一方面是共享资源的安全威胁^[2]；另一方面是特权安全威胁。其中共享资源的安全威胁源于云服务的资源共享特性^[3]。云服务的资源共享是通过虚拟化技术在同一个物理节点上运行多个虚拟操作系统实现的,可以提高资源的利用率。但由于资源共享,恶意用户可以绕过逻辑边界从而威胁云用户的安全。特权安全威胁则是由云服务外包特性产生的，在云环境中管理员可以对用户在云端的数据、信息等资源产生安全威胁。

针对服务的安全问题,在云环境中引入可信计算技术,建立云服务的主动可信监控机制,是一个有效的解决方案^[4]。Santos等^[5]在2009年首次提出“可信云”的概念,并设计了 可信云服务计算平台(Trusted Cloud Computing Platform,TCCP),平台通过可信计算模块(Trusted Platform Module,TPM)构建可信虚拟运行环境,并为远程用户提供系统可信验证。类似的方案^[5-6]在此基础上作了不同程度的改进，但此类方案主要保证了传统PC平台的静态可信。由于云服务的多域虚拟化环境,很难实现实时、动态的可信度量。周振吉等^[7]提出了一种树形可信度量模型(Tree Style Trust Measurement,TSTM),以实时完整性度量的方式判断用户域的系统行为可信。Zhang等^[8]则提出了一种基于无干扰理论的可信域层次模型(Trust Domain Hierarchical Model,TDHM),并给出了可信域行为可信的形式化描述以及证明,实现了虚拟机间的安全隔离与系统可信。

这些方案有效地推进了云服务可信的快速发展。但由于云环境的复杂性,在底层资源之上通常运行着管理域与大量用户域,域的可信度量难以实时、准确。其次在管理域上的监控与信任度量机制对用户域也存在着特权的安全威胁,因此还需要增加更加安全高效的安全机制来保证云服务的安全可信。

针对上述问题,本文提出了基于无干扰理论的云服务可信模型(Non-Interference Cloud service Trust Model,NICTM)。

1 基于无干扰理论的云服务可信模型

可信计算组(Trusted Computing Group,TCG)对可信的定义是计算平台状态是否可信,体现为其行为是否符合预期策略^[9]。因此,云服务的状态可信受各域的行为影响。但在实际应用中由于状态的无限性,度量每一个行为状态是不可行的,因此将对用户域系统状态的可信评价转化为对历史行为的信任评价,那么对于一个云服务系统任意一个状态的可信判定可以这样描述:

定义1 状态S可信满足以下条件(云服务系统可信判定条件)：

1) 从任意一个可信状态S₀开始；

2) S₀可以通过一系列状态转移到达状态S；

3) 状态转移序列是可信的。

以上定义为充分条件,可作为可信判定的依据。该定义完全符合TCG对系统可信的定义。

1.1 无干扰理论

信息流的无干扰思想最早由Goguen和Mesguer提出^[10],无干扰理论可以这样理解:通过引入一个“清除”函数f将动作运行序列中与一个特定域有关的无干扰的所有动作全部“清除”,只保留有干扰的动作,然后观察输出结果,判断是否有超出预期的域间干扰。无干扰模型定义了一种安全关系,并提供了系统安全的验证方法,可以保证系统的安全性。

1.2 基本符号定义

本文借鉴了文献^[8]的无干扰模型,并借用其中定义的符号。同TDHM相比,本模型简化了相关的抽象层次,把域、可信域、客户主机的多层抽象服务简化成从进程到域的抽象,模型仅过滤云服务系统中进程间以及用户域之间的干扰,可以减少相关的系统时间开销;同时,采用建立监控域的方式,以及拦截系统调用的方法实现模型,可以有效地解决特权级的安全威胁。下面给出模型的定义符号。

定义2 云服务系统M=(S,D,A,O,P)应包含如下元素:

S:M的状态集合,用s₁,s₂,…,s_n表示,s₀表示初始状态。

D:域的集合,用户程序在域内运行,用d₁,d₂,…,d_n表示。

A:动作集合表示用户域所发出的动作，用a₁a₂…a_n表示,α₁α₂…α_n表示动作序列。

O:输出结果集合,由于系统由用户域组成,所以输出结果实际上是域集合的输出结果。

P:域内进程集合,用p₁,p₂,…,p_n表示。

P^*：系统执行的进程序列,用ρ₁,ρ₂,…,ρ_n表示。

定义3 函数集。

1) 域到进程的映射函数。 f_dcomp:D×A→P，取得执行动作的进程。

2) 动作转换函数。 f_deact:S×A→D×P,将动作分解为域的进程执行。

3) 动作响应函数。 f_sstep:S×D×A→S，表示经过一个动作后系统进入下一个状态； f_soutp:S×D×A→O，得到动作的返回结果。

4) 动作序列函数。 f_dstep:S×D×A^*→S，表示经过一个动作序列之后状态的转移； f_doutp:S×D×A^*→O，经过动作序列之后的输出结果。

令“Λ”表示空的动作，“º”表示连接符，则根据以上定义以下各式成立:

f_dstep(s,d,Λ)=s

f_dstep(s,d,a)= f_sstep(s,f_deact(s,a))

f_dstep(s,d,aºα)= f_dstep(f_sstep(s,d,a),d,α)

f_doutp(s,d,aºα)= f_soutput(s,d,a)∪f_doutput(s,d,α)

定义4 二元关系集合,包含:

1) 域间等价关系“$\cong $”。表示域间的等价关系,如s₁$\cong $s₂表示由监控域,观察系统M的状态s₁与s₂是等价的。

2) 干扰关系“~>”。干扰关系具有自反性,当p₁~>p₂时,可得出p₂~>p₁;反之，则用p₁>p₂表示进程间无干扰，d₁~>d₂表示域间存在干扰关系。

2 模型描述

模型研究了可信的相关定义,给出了域的可信条件,描述在云服务过程中用户域可信的条件，并证明符合条件的用户域是可信的。

定义5 对于∀d∈D,p∈P和α∈A^*,清除函数f_delete(d,α):D×A^*→A^*,p∈d可以定义为：

f_delete(d,Λ)=Λ

$\begin{align} & {{f}_{delete}}(d,a\circ \alpha )= \\ & \left\{ \begin{matrix} a\circ {{f}_{delete}}(d,\alpha ) & {{f}_{dcomp}}(d,a)\sim >p\parallel {{f}_{dcomp}}(d,a)\sim >d \\ {{f}_{delete}}(d,\alpha ) & A \\ \end{matrix} \right. \\ \end{align}$

其他

由于干扰关系表明域间存在干扰,但无干扰理论关注的是非预期的干扰,因此引入清除函数的目的是清除动作序列中预期的、正常的干扰,通过比对清除前后的动作序列判断是否存在潜在的域间、进程间的干扰关系。

若用户域d行为可信,则满足

f_soutp(f_dstep(s,d,α),a)= f_soutp(f_dstep(s,f_delete(d,α)),a)

该定义完全符合TCG对可信的定义。

系统从一个初始状态s₀开始运行经过一系列动作α后到达状态f_dstep(s,d,α),此时由监控域发出一个动作a,观察系统状态,若经过清除函数的验证,无法区分两者的状态则不存在潜在的进程以及域间干扰，说明域d及其内部进程是可信的。

定义6 观察等价性。云服务系统的观察等价性,对于云服务的监控域而言,由监控域观察系统状态,若s₁$\cong $s₂则表示由监控域观察云服务系统状态s₁与s₂是等价的。

定义7 结果隔离性。对于云服务的用户域,若满足如下条件则称为满足隔离性。对用户域d有:

s₁$\cong $s₂ ⇒ f_soutp(s₁,d,a)= f_soutp(s₂,d,a)

等价状态下,域执行相同的动作,会产生相同的输出。

引理1 若云服务系统具有观察等价性以及结果隔离性的域d若满足以下条件,则域d行为可信。

${{f}_{dstep}}(s,d,\alpha )\cong {{f}_{dstep}}(s,{{f}_{delete}}(d,\alpha ))$

(1)

证明 因为有

f_dstep(s,d,α)$\cong $f_dstep(s,f_delete(d,α));

s₁$\cong $s₂ ⇒ f_soutp(s₁,d,a)= f_soutp(s₂,d,a)′

所以

f_soutp(f_dstep(s,d,α),a)= f_soutp(f_dstep(s,f_delete(d,α)),a)

满足域的可信条件。证毕。

隔离性表明域在运行过程中内部的进程间相互隔离,且域间的信息流也是隔离的。

定义8 无干扰隔离性。当

f_dcomp(d,a)>d ⇒ s$\cong $f_sstep(s,d,a)

定义9 单步隔离性。当

s₁$\cong $s₂ ⇒ f_sstep(s₁,d,a)= f_sstep(s₂,d,a)

由以上定义可推导得出域行为可信的定理。

定理1 域行为可信的定理。一个用户域,当其满足结果隔离、无干扰隔离和单步隔离性质，则这个域是可信的。

证明 设域d满足以上性质,则须证明满足

${{s}_{1}}\cong {{s}_{2}}\Rightarrow {{f}_{dstep}}({{s}_{1}},d,\alpha )\cong {{f}_{dstep}}({{s}_{2}},{{f}_{delete}}(d,\alpha ))$

(2)

对序列α作数学归纳：

当α=Λ时式(2)显然成立。

设动作序列α的长度为n时式(2)也成立,那么当动作序列α的长度为n+1时,有α₂=αºa,代入式(2)。

左式f_dstep(s₁,d,α):

$\begin{align} & {{f}_{dstep}}({{s}_{1}},d,{{\alpha }_{2}})={{f}_{dstep}}({{s}_{1}},d,\alpha \circ a)= \\ & {{f}_{dstep}}({{f}_{sstep}}({{s}_{1}},d,a),d,\alpha ) \\ \end{align}$

(3)

右式 f_dstep(s₂,f_delete(d,α)):

f_dstep(s₂,f_delete(d,α₂))= f_dstep(s₂,f_delete(d,αºa))

分类讨论：

情况1

1) f_dcomp(d,a)~>p‖f_dcomp(d,a)~>d

由清除函数定义可知：

f_dstep(s₂,f_delete(d,αºa))= f_dstep(s₂,aºf_delete(d,α))

由函数性质可得：

f_dstep(s₂,aºf_delete(d,α))= f_dstep(f_sstep(s₂,a),f_delete(d,α))

由单步隔离性可知：

${{f}_{sstep}}({{s}_{2}},a)\cong {{f}_{sstep}}({{s}_{1}},a)$

(4)

又由前提假设有：

${{f}_{dstep}}({{s}_{1}},d,\alpha )\cong {{f}_{dstep}}({{s}_{2}},{{f}_{delete}}(d,\alpha ))$

(5)

因此可得f_dstep(s₁,d,α₂)$\cong $f_dstep(s₂,f_delete(d,α₂))。

情况2

由清除函数定义可得:

f_dstep(s₂,f_delete(d,αºa))= f_dstep(s₂,f_delete(d,α))

由域的无干扰隔离性质s$\cong $f_sstep(s,d,a)。

综上:由于有s₁$\cong $s₂以及s₂$\cong $f_sstep(s₁,d,a)，所以:

f_dstep(f_sstep(s₁,d,a),d,α)= f_dstep(s₂,f_delete(d,α))

化简得：

f_dstep(s₁,d,α₂)$\cong $f_dstep(s₂,f_delete(d,α₂))

综合1)~2)可知，当序列长度为n+1时,式(2)成立,通过数学归纳可知对于任意长度的序列,式(2)都成立。证毕。

定理1给出了符合无干扰理论模型的云服务系统中用户域可信的条件:

1) 域间的信息流是无干扰的,不存在潜在的域间干扰行为；

2) 域内的进程是可信的,不会产生进程间的干扰；

3) 云服务系统是由多个用户域构成的。

因此需要相关机制保证,使用户域达到上述的可信条件,以实现云服务系统的可信。

3 模型整体架构

图 1给出了基于无干扰理论模型的云服务可信度量系统的整体架构,模型基于特权分离的思想将监控域与特权域相分离,仅使用监控域监控各个用户域的行为，避免特权域利用其特权以及监控行为对各用户域的安全产生影响。

模型利用传统的可信启动技术,以硬件TPM为可信根,通过链式度量的方法确保系统在启动时,初始状态s₀的安全可信。模型通过事件截获机制以及虚拟机自省^[11]技术,实现对用户域的监控，并验证相关的动作行为是否符合无干扰理论所构建的安全策略。

3.1 事件截获

本文基于文献^[12]中的虚拟化技术以及使用事件截获机制截取系统调用^[13]。具体工作流程如下:

1) 位于监控域的事件截获模块关闭用户域d_i的直接系统调用,修改调用相关的寄存器指针SYSENTER_CS_MSR以及SYSENTER_EIP_MSR为非法地址,因此由非法地址返回后,系统会陷入缺页异常，从而达到拦截系统调用的目的。

2) 用户域触发系统调用,产生缺页异常,在具有虚拟机监视器(Virtual Machine Monitor,VMM)的虚拟机系统中,会对系统发出VMexit指令,陷入VMM层,同时拦截此次调用并通过寄存器判断系统调用内容。

3) 保存用户域系统当前状态的快照,并暂停当前用户域的活动,通过语义重构的方式还原用户域内进程的相关信息。

4) 执行监控流程后返回正确的调用地址,使进程恢复到原本的运行状态,使流程继续正常执行。

实现用户域的行为监控,确保各用户域之间满足无干扰理论的要求,确保域间的隔离效果,并通过分析用户域内的进程分析,确保进程间的无干扰。

3.2 虚拟机自省

监控域可以通过内存拷贝技术从外部获取虚拟机内部信息,也就是虚拟机自省,监控域可以获取所监控的用户域中的数据信息,并且同时保证域间的隔离,由于这种域间通信是合法且高效的，不会对系统产生额外的域间干扰而影响系统的安全性,通过验证各用户域的数据可以完整描述系统当前状态s,以及监控云服务系统中的状态变化。

监控域调用管理域d₀的虚拟机自省组件来获取用户域d_i内部数据。具体流程如下:

1) d₁发出获取用户域d_i内核数据的请求；

2) 自省组件利用Libxc库映射被监控域的相关内存信息；

3) 利用SYSTEM.Map读取进程控制的初始地址,之后获取内存数据机器页框号,并指定将用户域d_i的内存信息向监控域内存块进行映射的参数。

由于Xen虚拟机的特点,利用机械地址映射(Physical To Machine,P2M)表实现由虚拟地址到物理地址再到机器地址的映射,并且使用内存拷贝函数memcopy将机器地址所存的数据拷贝到监控域内存中。

基于上述步骤,监控域可以有效地监控各用户域的运行状态、进程序列及动作行为,并判断是否符合理论模型的安全要求。

综上所述,模型通过可信启动技术,保证了云服务平台的初始状态s₀的安全可信,并采用事件截获与虚拟机自省的技术实现对系统状态s的描述,监控整个云服务系统中各用户域的内部进程以及域间动作,确保不存在违反模型设计安全规则的行为。即:各域的进程内部无干扰,各域之间不存在非法干扰。确保系统动作行为序列的完整可信，最终保证云服务系统的可信。模型完全符合定义1(云服务系统可信判定条件)对系统可信的定义。

4 测试及结果分析

本文基于Xen虚拟机建立了NICTM模型的原型系统,实验主要测试NICTM在发现潜在干扰以及系统可信验证的有效性，同时测算相关系统开销。实验的硬件环境如表 1所示,软件平台如表 2所示。

4.1 有效性测试

与典型的Xen虚拟化平台和树形可信度量模型TSTM以及TDHM进行比较,选取三种有代表性的恶意软件,KnarkRootkit、hxdef、adore-ng进行有效性测试。KnarkRootkit、adore-ng为Linux内核级rootkit,hxdef为Windows NT的内核级rootkit，本文用来验证NICTM的有效性。

将恶意软件分别投入纯虚拟化平台装有TSTM安全模型的系统,以及本文提出的NICTM的系统中运行。具体的实验结果如表 3所示。

从表 3可看出传统的虚拟化平台的安全性不足,完全不能防范各类内核级rootkit的攻击；同时TSTM这类基于代码完整性度量安全模型,可以有效检测出系统自检时的恶意软件,但对运行过程中、进程以及各个域间的信息流的渗透攻击发现得不够及时；而实验中,当三类恶意软件恶意篡改内核组件、传递域间非法信息时,立刻被NICTM模型发现并判断为非法的域间干扰,具有较强的实时性，能有效提高云服务环境下虚拟化平台的安全性。

4.2 性能实验

为了评估NICTM模型对系统性能的影响,通过对系统调用的运行进行性能实验。

测试中选取有代表性的lmbench作为测试用例,lmbench库覆盖了常用的系统调用操作,可以较为有效地反映系统开销的真实情况。实验将同样与Xen虚拟化平台以及搭载了TSTM的虚拟化平台进行对比测试,充分测试在各种系统调用的情况下,模型原型系统的搭载对系统开销产生的影响。为了使结果更为可靠,实验采用了较大量的测试用例,实验结果为单个用例调用开销的平均值(见表 4)。

表 4给出了NICTM模型在各种测试用例下系统时间开销的测试结果。通过比较可以发现,与无搭载原型系统的平台相比,模型普遍存在一定的开销,主要体现在系统监控过程中,对域间及域内进程等信息流的监控过程,系统的运行所产生的硬件开销,但在测试中可看出,在系统调用过程中包括null、open/close等对系统信息流影响不大,且较为常用的系统调用过程中,模型所产生的系统开销主要出现在系统调用拦截、内存定位与拷贝的过程中,因此与TSTM类似,在fork类的操作过程中会产生较大的系统开销。但与直接频繁计算文件hash值的TSTM模型相比,基于无干扰理论的NICTM模型在系统性能方面有着一定的提升。同时由于减少了抽象层次和系统监控,其性能相对于TDHM也有着一定的提升。

5 结语

本文将传统的无干扰理论引入到云服务环境中去,并结合可信计算技术,以保证云端服务环境的安全性。

针对云服务环境下远程虚拟平台的特点与安全需求,主要是云服务环境存在的特权以及资源共享型安全威胁，本文提出了一种适用于云服务条件下的云服务可信模型NITCM,基于特权分离的思想,将特权域与监控域分离,避免因为管理权限而存在的特权安全威胁。同时本文基于无干扰理论,将云服务环境中的各项元素进行抽象,并且相对于TDHM,抽象层次更少,系统开销更小,实现更加简单,之后借用了进程代数的思想,形式化地证明了本模型的安全性,设计的模型完全符合云服务可信系统的安全定义。

最后利用事件截获机制与域间拷贝技术在XEN平台上实现了模型的原型系统,经过实验验证了模型的可行性,且模型相对传统的完整性度量模型TSTM以及TDHM有一定的性能提升。