为了有效管理云系统间跨域互操作中安全策略的实施，提出一种适用于云计算计算机网络环境的多域安全策略验证管理技术。首先，研究了安全互操作环境的访问控制规则和安全属性，通过角色层次关系区分域内管理和域间管理，形式化定义了基于多域的角色访问控制(domRBAC)模型和基于计算树逻辑(CTL)的安全属性规范;其次，给出了基于有向图的角色关联映射算法，以实现domRBAC角色层次推理，进而构造出了云安全策略验证算法。性能实验表明，多域互操作系统的属性验证时间开销会随着系统规模的扩大而增加。技术采用多进程并行检测方式可将属性验证时间减少78.0%～86.3%70.1%～88.5%采用平均值表述有问题，根据表2的描述，现在改为这样，是否符合表达?请明确。，其模型优化检测模式相比正常模式的时间折线波动更小，且在大规模系统中的时间开销要明显低于正常模式。该技术在规模较大的云系统安全互操作中具有稳定和高效率的属性验证性能。
0引言
云计算(Cloud Computing)是一种基于因特网的全新商业计算模式，通过广泛的网络带宽接入技术为各类用户提供多租户、可扩展、弹性、按需支付以及可配置的资源，因商业经济效益的驱动得到迅速发展[1]。近年来，各种云计算系统层出不穷：公有云、私有云、混合云、社区云[2]等，然而它们大多是有界的单托管域系统，随着跨域性、动态性资源访问和数据共享需求的扩大，基于多管理域协作的云系统安全策略的实施成为目前工业界和学术界的关注热点[3]。在云计算系统的多域协作研究领域，如何实现访问控制、如何确保跨域互操作的安全性以及如何利用模型检测技术验证安全策略，是3个基本问题。由这3个基本问题延伸出3个重要的研究方向，即访问控制、安全互操作和模型检测。
在访问控制方面，目前的主流方案是基于角色的访问控制(RoleBased Access Control， RBAC)模型。文献[4]指出RBAC支持多种访问控制规则，具有很好的模型抽象和概括能力。文献[5-6]认为RBAC中角色、用户权限的映射关系与实际企业的组织架构层次相对应，适用实际应用环境且易于系统维护和交互管理。文献[7]提出并基于实验证明RBAC较好地解决了云计算应用环境下的企业问题。文献[8]研究了RBAC在云计算系统的现状，认为模型作为云的基础设施关键技术适用于多域环境，并且已经成功地应用在医疗、股票和社交网络中。同时，RBAC模型被大多数主流的云平台所采用，如：OpenStack、Xen、Windows Azure等。文献[9]提出使用中间件实现多域系统安全策略，并结合医疗案例证实访问控制策略在多域的云计算系统中具有可行性。
在安全互操作方面，大规模分布式环境促使越来越多单托管域的企业联合起来，形成多管理域协作环境成为趋势。文献[10]指出多域安全策略异构问题是各类云系统协作进程中的重要挑战，这个过程要既能有效地支持跨域互操作又能够保证安全。文献[11]通过研究相关文献，提出角色委托机制、映射机制、信任机制和策略合成机制等，是目前学术界涉及的几个研究方向。其中，基于RBAC模型的角色映射机制是安全互操作问题的研究热点，例如：文献[12]为实现分布环境的跨域访问，提出利用一种基于动态角色转换的策略来构建域间访问控制规则和属性约束;文献[13]在RBAC基础上，建立域域之间的角色映射关系，采用直接转换方式实现域间角色关联以保障单个自治域的安全。
综合上述方案，在RBAC策略域的互操作过程中的授权管理与访问控制问题在一定程度上得到了解决。然而，在实施过程中仍然可能出现违反域内安全约束和自治性问题。文献[14]仿真模拟了动态协同环境中安全策略的一致性维护，在定义和维护域间安全访问控制策略方面进行了有益尝试，但并未给出工具检测方法的形式化定义，且缺乏有效的域间访问控制策略的集成方案。
在安全策略验证方面，目前已存在多种模型检测技术[15-17]。这些技术的基本思想是：用形式化建模语言描述待验证的安全策略系统模型，用时态逻辑公式描述待验证的安全属性，然后将它们输入到检测工具中完成验证。例如，文献[15]提出一种通用访问控制属性验证模型，它能够维护各种静态、动态访问控制的安全约束，并且通过组合验证方式提供测试用例以检测模型和策略规则的一致性;同时生成基于扩展的访问控制标记语言(eXtensible Access Control Markup Language， XACML)访问控制认证策略，其中XACML2.0或XACML 3.0已经成为目前协同系统中策略规则的规范化描述语言。文献[16]提出使用黑盒模型检测技术来验证待检测的访问控制属性。文献[17]给出一种访问控制策略检测工具，该工具提供了设置访问控制策略和属性规则的图形化用户界面，可以通过符号模型检测器(Symbolic Model Verifier， SMV)进行访问控制策略的一致性验证。此外，研究还提供了完整的测试工具包以及生成XACML语言形式的策略输出。
综上所述，访问控制、安全互操作和模型检测之间是互相制约、相辅相成的，因此，研究一种有效的多域安全策略验证管理技术来实现上述功能具有重要的意义。从公开的国内外文献中还没有发现将上述三者统一起来进行形式化研究并转化应用的成果，类似的研究工作也甚少，且不具有普适性。例如，文献[18]提出一种面向网格系统中分布式访问控制策略的管理方法，研究不同策略行为的表现形式并给出了相应的安全策略验证方案。然而，由于缺乏对于安全互操作问题的关注，其系统模型存在严重的跨域访问安全风险。同时性能评估结果表明，该方案仅适用于小规模的分布式系统、只支持数目相对较小的安全策略的验证。
因此，本文提出了一种适用于云计算系统的多域安全策略验证管理技术，可以在大规模的安全互操作环境中实现形式化定义访问控制规则、规范安全属性和验证安全策略。实现过程表明，该技术通过引入RBAC角色层次推理，具有强大的角色关系表达能力，其形式化定义了RBAC规则表达式和属性命题，并进一步提出了安全策略验证算法，在大规模安全域模拟实验中显示出更强的通用性和可行性。
1预备知识
简单介绍安全互操作和模型检测的相关理论，RBAC模型的基础理论请读者自行参阅文献[4]，文中不再赘述。
1.1安全互操作
在多域系统中，安全互操作要兼顾自治性和安全性两大原则[3，12]。其中自治性原则是指如果一个访问请求在单个管理域系统中被允许，那么它在安全互操作中也必须被允许;安全性原则是指如果一个访问请求在单个管理域系统中被禁止，那么它在安全互操作中也须被禁止。在基于RBAC模型的安全互操作系统中，域间联合所增加的角色继承关系可能会造成本地安全策略的违反问题，而这种违反约束的行为可以通过相关的策略检测而被预先发现，提前避免安全风险。安全互操作属性有环继承、权限提升、职责分离(Separation of Duty， SoD)原则和自治性等[19]。下面，在给出上述安全属性定义之前，先进行如下约定。
1)r1 → r2，表示角色r1继承角色r2的权限。
2)如果角色rk属于域di的角色，则表示为dirk;同理，diut表示域di的用户ut，dipw表示域di的权限pw。
定义1继承环属性。
在域间互操作过程中，由于新的角色映射关系的引入，角色层次之间形成了环状结构的继承关系，导致下级角色非法拥有了上级角色权限，这种情况称为继承环，记为：dirj>>dirk。如图1(a)所示，在域di中，用户diut被指派给角色dirk，则用户diut同时获得到了它的上级角色dirj的权限。
定义2权限提升属性。
在域间互操作过程中，新的角色关联关系导致以前没有关联的角色之间形成某种继承关系，使得角色获取到更大的权限，这种情况称为权限提升，记为：dirj≥dirk。如图1(b)所示，域di用户diut被指派给角色dirj，用户diut在获得角色dirj权限的同时还获得了角色dirk的权限，即使用户diut与角色dirk之间并不存在直接指派关系。
定义3职责分离属性。
如果域di用户diut(或者域dn用户dnut)由于域间角色映射关系，使得它可以获取或在会话中激活存在SoD约束的两互斥角色dirj和dirk，那么就违反了SoD约束，如图1(c)所示。本文验证职责分离属性是基于下面两个性质[4]：
1)如果角色rk和rm之间不存在直接或间接的继承关系，那么rk和rm完全互斥;
2)如果角色rk和rm完全互斥，那么不存在有任何角色可以同时继承rk和rm。
定义4自治性属性。
自治性属性要求在域间互操作环境中的访问控制权限不能违反自治管理域的本地操作权限。安全互操作要求平衡自治性和交互性，违反任何单个域的安全策略都是不允许的。
1.2模型检测
模型检测技术是验证安全互操作属性的重要手段，它能够解决访问控制模型的通用属性验证问题。早在20世纪80年代，基于时序逻辑的模型检测技术[20]就被广泛关注，其原理如图2描述：假设，M表示状态迁移系统，F表示模态时序逻辑公式，将“系统是否具有所期望的性质”转化成数学问题来描述，即“M是否是公式F的一个模型”，记为M|=F?。
模型检测过程主要包括系统建模、建立系统性质规范和执行验证3个过程。其中，系统建模主要是建立与系统相对应的迁移系统或Kripke[16]结构，用来描述系统方案的动态行为;系统性质规范的建立要求统一系统性质的表达形式，多数会使用计算树逻辑(Computation Tree Logic， CTL)、线性时态逻辑(Linear Temporal Logic， LTL)等属性描述语言来规范表达;执行验证环节可以采用方便的自动验证模式，由模型检测器完成。
目前，存在大量支持模型检测技术应用的模型检测工具，如：SMV、简单进程元语言解释器(Simple Promela Interpreter， SPIN)[21]、改进符号模型检测器(New Symbolic Model Verifier， NuSMV)[22]和Uppaal[23]等。本文后续的研究工作选用NuSMV这款开放架构的模型检测器。
2云安全策略模型
在本章中，主要完成两方面的工作：
1)针对云系统中RBAC方案不能有效地解决不同云托管域的策略集成问题，引入域内管理和域间管理两类角色层次关系，对传统的适用于单域的RBAC模型进行重定义，从而建立一种基于多域的角色访问控制(multidomain Role Based Access Control， domRBAC)模型;
2)给出基于CTL语言的通用访问控制模型转换方法[17]，并对访问控制规则、安全属性和迁移系统的表达进行了规范。
2.1domRBAC模型
本文在ANSI INCITS 3592004 RBAC[4]的基础上，综合考虑了系统功能和审查功能，给出如下形式化定义。
2.1.1基本元素
1)USERS、ROLES、OPS、OBS分别表示用户、角色、操作、对象的集合。
2)UAUSERS×ROLES，表示用户与角色之间多对多的分配关系。
3)PRMS=2(OPS×OBS)，表示权限的集合。
4)PAPRMS×ROLES，表示权限与用户之间多对多的分配关系。
5)Op(p：PRMS) → {opOPS}，表示权限与操作之间的对应关系，指明为操作集分配的权限集p。
6)Ob(p：PRMS) → {obOBS}，表示权限与对象之间的对应关系，指明为对象集分配的权限集p。
2.1.2域内角色层次
1)assigned_users：SUdi(dirk：ROLES) → 2USERS，表示域di中角色dirk与用户集USERS之间的映射关系，即：SUdi(dirk)={diut∈USERS|(diut，dirk)∈UA}。
2)assigned_permissions：SPdi(dirk：ROLES) → 2PRMS，表示域di中角色dirk与权限集PRMS之间的映射关系，即：SPdi(dirk)={dipw∈PRMS|(dipw，dirk)∈PA}。
3)RHdiROLES×ROLES，表示域di中角色之间继承关系的偏序集合，记为问过，回复：表示正确。。若dirkdirm，那么dirm的权限集都是dirk的权限集，且dirk的用户集则都是dirm的用户集，即：dirkdirm UPdi(dirm)UPdi(dirk)∧UUdi(dirk)UUdi(dirm)。
4)authorized_users：UUdi(dirk：ROLES) → 2USERS，表示域di中角色dirk与域内角色层次用户集USERS之间的映射关系，这种映射只考虑角色dirk与域内的其他角色之间的继承关系，即：UUdi(dirk)={diut∈USERS|dirmdirk，(diut，dirm)∈UA}。
5)authorized_permissions：UPdi(dirk：ROLES) → 2PRMS，表示域di中角色dirk与域内角色层次权限集PRMS之间的映射关系，这种映射只考虑角色dirk与域内的其他角色之间的继承关系，即：UPdi(dirk)={dipw∈PRMS|dirkdirm，(dipw，dirm)∈PA}。
2.1.3域间角色层次
1)RHROLES×ROLES，表示域间角色之间继承关系的偏序集合，记为。若dirkdjrm，那么djrm的权限集都是dirk的权限集，且dirk的用户集都是djrm的用户集。即：dirkdjrm UP(djrm)UP(dirk)∧UU(dirk)UU(djrm)。
2)authorized_users：UU(dirk：ROLES) → 2USERS，表示角色dirk与域间角色层次用户集USERS之间的映射关系，这种映射的集合既包括dirk与域内角色之间的继承关系，又包括dirk与外域角色之间的继承关系，即：UU(dirk)=UUdi(dirk)∪{djut∈USERS|djrmdirk，(djut，djrm)∈UA}。
3)authorized_permissions：UP(dirk：ROLES) → 2PRMS，表示角色dirk与域间角色层次权限集PRMS之间的映射关系，这种映射关系既包括dirk与域内角色之间的继承，又包括dirk与外域角色之间的继承，即：UP(dirk)=UPdi(dirk)∪{djpw∈PRMS|dirkdjrm，(djpw，djrm)∈PA}。
2.1.4谓词
考虑到时序逻辑语言中缺乏关系算子，如：□和。下面，补充一些对应谓词的定义。
1)IR(rk，rm)表示两角色间存在(域间或域内)直接继承关系，即：IR(rk，rm)=true rk□rm。其中，符号□表示直接继承关系。
2)MRdi(dirk，dirm)表示域di角色层次中的两角色间存在一种(域间或域内)直接的或者间接的继承关系，即：MRdi(dirk，dirm)=true dirkdirm。
3)RP(rk，rm)表示对于存在直接继承关系的两角rk，rm(rk□rm)，角色rk的分配权限集是角色rm权限集的子集，即：RP(rk，rm)=true IR(rk，rm)∧SPdi(rk)UP(rm)。
4)IBdi(dirk，dirm，rn)表示如果任意域角色rn是所在域di中角色dirk和角色dirm的上级角色，那么，rn的权限集则同时包括了dirk的权限集和dirm的权限集，即：IBdi(dirk，dirm，rn)=true SPdi(dirk)∪SPdi(dirm)UP(rn)∧rndirk∧rndirm。
5)BA(dirk)表示角色dirk与域内角色层次中权限集的映射关系，是dirk与域间角色层次中权限集的映射关系的子集，即：BA(dirk)=true UPdi(dirk)UP(dirk)。
2.2转换系统
本文采用CTL时序逻辑来对有关的安全策略进行规范，如：访问控制规则、安全属性和变迁系统。
在CTL语言中，前缀路径量词可以断言关于线性时序算子的任意组合。据此，本文规定使用通用路径量词表示“对所有路径”，使用线性时序算子□表示“现在和以后所有状态”，使用线性时序算子◇表示“现在或以后某一状态”。另外，规定时序模式□Φ表示不变的Φ，时序模式◇Φ表示可变的Φ，其中，Φ是一个状态公式。
定义5一条domRBAC规则是形如“if c then d”的命题，其中，约束c是一个关于决策许可d的谓词表达式(r，UP(r))，因此，由一系列规则组成的domRBAC策略，可以表示成形如c(r，UP(r))的这种逻辑表达式形式。
定义6一个domRBAC访问控制属性p是形如“b → d”的公式，其中，访问权限许可d的结果取决于量化谓词b与(r，UP(r))之间的映射关系，其归约关系 → 描述了系统内部的推理方式。
定义7迁移系统TS是一个四元组(S，Act，δ，i0)，其中：
1)S是有限状态的集合，S={Permit，Deny};
2)Act是活动的集合，Act={(r1，UP(r1))， (r2，UP(r2))，…，(rn，UP(rn))};
3)δ是状态转移关系，且δ：S×Act → S;
4)i0∈S是初始状态。
根据定义6，访问控制属性p可以被表示成迁移系统TS的命题，如p：S×Act2 → S，因此，domRBAC策略可以对应地转换成逻辑公式：p=(Si*(r1，UP(r1))*(r2，UP(r2))*…*(rn，UP(rn))) → d，其中，p∈P，P代表属性集合，并且*是CTL中的布尔算子。此外，domRBAC模型的功能规则对应于转换系统TS的转换关系δ，因此，将domRBAC访问控制属性表示为时态逻辑表达式(即时态规范)，就可以断言属性p在TS下是否可满足，即验证TS|=□(b → ◇d)是否为真。2.3属性规范
结合前面2.1节内容，下面给出继承环属性、权限提升属性、职责分离属性以及自治性安全属性的时态逻辑定义。
定义8继承环属性为：
TSdomRBAC|=□(RP(dirj，dirk) → ◇Deny)(1)
其中dirj，dirk表示域di中的两个角色。通过验证命题RP(dirj，dirk) → ◇Deny是否满足TSdomRBAC中的不变式，来检测角色dirj是否存在环状继承。
定义9权限提升属性为：
TSdomRBAC|=□((MRdi(dirj，dirk)∧RP(dirj，dirk) → ◇Deny)(2)
其中dirj是用户diut对应的指派角色。通过验证命题(MRdi(dirj，dirk)∧RP(dirj，dirk) → ◇Deny是否满足不变式TSdomRBAC，来检测角色dirj，dirk之间是否因为域间映射关联导致用户diut的权限提升。
定义10职责分离属性为：
TSdomRBAC|=□((dirj∈dirsw∧dirk∈dirsw∧(RP(dirj，dirk)∨RP(dirk，dirj)∨IBdi(dirj，dirk，rm))) → ◇Deny)(3)
鉴于SoD属性是基于角色对实现的，这就需要检测互斥角色对的最小数量的约束关系：(dirs，n)∈SSD，其中，n≥2且dirs代表一个角色集。同样地，可以等价地表示成二项系数|di rs| C2 (|di rs|2)|di rs|!2!(|di rs|-2)!。
定义11自治性属性为：
TSdomRBAC|=□(BA(dirk) → ◇Permit)(4)
在互操作中，通过检测域di中角色dirk的所有指派权限和角色层次映射生成权限是否被保护，来验证自治性属性。
3技术实现
本章讨论云系统多域安全策略验证技术实现问题。首先，提出一种基于图论的角色关联(角色角色)映射算法，该算法通过引入RBAC角色层次推理来实现对系统模型中角色层次关系的准确模拟。该算法的核心思想是，用稀疏图数据结构表示角色层次关系，用链表替代传统矩阵模拟角色层次，以获取更高的属性验证性能。其次，给出了基于多域的云安全策略验证算法。下面，先给出实现部分的相关定义。
定义12G=(V，E)是一个表达域间角色层次的有向图，其中V(VROLES)代表一组有限、非空的角色顶点集合，E代表图中有向边的集合，并且，每条有向边都是相关两角色顶点的一对序偶(dirm，djrn)，其中两角色顶点的关系为dirmdjrn。
定义13图G中的一条路径是指由n-1条有向边所构成的序列集合{(dir1，dir2)，(dir2，dir3)，…，(dirn-1，dirn)}，连接从角色顶点dir1到角色顶点dirn，一条路径代表了两角色顶点dir1和dirn之间的间接继承关系。
定义14图G的邻接表是列表|V|的一个数组L，图G中的每个角色顶点都被包含在V集合里面。对于每个角色顶点dirm来说，都存在一个指针Ldirm指向一个涵盖与dirm相邻接的所有角色顶点的链接表。本文用AG表示图G的邻接表，用nil指针表示一个链表的终止。
定义15G*=(V，E*)是图G=(V，E)的传递闭包，其中，当且仅当图G中存在一条从顶点u到顶点v的路径时，E*集合中包含有一条边edge(u，v)。本文用TG表示一个基于邻接表存储的有向图G=(V，E)的传递闭包列表。
基于图论的角色关联映射算法的结构如算法1所示。这里，TG为算法返回的生成结果，期间采用的改进Warshall算法的相关信息可参考文献[24]。在角色关联映射算法中，第1步，根据domRBAC规则生成有向图G=(V，E)的邻接表AG，这个过程可以利用如文献[22]中提到的解析器(Simple API for XML， SAX)进行自动生成;第2步，根据AG计算图G的传递闭包列表TG，本文采用一种时间复杂度为O(|V||E|)的改进传递闭包算法[24]。
算法1基于图论的角色关联映射算法(如图3)。
示例1如图4所示是一个定义了两个域d1，d2之间互操作的域间访问控制策略应用场景。其中，在管理域d1中有角色d1ra，d1rb，d1rc，d1rd，d1re，角色d1ra继承d1rb的所有权限并间接继承d1re的权限，角色d1rc继承d1rd的所有权限并间接继承d1re的权限，并且角色d1rb和角色d1rc之间还存在SSD约束;在管理域d2中有两个角色d2rf，d2rg，角色d2rf继承d2rg的全部权限。此外，域d1和d2之间的域间继承关系定义如下：
1)角色d1rb继承角色d2rg;
2)角色d2rg继承角色d1rc。
如图5所示是AG和TG的生成结果，具体的计算过程如下所示。
首先，利用BOOST C++程序库[25]中的Boost Graph中adjacency_list类，生成一个通用的以邻接表AG结构存储的有向图G;其次，利用Boost Graph库中的transitive_closure()函数，将图G输入并转换生成传递闭包结构列表TG。
图5中的AGd1和TGd1分别表示管理域d1的邻接表和传递闭包列表。根据定义11，TGd1可以作为一种待检测的安全属性，用于验证原始单个管理域在与多域的互操作过程中是否违反了自治性原则。
基于多域的云安全策略验证算法的结构如算法2和图6所示。在该算法中，首先利用算法2，将根据云用户访问需求生成的domRBAC规则XML文件，经过解析器SAX生成记录域间角色关联关系的AG和TG;然后，利用迭代器(Iterator)，根据算法3，迭代生成新的XML文件，具体包括原有的访问控制规则、新增角色关系描述规则以及待验证的安全属性。由于这些XML文件是经过规范的逻辑程序，因而可以装载进入检测系统直接计算;最后，NuSMV系统可高效地计算它并返回查询结果R： 1)如果R=true，即TSdomRBAC|=p为真。说明属性p在TS下是可满足。
2)如果R=FALSE，即TSdomRBAC|=p为假。说明属性p在TS下是不可满足。
算法2云安全策略验证算法。只写了算法2，却没有看到具体算法，是否遗漏了?请明确。回复：算法2是用图6描述的，所以并没有遗漏。
算法3规则和属性生成算法。
程序前
procedure ITERATOR_SKELETON(TG)
for all vertex dri∈TG
for all adjacent vertex drj
此处的注释，是否改为操作。因为for语句后面没有执行语句了，而直接是结束语句了，请明确。//生成时态规范的规则和属性
end procedure
程序后
4性能评测
下面对本文提出的技术进行实验性能评估。实验说明如下：首先，利用NetworkX工具生成云端用户的访问控制请求，作为解析器的输入数据。其中，NetworkX是一款用Python语言开发的图论和复杂网建模工具，能够提供gnc_graph()函数动态生成用户请求和对应权限。其次，使用domRBAC模拟器模拟云托管域的角色指派。
假设分别有5，10，15，20个云托管域，其中每个托管域中含有50个角色。在此基础上，实验设计模拟4个不同规模大小的域间互操作环境，分别是具有250，500，750，1000个角色的云协同计算环境。系统的运行环境为Windows Server 2003 R2操作系统，CPU版本为Intel Core2 3.0GHz，内存为4GB DDR2，开发语言为C++。
实验提供了一系列有关安全属性验证时间的定量结果。如表1所示，给出了解析器和NuSMV验证器的实验数据，其中，TG的数量对应访问控制规则的数目。从表1看出，执行时间：1#<2#<3#4#，说明规模越大的系统，其属性验证的时间开销也越大。通过分析可知，系统中安全属性的检测耗时会随着安全属性数目以及domRBAC规则数量的增加而增大，这是因为属性数和规则数决定了检测器中有序二叉决策图(Binary Decision Diagram， BDD)的可到达状态数，直接影响了状态判断次数，那么，如何降低系统规模对于属性验证时间的影响?可以考虑采用并行检测的方式进行属性验证，并且，表1的检测数据是在NuSMV模型验证器的正常模式下实验采集的，如果采用优化模式，性能会因增加3个参数设置而相对提高，因为正常检测模式是不包含任何额外的命令行参数的。
基于上述分析，后续实验将围绕两个方面展开设计：一方面，引入并行检测和优化检测两种实验模式，分模式测试不同规模系统的属性验证时间;另一方面，分规模测试不同并行进程数的属性验证时间。
如表2所示，在8个进程并行检测模式下，分别测量了正常模式(N)和优化模式(O)的属性验证时间，N和O是指NuSMV模型检测器实验时的两种参数设置状态。其中，1#(5×50)规模的系统时间太小(<1min)，可忽略不计(表2中表示为“—”)。表2中的时间减少率(Reduction_time)，定量描述了多进程并行检测模式对比单进程串行检测模式的执行效率，它的具体计算方法如下：
Reduction_time=(1-maxT/Single_process_time)×100%(5)
其中：maxT表示(tPi)Ni=1的最大值，并且N表示并行执行的进程数;tPi表示进程Pi(1≤i≤N)的执行时间;∑Ni=1tPi则表示多个进程顺序执行的时耗总和。
上述实验结果表明：
1)并行检测显著地提高了系统的属性验证性能。例如，表2中的数据显示，当并行检测进程数为8时，Reduction_time的平均值在正常检测模式下为86.3%且在优化检测模式下为78.0%，在三种规模的系统中，正常模式下Reduction_time分别为88.5%、85.9%、84.5%;优化模式下Reduction_time分别为82.9%、70.1%、81.1%。用这个平均值比较不科学，有可能趋势不一致，因此改为现在这样的描述，是否符合表达?请明确。相比单个进程检测模式具有很好的时间性能。
2)时间随机波动，优化模式比正常模式具有更稳定的属性验证性能。从图7～9中看出，模型验证器NuSMV的执行时间在正常模式相比优化模式下显示出了更大的波动性和不可预测性。随着并行进程数的不断增加，系统安全属性的验证时间必然会因角色数量的增加而受到影响。随机波动则是由安全属性的数量、BDD可到达状态的数量等多因素共同影响所致。
3)在大规模系统中，优化模式下的属性验证时间开销要明显低于正常模式;然而，在中小规模系统中，反而是正常模式下的属性验证时间开销明显低于优化模式。例如，图7～9，在2#(10×50)和3#(15×50)系统中，存在maxTnormal 4)∑Ni=1tPi≠Single_process_time，说明在执行相同数目的属性验证时，多个进程顺序执行的时耗总和与单进程执行验证的总时间并不相等。
5结语
本文研究了基于访问控制规则和安全互操作属性的策略规范和验证问题，提出了一种适用于云计算系统的多域安全策略验证管理技术。文中的主要工作如下：1)提出一种基于多域环境的角色访问控制(domRBAC)模型;2)研究了安全互操作理论，建立了基于CTL时序逻辑的转换规范，并给出环继承属性、权限提升属性、职责分离属性以及自治性属性的时态逻辑表达形式;3)给出了技术的详细实现，为基于多域的安全策略验证管理提供了一整条工具链。实验结果表明，该技术方案能够较好地实现域间互操作中的安全策略表达、规范和安全策略验证，在较大规模的云系统中具有稳定性、高效性和可行性。下一步将完善跨域资源使用约束、模型检测算法和访问安全威胁消解等方面的研究，进一步提高云系统中多域安全策略的管理效果。
作者：蔡婷 蔡宇欧阳凯 来源：计算机应用 2016年7期
