位置約束的訪問控制模型及驗證方法

2018-08-06 03:40:56黃志球闞雙龍彭煥峰柯昌博

計算機研究與發展 2018年8期

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

1(南京航空航天大學計算機科學與技術學院南京 211106)2(高安全系統的軟件開發與驗證技術工業和信息化部重點實驗室(南京航空航天大學) 南京 211106)3(軟件新技術與產業化協同創新中心南京 210093)4 (南京郵電大學計算機學院南京 210023) (caoyan926@nuaa.edu.cn)

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

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

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

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

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

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

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

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

1 相關工作分析

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

Table 1 Comparison of Related Works表1 相關工作比較

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

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

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

信息物理融合系統和物聯網都是由傳感器節點、執行器節點、計算系統和網絡系統組成.傳感器節點實現對物理世界的感知，將感知信息通過網絡系統傳遞給計算系統，計算系統按照預先設定原則處理信息，并將處理結果通過網絡系統發送給執行器節點，最后由執行器節點接收消息，實現對物理世界的控制.依據以上系統的組成構件，2.1節引入位置約束訪問控制系統應用場景[21,24]，并對系統中基本概念進行分析；2.2節根據概念分析結果提出LCRBAC模型和EM模型.

2.1 應用場景

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

Fig. 1 Bank deployment diagram圖1 銀行部署結構圖

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

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

信息空間和物理空間的交互既可以是通過物理空間中的信息控制信息空間的訪問行為，如“只有在安全屋，銀行主管才能讀取用戶歷史交易信息”，也可以通過信息空間中的行為約束物理空間訪問，如“銀行主管只有刪除客戶歷史交易記錄才能離開安全屋”.物理實體、信息實體和混合實體統稱為客體.客體和人員統稱為實體.銀行區域內通過網關實現實體間互聯.文中不關注網絡系統，假設網絡系統是高可靠的.

2.2 LCRBAC模型與EM模型

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

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

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

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

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

在實際的物理空間中，許多不同物理位置域具有相同的訪問權限，提出邏輯位置角色的概念實現對相同訪問權限的物理位置域的統一.

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

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

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

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

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

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

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

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

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

3)P?OP×O表示權限集合.

4)PA?P×R表示權限和角色之間多對多關系.

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

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

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

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

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

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

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

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

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

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

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

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

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

①ObjLoco(o:Physicalen)→LocR；

②ObjLoco(o:Hybriden)→2LocR；

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

10)PA?P×R表示權限和角色之間多對多關系.

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

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

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

根據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相等.如“在安全區域，銀行主管可以打開安全屋中保險柜”，表示為(guard,open,safe,saferoom).

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

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

因位置約束訪問控制系統與空間拓撲結構緊密聯系，以下給出系統運行環境模型定義.

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

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

2)RoleLocation?Role×LocR表示當前環境下角色與位置關系集合；

3)RoleObject?Role×Object表示當前環境下角色對客體訪問關系集合；

4)ObjectLocation?Object×LocO表示當前環境下客體與位置關系集合；

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

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

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

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

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

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

針對位置約束訪問控制策略的建模，既要實現對EM模型定義的空間拓撲結構的形式化描述，也要實現對LCRBAC模型定義的位置約束的訪問控制策略的形式化描述.偶圖和偶圖反應系統是融合了Pi演算和環境演算的一種形式化建模方法，是同時強調位置和連接的圖形化模型，并能通過反應規則描述位置或連接關系的動態變化.因此，本文采用偶圖和偶圖反應系統建模EM和LCRBAC模型.

3.1 偶圖和偶圖反應系統

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

1) 偶圖(bigraphs)

Fig. 4 Bigraphs F structure diagram圖4 偶圖F結構圖

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

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

2) 偶圖反應系統(bigraphs reactive system, BRS)

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

Fig. 5 Reaction rule圖5 反應規則

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

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

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

其中，反應物和生成物用“→”連接.

Table 2 Term Languages表2 項語言

3.2 位置約束訪問控制系統環境模型建模

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

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

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

Table 3 System Signatures表3 系統標簽

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

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

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

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

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

轉換規則1. EM模型到偶圖的轉換規則.

VB:Role,Object,LocR?VB;

ctrlB:VB→K;*節點到控制的映射*

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∈;*地點數為k*

n=1;*區域數為1*

X=?；*內部名為空*

Y為Role和Hybriden節點端口對應的外部名.

其中，?表示轉換關系；K={LocR,Role,Hybriden,Cyberen,Physicalen}.

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

Fig. 6 Bigraphs of the environment model圖6 運行環境偶圖

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

利用反應規則建模基于LCRBAC模型的位置約束訪問控制策略，即實現策略(R,OPLocR,LocR)和(R,OPobjects,(Objects,LocO),LocR)到反應規則的轉換.轉換規則2中考慮了8種操作，具體應用中可根據需求進行擴展.轉換規則2中，針對混合實體和信息實體的操作，編號1為客體位置與主體位置不同，編號2表示客體位置與主體位置相同，編號3為客體位于主體內.

轉換規則2. 訪問控制策略到反應規則轉換.

(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.

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

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

如應用場景中位置約束的訪問控制策略“技術人員進入走廊”是允許的訪問行為，對應的反應規則根據轉換規則2得：

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

對應的圖形化表示如圖7所示:

Fig. 7 Reaction rule of the operation-enter圖7 進入反應規則

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

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

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

3.4 位置相關的安全屬性描述

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

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

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

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

Fig. 9 Example of a labeled transition system圖9 標號變遷系統示例

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

4.1 針對死鎖狀態策略修改方案

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

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

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

Fig. 10 Solutions of the deadlock state圖10 死鎖狀態解決方案

4.2 針對違反狀態策略修改方案

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

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

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

4.3 針對不可達狀態策略修改提議

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

2) 增加訪問控制策略.通過增加策略，實現策略互聯，使不可達狀態變為可達狀態，見表4中公式add3(sj).如案例中可通過增加訪問控制策略(guard,enter,saferoom)消除獨立策略(guard,open,safe,saferoom).

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

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

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

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

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

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

②dlpath=cp.getCounterPath(1);

③i=2;

④ for eachi≤cp.length

⑤ if(lts.outEdgeCount(cp.getCounterPath(i))==1)*反例路徑中狀態節點出度為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 偶圖建模工具

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

根據3.2節和3.3節提出的轉換規則，本文設計并實現了EM模型和LCRBAC模型到BigMC語言轉換的原型系統.如圖11所示，通過EM模型參數的輸入，得到初始模型(InitialModel)，通過訪問控制策略的輸入，得到對應的反應規則.

5.2 案例分析

5.2.1 EM模型和LCRBAC模型

根據2.1節中銀行訪問控制系統需求描述，基于邏輯位置角色，提取訪問控制策略，如表5所示.銀行區域的EM模型，如表6所示.

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

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

Table 5 Access Control Policies of the Bank表5 銀行系統訪問控制策略

Table 6 Environment Model of the Bank Access Control System

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

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

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

Table 8 States Implication of the Guard Labeled Transition System表8 銀行主管標號變遷系統狀態含義

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

Fig. 13 Counter path圖13 反例路徑

5.2.3 性質驗證和訪問控制策略調整

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

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

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

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

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

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

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

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

3) 技術人員訪問控制策略驗證與策略調整

① 死鎖檢測，經驗證性質不滿足.

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

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

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

6 結論及下一步工作

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

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

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

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

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

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).