蔡婷 蔡宇 歐陽凱

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

關(guān)鍵詞：

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

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

0引言

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

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

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

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

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

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

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

1預(yù)備知識

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

1.1安全互操作

在多域系統(tǒng)中，安全互操作要兼顧自治性和安全性兩大原則[3，12]。其中自治性原則是指如果一個訪問請求在單個管理域系統(tǒng)中被允許，那么它在安全互操作中也必須被允許；安全性原則是指如果一個訪問請求在單個管理域系統(tǒng)中被禁止，那么它在安全互操作中也須被禁止。在基于RBAC模型的安全互操作系統(tǒng)中，域間聯(lián)合所增加的角色繼承關(guān)系可能會造成本地安全策略的違反問題，而這種違反約束的行為可以通過相關(guān)的策略檢測而被預(yù)先發(fā)現(xiàn)，提前避免安全風(fēng)險。安全互操作屬性有環(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ān)系的引入，角色層次之間形成了環(huán)狀結(jié)構(gòu)的繼承關(guān)系，導(dǎo)致下級角色非法擁有了上級角色權(quán)限，這種情況稱為繼承環(huán)，記為：dirj>>dirk。如圖1（a）所示，在域di中，用戶diut被指派給角色dirk，則用戶diut同時獲得到了它的上級角色dirj的權(quán)限。

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

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

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

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

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

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

定義4自治性屬性。

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

1.2模型檢測

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

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

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

2云安全策略模型

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

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

2）給出基于CTL語言的通用訪問控制模型轉(zhuǎn)換方法[17]，并對訪問控制規(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分別表示用戶、角色、操作、對象的集合。

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

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

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

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

6）Ob（p：PRMS） → {obOBS}，表示權(quán)限與對象之間的對應(yīng)關(guān)系，指明為對象集分配的權(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)系的偏序集合，記為問過，回復(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謂詞

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

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

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

3）RP（rk，rm）表示對于存在直接繼承關(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的上級角色，那么，rn的權(quán)限集則同時包括了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時序邏輯來對有關(guān)的安全策略進(jìn)行規(guī)范，如：訪問控制規(guī)則、安全屬性和變遷系統(tǒng)。

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

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

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

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

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

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

2.3屬性規(guī)范

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

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

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

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

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

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

其中dirj是用戶diut對應(yīng)的指派角色。通過驗證命題（MRdi（dirj，dirk）∧RP（dirj，dirk） → ◇Deny是否滿足不變式TSdomRBAC，來檢測角色dirj，dirk之間是否因為域間映射關(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屬性是基于角色對實現(xiàn)的，這就需要檢測互斥角色對的最小數(shù)量的約束關(guān)系：（dirs，n）∈SSD，其中，n≥2且dirs代表一個角色集。同樣地，可以等價地表示成二項系數(shù)|di rs| C2 （|di rs|2）|di rs|！2！（|di rs|-2）！。

定義11自治性屬性為：

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

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

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

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

定義12G=（V，E）是一個表達(dá)域間角色層次的有向圖，其中V（VROLES）代表一組有限、非空的角色頂點(diǎn)集合，E代表圖中有向邊的集合，并且，每條有向邊都是相關(guān)兩角色頂點(diǎn)的一對序偶（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|的一個數(shù)組L，圖G中的每個角色頂點(diǎn)都被包含在V集合里面。對于每個角色頂點(diǎn)dirm來說，都存在一個指針Ldirm指向一個涵蓋與dirm相鄰接的所有角色頂點(diǎn)的鏈接表。本文用AG表示圖G的鄰接表，用nil指針表示一個鏈表的終止。

定義15G*=（V，E*）是圖G=（V，E）的傳遞閉包，其中，當(dāng)且僅當(dāng)圖G中存在一條從頂點(diǎn)u到頂點(diǎn)v的路徑時，E*集合中包含有一條邊edge（u，v）。本文用TG表示一個基于鄰接表存儲的有向圖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，這個過程可以利用如文獻(xiàn)[22]中提到的解析器（Simple API for XML， SAX）進(jìn)行自動生成；第2步，根據(jù)AG計算圖G的傳遞閉包列表TG，本文采用一種時間復(fù)雜度為O（|V||E|）的改進(jìn)傳遞閉包算法[24]。

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

示例1如圖4所示是一個定義了兩個域d1，d2之間互操作的域間訪問控制策略應(yī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中有兩個角色d2rf，d2rg，角色d2rf繼承d2rg的全部權(quán)限。此外，域d1和d2之間的域間繼承關(guān)系定義如下：

1）角色d1rb繼承角色d2rg；

2）角色d2rg繼承角色d1rc。

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

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

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

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

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

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

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

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

程序前

procedure ITERATOR_SKELETON（TG）

for all vertex dri∈TG

for all adjacent vertex drj

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

end procedure

程序后

4性能評測

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

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

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

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

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

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í)行時間；∑Ni=1tPi則表示多個進(jìn)程順序執(zhí)行的時耗總和。

上述實驗結(jié)果表明：

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

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

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

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

5結(jié)語

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

參考文獻(xiàn)：

[1]

楊健，汪海航，王劍，等.云計算安全問題研究綜述[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ā)展趨勢[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ī)應(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ī)學(xué)報，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/.