蔡婷 蔡宇 歐陽(yáng)凱

摘要：為了有效管理云系統(tǒng)間跨域互操作中安全策略的實(shí)施，提出一種適用于云計(jì)算環(huán)境的多域安全策略驗(yàn)證管理技術(shù)。首先，研究了安全互操作環(huán)境的訪問(wèn)控制規(guī)則和安全屬性，通過(guò)角色層次關(guān)系區(qū)分域內(nèi)管理和域間管理，形式化定義了基于多域的角色訪問(wèn)控制（domRBAC）模型和基于計(jì)算樹(shù)邏輯（CTL）的安全屬性規(guī)范；其次，給出了基于有向圖的角色關(guān)聯(lián)映射算法，以實(shí)現(xiàn)domRBAC角色層次推理，進(jìn)而構(gòu)造出了云安全策略驗(yàn)證算法。性能實(shí)驗(yàn)表明，多域互操作系統(tǒng)的屬性驗(yàn)證時(shí)間開(kāi)銷會(huì)隨著系統(tǒng)規(guī)模的擴(kuò)大而增加。技術(shù)采用多進(jìn)程并行檢測(cè)方式可將屬性驗(yàn)證時(shí)間減少78.0%～86.3%70.1%～88.5%采用平均值表述有問(wèn)題，根據(jù)表2的描述，現(xiàn)在改為這樣，是否符合表達(dá)？請(qǐng)明確。，其模型優(yōu)化檢測(cè)模式相比正常模式的時(shí)間折線波動(dòng)更小，且在大規(guī)模系統(tǒng)中的時(shí)間開(kāi)銷要明顯低于正常模式。該技術(shù)在規(guī)模較大的云系統(tǒng)安全互操作中具有穩(wěn)定和高效率的屬性驗(yàn)證性能。

關(guān)鍵詞：

云系統(tǒng)；多域；訪問(wèn)控制；安全互操作；策略；驗(yàn)證

中圖分類號(hào)： TP309.2 文獻(xiàn)標(biāo)志碼：A

0引言

云計(jì)算（Cloud Computing）是一種基于因特網(wǎng)的全新商業(yè)計(jì)算模式，通過(guò)廣泛的網(wǎng)絡(luò)帶寬接入技術(shù)為各類用戶提供多租戶、可擴(kuò)展、彈性、按需支付以及可配置的資源，因商業(yè)經(jīng)濟(jì)效益的驅(qū)動(dòng)得到迅速發(fā)展[1]。近年來(lái)，各種云計(jì)算系統(tǒng)層出不窮：公有云、私有云、混合云、社區(qū)云[2]等，然而它們大多是有界的單托管域系統(tǒng)，隨著跨域性、動(dòng)態(tài)性資源訪問(wèn)和數(shù)據(jù)共享需求的擴(kuò)大，基于多管理域協(xié)作的云系統(tǒng)安全策略的實(shí)施成為目前工業(yè)界和學(xué)術(shù)界的關(guān)注熱點(diǎn)[3]。在云計(jì)算系統(tǒng)的多域協(xié)作研究領(lǐng)域，如何實(shí)現(xiàn)訪問(wèn)控制、如何確?？缬蚧ゲ僮鞯陌踩砸约叭绾卫媚Ｐ蜋z測(cè)技術(shù)驗(yàn)證安全策略，是3個(gè)基本問(wèn)題。由這3個(gè)基本問(wèn)題延伸出3個(gè)重要的研究方向，即訪問(wèn)控制、安全互操作和模型檢測(cè)。

在訪問(wèn)控制方面，目前的主流方案是基于角色的訪問(wèn)控制（RoleBased Access Control， RBAC）模型。文獻(xiàn)[4]指出RBAC支持多種訪問(wèn)控制規(guī)則，具有很好的模型抽象和概括能力。文獻(xiàn)[5-6]認(rèn)為RBAC中角色、用戶權(quán)限的映射關(guān)系與實(shí)際企業(yè)的組織架構(gòu)層次相對(duì)應(yīng)，適用實(shí)際應(yīng)用環(huán)境且易于系統(tǒng)維護(hù)和交互管理。文獻(xiàn)[7]提出并基于實(shí)驗(yàn)證明RBAC較好地解決了云計(jì)算應(yīng)用環(huán)境下的企業(yè)問(wèn)題。文獻(xiàn)[8]研究了RBAC在云計(jì)算系統(tǒng)的現(xiàn)狀，認(rèn)為模型作為云的基礎(chǔ)設(shè)施關(guān)鍵技術(shù)適用于多域環(huán)境，并且已經(jīng)成功地應(yīng)用在醫(yī)療、股票和社交網(wǎng)絡(luò)中。同時(shí)，RBAC模型被大多數(shù)主流的云平臺(tái)所采用，如：OpenStack、Xen、Windows Azure等。文獻(xiàn)[9]提出使用中間件實(shí)現(xiàn)多域系統(tǒng)安全策略，并結(jié)合醫(yī)療案例證實(shí)訪問(wèn)控制策略在多域的云計(jì)算系統(tǒng)中具有可行性。

在安全互操作方面，大規(guī)模分布式環(huán)境促使越來(lái)越多單托管域的企業(yè)聯(lián)合起來(lái)，形成多管理域協(xié)作環(huán)境成為趨勢(shì)。文獻(xiàn)[10]指出多域安全策略異構(gòu)問(wèn)題是各類云系統(tǒng)協(xié)作進(jìn)程中的重要挑戰(zhàn)，這個(gè)過(guò)程要既能有效地支持跨域互操作又能夠保證安全。文獻(xiàn)[11]通過(guò)研究相關(guān)文獻(xiàn)，提出角色委托機(jī)制、映射機(jī)制、信任機(jī)制和策略合成機(jī)制等，是目前學(xué)術(shù)界涉及的幾個(gè)研究方向。其中，基于RBAC模型的角色映射機(jī)制是安全互操作問(wèn)題的研究熱點(diǎn)，例如：文獻(xiàn)[12]為實(shí)現(xiàn)分布環(huán)境的跨域訪問(wèn)，提出利用一種基于動(dòng)態(tài)角色轉(zhuǎn)換的策略來(lái)構(gòu)建域間訪問(wèn)控制規(guī)則和屬性約束；文獻(xiàn)[13]在RBAC基礎(chǔ)上，建立域域之間的角色映射關(guān)系，采用直接轉(zhuǎn)換方式實(shí)現(xiàn)域間角色關(guān)聯(lián)以保障單個(gè)自治域的安全。

綜合上述方案，在RBAC策略域的互操作過(guò)程中的授權(quán)管理與訪問(wèn)控制問(wèn)題在一定程度上得到了解決。然而，在實(shí)施過(guò)程中仍然可能出現(xiàn)違反域內(nèi)安全約束和自治性問(wèn)題。文獻(xiàn)[14]仿真模擬了動(dòng)態(tài)協(xié)同環(huán)境中安全策略的一致性維護(hù)，在定義和維護(hù)域間安全訪問(wèn)控制策略方面進(jìn)行了有益嘗試，但并未給出工具檢測(cè)方法的形式化定義，且缺乏有效的域間訪問(wèn)控制策略的集成方案。

在安全策略驗(yàn)證方面，目前已存在多種模型檢測(cè)技術(shù)[15-17]。這些技術(shù)的基本思想是：用形式化建模語(yǔ)言描述待驗(yàn)證的安全策略系統(tǒng)模型，用時(shí)態(tài)邏輯公式描述待驗(yàn)證的安全屬性，然后將它們輸入到檢測(cè)工具中完成驗(yàn)證。例如，文獻(xiàn)[15]提出一種通用訪問(wèn)控制屬性驗(yàn)證模型，它能夠維護(hù)各種靜態(tài)、動(dòng)態(tài)訪問(wèn)控制的安全約束，并且通過(guò)組合驗(yàn)證方式提供測(cè)試用例以檢測(cè)模型和策略規(guī)則的一致性；同時(shí)生成基于擴(kuò)展的訪問(wèn)控制標(biāo)記語(yǔ)言（eXtensible Access Control Markup Language， XACML）訪問(wèn)控制認(rèn)證策略，其中XACML2.0或XACML 3.0已經(jīng)成為目前協(xié)同系統(tǒng)中策略規(guī)則的規(guī)范化描述語(yǔ)言。文獻(xiàn)[16]提出使用黑盒模型檢測(cè)技術(shù)來(lái)驗(yàn)證待檢測(cè)的訪問(wèn)控制屬性。文獻(xiàn)[17]給出一種訪問(wèn)控制策略檢測(cè)工具，該工具提供了設(shè)置訪問(wèn)控制策略和屬性規(guī)則的圖形化用戶界面，可以通過(guò)符號(hào)模型檢測(cè)器（Symbolic Model Verifier， SMV）進(jìn)行訪問(wèn)控制策略的一致性驗(yàn)證。此外，研究還提供了完整的測(cè)試工具包以及生成XACML語(yǔ)言形式的策略輸出。

綜上所述，訪問(wèn)控制、安全互操作和模型檢測(cè)之間是互相制約、相輔相成的，因此，研究一種有效的多域安全策略驗(yàn)證管理技術(shù)來(lái)實(shí)現(xiàn)上述功能具有重要的意義。從公開(kāi)的國(guó)內(nèi)外文獻(xiàn)中還沒(méi)有發(fā)現(xiàn)將上述三者統(tǒng)一起來(lái)進(jìn)行形式化研究并轉(zhuǎn)化應(yīng)用的成果，類似的研究工作也甚少，且不具有普適性。例如，文獻(xiàn)[18]提出一種面向網(wǎng)格系統(tǒng)中分布式訪問(wèn)控制策略的管理方法，研究不同策略行為的表現(xiàn)形式并給出了相應(yīng)的安全策略驗(yàn)證方案。然而，由于缺乏對(duì)于安全互操作問(wèn)題的關(guān)注，其系統(tǒng)模型存在嚴(yán)重的跨域訪問(wèn)安全風(fēng)險(xiǎn)。同時(shí)性能評(píng)估結(jié)果表明，該方案僅適用于小規(guī)模的分布式系統(tǒng)、只支持?jǐn)?shù)目相對(duì)較小的安全策略的驗(yàn)證。

因此，本文提出了一種適用于云計(jì)算系統(tǒng)的多域安全策略驗(yàn)證管理技術(shù)，可以在大規(guī)模的安全互操作環(huán)境中實(shí)現(xiàn)形式化定義訪問(wèn)控制規(guī)則、規(guī)范安全屬性和驗(yàn)證安全策略。實(shí)現(xiàn)過(guò)程表明，該技術(shù)通過(guò)引入RBAC角色層次推理，具有強(qiáng)大的角色關(guān)系表達(dá)能力，其形式化定義了RBAC規(guī)則表達(dá)式和屬性命題，并進(jìn)一步提出了安全策略驗(yàn)證算法，在大規(guī)模安全域模擬實(shí)驗(yàn)中顯示出更強(qiáng)的通用性和可行性。

1預(yù)備知識(shí)

簡(jiǎn)單介紹安全互操作和模型檢測(cè)的相關(guān)理論，RBAC模型的基礎(chǔ)理論請(qǐng)讀者自行參閱文獻(xiàn)[4]，文中不再贅述。

1.1安全互操作

在多域系統(tǒng)中，安全互操作要兼顧自治性和安全性兩大原則[3，12]。其中自治性原則是指如果一個(gè)訪問(wèn)請(qǐng)求在單個(gè)管理域系統(tǒng)中被允許，那么它在安全互操作中也必須被允許；安全性原則是指如果一個(gè)訪問(wèn)請(qǐng)求在單個(gè)管理域系統(tǒng)中被禁止，那么它在安全互操作中也須被禁止。在基于RBAC模型的安全互操作系統(tǒng)中，域間聯(lián)合所增加的角色繼承關(guān)系可能會(huì)造成本地安全策略的違反問(wèn)題，而這種違反約束的行為可以通過(guò)相關(guān)的策略檢測(cè)而被預(yù)先發(fā)現(xiàn)，提前避免安全風(fēng)險(xiǎn)。安全互操作屬性有環(huán)繼承、權(quán)限提升、職責(zé)分離（Separation of Duty， SoD）原則和自治性等[19]。下面，在給出上述安全屬性定義之前，先進(jìn)行如下約定。

1）r1 → r2，表示角色r1繼承角色r2的權(quán)限。

2）如果角色rk屬于域di的角色，則表示為dirk；同理，diut表示域di的用戶ut，dipw表示域di的權(quán)限pw。

定義1繼承環(huán)屬性。

在域間互操作過(guò)程中，由于新的角色映射關(guān)系的引入，角色層次之間形成了環(huán)狀結(jié)構(gòu)的繼承關(guān)系，導(dǎo)致下級(jí)角色非法擁有了上級(jí)角色權(quán)限，這種情況稱為繼承環(huán)，記為：dirj>>dirk。如圖1（a）所示，在域di中，用戶diut被指派給角色dirk，則用戶diut同時(shí)獲得到了它的上級(jí)角色dirj的權(quán)限。

定義2權(quán)限提升屬性。

在域間互操作過(guò)程中，新的角色關(guān)聯(lián)關(guān)系導(dǎo)致以前沒(méi)有關(guān)聯(lián)的角色之間形成某種繼承關(guān)系，使得角色獲取到更大的權(quán)限，這種情況稱為權(quán)限提升，記為：dirj≥dirk。如圖1（b）所示，域di用戶diut被指派給角色dirj，用戶diut在獲得角色dirj權(quán)限的同時(shí)還獲得了角色dirk的權(quán)限，即使用戶diut與角色dirk之間并不存在直接指派關(guān)系。

定義3職責(zé)分離屬性。

如果域di用戶diut（或者域dn用戶dnut）由于域間角色映射關(guān)系，使得它可以獲取或在會(huì)話中激活存在SoD約束的兩互斥角色dirj和dirk，那么就違反了SoD約束，如圖1（c）所示。本文驗(yàn)證職責(zé)分離屬性是基于下面兩個(gè)性質(zhì)[4]：

1）如果角色rk和rm之間不存在直接或間接的繼承關(guān)系，那么rk和rm完全互斥；

2）如果角色rk和rm完全互斥，那么不存在有任何角色可以同時(shí)繼承rk和rm。

定義4自治性屬性。

自治性屬性要求在域間互操作環(huán)境中的訪問(wèn)控制權(quán)限不能違反自治管理域的本地操作權(quán)限。安全互操作要求平衡自治性和交互性，違反任何單個(gè)域的安全策略都是不允許的。

1.2模型檢測(cè)

模型檢測(cè)技術(shù)是驗(yàn)證安全互操作屬性的重要手段，它能夠解決訪問(wèn)控制模型的通用屬性驗(yàn)證問(wèn)題。早在20世紀(jì)80年代，基于時(shí)序邏輯的模型檢測(cè)技術(shù)[20]就被廣泛關(guān)注，其原理如圖2描述：假設(shè)，M表示狀態(tài)遷移系統(tǒng)，F(xiàn)表示模態(tài)時(shí)序邏輯公式，將“系統(tǒng)是否具有所期望的性質(zhì)”轉(zhuǎn)化成數(shù)學(xué)問(wèn)題來(lái)描述，即“M是否是公式F的一個(gè)模型”，記為M|=F？。

模型檢測(cè)過(guò)程主要包括系統(tǒng)建模、建立系統(tǒng)性質(zhì)規(guī)范和執(zhí)行驗(yàn)證3個(gè)過(guò)程。其中，系統(tǒng)建模主要是建立與系統(tǒng)相對(duì)應(yīng)的遷移系統(tǒng)或Kripke[16]結(jié)構(gòu)，用來(lái)描述系統(tǒng)方案的動(dòng)態(tài)行為；系統(tǒng)性質(zhì)規(guī)范的建立要求統(tǒng)一系統(tǒng)性質(zhì)的表達(dá)形式，多數(shù)會(huì)使用計(jì)算樹(shù)邏輯（Computation Tree Logic， CTL）、線性時(shí)態(tài)邏輯（Linear Temporal Logic， LTL）等屬性描述語(yǔ)言來(lái)規(guī)范表達(dá)；執(zhí)行驗(yàn)證環(huán)節(jié)可以采用方便的自動(dòng)驗(yàn)證模式，由模型檢測(cè)器完成。

目前，存在大量支持模型檢測(cè)技術(shù)應(yīng)用的模型檢測(cè)工具，如：SMV、簡(jiǎn)單進(jìn)程元語(yǔ)言解釋器（Simple Promela Interpreter， SPIN）[21]、改進(jìn)符號(hào)模型檢測(cè)器（New Symbolic Model Verifier， NuSMV）[22]和Uppaal[23]等。本文后續(xù)的研究工作選用NuSMV這款開(kāi)放架構(gòu)的模型檢測(cè)器。

2云安全策略模型

在本章中，主要完成兩方面的工作：

1）針對(duì)云系統(tǒng)中RBAC方案不能有效地解決不同云托管域的策略集成問(wèn)題，引入域內(nèi)管理和域間管理兩類角色層次關(guān)系，對(duì)傳統(tǒng)的適用于單域的RBAC模型進(jìn)行重定義，從而建立一種基于多域的角色訪問(wèn)控制（multidomain Role Based Access Control， domRBAC）模型；

2）給出基于CTL語(yǔ)言的通用訪問(wèn)控制模型轉(zhuǎn)換方法[17]，并對(duì)訪問(wèn)控制規(guī)則、安全屬性和遷移系統(tǒng)的表達(dá)進(jìn)行了規(guī)范。

2.1domRBAC模型

本文在ANSI INCITS 3592004 RBAC[4]的基礎(chǔ)上，綜合考慮了系統(tǒng)功能和審查功能，給出如下形式化定義。

2.1.1基本元素

1）USERS、ROLES、OPS、OBS分別表示用戶、角色、操作、對(duì)象的集合。

2）UAUSERS×ROLES，表示用戶與角色之間多對(duì)多的分配關(guān)系。

3）PRMS=2（OPS×OBS），表示權(quán)限的集合。

4）PAPRMS×ROLES，表示權(quán)限與用戶之間多對(duì)多的分配關(guān)系。

5）Op（p：PRMS） → {opOPS}，表示權(quán)限與操作之間的對(duì)應(yīng)關(guān)系，指明為操作集分配的權(quán)限集p。

6）Ob（p：PRMS） → {obOBS}，表示權(quán)限與對(duì)象之間的對(duì)應(yīng)關(guān)系，指明為對(duì)象集分配的權(quán)限集p。

2.1.2域內(nèi)角色層次

1）assigned_users：SUdi（dirk：ROLES） → 2USERS，表示域di中角色dirk與用戶集USERS之間的映射關(guān)系，即：SUdi（dirk）={diut∈USERS|（diut，dirk）∈UA}。

2）assigned_permissions：SPdi（dirk：ROLES） → 2PRMS，表示域di中角色dirk與權(quán)限集PRMS之間的映射關(guān)系，即：SPdi（dirk）={dipw∈PRMS|（dipw，dirk）∈PA}。

3）RHdiROLES×ROLES，表示域di中角色之間繼承關(guān)系的偏序集合，記為問(wèn)過(guò)，回復(fù)：表示正確。。若dirkdirm，那么dirm的權(quán)限集都是dirk的權(quán)限集，且dirk的用戶集則都是dirm的用戶集，即：dirkdirm UPdi（dirm）UPdi（dirk）∧UUdi（dirk）UUdi（dirm）。

4）authorized_users：UUdi（dirk：ROLES） → 2USERS，表示域di中角色dirk與域內(nèi)角色層次用戶集USERS之間的映射關(guān)系，這種映射只考慮角色dirk與域內(nèi)的其他角色之間的繼承關(guān)系，即：UUdi（dirk）={diut∈USERS|dirmdirk，（diut，dirm）∈UA}。

5）authorized_permissions：UPdi（dirk：ROLES） → 2PRMS，表示域di中角色dirk與域內(nèi)角色層次權(quán)限集PRMS之間的映射關(guān)系，這種映射只考慮角色dirk與域內(nèi)的其他角色之間的繼承關(guān)系，即：UPdi（dirk）={dipw∈PRMS|dirkdirm，（dipw，dirm）∈PA}。

2.1.3域間角色層次

1）RHROLES×ROLES，表示域間角色之間繼承關(guān)系的偏序集合，記為。若dirkdjrm，那么djrm的權(quán)限集都是dirk的權(quán)限集，且dirk的用戶集都是djrm的用戶集。即：dirkdjrm UP（djrm）UP（dirk）∧UU（dirk）UU（djrm）。

2）authorized_users：UU（dirk：ROLES） → 2USERS，表示角色dirk與域間角色層次用戶集USERS之間的映射關(guān)系，這種映射的集合既包括dirk與域內(nèi)角色之間的繼承關(guān)系，又包括dirk與外域角色之間的繼承關(guān)系，即：UU（dirk）=UUdi（dirk）∪{djut∈USERS|djrmdirk，（djut，djrm）∈UA}。

3）authorized_permissions：UP（dirk：ROLES） → 2PRMS，表示角色dirk與域間角色層次權(quán)限集PRMS之間的映射關(guān)系，這種映射關(guān)系既包括dirk與域內(nèi)角色之間的繼承，又包括dirk與外域角色之間的繼承，即：UP（dirk）=UPdi（dirk）∪{djpw∈PRMS|dirkdjrm，（djpw，djrm）∈PA}。

2.1.4謂詞

考慮到時(shí)序邏輯語(yǔ)言中缺乏關(guān)系算子，如：□和。下面，補(bǔ)充一些對(duì)應(yīng)謂詞的定義。

1）IR（rk，rm）表示兩角色間存在（域間或域內(nèi)）直接繼承關(guān)系，即：IR（rk，rm）=true rk□rm。其中，符號(hào)□表示直接繼承關(guān)系。

2）MRdi（dirk，dirm）表示域di角色層次中的兩角色間存在一種（域間或域內(nèi)）直接的或者間接的繼承關(guān)系，即：MRdi（dirk，dirm）=true dirkdirm。

3）RP（rk，rm）表示對(duì)于存在直接繼承關(guān)系的兩角rk，rm（rk□rm），角色rk的分配權(quán)限集是角色rm權(quán)限集的子集，即：RP（rk，rm）=true IR（rk，rm）∧SPdi（rk）UP（rm）。

4）IBdi（dirk，dirm，rn）表示如果任意域角色rn是所在域di中角色dirk和角色dirm的上級(jí)角色，那么，rn的權(quán)限集則同時(shí)包括了dirk的權(quán)限集和dirm的權(quán)限集，即：IBdi（dirk，dirm，rn）=true SPdi（dirk）∪SPdi（dirm）UP（rn）∧rndirk∧rndirm。

5）BA（dirk）表示角色dirk與域內(nèi)角色層次中權(quán)限集的映射關(guān)系，是dirk與域間角色層次中權(quán)限集的映射關(guān)系的子集，即：BA（dirk）=true UPdi（dirk）UP（dirk）。

2.2轉(zhuǎn)換系統(tǒng)

本文采用CTL時(shí)序邏輯來(lái)對(duì)有關(guān)的安全策略進(jìn)行規(guī)范，如：訪問(wèn)控制規(guī)則、安全屬性和變遷系統(tǒng)。

在CTL語(yǔ)言中，前綴路徑量詞可以斷言關(guān)于線性時(shí)序算子的任意組合。據(jù)此，本文規(guī)定使用通用路徑量詞表示“對(duì)所有路徑”，使用線性時(shí)序算子□表示“現(xiàn)在和以后所有狀態(tài)”，使用線性時(shí)序算子◇表示“現(xiàn)在或以后某一狀態(tài)”。另外，規(guī)定時(shí)序模式□Φ表示不變的Φ，時(shí)序模式◇Φ表示可變的Φ，其中，Φ是一個(gè)狀態(tài)公式。

定義5一條domRBAC規(guī)則是形如“if c then d”的命題，其中，約束c是一個(gè)關(guān)于決策許可d的謂詞表達(dá)式（r，UP（r）），因此，由一系列規(guī)則組成的domRBAC策略，可以表示成形如c（r，UP（r））的這種邏輯表達(dá)式形式。

定義6一個(gè)domRBAC訪問(wèn)控制屬性p是形如“b → d”的公式，其中，訪問(wèn)權(quán)限許可d的結(jié)果取決于量化謂詞b與（r，UP（r））之間的映射關(guān)系，其歸約關(guān)系 → 描述了系統(tǒng)內(nèi)部的推理方式。

定義7遷移系統(tǒng)TS是一個(gè)四元組（S，Act，δ，i0），其中：

1）S是有限狀態(tài)的集合，S={Permit，Deny}；

2）Act是活動(dòng)的集合，Act={（r1，UP（r1））， （r2，UP（r2）），…，（rn，UP（rn））}；

3）δ是狀態(tài)轉(zhuǎn)移關(guān)系，且δ：S×Act → S；

4）i0∈S是初始狀態(tài)。

根據(jù)定義6，訪問(wèn)控制屬性p可以被表示成遷移系統(tǒng)TS的命題，如p：S×Act2 → S，因此，domRBAC策略可以對(duì)應(yīng)地轉(zhuǎn)換成邏輯公式：p=（Si*（r1，UP（r1））*（r2，UP（r2））*…*（rn，UP（rn））） → d，其中，p∈P，P代表屬性集合，并且*是CTL中的布爾算子。此外，domRBAC模型的功能規(guī)則對(duì)應(yīng)于轉(zhuǎn)換系統(tǒng)TS的轉(zhuǎn)換關(guān)系δ，因此，將domRBAC訪問(wèn)控制屬性表示為時(shí)態(tài)邏輯表達(dá)式（即時(shí)態(tài)規(guī)范），就可以斷言屬性p在TS下是否可滿足，即驗(yàn)證TS|=□（b → ◇d）是否為真。

2.3屬性規(guī)范

結(jié)合前面2.1節(jié)內(nèi)容，下面給出繼承環(huán)屬性、權(quán)限提升屬性、職責(zé)分離屬性以及自治性安全屬性的時(shí)態(tài)邏輯定義。

定義8繼承環(huán)屬性為：

TSdomRBAC|=□（RP（dirj，dirk） → ◇Deny）（1）

其中dirj，dirk表示域di中的兩個(gè)角色。通過(guò)驗(yàn)證命題RP（dirj，dirk） → ◇Deny是否滿足TSdomRBAC中的不變式，來(lái)檢測(cè)角色dirj是否存在環(huán)狀繼承。

定義9權(quán)限提升屬性為：

TSdomRBAC|=□（（MRdi（dirj，dirk）∧RP（dirj，dirk） → ◇Deny）（2）

其中dirj是用戶diut對(duì)應(yīng)的指派角色。通過(guò)驗(yàn)證命題（MRdi（dirj，dirk）∧RP（dirj，dirk） → ◇Deny是否滿足不變式TSdomRBAC，來(lái)檢測(cè)角色dirj，dirk之間是否因?yàn)橛蜷g映射關(guān)聯(lián)導(dǎo)致用戶diut的權(quán)限提升。

定義10職責(zé)分離屬性為：

TSdomRBAC|=□（（dirj∈dirsw∧dirk∈dirsw∧（RP（dirj，dirk）∨RP（dirk，dirj）∨IBdi（dirj，dirk，rm））） → ◇Deny）（3）

鑒于SoD屬性是基于角色對(duì)實(shí)現(xiàn)的，這就需要檢測(cè)互斥角色對(duì)的最小數(shù)量的約束關(guān)系：（dirs，n）∈SSD，其中，n≥2且dirs代表一個(gè)角色集。同樣地，可以等價(jià)地表示成二項(xiàng)系數(shù)|di rs| C2 （|di rs|2）|di rs|！2！（|di rs|-2）！。

定義11自治性屬性為：

TSdomRBAC|=□（BA（dirk） → ◇Permit）（4）

在互操作中，通過(guò)檢測(cè)域di中角色dirk的所有指派權(quán)限和角色層次映射生成權(quán)限是否被保護(hù)，來(lái)驗(yàn)證自治性屬性。

3技術(shù)實(shí)現(xiàn)

本章討論云系統(tǒng)多域安全策略驗(yàn)證技術(shù)實(shí)現(xiàn)問(wèn)題。首先，提出一種基于圖論的角色關(guān)聯(lián)（角色角色）映射算法，該算法通過(guò)引入RBAC角色層次推理來(lái)實(shí)現(xiàn)對(duì)系統(tǒng)模型中角色層次關(guān)系的準(zhǔn)確模擬。該算法的核心思想是，用稀疏圖數(shù)據(jù)結(jié)構(gòu)表示角色層次關(guān)系，用鏈表替代傳統(tǒng)矩陣模擬角色層次，以獲取更高的屬性驗(yàn)證性能。其次，給出了基于多域的云安全策略驗(yàn)證算法。下面，先給出實(shí)現(xiàn)部分的相關(guān)定義。

定義12G=（V，E）是一個(gè)表達(dá)域間角色層次的有向圖，其中V（VROLES）代表一組有限、非空的角色頂點(diǎn)集合，E代表圖中有向邊的集合，并且，每條有向邊都是相關(guān)兩角色頂點(diǎn)的一對(duì)序偶（dirm，djrn），其中兩角色頂點(diǎn)的關(guān)系為dirmdjrn。

定義13圖G中的一條路徑是指由n-1條有向邊所構(gòu)成的序列集合{（dir1，dir2），（dir2，dir3），…，（dirn-1，dirn）}，連接從角色頂點(diǎn)dir1到角色頂點(diǎn)dirn，一條路徑代表了兩角色頂點(diǎn)dir1和dirn之間的間接繼承關(guān)系。

定義14圖G的鄰接表是列表|V|的一個(gè)數(shù)組L，圖G中的每個(gè)角色頂點(diǎn)都被包含在V集合里面。對(duì)于每個(gè)角色頂點(diǎn)dirm來(lái)說(shuō)，都存在一個(gè)指針Ldirm指向一個(gè)涵蓋與dirm相鄰接的所有角色頂點(diǎn)的鏈接表。本文用AG表示圖G的鄰接表，用nil指針表示一個(gè)鏈表的終止。

定義15G*=（V，E*）是圖G=（V，E）的傳遞閉包，其中，當(dāng)且僅當(dāng)圖G中存在一條從頂點(diǎn)u到頂點(diǎn)v的路徑時(shí)，E*集合中包含有一條邊edge（u，v）。本文用TG表示一個(gè)基于鄰接表存儲(chǔ)的有向圖G=（V，E）的傳遞閉包列表。

基于圖論的角色關(guān)聯(lián)映射算法的結(jié)構(gòu)如算法1所示。這里，TG為算法返回的生成結(jié)果，期間采用的改進(jìn)Warshall算法的相關(guān)信息可參考文獻(xiàn)[24]。在角色關(guān)聯(lián)映射算法中，第1步，根據(jù)domRBAC規(guī)則生成有向圖G=（V，E）的鄰接表AG，這個(gè)過(guò)程可以利用如文獻(xiàn)[22]中提到的解析器（Simple API for XML， SAX）進(jìn)行自動(dòng)生成；第2步，根據(jù)AG計(jì)算圖G的傳遞閉包列表TG，本文采用一種時(shí)間復(fù)雜度為O（|V||E|）的改進(jìn)傳遞閉包算法[24]。

算法1基于圖論的角色關(guān)聯(lián)映射算法（如圖3）。

示例1如圖4所示是一個(gè)定義了兩個(gè)域d1，d2之間互操作的域間訪問(wèn)控制策略應(yīng)用場(chǎng)景。其中，在管理域d1中有角色d1ra，d1rb，d1rc，d1rd，d1re，角色d1ra繼承d1rb的所有權(quán)限并間接繼承d1re的權(quán)限，角色d1rc繼承d1rd的所有權(quán)限并間接繼承d1re的權(quán)限，并且角色d1rb和角色d1rc之間還存在SSD約束；在管理域d2中有兩個(gè)角色d2rf，d2rg，角色d2rf繼承d2rg的全部權(quán)限。此外，域d1和d2之間的域間繼承關(guān)系定義如下：

1）角色d1rb繼承角色d2rg；

2）角色d2rg繼承角色d1rc。

如圖5所示是AG和TG的生成結(jié)果，具體的計(jì)算過(guò)程如下所示。

首先，利用BOOST C++程序庫(kù)[25]中的Boost Graph中adjacency_list類，生成一個(gè)通用的以鄰接表AG結(jié)構(gòu)存儲(chǔ)的有向圖G；其次，利用Boost Graph庫(kù)中的transitive_closure（）函數(shù)，將圖G輸入并轉(zhuǎn)換生成傳遞閉包結(jié)構(gòu)列表TG。

圖5中的AGd1和TGd1分別表示管理域d1的鄰接表和傳遞閉包列表。根據(jù)定義11，TGd1可以作為一種待檢測(cè)的安全屬性，用于驗(yàn)證原始單個(gè)管理域在與多域的互操作過(guò)程中是否違反了自治性原則。

基于多域的云安全策略驗(yàn)證算法的結(jié)構(gòu)如算法2和圖6所示。在該算法中，首先利用算法2，將根據(jù)云用戶訪問(wèn)需求生成的domRBAC規(guī)則XML文件，經(jīng)過(guò)解析器SAX生成記錄域間角色關(guān)聯(lián)關(guān)系的AG和TG；然后，利用迭代器（Iterator），根據(jù)算法3，迭代生成新的XML文件，具體包括原有的訪問(wèn)控制規(guī)則、新增角色關(guān)系描述規(guī)則以及待驗(yàn)證的安全屬性。由于這些XML文件是經(jīng)過(guò)規(guī)范的邏輯程序，因而可以裝載進(jìn)入檢測(cè)系統(tǒng)直接計(jì)算；最后，NuSMV系統(tǒng)可高效地計(jì)算它并返回查詢結(jié)果R：

1）如果R=true，即TSdomRBAC|=p為真。說(shuō)明屬性p在TS下是可滿足。

2）如果R=FALSE，即TSdomRBAC|=p為假。說(shuō)明屬性p在TS下是不可滿足。

算法2云安全策略驗(yàn)證算法。只寫了算法2，卻沒(méi)有看到具體算法，是否遺漏了？請(qǐng)明確?；貜?fù)：算法2是用圖6描述的，所以并沒(méi)有遺漏。

算法3規(guī)則和屬性生成算法。

程序前

procedure ITERATOR_SKELETON（TG）

for all vertex dri∈TG

for all adjacent vertex drj

此處的注釋，是否改為操作。因?yàn)閒or語(yǔ)句后面沒(méi)有執(zhí)行語(yǔ)句了，而直接是結(jié)束語(yǔ)句了，請(qǐng)明確。//生成時(shí)態(tài)規(guī)范的規(guī)則和屬性

end procedure

程序后

4性能評(píng)測(cè)

下面對(duì)本文提出的技術(shù)進(jìn)行實(shí)驗(yàn)性能評(píng)估。實(shí)驗(yàn)說(shuō)明如下：首先，利用NetworkX工具生成云端用戶的訪問(wèn)控制請(qǐng)求，作為解析器的輸入數(shù)據(jù)。其中，NetworkX是一款用Python語(yǔ)言開(kāi)發(fā)的圖論和復(fù)雜網(wǎng)建模工具，能夠提供gnc_graph（）函數(shù)動(dòng)態(tài)生成用戶請(qǐng)求和對(duì)應(yīng)權(quán)限。其次，使用domRBAC模擬器模擬云托管域的角色指派。

假設(shè)分別有5，10，15，20個(gè)云托管域，其中每個(gè)托管域中含有50個(gè)角色。在此基礎(chǔ)上，實(shí)驗(yàn)設(shè)計(jì)模擬4個(gè)不同規(guī)模大小的域間互操作環(huán)境，分別是具有250，500，750，1000個(gè)角色的云協(xié)同計(jì)算環(huán)境。系統(tǒng)的運(yùn)行環(huán)境為Windows Server 2003 R2操作系統(tǒng)，CPU版本為Intel Core2 3.0GHz，內(nèi)存為4GB DDR2，開(kāi)發(fā)語(yǔ)言為C++。

實(shí)驗(yàn)提供了一系列有關(guān)安全屬性驗(yàn)證時(shí)間的定量結(jié)果。如表1所示，給出了解析器和NuSMV驗(yàn)證器的實(shí)驗(yàn)數(shù)據(jù)，其中，TG的數(shù)量對(duì)應(yīng)訪問(wèn)控制規(guī)則的數(shù)目。從表1看出，執(zhí)行時(shí)間：1#<2#<3#4#，說(shuō)明規(guī)模越大的系統(tǒng)，其屬性驗(yàn)證的時(shí)間開(kāi)銷也越大。通過(guò)分析可知，系統(tǒng)中安全屬性的檢測(cè)耗時(shí)會(huì)隨著安全屬性數(shù)目以及domRBAC規(guī)則數(shù)量的增加而增大，這是因?yàn)閷傩詳?shù)和規(guī)則數(shù)決定了檢測(cè)器中有序二叉決策圖（Binary Decision Diagram， BDD）的可到達(dá)狀態(tài)數(shù)，直接影響了狀態(tài)判斷次數(shù)，那么，如何降低系統(tǒng)規(guī)模對(duì)于屬性驗(yàn)證時(shí)間的影響？可以考慮采用并行檢測(cè)的方式進(jìn)行屬性驗(yàn)證，并且，表1的檢測(cè)數(shù)據(jù)是在NuSMV模型驗(yàn)證器的正常模式下實(shí)驗(yàn)采集的，如果采用優(yōu)化模式，性能會(huì)因增加3個(gè)參數(shù)設(shè)置而相對(duì)提高，因?yàn)檎z測(cè)模式是不包含任何額外的命令行參數(shù)的。

基于上述分析，后續(xù)實(shí)驗(yàn)將圍繞兩個(gè)方面展開(kāi)設(shè)計(jì)：一方面，引入并行檢測(cè)和優(yōu)化檢測(cè)兩種實(shí)驗(yàn)?zāi)Ｊ?，分模式測(cè)試不同規(guī)模系統(tǒng)的屬性驗(yàn)證時(shí)間；另一方面，分規(guī)模測(cè)試不同并行進(jìn)程數(shù)的屬性驗(yàn)證時(shí)間。

如表2所示，在8個(gè)進(jìn)程并行檢測(cè)模式下，分別測(cè)量了正常模式（N）和優(yōu)化模式（O）的屬性驗(yàn)證時(shí)間，N和O是指NuSMV模型檢測(cè)器實(shí)驗(yàn)時(shí)的兩種參數(shù)設(shè)置狀態(tài)。其中，1#（5×50）規(guī)模的系統(tǒng)時(shí)間太?。?1min），可忽略不計(jì)（表2中表示為“—”）。表2中的時(shí)間減少率（Reduction_time），定量描述了多進(jìn)程并行檢測(cè)模式對(duì)比單進(jìn)程串行檢測(cè)模式的執(zhí)行效率，它的具體計(jì)算方法如下：

Reduction_time=（1-maxT/Single_process_time）×100%（5）

其中：maxT表示（tPi）Ni=1的最大值，并且N表示并行執(zhí)行的進(jìn)程數(shù)；tPi表示進(jìn)程Pi（1≤i≤N）的執(zhí)行時(shí)間；∑Ni=1tPi則表示多個(gè)進(jìn)程順序執(zhí)行的時(shí)耗總和。

上述實(shí)驗(yàn)結(jié)果表明：

1）并行檢測(cè)顯著地提高了系統(tǒng)的屬性驗(yàn)證性能。例如，表2中的數(shù)據(jù)顯示，當(dāng)并行檢測(cè)進(jìn)程數(shù)為8時(shí)，Reduction_time的平均值在正常檢測(cè)模式下為86.3%且在優(yōu)化檢測(cè)模式下為78.0%，在三種規(guī)模的系統(tǒng)中，正常模式下Reduction_time分別為88.5%、85.9%、84.5%；優(yōu)化模式下Reduction_time分別為82.9%、70.1%、81.1%。用這個(gè)平均值比較不科學(xué)，有可能趨勢(shì)不一致，因此改為現(xiàn)在這樣的描述，是否符合表達(dá)？請(qǐng)明確。相比單個(gè)進(jìn)程檢測(cè)模式具有很好的時(shí)間性能。

2）時(shí)間隨機(jī)波動(dòng)，優(yōu)化模式比正常模式具有更穩(wěn)定的屬性驗(yàn)證性能。從圖7～9中看出，模型驗(yàn)證器NuSMV的執(zhí)行時(shí)間在正常模式相比優(yōu)化模式下顯示出了更大的波動(dòng)性和不可預(yù)測(cè)性。隨著并行進(jìn)程數(shù)的不斷增加，系統(tǒng)安全屬性的驗(yàn)證時(shí)間必然會(huì)因角色數(shù)量的增加而受到影響。隨機(jī)波動(dòng)則是由安全屬性的數(shù)量、BDD可到達(dá)狀態(tài)的數(shù)量等多因素共同影響所致。

3）在大規(guī)模系統(tǒng)中，優(yōu)化模式下的屬性驗(yàn)證時(shí)間開(kāi)銷要明顯低于正常模式；然而，在中小規(guī)模系統(tǒng)中，反而是正常模式下的屬性驗(yàn)證時(shí)間開(kāi)銷明顯低于優(yōu)化模式。例如，圖7～9，在2#（10×50）和3#（15×50）系統(tǒng)中，存在maxTnormal

4）∑Ni=1tPi≠Single_process_time，說(shuō)明在執(zhí)行相同數(shù)目的屬性驗(yàn)證時(shí)，多個(gè)進(jìn)程順序執(zhí)行的時(shí)耗總和與單進(jìn)程執(zhí)行驗(yàn)證的總時(shí)間并不相等。

5結(jié)語(yǔ)

本文研究了基于訪問(wèn)控制規(guī)則和安全互操作屬性的策略規(guī)范和驗(yàn)證問(wèn)題，提出了一種適用于云計(jì)算系統(tǒng)的多域安全策略驗(yàn)證管理技術(shù)。文中的主要工作如下：1）提出一種基于多域環(huán)境的角色訪問(wèn)控制（domRBAC）模型；2）研究了安全互操作理論，建立了基于CTL時(shí)序邏輯的轉(zhuǎn)換規(guī)范，并給出環(huán)繼承屬性、權(quán)限提升屬性、職責(zé)分離屬性以及自治性屬性的時(shí)態(tài)邏輯表達(dá)形式；3）給出了技術(shù)的詳細(xì)實(shí)現(xiàn)，為基于多域的安全策略驗(yàn)證管理提供了一整條工具鏈。實(shí)驗(yàn)結(jié)果表明，該技術(shù)方案能夠較好地實(shí)現(xiàn)域間互操作中的安全策略表達(dá)、規(guī)范和安全策略驗(yàn)證，在較大規(guī)模的云系統(tǒng)中具有穩(wěn)定性、高效性和可行性。下一步將完善跨域資源使用約束、模型檢測(cè)算法和訪問(wèn)安全威脅消解等方面的研究，進(jìn)一步提高云系統(tǒng)中多域安全策略的管理效果。

參考文獻(xiàn)：

[1]

楊健，汪海航，王劍，等.云計(jì)算安全問(wèn)題研究綜述[J].小型微型計(jì)算機(jī)系統(tǒng)，2012，33（3）：472-479.（YANG J， WANG H H， WANG J， et al. Survey on some security issues of cloud computing [J]. Journal of Chinese Computer Systems， 2012， 33（3）： 472-479.）

[2]

ARMBRUST M， FOX A， GRIFFITH R， et al. A view of cloud computing [J]. Communications of the ACM， 2010， 53（5）： 50-58.

[3]

陳華山，皮蘭，劉峰，等.網(wǎng)絡(luò)空間安全科學(xué)基礎(chǔ)的研究前沿及發(fā)展趨勢(shì)[J].信息網(wǎng)絡(luò)安全，2015（3）：1-5.（CHEN H S， PI L， LIU F， et al. Research on frontier and trends of science of cybersecurity [J]. Netinfo Security， 2015（3）： 1-5.）

[4]

American National Standard Institute. ANSI INCITS 3592004， American national standard for information technologyrole based access control [S]. New York： American National Standards Institute， 2004.

[5]

SCHEFERWENZL S， STREMBECK M. Modeling contextaware RBAC models for business processes in ubiquitous computing environments [C]// Proceedings of the 2012 Third FTRA International Conference on Mobile， Ubiquitous， and Intelligent Computing. Piscataway， NJ： IEEE， 2012： 126-131.

[6]

YAN D， TIAN Y， HUANG J， et al. Privacyaware RBAC model for Web services composition [J]. The Journal of China Universities of Posts and Telecommunications， 2013， 20（S1）： 30-34.

[7]

LI W， WAN H， REN X， et al. A refined RBAC model for cloud computing [C]// Proceedings of the 2012 IEEE/ACIS 11th International Conference on Computer and Information Science. Piscataway， NJ： IEEE， 2012： 43-48.

[8]

葉春曉，郭東恒.多域環(huán)境下安全互操作研究[J].計(jì)算機(jī)應(yīng)用，2012，32（12）：3422-3425.（YE C X， GUO D H. Research on secure interoperation in multidomain environment [J]. Journal of Computer Applications， 2012， 32（12）： 3422-3425.）

[9]

MIGLIAVACCA M， PAPAGIANNIS I， EYERS D M， et al. Distributed middleware enforcement of event flow security policy [C]// Proceedings of the 2010 ACM/IFIP/USENIX 11th International Conference on Middleware. Berlin： Springer， 2010： 334-354.

[10]

TAKABI H， JOSHI J B D， AHN G J. Security and privacy challenges in cloud computing environments [J]. IEEE Security & Privacy， 2010， 8（6）： 24-31.

[11]

鄒德清，鄒永強(qiáng)，羌衛(wèi)中，等.網(wǎng)格安全互操作及其應(yīng)用研究[J].計(jì)算機(jī)學(xué)報(bào)，2010，33（3）：514-525.（ZOU D Q， ZOU Y Q， QIANG W Z， et al. Grid security interoperation and its application [J]. Chinese Journal of Computers， 2010， 33（3）： 514-525.）

[12]

KAPADIA A， ALMUHTADI J， ROY C， et al. IRBAC 2000： secure interoperability using dynamic role translation [R]. Champaign， IL： University of Illinois at UrbanaChampaign， 1999： 1-7.

[13]

ALMUHTADI J， KAPADIA A， CAMPBELL R， et al. The AIRBAC 2000 model： administrative interoperable rolebased access control [R]. Champaign， IL： University of Illinois at UrbanaChampaign， 2000： 1-9.

[14]

HU V C， KUHN D R， XIE T. Property verification for generic access control models [C]// EUC08： Proceedings of the 2008 IEEE/IFIP International Conference on Embedded and Ubiquitous Computing. Piscataway， NJ： IEEE， 2008， 2： 243-250.

[15]

BRYANS J W， FITZGERALD J S. Formal Engineering of XACML Access Control Policies in VDM++ [M]. Berlin： Springer， 2007： 1-23.

[16]

HU V C， KUHN D R， XIE T， et al. Model checking for verification of mandatory access control models and properties [J]. International Journal of Software Engineering and Knowledge Engineering， 2011， 21（1）： 103-127.

[17]

HWANG J H， XIE T， HU V， et al. ACPT： a tool for modeling and verifying access control policies [C]// Proceedings of the 2010 IEEE International Symposium on Policies for Distributed Systems and Networks. Piscataway， NJ： IEEE， 2010： 40-43.

[18]

HWANG J H， ALTUNAY M， XIE T， et al. Model checking grid policies [EB/OL]. [20151128]. http：//hwang250.googlecode.com/.

[19]

SHAFIQ B， JOSHI J B D， BERTINO E， et al. Secure interoperation in a multidomain environment employing RBAC policies [J]. IEEE Transactions on Knowledge and Data Engineering， 2005， 17（11）： 1557-1577.

[20]

CLARKE E M， EMERSON E A. Design and synthesis of synchronization skeletons using branching time temporal logic [M]// 25 Years of Model Checking. Berlin： Springer， 2008： 196-215.

[21]

HOLZMANN G J. The model checker SPIN [J]. IEEE Transactions on Software Engineering， 1997， 23（5）： 279-295.

[22]

CIMATTI A， CLARKE E， GIUNCHIGLIA F， et al. NuSMV： a new symbolic model checker [J]. International Journal on Software Tools for Technology Transfer， 2000， 2（4）： 410-425.

[23]

BERHMANN G， DAVID A， LARSEN K G. A tutorial on UPPAAL [M]// Formal Methods for the Design of RealTime Systems. Berlin： Springer， 2004： 200-236.

[24]

PAPADIMITRIOU C， SIDERI M. On the FloydWarshall algorithm for logic programs [J]. Journal of Logic Programming， 1999， 41（1）： 129-137.

[25]

HERB S， ANDREI A. Boost C++ libraries 1.58.0 [EB/OL]. [20150417]. http：//www.boost.org/.