曹 彥 黃志球,2,3 闞雙龍 彭煥峰 柯昌博,4

1(南京航空航天大學(xué)計算機科學(xué)與技術(shù)學(xué)院 南京 211106)2(高安全系統(tǒng)的軟件開發(fā)與驗證技術(shù)工業(yè)和信息化部重點實驗室(南京航空航天大學(xué)) 南京 211106)3(軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心 南京 210093)4 (南京郵電大學(xué)計算機學(xué)院 南京 210023) (caoyan926@nuaa.edu.cn)

隨著無線定位技術(shù)、無線通信技術(shù)的發(fā)展以及移動終端的普及，基于位置的信息服務(wù)已經(jīng)深入人們的日常生活.位置服務(wù)幾乎涵蓋了人類生活的方方面面，包括軍事、交通、物流等[1-3].但位置服務(wù)為人們生活帶來便利的同時，其安全問題受到越來越多的關(guān)注.訪問控制作為一種有效的網(wǎng)絡(luò)安全防護和保護手段，一直備受人們的青睞，其通過限制主體對虛擬信息空間中客體的訪問權(quán)限，保證客體不被非法使用和訪問.為保證基于用戶位置服務(wù)中網(wǎng)絡(luò)資源的安全性，現(xiàn)已有大量研究人員針對位置服務(wù)在傳統(tǒng)訪問控制模型的基礎(chǔ)上進行了位置屬性的擴展，把用戶當(dāng)前的位置信息作為定義用戶是否能夠獲得訪問權(quán)限的限制之一[4].隨著微機電系統(tǒng)技術(shù)、傳感器技術(shù)等在物理設(shè)備中的應(yīng)用，物理設(shè)備已逐步具有計算能力、感知能力和通信能力，從而催生了以實現(xiàn)虛擬信息世界與現(xiàn)實物理世界高度融合為目標的新一代信息技術(shù)，如物聯(lián)網(wǎng)、信息物理融合系統(tǒng).這也使得位置服務(wù)訪問控制策略的制定在該場景下具有了新內(nèi)涵.由于物理世界的融入，訪問控制系統(tǒng)不僅要關(guān)注位置對虛擬信息空間中訪問行為的約束，還要關(guān)注其對物理空間以及兩空間交互行為的約束[5].如何針對新需求下的位置服務(wù)建立訪問控制模型以及驗證模型的正確性，是保證新一代信息技術(shù)下位置服務(wù)安全的一個重要方面[6].

傳統(tǒng)的訪問控制模型，包括強制訪問控制(mandatory access control, MAC)、自主訪問控制(discretionary access control, DAC)和基于角色的訪問控制模型(role based access control, RBAC)[7].但以上模型是非上下文敏感的，對用戶的位置信息都無法進行描述.雖已有大量研究人員在傳統(tǒng)訪問控制模型上進行位置屬性擴展，但現(xiàn)有的模型與驗證方法主要存在如下問題:

1) 已有的位置約束訪問控制模型，多是在傳統(tǒng)訪問控制模型的基礎(chǔ)上，引入位置屬性對角色、權(quán)限和客體進行限制，實現(xiàn)建立用戶-角色賦予/撤銷、角色-權(quán)限賦予/撤銷、角色層次、職責(zé)分離等關(guān)系或約束時符合位置屬性.但這些模型大多針對信息空間，不能描述物理空間的訪問行為和實體的動態(tài)行為.

2) 已有的位置約束訪問控制模型驗證方法，多數(shù)未考慮物理空間訪問行為以及實體動態(tài)行為的建模.文獻[8]雖利用環(huán)境演算[9]能夠解決已有模型無法表達物理空間訪問策略的限制，但因環(huán)境演算對連接關(guān)系不能很好地表達，導(dǎo)致其對信息空間訪問策略的建模能力受限.

針對以上2個問題，本文提出位置約束訪問控制模型以及基于該模型的正確性驗證方法和策略修改方案.主要貢獻有3個方面：

1) 提出同時關(guān)注信息空間與物理空間的位置約束訪問控制(location-constrained role-based access control, LCRBAC)模型和描述系統(tǒng)運行環(huán)境的環(huán)境模型(environment model, EM).利用LCRBAC模型實現(xiàn)物理空間、信息空間及兩空間交互的訪問控制策略的制定，EM模型實現(xiàn)對信息空間和物理空間拓撲結(jié)構(gòu)的刻畫.

2) 利用由英國學(xué)者Milner[10]提出的偶圖和偶圖反應(yīng)系統(tǒng)建模位置約束訪問控制模型并給出相應(yīng)的轉(zhuǎn)換規(guī)則.利用偶圖在EM模型的基礎(chǔ)上建立初始模型，偶圖反應(yīng)規(guī)則描述LCRBAC模型定義的位置約束訪問控制策略，通過初始模型與反應(yīng)規(guī)則中反應(yīng)物的匹配，生成以訪問控制策略標注轉(zhuǎn)移邊的標號變遷系統(tǒng).

3) 提出訪問控制策略修改方案.根據(jù)標號變遷系統(tǒng)對安全屬性的驗證結(jié)果，提出針對死鎖狀態(tài)、違反狀態(tài)和不可達狀態(tài)的策略修改方案.

1 相關(guān)工作分析

為實現(xiàn)訪問控制中位置屬性的描述，國內(nèi)外的研究人員在傳統(tǒng)訪問控制模型基礎(chǔ)上提出具有上下文約束的訪問控制模型.表1從位置約束的訪問控制模型與訪問控制策略的驗證2個方面對相關(guān)工作進行比較分析.

Table 1 Comparison of Related Works表1 相關(guān)工作比較

Notes：√:support;×:no support;⊙:partial support;CS:cyber space;PS:physical space;CPS:the interaction between cyber spaces and physical space; EL: support for entities location; EM: support for entities mobility; FD: formal description; VT: verification tools.

在位置約束的訪問控制模型方面，GEO-RBAC[11]，LRBAC[12],SC-RBAC[13]在RBAC模型的基礎(chǔ)上進行了位置屬性的擴展，用于約束角色、權(quán)限和客體以及模型中關(guān)系的建立.之后又陸續(xù)提出了有關(guān)位置-時序約束的訪問控制模型[14-20]，在模型中同時考慮位置和時間對實體的約束.但以上模型的定義大多是針對信息空間，并沒有考慮物理空間和實體移動特性.因此，現(xiàn)有模型并不適用于物聯(lián)網(wǎng)、信息物理融合系統(tǒng)等范型.1)由于物理空間的引入，需要實現(xiàn)物理訪問控制與信息訪問控制的融合.物理空間劃定了訪問控制策略在物理世界的作用范圍，因此，空間拓撲結(jié)構(gòu)將約束訪問控制策略的制定；另一方面需要考慮兩空間交互策略，包括物理空間狀態(tài)對信息空間訪問行為的約束和信息空間狀態(tài)對物理空間訪問行為的約束.2)拓撲空間中實體移動行為的描述，包括主體的移動和客體的移動.已有的位置約束訪問控制模型，大多是靜態(tài)的描述位置關(guān)系，如SC-RBAC,GSTRABC等模型中定義(teacher,class1)和(teacher,class2)表示用戶在class1和class2都可以賦予teacher角色，但不能表示teacher從class1至class2的移動行為.表1從是否支持信息空間、物理空間及兩空間交互、是否支持實體位置描述以及實體位置動態(tài)變化5個方面對相關(guān)工作進行比較分析.

在位置約束的訪問控制模型驗證方面，已提出多種形式化建模方法，包括Z語言[12]、UML/OCL[16,18]、UML to Alloy[20]、CPN[19]、時間自動機[17]和環(huán)境演算[22- 23].Z語言缺乏自動化的檢測工具；UML/OCL是一種半形式的驗證方法，并不能驗證行為屬性，因此文獻[20]提出UML to Alloy方法，將UML轉(zhuǎn)換到形式化的Alloy語言進行模型檢測，但UML至Alloy轉(zhuǎn)換的正確性是無法保證的；CPN和時間自動機并不能直觀地表達位置屬性，需要不斷地定義變量來表達位置以及位置之間的關(guān)系；文獻[23]中利用環(huán)境演算建模訪問控制模型，環(huán)境演算以描述進程間的位置移動性為主要特征，對于連接關(guān)系及其變化并不能很好地表達，導(dǎo)致其對信息空間訪問行為的描述能力有限.表1從是否對模型有形式化的建模方法以及工具支持2個方面對相關(guān)工作進行比較分析.

2 位置約束的訪問控制模型

信息物理融合系統(tǒng)和物聯(lián)網(wǎng)都是由傳感器節(jié)點、執(zhí)行器節(jié)點、計算系統(tǒng)和網(wǎng)絡(luò)系統(tǒng)組成.傳感器節(jié)點實現(xiàn)對物理世界的感知，將感知信息通過網(wǎng)絡(luò)系統(tǒng)傳遞給計算系統(tǒng)，計算系統(tǒng)按照預(yù)先設(shè)定原則處理信息，并將處理結(jié)果通過網(wǎng)絡(luò)系統(tǒng)發(fā)送給執(zhí)行器節(jié)點，最后由執(zhí)行器節(jié)點接收消息，實現(xiàn)對物理世界的控制.依據(jù)以上系統(tǒng)的組成構(gòu)件，2.1節(jié)引入位置約束訪問控制系統(tǒng)應(yīng)用場景[21,24]，并對系統(tǒng)中基本概念進行分析；2.2節(jié)根據(jù)概念分析結(jié)果提出LCRBAC模型和EM模型.

2.1 應(yīng)用場景

圖1為某銀行部署結(jié)構(gòu)圖，該部署結(jié)構(gòu)圖展示了銀行的物理空間結(jié)構(gòu)和信息空間結(jié)構(gòu).訪問控制管理系統(tǒng)部署于銀行小云服務(wù)器(cloudlet)，控制著主體對客體的訪問行為以及物理空間出入行為.

Fig. 1 Bank deployment diagram圖1 銀行部署結(jié)構(gòu)圖

物理空間用于描述物理實體及相應(yīng)位置、區(qū)域人員及相應(yīng)位置、建筑分布.物理實體是指物理空間中與數(shù)據(jù)信息無關(guān)的硬件設(shè)備.圖1中銀行的物理實體為資金存儲保險柜(safe).資金存儲保險柜主要用于銀行資金的儲備，通過在保險柜中嵌入感知器，感知保險柜的開關(guān)狀態(tài)和位置信息.銀行區(qū)域中的人員按照角色劃分為客戶(customer)、銀行主管(guard)、銀行職員(banker)和技術(shù)維護人員(technician).利用用戶所帶手機(phone)對進入?yún)^(qū)域中的人員進行位置感知，銀行主管、銀行職員和技術(shù)維護人員通過手機登入訪問控制管理系統(tǒng)實現(xiàn)角色分配，其他未登入用戶分配角色為客戶.物理實體和人員位置在圖1中已清晰標注.銀行建筑分布包括大廳(mainarea)、走廊(corridor)、安全屋(saferoom)、職員辦公室(office1,office2)和服務(wù)器房間(serverroom).大廳主要是為用戶提供柜面服務(wù)，所有人員可自由出入；走廊連接各個房間，除用戶之外其他人員可自由出入；安全屋內(nèi)放置一臺服務(wù)器和保險柜，只有銀行主管具有權(quán)限可以出入該房間并讀取客戶歷史交易信息；職員辦公室為銀行職員辦公區(qū)域，銀行主管和銀行職員可自由出入；服務(wù)器房間內(nèi)放置小云服務(wù)器，為銀行日常工作提供技術(shù)支撐，銀行主管和技術(shù)人員可以進入.每個房間的門都具有執(zhí)行器，控制著門的開關(guān).

信息空間用于描述信息實體及位置.信息實體是指數(shù)據(jù)信息.銀行的信息實體包括客戶歷史交易記錄 (historydata)、客戶當(dāng)天交易記錄(currentdata).每個信息實體的位置在圖1中已清晰標注.除物理實體和信息實體之外，還有一類特殊的實體，稱為混合實體，其是對能夠存儲信息實體的物理實體的一種描述.圖1中混合實體包括小云服務(wù)器、安全屋中服務(wù)器(server)以及手機.為簡單起見，圖1利用人員節(jié)點表示手機節(jié)點.

信息空間和物理空間的交互既可以是通過物理空間中的信息控制信息空間的訪問行為，如“只有在安全屋，銀行主管才能讀取用戶歷史交易信息”，也可以通過信息空間中的行為約束物理空間訪問，如“銀行主管只有刪除客戶歷史交易記錄才能離開安全屋”.物理實體、信息實體和混合實體統(tǒng)稱為客體.客體和人員統(tǒng)稱為實體.銀行區(qū)域內(nèi)通過網(wǎng)關(guān)實現(xiàn)實體間互聯(lián).文中不關(guān)注網(wǎng)絡(luò)系統(tǒng)，假設(shè)網(wǎng)絡(luò)系統(tǒng)是高可靠的.

2.2 LCRBAC模型與EM模型

在不同領(lǐng)域中提出的位置描述主要分為2類：層次式的(比如房間)和笛卡兒的(比如GPS).由于層次式具有良好的用戶可讀性，且能很好地表達位置之間的關(guān)系[13]，本文采用它來表達位置.層次式的位置模型可把物理空間結(jié)構(gòu)分為不同的層次，如案例中的位置關(guān)系采用層次式描述如圖2所示：

Fig. 2 Hierarchical spatial tree圖2 層次空間樹

位置約束訪問控制系統(tǒng)運行的物理空間，劃定了訪問控制策略在物理世界的作用范圍.用Loc表示建筑分布中空間區(qū)域集合,Loc={l1,l2,…,ln|n∈+},li(i∈+)為某個具體物理空間區(qū)域，稱為物理位置域，如案例中包括6個物理位置域.

定義1. 物理位置域鄰近關(guān)系.在層次空間樹中，如果物理位置域li與物理位置域lj為兄弟節(jié)點，則稱物理位置域lj與物理位置域li為鄰近關(guān)系，表示為li∞lj.

定義2. 物理位置域包含關(guān)系.在層次空間樹中，如果物理位置域li為物理位置域lj的孩子節(jié)點，則稱物理位置域lj包含物理位置域li，表示為li?lj.

在實際的物理空間中，許多不同物理位置域具有相同的訪問權(quán)限，提出邏輯位置角色的概念實現(xiàn)對相同訪問權(quán)限的物理位置域的統(tǒng)一.

定義3. 邏輯位置角色.邏輯位置角色代表物理空間和信息空間中特定的訪問權(quán)限.

由所有邏輯位置角色組成的集合表示為LocR={lr1,lr2,…,lrk|k∈+,k≤n}，lri(i∈+)為某個具體邏輯位置角色，n為物理位置域個數(shù).

具有包含和鄰近關(guān)系的物理位置域映射為邏輯位置角色時，需要根據(jù)物理位置域訪問權(quán)限的不同映射為不同的邏輯位置角色.如圖3所示，當(dāng)li和lj具有相同的訪問權(quán)限時，li和lj物理位置域映射為同一個邏輯位置角色lri;當(dāng)li和lj區(qū)域的訪問權(quán)限不同時，映射為不同的邏輯位置角色lri和lrj.注意，在包含關(guān)系的物理位置域具有不同的訪問權(quán)限時，li映射為邏輯位置角色lri，灰色區(qū)域映射為邏輯位置角色lrj.因此，不同的邏輯位置角色代表不同的權(quán)限范圍.

Fig. 3 Physical local to logical location role mapping圖3 物理位置域到邏輯位置角色映射

定義4. 物理位置域與邏輯位置角色之間映射函數(shù).物理位置域與邏輯位置角色的映射函數(shù)為f:Loc→LocR，表示物理位置域li到邏輯位置角色lri的映射，函數(shù)f為多對一的關(guān)系.而函數(shù)f′:LocR→Loc表示邏輯位置角色lri到物理位置域li的映射，函數(shù)f′為一對多的關(guān)系.

傳統(tǒng)的訪問控制模型中，RBAC模型是目前公認最有效的模型，相比MAC和DAC具有簡單的表達能力，其通過將權(quán)限與角色相關(guān)聯(lián)，用戶通過成為適當(dāng)角色獲取相應(yīng)權(quán)限.本文在RBAC的基礎(chǔ)上提出LCRBAC模型，以下先給出RBAC模型定義.

定義5. RBAC模型[7].RBAC模型定義如下：

1)U，R，OP，O，S.其中，U表示用戶集合;R表示角色集合;OP表示操作集合;O表示客體集合;S表示會話集合.

2)UA?U×R表示用戶和角色之間多對多關(guān)系.

3)P?OP×O表示權(quán)限集合.

4)PA?P×R表示權(quán)限和角色之間多對多關(guān)系.

5)S→U表示會話到用戶的映射函數(shù).

6)S→2R表示會話到角色的映射函數(shù).

針對信息空間，現(xiàn)有的位置約束訪問控制模型，如GSTRBAC[16]是在RBAC中對角色、權(quán)限和客體進行位置屬性關(guān)聯(lián).(r,lrr)表示當(dāng)用戶的位置為lrr時，用戶可具有角色r；(p,lrp)表示只有在位置lrp，才能執(zhí)行權(quán)限p；(o,lro)表示客體o位于位置lro.因為權(quán)限p是由角色r執(zhí)行，所以在1條策略中(u,(r,lrr)(p,lrp))權(quán)限p的位置lrp與角色r的位置lrr是一致的,即lrp=lrr=lr.因此在LCRBAC模型中策略修改為(u,r,p,lr)，表示當(dāng)用戶u位于lr時，可具有角色r并獲得權(quán)限p.針對物理空間，要描述用戶出入行為，邏輯位置角色成為操作對象，策略描述為(u,r,op,lr).通過以上分析，給出LCRBAC模型定義.

定義6. LCRBAC模型.LCRBAC模型定義如下：

1)U，R，OP，O，LocR.其中，U表示用戶集合；R表示角色集合；OP表示操作集合；O表示客體及相應(yīng)位置集合，為可選項；LocR表示邏輯位置角色集合.

2)UA?U×R表示用戶和角色之間多對多關(guān)系.

3)OP?{OPLocR,OPobjects}表示操作集合.

4)OPLocR={enter,exit}表示物理空間操作集合.

5)OPobjects={Oph,Opp,Opc}分別表示混合實體、物理實體和信息實體操作集合，需根據(jù)具體需求定義.

6)O?Objects×LocO表示客體與其位置之間一對多的關(guān)系.

7)Objects={Physicalen,Hybriden,Cyberen}表示客體集合，由物理實體、混合實體、信息實體組成.

8)LocO?LocR∪Hybriden表示客體位置集合.

9)ObjLoco(o:Objects)→2LocO表示客體到位置的映射函數(shù).其中：

①ObjLoco(o:Physicalen)→LocR；

②ObjLoco(o:Hybriden)→2LocR；

③ObjLoco(o:Cyberen)→2Hybriden×LocR.

10)PA?P×R表示權(quán)限和角色之間多對多關(guān)系.

11)P?P1∪P2表示訪問權(quán)限的集合且P1∩P2=?.

12)P1=2OPLocR×LocR表示物理空間中出入行為控制策略.

13)P2=2OPobjects×Objects×LocO×LocR表示客體上操作行為的控制策略.

根據(jù)LCRBAC模型的定義，位置約束的訪問控制策略有2種表達方式，分別為(U,R,OPLocR,LocR)和(U,R,OPobjects(Objects,LocO),LocR).

1) (R,OPLocR,LocR)用于描述物理空間中主體出入行為的訪問控制策略，如“銀行職員進入走廊”,表示為(banker,enter,corridor).

2) (R,OPobjects,(Objects,LocO),LocR)分3類：

① (R,Opp,(Physicalen,LocO),LocR)表示物理空間中主體在某位置對物理實體的訪問策略，由于物理實體不可遠程訪問，所以LocO與LocR相等.如“在安全區(qū)域，銀行主管可以打開安全屋中保險柜”，表示為(guard,open,safe,saferoom).

② (R,Opc,(Cyberen,LocO),LocR)表示信息空間中主體在某位置對信息實體的訪問策略.信息實體的位置包括2層結(jié)構(gòu)，1層為信息實體所處的混合實體，1層為混合實體所在的邏輯位置角色區(qū)域.因為信息實體可以遠程訪問，LocO與LocR可以不同.如“在安全區(qū)域，銀行主管可以獲得小云服務(wù)器上的用戶當(dāng)前交易記錄”，表示(guard,copy,(currentdata,cloudlet,serverroom),saferoom).

③ (R,Oph,(Hybriden,LocO),LocR)表示主體在某位置對混合實體的訪問策略，其中，LocO與LocR也可不同.如“在大廳區(qū)域，銀行職員可以登入小云服務(wù)器”，表示為(banker,login,(cloudlet,serverroom),mainarea).

因位置約束訪問控制系統(tǒng)與空間拓撲結(jié)構(gòu)緊密聯(lián)系，以下給出系統(tǒng)運行環(huán)境模型定義.

定義7. 系統(tǒng)運行環(huán)境模型.EM模型為8元組EM=(LocR,Role,Object,LocO,Locrelation,RoleObject,RoleLocation,ObjectLocation)：

1)LocR，Role，Object，LocO分別表示邏輯位置角色集合、角色集合、客體集合和客體位置集合；

2)RoleLocation?Role×LocR表示當(dāng)前環(huán)境下角色與位置關(guān)系集合；

3)RoleObject?Role×Object表示當(dāng)前環(huán)境下角色對客體訪問關(guān)系集合；

4)ObjectLocation?Object×LocO表示當(dāng)前環(huán)境下客體與位置關(guān)系集合；

5)Locrelation?LocR×LocR,表示物理空間可達關(guān)系，集合元素(lri,lrj)表示從建筑物入口出發(fā)可以經(jīng)f′(lri)到達f′(lrj).

定義8. 邏輯位置角色等價關(guān)系.如果物理位置f′(lri)可以執(zhí)行的權(quán)限集合P2i與物理位置f′(lrj)可以執(zhí)行的權(quán)限集合P2j相等，則邏輯位置角色lri與lrj等價，表示為lri=lrj.

具有等價關(guān)系的邏輯位置角色lri和lrj可以合并為一個邏輯位置角色lrk,且f′(lrk)=f′(lri)+f′(lrj)，即具有相同訪問權(quán)限的物理位置域賦予相同的邏輯位置角色，且邏輯位置角色對應(yīng)的物理位置空間為相同訪問權(quán)限物理位置域的和.如銀行應(yīng)用場景中office1和office2具有相同的訪問權(quán)限，將這2個物理位置域都賦予邏輯位置角色office，則邏輯位置角色office對應(yīng)的物理位置域為office1區(qū)域與office2區(qū)域的和.具有等價關(guān)系的邏輯位置角色的合并，使每個邏輯位置角色的訪問權(quán)限都不相同.

定義9. 權(quán)限依賴關(guān)系.如果用戶在執(zhí)行權(quán)限pi前一定要執(zhí)行權(quán)限pj，則稱pi依賴于pj，表示為pi≤pj.如果邏輯位置角色lri的訪問權(quán)限集合Pi中操作行為發(fā)生前一定存在邏輯位置角色lrj的訪問權(quán)限集合Pj中操作行為的發(fā)生，則稱Pi依賴于Pj，表示為Pi≤Pj.

定義10. 邏輯位置角色包含關(guān)系.如果邏輯位置角色lri的訪問權(quán)限Pi和邏輯位置角色lrj的訪問權(quán)限Pj之間存在Pi≤Pj依賴關(guān)系，則稱邏輯位置角色lrj包含邏輯位置角色lri，表示為lri?lrj.

3 位置約束訪問控制策略建模與驗證

針對位置約束訪問控制策略的建模，既要實現(xiàn)對EM模型定義的空間拓撲結(jié)構(gòu)的形式化描述，也要實現(xiàn)對LCRBAC模型定義的位置約束的訪問控制策略的形式化描述.偶圖和偶圖反應(yīng)系統(tǒng)是融合了Pi演算和環(huán)境演算的一種形式化建模方法，是同時強調(diào)位置和連接的圖形化模型，并能通過反應(yīng)規(guī)則描述位置或連接關(guān)系的動態(tài)變化.因此，本文采用偶圖和偶圖反應(yīng)系統(tǒng)建模EM和LCRBAC模型.

3.1 偶圖和偶圖反應(yīng)系統(tǒng)

偶圖和偶圖反應(yīng)系統(tǒng)不但具有完備的公理系統(tǒng)，而且提供了圖形化的表示方法，相比進程代數(shù)等其他形式化方法，有利于軟件開發(fā)人員和用戶之間對系統(tǒng)理解的一致性[25].本節(jié)采用非形式化的方式介紹偶圖和偶圖反應(yīng)系統(tǒng)的基本概念.

1) 偶圖(bigraphs)

Fig. 4 Bigraphs F structure diagram圖4 偶圖F結(jié)構(gòu)圖

偶圖用于描述靜態(tài)結(jié)構(gòu)，由位置圖(place graph)和連接圖(link graph)組成.位置圖用于表示各個節(jié)點之間的嵌套關(guān)系；連接圖用于表示節(jié)點之間的連接關(guān)系.位置圖與連接圖是相互獨立的，是從不同視角對同一個偶圖觀測得到的不同結(jié)果.以下結(jié)合圖4對相關(guān)概念加以介紹，圖4(a)為一個偶圖F，圖4(b)(c)分別為F分解得到的位置圖和連接圖.圖4(a)中虛線框表示一個區(qū)域(region)，每個區(qū)域用一個自然數(shù)n標識，V1,V3,V4,V5為節(jié)點標識(node)，節(jié)點之間根據(jù)建模對象位置關(guān)系建立嵌套關(guān)系.偶圖中的每個節(jié)點對應(yīng)控制(control)類型，控制是對相同類型節(jié)點的描述.每個節(jié)點上的黑色圓點表示端口(port)，端口之間通過邊連接(link)，連接分為封閉連接(closed link)，如e1,e2，開放連接(open link)，如x,y.x和y為外部名(outer name)，圖4利用上方伸出的邊表示外部名，從下方伸出的邊表示內(nèi)部名(inner name).F的位置圖FP對應(yīng)以區(qū)域數(shù)為根節(jié)點的森林，連接圖FL對應(yīng)超圖.

位置圖是以序數(shù)集為對象的態(tài)射，F(xiàn)P:m→n表示FP有m個地點、n個區(qū)域.連接圖是以名字集為對象的態(tài)射，F(xiàn)L:X→Y表示FL的內(nèi)部名為X、外部名為Y.偶圖為位置圖和連接圖的合成，是以序數(shù)集和名字集為對象的態(tài)射，即F:m,X→n,Y.m,X稱為內(nèi)部界面(inner face)，n,Y稱為外部界面(outer face).

2) 偶圖反應(yīng)系統(tǒng)(bigraphs reactive system, BRS)

偶圖反應(yīng)系統(tǒng)用于描述動態(tài)結(jié)構(gòu)，通過定義反應(yīng)規(guī)則(T,T′)對自身進行重構(gòu)，反應(yīng)規(guī)則中T稱為反應(yīng)物(redex)，T′稱為生成物(reactum).反應(yīng)物和生成物都是偶圖.反應(yīng)規(guī)則可以根據(jù)具體的應(yīng)用自由地加以定義.如圖5上面為反應(yīng)物T，圖5下面為生成物T′，反應(yīng)規(guī)則表示V3節(jié)點位置的變化和V2節(jié)點的刪除，變遷過程中連接關(guān)系不變.如果偶圖或者偶圖部分與反應(yīng)物匹配，則將該偶圖中與反應(yīng)物匹配的部分替換成生成物.

Fig. 5 Reaction rule圖5 反應(yīng)規(guī)則

偶圖和偶圖反應(yīng)系統(tǒng)的圖形表示具有直觀性的特點，但是不利于系統(tǒng)的理解和處理，因此Milner等人提出了利用代數(shù)系統(tǒng)來描述偶圖和偶圖反應(yīng)系統(tǒng)模型.表2中給出了偶圖和偶圖反應(yīng)系統(tǒng)的部分代數(shù)表示，具體可參看文獻[25].相對于圖形化的表示，代數(shù)系統(tǒng)便于系統(tǒng)的構(gòu)建、演化和推導(dǎo).

根據(jù)表2，可得圖5的項語言描述如下：

x.y.z.V0.(V1xy|V2.(V3yz))‖V4xz.(V5z)→
x.y.z.V0.(V1xy.(V3yz))‖V4xz.(V5z)，

其中，反應(yīng)物和生成物用“→”連接.

Table 2 Term Languages表2 項語言

3.2 位置約束訪問控制系統(tǒng)環(huán)境模型建模

偶圖的位置圖和連接圖能夠從不同的側(cè)面建模位置約束訪問控制系統(tǒng)的運行環(huán)境.通過偶圖的位置圖，能夠清晰地表達建筑分布、人員分布、物理實體、信息實體和混合實體的位置.通過偶圖的連接圖，能夠表達主體對客體的訪問行為.以下先介紹位置約束訪問控制系統(tǒng)偶圖的形式化定義，然后給出EM模型到偶圖的轉(zhuǎn)換規(guī)則.

定義11. 標簽.標簽為一個三元組R=(K,ar,st),其中K為控制節(jié)點集合，ar:K→為控制節(jié)點與其上端口數(shù)的映射,st為控制節(jié)點的狀態(tài)st∈{atomic,active,passive}.其中：原子節(jié)點(atomic)不允許有孩子節(jié)點和施加反應(yīng)規(guī)則；活躍節(jié)點(active)和不活躍節(jié)點(passive)統(tǒng)稱為復(fù)合節(jié)點，復(fù)合節(jié)點可以有孩子節(jié)點，但活躍節(jié)點可以施加反應(yīng)規(guī)則，不活躍節(jié)點不允許施加反應(yīng)規(guī)則.

EM模型中邏輯位置角色和實體對應(yīng)的標簽如表3所示.Role和Hybriden的端口數(shù)為1，表達角色對混合實體的訪問.圖形形狀的不同只是為了標識不同的控制類型，與具體含義無關(guān).

Table 3 System Signatures表3 系統(tǒng)標簽

定義12. 位置約束訪問控制系統(tǒng)偶圖.位置約束訪問控制系統(tǒng)偶圖是由位置圖FP與連接圖FL組成的五元組:

B=(VB,EB,ctrlB,prntB,linkB):m,X→n,Y.

1) 位置圖FP=(VB,ctrlB,prntB):m→n.其中，m為地點數(shù)，n為區(qū)域數(shù)，VB為節(jié)點集合，ctrlB為節(jié)點到控制的映射，ctrlB:VB→K，prntB為節(jié)點間嵌套關(guān)系，prntB:m+ ∪VB| →VB+ ∪n,“| →”指向節(jié)點嵌套箭頭尾部節(jié)點.

2) 連接圖FL=(VB,EB,ctrlB,linkB):X→Y.其中，X為內(nèi)部名，Y為外部名，VB為節(jié)點集合，EB為連接邊集合，ctrlB為節(jié)點到控制的映射，linkB為邊的映射關(guān)系，linkB:X+ ∪PB?EB+ ∪Y，PB為節(jié)點端口集合.

由定義7可知，EM模型表達了系統(tǒng)運行環(huán)境中實體以及實體連接關(guān)系和位置關(guān)系.由定義12可知，位置約束訪問控制系統(tǒng)偶圖是由位置圖和連接圖組成，能夠與EM模型形成概念上的映射.

轉(zhuǎn)換規(guī)則1. EM模型到偶圖的轉(zhuǎn)換規(guī)則.

VB:Role,Object,LocR?VB;

ctrlB:VB→K;*節(jié)點到控制的映射*

prntB:Locrelation(lri,lrj)?lrj| →lri;

RoleLocation(lri,ri)?ri| →lri;

ObjectLocation(loi,oi)?oi| →loi;

linkB:RoleObject(ri,oi)?ri?oi;

PB?Y;*實體的外部名*

EB:linkB中連接邊的集合;

m=k,k∈;*地點數(shù)為k*

n=1;*區(qū)域數(shù)為1*

X=?；*內(nèi)部名為空*

Y為Role和Hybriden節(jié)點端口對應(yīng)的外部名.

其中，?表示轉(zhuǎn)換關(guān)系；K={LocR,Role,Hybriden,Cyberen,Physicalen}.

如應(yīng)用場景中，通過大廳能夠到達走廊，則大廳對應(yīng)的節(jié)點嵌套走廊對應(yīng)的節(jié)點.人員分布、物理實體、信息實體和混合實體嵌套關(guān)系，則對應(yīng)著現(xiàn)實中嵌套關(guān)系.如圖1中所有人員位于大廳，則人員節(jié)點位于大廳節(jié)點內(nèi)、走廊節(jié)點外；小云服務(wù)器位于服務(wù)器房間內(nèi)，則表示為小云服務(wù)器的節(jié)點嵌套在代表服務(wù)器房間的節(jié)點內(nèi).銀行職員在大廳內(nèi)可以連接小云服務(wù)器，則通過邊實現(xiàn)銀行職員與小云服務(wù)器端口的互連.根據(jù)轉(zhuǎn)換規(guī)則1和表3標簽的定義，得到圖1中EM模型的圖形化偶圖如圖6所示:

Fig. 6 Bigraphs of the environment model圖6 運行環(huán)境偶圖

3.3 基于LCRBAC模型的訪問控制策略建模

利用反應(yīng)規(guī)則建?；贚CRBAC模型的位置約束訪問控制策略，即實現(xiàn)策略(R,OPLocR,LocR)和(R,OPobjects,(Objects,LocO),LocR)到反應(yīng)規(guī)則的轉(zhuǎn)換.轉(zhuǎn)換規(guī)則2中考慮了8種操作，具體應(yīng)用中可根據(jù)需求進行擴展.轉(zhuǎn)換規(guī)則2中，針對混合實體和信息實體的操作，編號1為客體位置與主體位置不同，編號2表示客體位置與主體位置相同，編號3為客體位于主體內(nèi).

轉(zhuǎn)換規(guī)則2. 訪問控制策略到反應(yīng)規(guī)則轉(zhuǎn)換.

(R,enter,LocR)?Ra.-0|LocR.-1|-2→

LocR.(Ra.-0|-1)|-2.

(R,exit,LocR)?LocR.(Ra.-0|-1)|-2→

Ra.-0|LocR.-1|-2.

(R,open,Physicalen,LocR)?LocR.(Ra.-0|

(R,close,Physicalen,LocR)?LocR.

(R,login,(Hybriden,LocO),LocR)?

1)LocR.(Ra.-0|-1)|LocO.(Hybridenb.-2|-3)|-4→x.LocR.(Rx.-0|-1)|LocO.(Hybridenx.-2|-3)|-4;

2)LocR.(Ra.-0|Hybridenb.-1|-2)|-3→x.LocR.(Rx.-0|Hybridenx.-1|-2)|-3.

(R,logout,(Hybriden,LocO),LocR)?

(R,copy,(Cyberen,Hybriden,LocO),LocR)?

(R,delete,(Cyberen,Hybriden,LocO),LocR)?

3)LocR.(Ra.(Cyberen|-0)|-1)|-2→LocR.(Ra.-0|-1)|-2.

通過轉(zhuǎn)換規(guī)則2得到的反應(yīng)規(guī)則作用于轉(zhuǎn)換規(guī)則1得到的偶圖模型，從而不斷產(chǎn)生新的狀態(tài)，最終形成以訪問控制策略標注轉(zhuǎn)移邊的標號變遷系統(tǒng)(labeled transition system)[26].

定義13. 標號變遷系統(tǒng).標號變遷系統(tǒng)為六元組(S,I,Act,→,AP,L).其中，S表示所有狀態(tài)的集合；I表示初始狀態(tài)；Act表示轉(zhuǎn)移邊的集合；→?S×Act×S表示變遷關(guān)系；AP表示原子命題的集合；L:S→2AP用于標記每個狀態(tài)滿足的原子命題.

如應(yīng)用場景中位置約束的訪問控制策略“技術(shù)人員進入走廊”是允許的訪問行為，對應(yīng)的反應(yīng)規(guī)則根據(jù)轉(zhuǎn)換規(guī)則2得：

techniciant.-0|corridor.-1|-2→
corridor.(techniciant.-0|-1)|-2,

對應(yīng)的圖形化表示如圖7所示:

Fig. 7 Reaction rule of the operation-enter圖7 進入反應(yīng)規(guī)則

其中，灰色虛線框表示地點(site)，它是一類特殊的節(jié)點，用于抽象無需關(guān)心的信息.

圖7中反應(yīng)物與圖6中的偶圖進行匹配，圖6中technician和corridor之間的關(guān)系與反應(yīng)物中兩者之間的關(guān)系是一致的，就利用生成物代替反應(yīng)物，即圖6中偶圖在圖7反應(yīng)規(guī)則的作用下，變遷為新的狀態(tài)，如圖8所示.如此反復(fù)下去，不斷應(yīng)用反應(yīng)規(guī)則產(chǎn)生新的狀態(tài)，最終可形成訪問控制策略標注轉(zhuǎn)移邊的標號變遷系統(tǒng).

Fig. 8 Reactum model圖8 生成物模型

3.4 位置相關(guān)的安全屬性描述

由于安全需求可以利用偶圖描述，那么驗證一個偶圖A是否滿足某個安全屬性B，等價于檢測偶圖A是否與偶圖B匹配，類似反應(yīng)規(guī)則中反應(yīng)物與偶圖之間的匹配過程.當(dāng)匹配成功，則表示偶圖A滿足安全需求；否則，不滿足安全需求，為違反狀態(tài).對安全屬性的驗證本質(zhì)上就是檢測標號變遷系統(tǒng)中，是否所有狀態(tài)都與安全屬性的偶圖B一致.

在訪問控制策略正確性的驗證方面，本文遵循關(guān)注點分離的思想采用分層的方式.首先驗證單個角色訪問控制策略的正確性，在保證單個角色訪問控制策略正確性的基礎(chǔ)上，建立所有角色訪問控制策略模型，驗證多個角色策略交互行為的正確性，以此減少在所有角色訪問控制策略上的驗證負擔(dān).如案例中首先針對銀行主管、職員、技術(shù)人員和客戶的訪問控制策略分別進行驗證，然后再對4個角色之間交互行為的訪問控制策略進行驗證，具體可參看5.2節(jié)的案例分析.

4 位置約束的訪問控制策略修改方案

根據(jù)模型檢測結(jié)果，依據(jù)訪問控制策略在標號變遷系統(tǒng)中的作用把訪問控制策略分為4類：導(dǎo)致死鎖的訪問控制策略、導(dǎo)致違反狀態(tài)的訪問控制策略、不可達訪問控制策略、正常的訪問控制策略.根據(jù)訪問控制策略分類得到標號變遷系統(tǒng)中4種狀態(tài)：死鎖狀態(tài)、違反狀態(tài)、不可達狀態(tài)、正常狀態(tài).如圖9所示，e為死鎖狀態(tài)，h為違反狀態(tài)，j為不可達狀態(tài).死鎖狀態(tài)、違反狀態(tài)和不可達狀態(tài)統(tǒng)稱為非正常狀態(tài)；其余節(jié)點為正常狀態(tài).

Fig. 9 Example of a labeled transition system圖9 標號變遷系統(tǒng)示例

介紹具體的策略修改方案之前，定義一些約定符號：policies表示所有訪問控制策略集合；pl(st,sk)表示狀態(tài)st與狀態(tài)sk之間的策略邊；deadlockstates表示死鎖狀態(tài)集合；violatestates表示違反狀態(tài)集合；unreachablestates表示不可達狀態(tài)集合；inpolicies(s)表示狀態(tài)s的入度邊訪問控制策略集；outpolicies(s)表示狀態(tài)s的出度邊訪問控制策略集；outedgecount(s)表示狀態(tài)s的出度.

4.1 針對死鎖狀態(tài)策略修改方案

1) 刪除訪問控制策略.刪除導(dǎo)致死鎖狀態(tài)的訪問,控制策略需要從死鎖狀態(tài)反向追蹤，直到遇到出度不為1的狀態(tài)，將該狀態(tài)轉(zhuǎn)移至死鎖狀態(tài)路徑上的策略邊全部刪除，即刪除表4中delete1(si,sj)定義的策略集合.如圖10(a)中，通過刪除策略a2,a3,a4消除死鎖狀態(tài)e.

2) 增加訪問控制策略.位置約束訪問控制策略的制定，不僅要能夠保證所有的訪問控制策略不會造成死鎖，還要保證所有策略不會形成活鎖，即不僅要控制訪問的行為，還要控制退出的行為.需要增加的策略集合為表4中add1(si,sj)定義的策略集，其中，addpolicies(sj,si)表示從si到sj可增加的反向邊集合，selectpolicies(sj,si)表示sj到si的可達路徑，即從addpolicies(sj,si)中選取反向邊能夠連接狀態(tài)sj到si.如圖10(a)中解決死鎖狀態(tài)e，可增加的訪問控制策略集合為：addpolicies(e,b)={d1,d2,d3,d4,d5,d6}add1(e,b)={(d3),(d1,d5),(d2,d6),(d1,d4,d6)}.也可通過增加邊引入新狀態(tài)輔助死鎖狀態(tài)的消除，如圖10(b)中增加1條邊a5引入新狀態(tài)f，從selectpolicies(f,b)集合中選擇1組反向邊實現(xiàn)死鎖狀態(tài)的消除.

Table 4 Location-Constrained Access Control Policies Modifications表4 位置約束訪問控制策略調(diào)整

Fig. 10 Solutions of the deadlock state圖10 死鎖狀態(tài)解決方案

4.2 針對違反狀態(tài)策略修改方案

1) 刪除訪問控制策略.刪除導(dǎo)致違反狀態(tài)的入度邊策略inpolicies和出度邊策略outpolicies，即刪除表4中delete2(sn)定義的策略集合.如圖9中，通過刪除狀態(tài)h的入度邊策略a8和出度邊策略a9與a12解決違反狀態(tài)h.

2) 增加訪問控制策略.需根據(jù)具體問題分析增加策略，見表4中add2(sn)公式，Ak表示需要增加的策略邊集合.如案例中，“要求技術(shù)人員在服務(wù)器房間時，必須有銀行主管陪同”，定義an為(technician,enter,serverroom),若系統(tǒng)中無策略ak為(guard,enter,serverroom)，則sn處于違反狀態(tài)，需要在an前增加策略ak.無形中定義了訪問控制策略間的依賴關(guān)系.

3) 定義策略依賴關(guān)系.通過定義策略間的依賴關(guān)系，消除違反狀態(tài)，見表4中公式priority(sn).如案例中，“要求技術(shù)人員在服務(wù)器房間時，必須有銀行主管陪同”，an-1為(technician,enter,serverroom),ak為(guard,enter,serverroom)，則要求an-1≤ak.

4.3 針對不可達狀態(tài)策略修改提議

1) 刪除訪問控制策略.對于不可達策略，可直接刪除，具體定義為表4中公式delete3(sj).如圖9中，可將策略a11刪除，解決狀態(tài)j的不可達問題.

2) 增加訪問控制策略.通過增加策略，實現(xiàn)策略互聯(lián)，使不可達狀態(tài)變?yōu)榭蛇_狀態(tài)，見表4中公式add3(sj).如案例中可通過增加訪問控制策略(guard,enter,saferoom)消除獨立策略(guard,open,safe,saferoom).

以上3種策略調(diào)整方案為非正常狀態(tài)的消除提供建議，但在某些情況下并非最優(yōu)方案，如要求策略調(diào)整所帶來的成本最小等，因此，實際應(yīng)用中需要根據(jù)具體需求進行方案選取.對于訪問控制策略的修改，在滿足安全需求的前提下，優(yōu)先選擇刪除策略和定義策略依賴關(guān)系，然后選擇增加策略方案.訪問控制策略的增加，需要重新考慮策略間的一致性問題[27-28].以下給出訪問控制策略修改路徑生成算法.

算法1. 策略修改路徑生成算法.

輸入：標號變遷系統(tǒng)lts、反例路徑cp、安全屬性規(guī)約類型spec、訪問控制策略編號集合pi；

輸出：需修改的策略路徑.

Fig.11 Conversion toolkit from the location-constrained access control model to the BigMC language圖11 位置約束訪問控制模型至BigMC語言轉(zhuǎn)換工具

① if(spec==1)*屬性規(guī)約為死鎖類型*

②dlpath=cp.getCounterPath(1);

③i=2;

④ for eachi≤cp.length

⑤ if(lts.outEdgeCount(cp.getCounterPath(i))==1)*反例路徑中狀態(tài)節(jié)點出度為1*

⑥pl=lts.Read(cp.getCounterPath(i),cp.getCounterPath(i-1));

⑦dlpath=dlpath+pl+cp.getCounter-

Path(i);

⑧ end if

⑨i++;

⑩ end for

cp.getCounterPath(i-1));

5 偶圖建模工具介紹和案例分析

5.1 偶圖建模工具

針對偶圖和偶圖反應(yīng)系統(tǒng)已有很多工具支持，如DBtk工具[29]、 BigRed[30]原型編輯器、BigMC[31]工具.其中，BigMC語言描述與偶圖和偶圖反應(yīng)系統(tǒng)的項語言描述比較相近，有利于理解.BigMC可以檢驗偶圖和偶圖反應(yīng)系統(tǒng)模型是否滿足系統(tǒng)安全需求屬性，如果不滿足，給出反例.BigMC可以將衍化過程生成dot腳本，使用XDOT軟件、graphviz軟件進行圖形化的表達.

根據(jù)3.2節(jié)和3.3節(jié)提出的轉(zhuǎn)換規(guī)則，本文設(shè)計并實現(xiàn)了EM模型和LCRBAC模型到BigMC語言轉(zhuǎn)換的原型系統(tǒng).如圖11所示，通過EM模型參數(shù)的輸入，得到初始模型(InitialModel)，通過訪問控制策略的輸入，得到對應(yīng)的反應(yīng)規(guī)則.

5.2 案例分析

5.2.1 EM模型和LCRBAC模型

根據(jù)2.1節(jié)中銀行訪問控制系統(tǒng)需求描述，基于邏輯位置角色，提取訪問控制策略，如表5所示.銀行區(qū)域的EM模型，如表6所示.

5.2.2 位置約束訪問控制策略建模

利用LCRBAC TO BIGMC轉(zhuǎn)換工具，得到銀行主管的訪問控制策略對應(yīng)的反應(yīng)規(guī)則(表7所示)和位置約束訪問控制系統(tǒng)初始模型：

Table 5 Access Control Policies of the Bank表5 銀行系統(tǒng)訪問控制策略

Table 6 Environment Model of the Bank Access Control System

Table 7 Reaction Rules of Guard Access Control Policies表7 銀行主管訪問控制策略對應(yīng)的反應(yīng)規(guī)則

*Edge num indicates the edge number in Fig.12 and Fig.14.

mainarea.(guard[g]|banker[b]|technician[t]|customer[a]|corridor.(office|saferoom.(safe|server[s].historydata)|serverroom.(cloudlet[c].currentdata))).在系統(tǒng)初始模型的基礎(chǔ)上，根據(jù)銀行主管訪問控制策略，生成的標號變遷系統(tǒng)如圖12所示.圖12中的11條遷移邊對應(yīng)表7中定義的編號(1)～(11)的訪問控制策略，圖12中的8個狀態(tài)對應(yīng)表8中編號0～7.類似地，可生成銀行職員和技術(shù)維護人員的訪問控制策略標號變遷系統(tǒng).

Fig. 12 Labeled transition system of guard access control policies圖12 銀行主管訪問控制策略標號變遷系統(tǒng)

Table 8 States Implication of the Guard Labeled Transition System表8 銀行主管標號變遷系統(tǒng)狀態(tài)含義

*Node num indicates the node number in Fig.12 and Fig.14.

Fig. 13 Counter path圖13 反例路徑

5.2.3 性質(zhì)驗證和訪問控制策略調(diào)整

1) 銀行主管的訪問控制策略驗證與調(diào)整

① 死鎖檢測.經(jīng)驗證性質(zhì)滿足，如圖13所示.反例路徑為5(11)2(7)1(1)0，狀態(tài)5為死鎖狀態(tài).根據(jù)訪問控制策略修改算法，得到修改路徑為5(11)2.可通過2種方式修改策略：刪除策略(11)，即禁止銀行主管打開保險柜的權(quán)限；增加編號為(12)的策略(guard,close,safe,saferoom)，實現(xiàn)狀態(tài)5至狀態(tài)2的遷移，即銀行主管打開保險柜后，一定要執(zhí)行關(guān)閉保險柜的動作才能離開安全屋.

② 死鎖檢測.經(jīng)驗證性質(zhì)滿足，反例路徑為7(9)6(10)2(7)1(1)0，狀態(tài)7為死鎖狀態(tài).根據(jù)訪問控制策略修改算法，得修改路徑為7(9)6(10)2.可通過2種方式修改策略：刪除策略(9)(10)，即禁止銀行主管登入安全屋中服務(wù)器和讀取用戶歷史交易信息；增加策略(guard,logout,(server,saferoom),saferoom)和(guard,delete,(historydata,guard-phone,saferoom),saferoom)，編號分別為(13)和(14).

最終,針對銀行主管的訪問控制策略修改為(1)～(14)，生成的標號變遷系統(tǒng)包括9個狀態(tài)，14條變遷.具體如圖14所示：

Fig. 14 Modified labeled transition system of guard access control policies圖14 銀行主管訪問控制策略更改后標號變遷系統(tǒng)

2) 銀行職員訪問控制策略驗證與策略調(diào)整

① 不可達策略檢測.根據(jù)訪問控制策略修改算法，得到訪問控制策略(banker,copy,(currentdata,cloudlet),mainarea)為未執(zhí)行狀態(tài).通過2種方式調(diào)整策略：刪除該策略；增加策略(banker,login,(cloudlet,serverroom),mainarea)，使不可達策略可執(zhí)行.

② 死鎖檢測.經(jīng)驗證性質(zhì)滿足.通過2種方式修改策略：增加策略(banker,logout,(cloudlet,server-room),office)或(banker,logout,(cloudlet,server-room),mainarea)，即銀行職員只有退出登入，才能離開相應(yīng)區(qū)域；刪除策略(banker,login,(cloudlet,serverroom),office)和(banker,copy,(currentdata,cloudlet),mainarea)，即禁止銀行職員在辦公室登入小云服務(wù)器和在大廳獲取客戶當(dāng)天交易記錄.

3) 技術(shù)人員訪問控制策略驗證與策略調(diào)整

① 死鎖檢測，經(jīng)驗證性質(zhì)不滿足.

② 安全需求描述為：要求技術(shù)人員進入服務(wù)器房間時，必須有銀行主管陪同.經(jīng)驗證訪問控制策略違反該安全需求.2種修改方案：刪除策略(techni-cian,enter,serverroom),即禁止技術(shù)人員進入服務(wù)器房間；定義策略依賴關(guān)系，限定(technician,enter,serverroom)之前有策略(guard,enter,serverroom).

4) 全局訪問控制策略正確性驗證

基于單個角色訪問控制策略的調(diào)整，建立全局訪問控制策略變遷圖，最終訪問控制策略為28條，生成的標號遷移系統(tǒng)共有87個狀態(tài).經(jīng)檢測，訪問控制策略不存在死鎖狀態(tài).通過對單個角色訪問控制策略的修改，在較小的狀態(tài)空間中進行檢測，能夠簡化驗證復(fù)雜度.在全局訪問控制策略中只需關(guān)注策略之間交互行為的驗證即可.

6 結(jié)論及下一步工作

物聯(lián)網(wǎng)、信息物理融合系統(tǒng)等新一代信息技術(shù)的出現(xiàn)，為位置約束的訪問控制模型提出了新需求，不僅要關(guān)注信息空間中位置對訪問行為的約束，還要考慮物理空間以及兩空間交互過程中位置對訪問行為的約束.如何在這種新需求下實現(xiàn)位置約束訪問控制模型的建立與驗證成為當(dāng)前信息安全領(lǐng)域的研究熱點之一.本文針對物理空間、信息空間和兩空間的交互，制定不同的訪問控制策略，提出LCRBAC模型，并通過EM模型實現(xiàn)對系統(tǒng)運行環(huán)境的描述.利用偶圖和偶圖反應(yīng)系統(tǒng)對EM和LCRBAC模型進行形式化建模，并對位置約束的安全屬性進行驗證，根據(jù)驗證結(jié)果，提出對非正常狀態(tài)的策略修改方案.最后，結(jié)合案例和原型工具說明了方法的有效性.

下一步工作將從以下3個方面展開：

1) 本文未考慮全局訪問控制策略正確性驗證的狀態(tài)空間約減問題.全局訪問控制模型涉及多個角色，容易導(dǎo)致標號變遷系統(tǒng)過大，引發(fā)狀態(tài)空間爆炸問題.由于單個角色的相關(guān)屬性在前期已經(jīng)得到驗證，如何在全局訪問控制模型中對其進行抽象，是實現(xiàn)狀態(tài)空間約減的關(guān)鍵.

2) 本文未考慮用戶安全需求保持的策略更新方法.策略的每次調(diào)整需要重新對策略集進行驗證，效率較低.如何針對不同類型的用戶安全需求，提出相應(yīng)的策略更新方案或者部分策略的選取與驗證方法，是提高策略更新效率的關(guān)鍵.

3) 本文所提模型和方法只針對一個物理區(qū)域，不適用于跨域環(huán)境下模型的建立與驗證.由于移動終端的普及，如何在開放的網(wǎng)絡(luò)環(huán)境下實現(xiàn)跨域的訪問控制策略的制定與驗證也是我們下一步的研究方向.

CaoYan, born in 1985. PhD candidate. Member of CCF. Her main research interests include service-oriented architecture, formal verification, and security and privacy information system.

HuangZhiqiu, born in 1965. PhD, professor, PhD supervisor. Senior member of CCF. His main research interests include software engineering, formal methods and service-oriented architecture.

KanShuanglong, born in 1988. PhD. Member of CCF. His main research interests include model checking, theoreom proving, and refinement-based software development (61707227@qq.com).

PengHuanfeng, born in 1978. PhD candidate. His main research interests include cloud computing and service computing, privacy protection, and formal verification (penghf@njit.edu.cn).

KeChangbo, born in 1984. PhD. Member of CCF. His main research interests include security and privacy information system, cloud computing, and ontology-based software engineering (brobo.ke@njupt.edu.cn).