云计算具有资源高度集中、动态可扩展、外包服务等特点,使得用户丧失了对数据及资源的可见性与可控性,信任问题凸显.根据埃森哲的调研报告显示,用户对云服务缺乏信任是拒绝使用云服务的重要因素^[1].云平台作为云服务的重要载体,如何对云平台安全展开分析与评价,使用户能够信任云服务提供商以及其所提供的云平台,是云计算推广和普及的关键因素之一.

学术界对于信任与可信的含义存在不同的理解,国际标准化组织与国际电子技术委员会以及TCG均从行为的可预测性或预期性来定义可信^[2,3];IEEE CS可信计算与容错技术委员会(IEEE Computer Society Technical Committee on Dependable Computing and Fault Tolerance)从可信赖角度来描述可信性,强调系统的可靠性与可用性^[4];文献^[5]提出了可信≈安全+可靠的学术观点,提出可信性必须综合考虑系统的可靠性、可用性、主体行为与信息的安全性.上述定义与描述中,文献^[3]的定义难以进行定性与定量的分析,文献^[4]偏向于系统可靠性描述,而文献^[5]综合考虑了可用、可靠与安全多方面的影响.结合近年来云服务出现的服务故障事故,这其中既有安全事故的发生,例如CSDN云数据中心隐私泄露事件以及sony网络受云平台攻击事件,还包括一些服务设计缺陷而导致的可靠性事故,例如亚马逊云服务大面积中断事故,因此我们认为:文献^[5]的学术观点较能符合云平台的特点,只有对可用属性、可靠属性和安全属性等多项属性进行综合的分析研究,才能对云平台可信性进行更准确的评价.

目前已经有了一些对云环境进行建模分析的方法,并发现了部分安全问题^[6,7],这些研究为进一步实现云平台的安全增强方案提供了理论指导与现实基础.但总结来看,现有的对于云平台的建模与分析方法存在以下问题和挑战:

· 目前,云平台可信性的定义以及其所包含的内容尚不完善的,这就导致了目前的分析方法大多缺乏明确的分析目的、适用范围与分析依据;

· 现有的大部分分析方法仅关注安全性分析,且在云环境中提及的安全性更多是数据与隐私安全^[8-11],不能分析发现因平台设计或执行缺陷导致的故障.根据文献^[5]中对可信的描述,对安全性的分析仅仅是可信性的部分体现,不能充分让用户信任云平台;

· 目前,对于云环境的建模方法,通常以进程代数^[6]、图论^[7]或贝叶斯网络^[11]为基础,建立的大多是对于云环境的静态描述模型,不能体现平台提供服务时的状态变化过程,不适用于对可信性中,可用与可靠等动态属性的分析.

针对上述问题,本文在结合云平台特点的基础上,首先定义云环境的可信性,并明确其包括的具体内容,以明确本文的分析依据、范围以及目的;随后提出一种云平台建模方法,以标记变迁系统(LTS)为语义描述工具,模型建立过程依赖于云平台的组件,以便完整反映用户使用云服务时组件的交互过程以及系统的状态变迁过程;最后,通过模型分析检测工具对平台可用性、环境稳定性以及组件的安全约束能力等可信性属性进行定性和定量的验证,进而实现在实际部署时做出相应的安全应对,尽可能减少云平台故障发生的可能,提高云环境的可信性.

本文的主要贡献在于较为完善地明确了云平台可信性分析内容与评判标准,建立了对平台可信性部分动态属性进行统一综合描述分析的模型,提出的建模方法能够兼顾可用性、可靠性以及安全执行能力等多方面的分析需求,解决了对于可信性中部分属性形式化分析困难的问题.

本文第1节分析国内外相关工作.第2节给出云平台的基本架构与硬件逻辑构成,并对云平台进行抽象描述,还对用户基础服务种类进行抽象划分.第3节首先给出可信性定义,并详细说明本文模型的分析依据、适用范围以及目的;随后,利用LTS相关理论构建语义模型,构建云平台的运行状态模型,并针对其状态空间过于复杂的问题进行约减.第4节结合第3.1节的定义提出分析思路,采用模型分析检测工具Kronos进行可信性分析.第5节总结全文,结合第4节分析得出的隐患,讨论下一步的研究方向.

1 相关工作

在云环境的可信性分析研究方面,文献^[6]利用形式化方法对云环境以及构成云的组件进行形式化描述,从云环境的可用性和安全性方面给出了严格的数学定义和证明;在此基础上,还给出了云环境扩展、限制以及更新的严格定义,为进一步分析奠定了基础.但是文中建立的模型是一种静态描述模型,不适用于对一个动态系统进行可靠性分析.

文献^[12]提出一种云计算模式下的运行环境可信性验证方法,通过引入可信第三方,对云平台的可信性进行远程验证和审计,能够分析发现针对内存和文件系统的威胁.但是内存和文件系统仅是可信性中安全属性的一小部分,方法不能完整反映服务的可信性.

在服务与其依赖平台关联的分析与验证方面,现有的研究大多集中于Web与物联网,其方法都是以进程代数、自动机或Petri网为理论基础构建服务提供时的平台运行模型,并利用模型验证工具对模型进行进一步分析与验证^[13-18].在这些研究中,状态机模型一般是将服务过程映射为对应的形式化描述,特别适用于强调服务提供时平台组件间的交互行为与关系,在动态反映建模对象的行为和过程方面具有优势^[16-18].

文献^[16]提出了Web服务属性分析和验证模型,通过将服务组合进程转换为自动机,并进一步将自动机解释为能被模型检测工具SPIN所接受的输入语言来验证的相关属性;文献^[17]通过扩展自动机的逻辑表达式,加强了对于服务行为的描述,并能够形式化描述服务的消息序列,最终实现服务行为的准确匹配;文献^[18]专注于如何对物联网服务进行建模与分析,通过引入时间自动机,增加了对于时间属性的刻画,将物联网服务行为建模为其与相关平台实体的交互过程,解决了连续性建模与验证的问题.

上述研究都将状态机理论用于Web或物联网的建模与验证,而Web、物联网与云计算的本质都是用户通过网络来使用系统功能,其性质是可类比的,因此,状态机理论也适用于对于云平台的建模与验证.

与相关研究工作相比,本文更关注于如何结合云环境的特点建立对云平台进行动态的模型描述,以便对平台的可信性进行分析与验证.

2 云平台的基础逻辑构成

云平台是一个构造复杂的系统,外部包括数量庞大的用户,内部包含海量的控制、计算与存储实体以及软件,这些实体之间彼此互相关联,依存度极高,对如此之多且关联紧密的实体进行建模是困难且不现实的,因此,首先有必要对实体按照逻辑功能进行划分,并对其进行进一步的抽象.

2.1 云平台的逻辑构成

现有的云平台按其透明度又分为开源和不开源两种.不开源的云环境往往不公开其内部细节^[19],我们无法得知其部署方式与内部结构,因此本文不做讨论.因此,本文的研究重点是以开源项目为基础来进行构建和部署的云平台,例如惠普云以及At&T的Cloud Architect^[20,21].开源云平台包括了基础硬件、虚拟化相关软件、基础设施层管理软件(Eucalyptus,OpenStack以及OpenNebula)^[22-24]以及用户等主要组件,其基础框架与运行过程基本类似,如图1所示.

从逻辑上看,云平台的基础框架主要包括4个主要部分,每一部分都由若干最小功能组件构成:

(1) 接入用户:既包括普通用户(简称租户),又包括云提供商的管理员用户(简称管理员),他们是云平台的管理者和使用者,通过管理中心接入云中,是使用和管理系统资源和功能的主体;

(2) 基础设施层管理中心:既是云对外服务的接口,也是云资源的统一管理、监控和调度中心.标准的云管理中心又包括接入服务器、调度服务器、元数据库以及监控服务器.其中,监控服务器负责监控云环境的运行状态并记录日志,不是提供的云服务的必备组件,因此,在进行建模分析时可忽略这一模块;

(3) 计算资源中心:由逻辑上可管理的物理计算资源组成,是用户管理和使用的虚拟机的宿主机,同时被平台调用.云资源计算中心又包括计算集群控制节点以及控制节点下属的若干台计算节点.在计算节点上,安装虚拟机监控器、虚拟机以及其他应用软件;

(4) 存储资源中心:由逻辑上可管理的物理存储资源组成,这里的存储资源是指用于存储虚拟机模板和用户虚拟机镜像的统一管理存储节点,不用于存储一般性用户数据.一个云资源存储中心同样包括存储集群控制节点以及控制节点下属的若干台存储节点.存储节点上存放的是虚拟机镜像与虚拟机模板.

上述架构既包括了外部用户,又包括了内部控制、计算与存储组件,基本可以很好地刻画云平台运行时的参与主体与客体,具有较好的完备性.

2.2 云平台的抽象描述

基于第2.1节中描述的基本框架与逻辑构成,我们将云平台做如下抽象定义:

定义 1. 云平台是三元组(S,Ob,Op),其中,S代表系统主体集,Ob代表系统客体集,Op代表用户服务功能集.

定义 2. S为系统主体集合,系统主体包括所有管理员用户与普通用户,为了方便表述,下文中将系统主体统称为用户,普通用户统称为租户,记为S=Admins∪Users.

定义 3. Ob为系统客体集合,系统客体为云平台内部的所有组件,记为

  Ob=MC(manage center)∪CRC(Compter Resource Center)∪SRC(Storage Resource Center).

其中,

· MC=LS(login server)∪CS(control server)∪mDB(meta datebase);

· CRC=CN(computer node)∪CCC(computer cluster controller)∪VMMs(virtual machine monitors)∪VMs (virtual machines);

· SRC=SN(storage node)∪SCC(storage cluster controller)∪VMimas(virtual machine images)∪Vmmous (virtual machine moulds).

定义 4. Op是用户服务功能集,包括了系统主体使用云平台的一些基本操作,记为

  Op={Login,Logout,VMapply,VMuse,VMrelease,Ima-Mou-manage}.

· Login,Logout:用户登入与登出云的操作,一般通过主体与接入服务器交互完成;

· VMapply:Users申请资源操作,一般表现为租户申请创建一个新的VM实例;

· VMuse:Users使用资源操作,使用过程包括虚拟机实例的连接使用、启动、暂停、恢复和关闭.由于虚拟机迁移是云的内部操作,不由租户控制和操作,因此在本文中不作考虑;

· VMrelease:Users释放资源操作,一般表现为Users释放销毁一个VM;

· Ima-Mou-manage:用户对于虚拟机镜像或者虚拟机模板的管理操作,包括上传、注册、激活发布与删除.其中,Users有权对镜像进行管理,而Admins负责对于虚拟机模板进行管理.

集合Op包括了从虚拟机模板创建一直到资源释放的全部动作,是一个用户使用资源的完整生命周期,因此具有较好的概括性与完备性.

3 云平台的形式化建模 3.1 云平台的可信性定义

根据云平台的特点,结合IEEE CS可信计算与容错技术委员会的观点、文献^[5]的内容以及我们自己对于可信的理解,我们认为:可信云平台除了提供安全的云计算服务、明确向用户保证隐私和数据的安全外,还必须详细规定平台在可用性、可靠性等方面的属性.因此我们认为,可信性应该包括3个子属性,分别是安全性、可用性以及可靠性.

我们进一步参考云计算安全联盟(cloud security alliance,简称CSA)发布的《云安全指南》^[25]、全国信息安全标准化技术委员会(TC260)制定的安全标准^[26-28]以及云计算发展与政策论坛(3CPP)制定的《可信云服务认证评估方法》和《可信云服务认证评估操作办法》^[29,30],从易于理论分析和可信性评估的角度出发,对安全性、可用性以及可靠性的具体内容给出了详细定义与描述(定义5),并以此作为本文提出模型的分析依据.

定义 5. 可信性={安全性,可用性,可靠性},其中,安全性主要包括密码机制、网络安全、租户数据安全、安全隔离、认证与访问控制策略以及策略执行等,可用性主要包括服务可用与组件负载等,可靠性主要包括健壮性、可控性与故障等级等.

对于定义5中各项属性的含义与解释见表1.

根据我们的理解给出的可信性中有众多属性,仅仅用一个模型就想分析全部内容是困难且不现实的,因此,首先要明确本文建立模型主要针对上述哪些属性进行分析,以便确定分析范围.

在云平台中,对于安全性的大部分属性分析已经较为完善:密码机制是属于密码学的范畴,而网络安全、租户数据安全、安全隔离、认证与访问控制策略均可通过安全协议和访问安全策略并结合管理手段来保障.如何设计这些协议与策略不是本文的研究范围,且对于现有安全协议与安全策略的验证,利用pi演算、BAN逻辑等形式化工具也有了较为成熟的建模验证方法^[31,32],并能够通过这些方法发现一些安全问题,因此,这些属性的分析不是本文研究的重点.

本文着重解决针对云平台的可用性、可靠性以及部分安全属性的建模与分析困难问题,具体包括:策略执行、服务可用、组件负载、健壮性、可控性、故障等级等,这些属性均是云平台在提供服务过程中不同组件的动态执行表现,是云平台可信性的重要组成,目前尚缺乏能够对它们进行统一分析的模型与方法.通过本文提出的方法分析,可以解决目前只能分析云平台部分可信属性的问题,能够为进一步进行可信云评估并构建可信云环境提供重要理论补充.

3.2 建模目的与思路

根据第3.1节中的定义与描述,我们提出本文建模的目的:通过建立模型对云平台可信性中的部分属性进行分析,发现潜在的可信性问题,提出一些解决建议,为后续的云平台可信评估以及进一步构建可信云提供了理论支撑.建模的内容和思路包括:

首先,服务的可用性是用户的基本需求之一,如果云平台提供的某些服务由于设计缺陷不可用,那么一切安全也就无从谈起.因此,实现服务可信的基本前提之一就是保证云环境提供的所有服务都是可用的.在对云平台的具体分析中,我们首先需要明确所有用户都能使用的基础功能以及不同权限用户能够使用特殊功能;在此基础上,对用户与云环境之间的交互过程进行建模,通过建立模型来分析功能的可用性以及不同组件的负载情况.

其次,在安全协议和策略的保障下,用户隐私数据在一定程度上得到了保障,但是用户不仅希望使用的服务是安全的,还希望在任何时刻都能不间断的按需使用服务,这就依赖于系统的可靠性.云平台是一个构造复杂的系统,内部包含海量的控制、计算与存储实体以及大量的系统与软件,用户的任意服务请求都会引发云内部组件的交互,因此,我们还需要对参与用户服务的组件进行建模,并进一步将其整合为系统整体状态变迁模型,进而分析云平台在服务提供中可能存在的性能瓶颈与死锁隐患,并给出容错性建议.此外,我们还需要分析系统组件切换与状态转换过程中的潜在威胁,并根据故障组件的重要程度对可能出现的故障提供等级划分基础.

最后,服务的安全性还和安全策略能否严格正确执行有关.在配置了完善的安全策略之后,这些策略不能被正确的执行,或是相关配置文件本身容易被攻击者篡改,都会对导致信息泄露而引发服务故障.在云平台中,安全策略配置存放在相关组件中并由它们负责执行,因此,我们还需要对这些存放、执行安全策略组件的约束能力进行分析.

3.3 建模目标与约束

基于第3.1节和第3.2节中的内容,我们提出模型建立的目标:建立用户与平台之间以及平台内部组件的动态交互模型,并从可用、可靠以及安全约束能力这3个方面分析其对外提供服务时可能存在的可信性问题.针对以上目标,我们还为本模型设定以下约束.

· 模型是一个抽象的交互模型,刻画了用户服务引发的云内部组件交互过程,但是不对具体的实现细节进行建模;

· 模型必须具有整体性,即,能够反映出云平台逻辑组件之间的关系,不能仅仅只是对云平台的部分组件进行多次独立的描述;

· 模型必须是动态的,能够反映出系统的动态变化,以体现服务的动态性;

· 模型不包括对云平台存在的安全协议和策略本身进行建模,而主要体现执行这些策略和协议的组件的安全约束能力.

3.4 云平台运行状态变迁模型

标记变迁系统是能够用于形式化描述并发系统的可观察行为,成为系统说明与深入研究的可靠工具^[33-35].此外,LTS还能够作为许多进形式化描述语言的语义模型,比如CCS,CSP等.因此,我们采用LTS相关理论刻画建立模型.

3.4.1 LTS相关理论定义

一个标记变迁系统由状态以及带有标记的变迁动作组成,对于任意一个给定的模型,给出原子动作和状态变迁规则,就可以描述出对应的变迁系统.

LTS的相关语法如下所示:

下面给出标记变迁系统的操作语义定义.

定义 6. 标记变迁系统是四元组(S,L,-µ→,s₀):S是非空有限状态集合;L是有限标号(动作)集合,它表示了系统所有的可观察动作,而外部不可观察的内部动作记为特殊标记t;-µ→是S上的二元关系,其中的元素可记为s-µ→s′,s,s′∈S,µ∈L∪{t},表示系统在执行动作µ后,由状态s变迁到s′;s₀是系统的初始状态,且s₀∈S.

标记变迁系统中,还存在一些重要性质,例如迹的相关概念与性质、状态收敛的判定、LTS树的判定等,下面分别给出定义.

定义 7. 迹(traces)是LTS中的重要概念,它表示系统可观察动作所组成的一个有限序列.L上所有迹的集合用L^*表示.迹相关的重要性质有:

(1) Trace(s)={a∈L^*|s=a⇒};

(2) con(a₁,a₂)=a₁×a₂,a₁,a₂∈L^*;

(3) len(a)=|a|,a∈L^*;

(4) after(s,a)={s′∈S|s=a⇒s′};

(5) sub(s,s′)={s′∈S|∃a∈L^*:|s=a⇒s′}.

定义 7 中:性质(1)给出了迹的定义;性质(2)定义了迹的连接表示符号;性质(3)定义了迹的长度表示方法;性质(4)描述了状态改变过程,即状态s经过动作a后到达状态s′;性质(5)描述了动作迹存在性的表示方法,即,L中存在一条由状态s到状态s′的动作迹a.

定义 8. s⇓表示状态s收敛,s,s′∈S,则有:

(1) if s⇓,s⇓e;

(2) if s⇓ and s=µ⇒s′,s⇓µ;

(3) if s-µ→s′,then s⇓,s′⇓.

定义 8(1)说明:如果状态s在不可见动作集上收敛,可得出其在空序列上也是收敛的;定义8(2)说明:如果状态s在空序列的上收敛,且能够经过一个动作迹到达另一确定状态,则s收敛于动作µ;定义8(3)常用于检测标记变迁系统中是否存在不可观察的无限动作序列.

定义 9. if s′∈LTS(s′),s∈LTS(s); s′≤_trs=_deftrace(s′)⊆trace(s).

定义 9 描述了子树判定准则,即:如果存在LTS(s′)是LTS(s)的子树,则两者应满足二元关系≤_tr.

3.4.2 云平台组件建模

我们首先对第2.2节中定义的主要客体分别建模,每一个组件的LTS状态图都可以看做是构成云平台整体状态图的一个组成部分.

根据云平台结构的特点,我们将集合Ob中MC,CRC和SRC三者之间的通信过程、MC内部的客体交互过程以及CCC与SCC的控制管理过程定义为系统可观察动作,而CRC与CN、SRC与SN的交互过程以及各个逻辑组件内部处理过程为系统不可观察的内部动作.

根据第3.4.1节中描述的LTS语法与语义,我们对重要的组件建模过程如下.

(1) LS建模

登录服务器负责对云环境主体的登录请求进行验证,验证当前是Admins还是Users登录,并分别赋予不同权限,若口令错误,则返回等待状态.其过程的LTS语义表述为

$\eqalign{ & wait - error - wait; \cr & wait - Users \to User\_Login; \cr & wait - Ad\min \to Ad\min \_Login. \cr} $

LS的LTS模型LTS(S_LS)如图2所示.

(2) CS建模

调度服务器负责接收从登录服务器传来的用户指令,并进行查询元数据库处理.如果查询正确,则转发给相应组件进行下一步处理;否则返回初始状.同时,调度服务器还负责接受计算集群和存储集群发来的操作信息,并进行相应的元数据库更新操作.其LTS语义表述为

$\eqalign{ & wait - receive - judge and process; \cr & judge and process - sent from LS \to wait reult \cr & judge and process{\text{ }} - sent from{\text{CCC}} \to {\text{process}}; \cr & judge and process - sent from{\text{SCC}} \to {\text{process}}; \cr & {\text{process}} - {\text{update }} \to {\text{wait;}} \cr & {\text{wait result }} - {\text{receive}} \to {\text{ judge and compute;}} \cr & {\text{judge and compute }} - {\text{error}} \to {\text{ wait;}} \cr & {\text{judge and compute}} - {\text{correct}} \to {\text{next state}}{\text{.}} \cr} $

CS的LTS模型LTS(S_CS)如图3所示.

(3) mDB建模

元数据库仅仅接收调度服务器发送的指令,并进行相应处理后返回结果,处理过程是一个不可见的内部动作.其LTS语义表述为

$\eqalign{ & wait - receive \to {\text{process}}; \cr & {\text{process}} - sent \to wait. \cr} $

mDB的LTS模型LTS(S_mDB)如图4所示.

(4) CCC建模

计算集群控制节点是CRC内部对外交互通信的唯一组件,它负责接收CS发来的指令,并在集群内部做相应处理后,返回结果.在某些情况下,CCC会返回再次执行指令,例如在释放资源时发现VM未关闭,则需要返回先关闭VM.其LTS语义表述为

$\eqalign{ & wait - receive \to {\text{process}}; \cr & {\text{process}} - sent \to {\text{wait result}}; \cr & {\text{wait result}} - {\text{receive}} \to {\text{judge and compute;}} \cr & {\text{judge and compute }} - {\text{release VM}} \to {\text{process;}} \cr & {\text{judge and compute }} - {\text{send}} \to {\text{wait}}{\text{.}} \cr} $

CCC的LTS模型LTS(S_CCC)如图5所示.

(5) SCC建模

存储集群控制节点是SRC内部对外交互通信的唯一组件,它与CCC具有类似功能.不同的是,在某些指令控制下,它还能向CCC发送信息.其LTS语义表述为

$\begin{align} & \text{wait-receive}\to \text{judge and process;} \\ & \text{judge and process}-\text{send to CS}\to \text{wait}; \\ & \text{judge and process}-\text{send to CCC}\to \text{next state}. \\ \end{align}$

SCC的LTS模型LTS(S_SCC)如图6所示.

3.4.3 整体状态变迁模型

第3.4.2节中给出的组件模型,描述的是用户使用服务时各个组件的状态变化.但是这些相互独立的组件状态变迁不能准确反映系统整体的动态属性,比如在使用不同服务时,组件之间的冲突、负载等动态特征以及处于某时刻的整体状态等.因此,有必要对第3.4.2节进一步整合,使之成为统一整体.

在用户行为集Op基础上,结合组件模型以及变迁规则(见附表1),我们就可以进一步刻画出云平台运行时的状态变迁图LTS(s)如图7所示.

为了说明LTS(s)建模的正确性与合理性,我们提出如下定义与定理,并进行部分证明.

定理 1. LTS(s)满足s₀,s′∈S,∀Sub(s₀),都有s′⇓.

证明:假定∃Sub(s₀),有s′⇑,就能得到∃s′∈S,∃α ∈L^*_S,在满足s₀=a⇒s′的情况下,使得s′⇑.由于s₀⇓,根据定义8可知,LTS(s)中不存在无限的动作序列a,因此必然有s₀⇑.但是在LTS(s)中,s₀是系统初始等待接受输入的状态,显然状态s₀是收敛的,因此产生矛盾.定理1得证.

定理 1 说明了云平台运行状态是收敛的.这也是符合平台实际特征的,即:在符合正确访问控制策略的控制下,用户从初始登录状态开始,经过一系列动作变迁,最终能够实现状态的收敛.定理 1 同时也说明:在状态收敛性上,建模过程具备合理性.

定义 10. ∀a₁,a₂,…,a_n∈L:

$\eqalign{ & {\text{Max |L| = Max\{ len|}}{{\text{a}}_1}|,len|{a_2}|, \cdots len|{a_n}|\} , \cr & {\text{Max |L| = Min\{ len|}}{{\text{a}}_1}|,len|{a_2}|, \cdots len|{a_n}|\} . \cr} $

定义10描述了一个LTS图中,最长动作迹与最短动作迹的长度.

定理 2. 令A={Min|LTS(S_LS)|,Min|LTS(S_CS)|,Min|LTS(S_mDB)|,Min|LTS(S_CCC)|,Min|LTS(S_SCC)|},则满足:

$Min\left\{ \sum\limits_{\begin{matrix} k=m+1=n+2\text{ } \\ k,m,n≤|B| \\ \end{matrix}}{{{b}_{k}}+{{b}_{m}}+{{b}_{n}}} \right\}=Min|LTS(s)|.$

证明:根据图2~图6,有A={1,3,2,4,2},因此:

$Min\left\{ \sum\limits_{\begin{matrix} k=m+1=n+2 \\ k,m,n≤|B| \\ \end{matrix}}{{{b}_{k}}+{{b}_{m}}+{{b}_{n}}} \right\}=\{{{b}_{1}}+{{b}_{2}}+{{b}_{3}}\}=6.$

而Min|LTS(s)|=|a₁a₃a₁₄a₁₅a₁₆a₂₀|=6,因此定理2得证.

定理 2 说明从初始状态到结束状态,最少情况下组件的参与运行情况,即:最少需要LS,CS以及mDB的协同,这也是与云平台的整体变迁过程和实际的运行过程是相符合的.定理2也说明:从组件参与过程的角度,建立的模型具备正确性.

图中,s₁₄,s₁₅,s₁₆以及s₃₄,s₃₅,s₃₆这6个状态是系统的关键状态,s₁₄和s₃₄是调度服务器接收到用户发送来的操作指令,s₁₅和s₃₅是调度服务器根据需要查询元数据,s₁₆和s₃₆是元数据库返回有效查询结果给调度服务器,这3个状态也是用户发送大多数操作指令必须经过的状态.状态s₀是系统的起点,是用户登陆之前的状态,但s₁₉,s₂₉和s₄₁不是整个系统终结状态,而是指一条用户操作请求的完成.

图2描述了在外部用户输入不同指令时,内部组件交互引起的不同系统状态共计41种、LTS(s)中的可观察动作集合L={a_i|0≤i≤48},S X S上的二元关系共70种.如此复杂的可观察动作和状态不利于进一步对系统安全进行分析,因此有必要对图2进行简化.

3.4.4 状态图约减

对于云平台的主体与客体而言,LS仅验证用户身份后转发一次用户操作请求,而不对操作请求做任何处理; CS在处理LS发送数据时,命令权限已经由接入服务器验证,CS仅执行操作;对于SCC和CCC而言,都是直接执行由CS发送的指令,并与自身集群内部的SN和SN进行交互;并且,不论是以何种用户身份登录,一个操作指令的终止状态要么是更新元数据库,要么是建立了一个远程连接以供用户使用.根据以上特点,状态图约减规则可以总结为:

· M1:状态s₃~s₁₃以及状态s₃₀~s₃₃是可以去除的;

· M2:状态s₁₄与s₃₄、s₁₅与s₃₅,s₁₆与s₃₆这3组状态是可以合并的;

· M3:M2中合并的3组状态必须被保留;

· M4:LTS(s)的终止状态s₂₉和s₄₁是可以合并的;

· M5:s₀是LTS(s)的起始状态,LTS(s)的结束状态是s₁₉以及P4中合并的状态.

按照上述简化规则约减后的状态图如图8所示.

如图所示,经过简化后LTS(s′)中,状态约减为11种,可观察动作集合L′={a_i|0≤i≤17},S X S上的二元关系仅剩余18种.为了说明LTS(s)到LTS(s′)约减过程的正确性,我们还需要进行必要的数学证明.

定理 3. 如果LTS(s′)是LTS(s)经过正确的动作约减而成,则满足s′≤_trs,s′∈LTS(s′),s′∈LTS(s).

证明:对于s′∈LTS(s′),s′∈ LTS(s),根据定义9,要证明s′≤_trs,只需证明trace(s′)⊆trace(s).

又根据定义7(1),Trace(s)={a∈L^*|s=a⇒},因此,定理3的证明转为证明{a_s′}⊆{a_s}.

{α_s′} L_s′^* ,{α_s} ∈L_s^* ,而根据定理条件,有L_s′^*∈L_s^*,因此有{a_s′}⊆{a_s}.证毕.

定理3说明:LTS(s′)是LTS(s)经过正确的动作约减而成,且经过约减的LTS(s′)中的动作序列是原始状态 图LTS(s)中动作序列的子集.说明了动作序列约减过程的正确性.

4 模型分析与验证 4.1 验证内容分析

结合第3.1节中对可信属性的分解描述,我们提出以下针对建立的模型的验证分析内容,并根据分析结果给出一定的建议.

1) 可用性.该属性的子属性是服务可用性与组件负载,其中:服务可用性描述的是各项服务是否存在并且能被正确执行的属性,主要关注系统状态转变,表示在控制策略范围内,系统主体期望的服务是否可用,在对应状态图中可以表述为LTS(s′)中的任何一个 状态是否都由初始状态s₀可达;组件负载主要体现服务的易用性,可以根据LTS(s)以及LTS(s′)中的路径经过的节点情况,给出不同组件的负载的量化数据.

2) 可靠性.该属性又包括健壮性、可控性与故障等级划分.下面分别进行说明.

(1) 健壮性,我们不仅希望系统主体的期望能够正确执行,也希望云环境不会因为误操作或攻击而陷入错误的状态,因此,我们针对系统死锁和性能瓶颈进行分析,并在此基础上给出一些容错性建议.例如,大多数服务都会经过查询元数据这一步骤,因此,我们希望系统能够识别有效的服务请求与恶 意的攻击指令,保证系统不会因为执行攻击者精心构建的大量无效元数据库查询请求而陷入死锁状态,尽量减少拒绝服务类攻击的可能;

(2) 可控性,表示云环境能够执行正确的选择,即:系统处于某一状态时,能够受控制的进入另一正确状态.我们将对系统状态切换、控制组件的管控能力进行分析,例如,当元数据库查询结果错误时,能够返回User等待状态;

(3) 故障等级,结合可用性中的组件负载情况,可以分析故障等级的严重程度,负载较高组件故障时,往往意味着严重故障出现.

3) 安全约束能力.该属性描述的是执行访问控制策略的组件的参与能力的属性.在云平台中,一般由LS来负责赋予用户角色权限,由CS来执行主要访问策略,是云中的关键组件.因此,需要验证系统中所有规定的从初始状态到结束状态的路径都经过关键节点,即:系统中不存在越权操作、有绕过关键组件控制的路径存在.

4.2 模型验证

我们使用模型检测工具Kronos来进行检验分析,Kronos是一种用于实时系统的分析验证工具,它可以使用计数的或者带有标记的程序搜索带自动机,支持各种过程代数标记的模型验证^[36].标记变迁系统由一组带有标记的变迁动作构成,且在本文的模型中,状态转换从时序上可以看做是无时间约束的顺序转换,因此,也可以使用Kronos来对本文构建的状态图进行验证分析^[37].

我们采用的实验环境是Intel i5-2450,4G内存,系统采用Ubuntu 12.10,Kronos版本号为2.52.

4.2.1 参数设定

对模型进行分析前,我们首先要对状态节点进行分析并进行参数设定.在LTS(s′)中所经历涉及的状态节点均包含以下3个状态:(1) 等待触发事件(Idele_i);(2) 获取并同步传输消息(T_i,ST_i);(3) 获取并异步传输消息(T_i,AT_i).其中,状态转换由消息队列的阻塞程度决定.因此,我们对每一个状态节点均使用3个参数记录事件触发的次数,T_i记录当前节点交互的任务,ST_i记录同步消息传输次数,AT_i记录异步消息传输触发次数.在本文的模型中,我们可以假定因消息阻塞而导致的异步传输延时TTL≈0.

同时,我们使用一个栈来存储一个状态节点所处理的消息.具体过程是:当有消息到达节点s_i时,先进入消息处理缓冲队列,根据当前节点空闲状态判断异步传输或同步传输;消息处理完毕后,将节点s_i压入当前任务的栈Trace中.节点s_i的行为被描述为一个自动机Station_i.

对于整个LTS(s′),我们将其描述成一个积自动机LOGIN=protocol||Station₁||…||Station_i.为验证方便,实验中将具有类似属性的节点描述为同类节点,Kronos中节点和交互过程分别用文件station.tg和protocol.tg表示.由于节点状态以及交互过程的复杂性性,导致验证的输入冗长,本文中仅给出部分描述以作说明.

以节点s₁为例,在station.tg中部分描述如下:

$\eqalign{ & \# states 3 \cr & \# trans 6 \cr & \# colcks 0 \cr & \# sync IN OUT \cr & \cr & state:0 \cr & in\operatorname{var} :TRUE \cr & states: \cr & TRUE \Rightarrow IN;reset\{ \} ;goto1 \cr & TRUE \Rightarrow OUT;reset\{ \} ;goto2 \cr} $

交互过程在protocol.tg中的部分描述如下:

$\eqalign{ & state:1 \cr & prop:R\_O\_S \cr & in\operatorname{var} :TRUE \cr & states: \cr & TRUE \Rightarrow HEAD\_0;reset\{ \} ;goto2 \cr & TRUE \Rightarrow HEAD\_1;reset\{ \} ;goto2 \cr & TRUE \Rightarrow ADD\_0;reset\{ \} ;goto0 \cr & TRUE \Rightarrow ADD\_1;reset\{ \} ;goto2 \cr & TRUE \Rightarrow ADD\_01;reset\{ \} ;goto2 \cr & TRUE \Rightarrow OUT\_01;reset\{ \} ;goto2 \cr & TRUE \Rightarrow HEAD\_0ADD\_0;reset\{ \} ;goto1 \cr & TRUE \Rightarrow HEAD\_0ADD\_1;reset\{ \} ;goto2 \cr & TRUE \Rightarrow HEAD\_0ADD\_01;reset\{ \} ;goto2 \cr & TRUE \Rightarrow HEAD\_0OUT;reset\{ \} ;goto2 \cr & TRUE \Rightarrow HEAD\_0ADD\_0OUT;reset\{ \} ;goto2 \cr & TRUE \Rightarrow HEAD\_1ADD\_0;reset\{ \} ;goto2 \cr & TRUE \Rightarrow HEAD\_1ADD\_1;reset\{ \} ;goto2 \cr & TRUE \Rightarrow HEAD\_1ADD\_01;reset\{ \} ;goto2 \cr & TRUE \Rightarrow HEAD\_1OUT;reset\{ \} ;goto2 \cr & TRUE \Rightarrow HEAD\_1ADD\_0OUT;reset\{ \} ;goto2 \cr} $

4.2.2 模型分析

篇幅所限,在此仅给出2个验证实例进行详细说明.

首先,我们希望不会因为无效的数据库查询请求而发生拒绝服务攻击.如果图中不存在闭环,就能很大程度上减少上述攻击发生的可能.因此,上述攻击性质在图中表示为不存在死锁.

结合第4.1节的设定,我们定义经过状态节点s_i次数Count_i=ST_i+AT_i,这一验证结论如果存在死锁,则在Kronos中应该表达为Count_i≥3,该性质描述存于文件bt1.tctl中.

通过Kronos分析得到的结果部分截图如图9所示.

运行结果表明:图中存在发生死锁的动作迹a₃a₅a₆和a₄a₅a₇,表明攻击者可持续构造错误的查询指令,消耗CS与mDB的资源.验证结果说明了CS,mDB这两个系统组件由于有安全隐患而更易受到拒绝服务类攻击.在实际的部署中,我们就可以在这些组件中设置控制策略.比如:对可能引起类似攻击的服务,增加使用间隔阈值、发现大量类似服务请求时随机丢弃等方式来应对.

其次,我们希望验证在正确的访问控制策略下,用户使用VM的诉求能否达成,即,验证状态s₈是否可达.这条性质属于服务可用性的验证.

根据第4.2.1节中的描述,我们假设每个站点获得的消息不为空,则该性质在Kronos中表达为栈Trace中必存在记录s₁→s₈.通过Kronos分析得到的结果部分截图如图10所示.

运行轨迹说明:云平台的各个组件在正常的访问控制策略下能够满足用户提出的服务请求,攻击者不能绕过权限来越级使用某些不属于自身权限范围内的功能.

4.3 验证结论

基于状态图LTS(s′)与模型检测工具Kronos,我们对第4.1节中提出的分析内容分别进行了验证,得到验证结果如下:

(1) 满足可用性.我们利用Kronos对用户服务功能集OP中的功能进行了逐条验证,每一个功能所代表的状态节点都是可达的,说明云平台提供给用户的相关功能都是可用的.但是在可用性分析中我们也发现:用户不但可以使用自己拥有使用权限的功能,还可能绕过访问控制权限越级使用某些非法功能,例如,攻击者利用漏洞实现使用User身份登陆后访问其他User的数据域信息等.这就需要在安全约束分析中进一步展开分析.

(2) 不满足可靠性.在健壮性方面,LTS(s′)中存在4个环,与之相关的组件有LS,CS,mDB以及CCC.验证结果说明:潜在攻击者可以构造合理命令,使得系统陷入死循环,从而消耗系统资源.此外,运行轨迹显示:从初始状态到终止状态的所有运行轨迹中,有较多的运动轨迹经过LS以及mDB,说明调度服务器的处理能力与元数据查询能力是系统瓶颈资源,一旦这两个系统组件发生故障,容易造成系统的崩溃.我们还可以根据运行轨迹经过的组件情况来判定组件在服务提供中的重要程度,为故障等级划分提供依据.在可控性方面,系统主要控制客体能够按照合理的访问控制策略满足云平台使用主体的诉求,即,具有控制功能的组件,包括接入服务器、调度服务器以及计算、存储集群控制节点能够按照预设的策略来控制系统的状态切换,说明具有较好的可控性.

相关组件具有安全约束能力.在状态图LTS(s′)中,s₃,s₄,s₅是接入服务器和调度服务器参与工作的状态转换节点,图中所有动作迹都经过了这3个状态节点,说明了接入服务器和调度服务器具有关键的约束功能,配置的访问控制策略都能够发挥作用.但是这不保证接入服务器和调度服务器本身的安全,攻击者仍然能对关键组件本身发起攻击,篡改一些关键安全配置.因此在实际部署中,接入服务器和调度服务器是安全防护的重点关注对象,需要使用密码和安全协议等技术对其进行保护.

此外,我们还将本文的贡献和同类研究进行了对比,对比对象是文献^[6-38],这3个研究都是用不同方法对云环境的部分或是整体进行建模,并对其中某些属性进行分析,对比结果见表2.对比结果显示:本文提出的方法相对比较全面,能够对平台整体的各个不同属性进行综合分析,具有一定的优越性.

通过Kronos对LTS(s′)进行验证,我们可以发现:现有的大多数云平台存在一定的可信性问题,一般来说,服务满足了服务可用性,相关组件也具有较好的控制和安全约束能力;但是不具备较好的容错能力,且易受到资源消耗类的攻击.此外,对于分析得出的重要组件的保护也是保障服务可信的重点.在实际部署中,我们就可以针对以上安全隐患做出应对,例如对安全策略配置文件进行加密,增加关键组件的热备份服务器,对于某些服务设置使用间隔阈值,随机丢弃可能无效的数据包等.但是这些解决方案不是本文要讨论的重点,在此就不一一列举.我们将在下一步研究中对于这些存在的可信性问题展开更深入的研究.

5 结束语

由于商业云故障频发,企业与普通用户仍然对其应用场景的服务是否安全可靠存在很大疑虑,这也不利于云计算的进一步推广与发展,因此,对云平台的可信性进行分析验证是非常有必要的.

针对目前的模型不适用于对服务可信性中的部分动态属性进行有效分析的问题,本文利用LTS理论,提出一种新的模型建立方法:在抽象出云平台的逻辑组件基础上,从用户行为引发的组件交互过程出发,对关键组件进行建模,并对这些相对独立的单个模型进行整合,从动态的角度刻画出云平台在服务提供时,云环境的整体运行状态变迁图;同时,针对状态空间过于复杂问题进行了简化,解决了云平台可信性建模与分析困难的问题.以Kronos为工具对状态图进行检测时,除了发现云平台对外提供服务时一些已知的可靠性隐患外,还发现了存在一些未知的可靠性问题,如容错能力的具体量化数据等.

我们下一步工作将结合本文发现的问题,提出在实际部署时的解决措施,解决诸如绕过安全组件的旁路攻击、针对LS和mDB的资源消耗类攻击等;此外,还将基于路径对云平台关键组件的负载能力进行量化,并基于本文的分析结果构建故障等级评价体系,为可信云测评提供基础.