云系統中多域安全策略規范與驗證方法

蔡婷 蔡宇 歐陽凱

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

關鍵詞：

云系統；多域；訪問控制；安全互操作；策略；驗證

中圖分類號： TP309.2 文獻標志碼：A

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）給出了技術的詳細實現，為基于多域的安全策略驗證管理提供了一整條工具鏈。實驗結果表明，該技術方案能夠較好地實現域間互操作中的安全策略表達、規范和安全策略驗證，在較大規模的云系統中具有穩定性、高效性和可行性。下一步將完善跨域資源使用約束、模型檢測算法和訪問安全威脅消解等方面的研究，進一步提高云系統中多域安全策略的管理效果。

參考文獻：

[1]

楊健，汪海航，王劍，等.云計算安全問題研究綜述[J].小型微型計算機系統，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]

陳華山，皮蘭，劉峰，等.網絡空間安全科學基礎的研究前沿及發展趨勢[J].信息網絡安全，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]

葉春曉，郭東恒.多域環境下安全互操作研究[J].計算機應用，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]

鄒德清，鄒永強，羌衛中，等.網格安全互操作及其應用研究[J].計算機學報，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/.