基于模型檢測的工作流訪問控制策略驗(yàn)證

摘 要:訪問控制策略的有效性對工作流管理系統(tǒng)的安全穩(wěn)定運(yùn)行具有重要影響，針對這一問題，提出了一種基于模型檢測的工作流管理系統(tǒng)訪問控制策略驗(yàn)證方法。建立了工作流管理系統(tǒng)的訪問控制策略模型與工作流執(zhí)行主體任務(wù)權(quán)限狀態(tài)模型，并在此基礎(chǔ)上對訪問控制策略的有效性進(jìn)行驗(yàn)證。實(shí)驗(yàn)表明該算法具有有效性和合理性，為訪問控制策略的驗(yàn)證提供了一條新的解決途徑。

關(guān)鍵詞:工作流; 訪問控制策略; 策略驗(yàn)證; 模型檢測

中圖分類號:TP393.08

文獻(xiàn)標(biāo)志碼:A

文章編號:1001-3695(2010)02-0692-05

doi:10.3969/j.issn.1001-3695.2010.02.080

Validation of access control policies of workflow managementsystem based on model checking

CHEN Yan1， TANG Cheng-hua2， WU Dan1

(1.Laboratory for Computer Network Defence Technology， Beijing Institute of Technology， Beijing 100081， China

; 2.School of Computer Control， Guilin University of Electronic Technology， GuilinGuangxi 541004， China)

Abstract:The validity of access control policies seriously affects the safe and stable operation of the workflow management system. To deal with this problem， this paper presented a validation method of access control policies of the workflow management system based on the model checking. On the basis of the establishment of the access control policy model and the task permission state of the subjects of the workflow management system the effectiveness of policies were validated. The experiments show that the algorithm is effective and rational， and provides a new solution to validate the access control polices.

Key words:workflow; access control policies; policy validation; model checking

當(dāng)前，工作流管理系統(tǒng)已廣泛應(yīng)用于金融、銀行、制造等諸多涉及民生的支柱領(lǐng)域中，工作流管理系統(tǒng)的安全問題也因此受到了廣泛關(guān)注。訪問控制系統(tǒng)是工作流管理系統(tǒng)安全保障的重要組成部分。一個安全的工作流管理系統(tǒng)對系統(tǒng)中數(shù)據(jù)的訪問進(jìn)行控制，是其高效率且安全地執(zhí)行任務(wù)的基礎(chǔ)。訪問控制策略漏洞的出現(xiàn)會使工作流管理系統(tǒng)存在隱患，威脅工作流管理系統(tǒng)的穩(wěn)定運(yùn)行。為解決這一問題，本文提出了一種基于模型檢測的工作流管理系統(tǒng)訪問控制策略的驗(yàn)證方法。

1 相關(guān)研究

近年來，訪問控制策略的自動驗(yàn)證技術(shù)受到了廣大研究者的關(guān)注。主要方法可劃分為以下四類:

a)基于測試的訪問控制策略驗(yàn)證技術(shù)。例如Martin在文獻(xiàn)[1]中將軟件工程中的測試方法與訪問控制策略的測試進(jìn)行對比，并結(jié)合訪問控制策略自身的特點(diǎn)形成了基于測試的訪問控制策略的驗(yàn)證方法。該方法的局限在于只能在有限的場景下對訪問控制策略功能的正確性進(jìn)行驗(yàn)證。

b)基于形式化分析的方法。相對于基于測試的驗(yàn)證方法的局限性，形式化方法更具一般性。該方法在訪問控制策略形式化模型基礎(chǔ)上，對其進(jìn)行分析。如Fisler等人[2]借助MTBDD形式化方法表示訪問控制策略，并在此基礎(chǔ)上進(jìn)行安全屬性驗(yàn)證及訪問控制策略動態(tài)變化影響分析，主要的研究成果是工具M(jìn)argrave。該方法的缺陷在于形式化過程中，忽略了規(guī)則間的相互影響因素及規(guī)則中時(shí)序因素所產(chǎn)生的一系列問題，因此對于訪問控制策略的分析能力尚顯一定的局限性，且隨著訪問控制策略復(fù)雜度的增加，MTBDD結(jié)構(gòu)增大而不便于工具的推理。該局限也是形式化分析方法所具有的缺陷。

c)基于符號執(zhí)行的驗(yàn)證方法。該方法介于測試與形式化分析之間，其驗(yàn)證過程多依賴于Petri網(wǎng)。例如Knorr等人[3，4]利用Petri網(wǎng)的異步并發(fā)特性，采用直觀的圖形表示，對訪問控制策略進(jìn)行建模，并通過對其進(jìn)行可達(dá)性分析，對訪問控制策略進(jìn)行驗(yàn)證。文獻(xiàn)[5]對強(qiáng)制訪問控制模型進(jìn)行了形式化的描述和定義，并給出了與其等價(jià)的著色Petri網(wǎng)模型。在Petri網(wǎng)狀態(tài)可達(dá)圖的基礎(chǔ)上，對強(qiáng)制訪問控制模型的有關(guān)安全屬性，如主體訪問客體的時(shí)序關(guān)系，主體訪問的可達(dá)性等進(jìn)行了較為詳細(xì)的分析。該類方法對訪問控制的模擬具有一定的表達(dá)能力，但隨著訪問控制策略復(fù)雜度及規(guī)模的增大，將其轉(zhuǎn)換為Petri網(wǎng)的復(fù)雜性也將劇增，為驗(yàn)證帶來諸多不便。且與以下介紹的模型檢測方法相比，缺乏反例輸出特性，不便于后期對訪問控制策略漏洞的修改。

d)基于模型檢測的方法。該類方法主要是將訪問控制策略所應(yīng)用系統(tǒng)通過FSM進(jìn)行描述，并將系統(tǒng)應(yīng)滿足的屬性使用合適的公式進(jìn)行描述，通過狀態(tài)空間搜索驗(yàn)證在訪問控制策略作用下，系統(tǒng)是否滿足一定的屬性。該類方法的優(yōu)勢在于，具有良好的理論基礎(chǔ)和對并發(fā)及反應(yīng)系統(tǒng)的良好描述能力，且具備自動工具支持，并可對不滿足規(guī)定屬性的狀態(tài)進(jìn)行輸出，便于對訪問控制系統(tǒng)進(jìn)行相應(yīng)改進(jìn)。例如Zhang等人[6]使用該方法對訪問控制權(quán)限進(jìn)行驗(yàn)證，但該方法并未針對工作流訪問控制策略進(jìn)行描述，在FSM建立過程中與工作流任務(wù)聯(lián)系不夠緊密，因此在工作流訪問控制策略驗(yàn)證分析上尚顯不足。Schaad等人[7]則針對基于工作流的企業(yè)資源管理系統(tǒng)(ERP)的訪問控制授權(quán)進(jìn)行驗(yàn)證分析，通過建立工作流與授權(quán)模型，對一系列使用LTL 表示的職責(zé)分離(SoD)屬性進(jìn)行驗(yàn)證。該方法局限在于僅對工作流訪問控制中職責(zé)分離權(quán)限進(jìn)行了時(shí)序上的分析，未將職權(quán)與工作狀態(tài)相聯(lián)系，導(dǎo)致訪問控制策略對工作流任務(wù)的支持度驗(yàn)證分析不足。Schaad等人[8]使用模型檢測工具Alloy對策略更改而造成的職權(quán)分離約束沖突進(jìn)行驗(yàn)證。然而由于Alloy時(shí)序推理差，而造成模型復(fù)雜且推理效率低下。

針對以上工作中的不足，本文旨在針對工作流管理系統(tǒng)自身的特點(diǎn)建立訪問控制策略模型。在此基礎(chǔ)上建立工作流任務(wù)狀態(tài)遷移系統(tǒng)，并將驗(yàn)證屬性與工作流任務(wù)相結(jié)合。驗(yàn)證屬性為工作流執(zhí)行主體在訪問控制策略的支持下完成相應(yīng)任務(wù)的能力，該能力通過訪問控制策略對主體完成相應(yīng)任務(wù)所賦予的權(quán)限體現(xiàn)，因此通過檢測工作流的任務(wù)完成狀態(tài)對支持其的訪問控制策略進(jìn)行驗(yàn)證。驗(yàn)證分為授權(quán)主體驗(yàn)證和惡意主體驗(yàn)證。若授權(quán)主體在訪問控制策略支持下完成相應(yīng)任務(wù)目標(biāo)，則說明訪問控制策略賦予授權(quán)主體足夠的訪問權(quán)限使其完成相應(yīng)工作目標(biāo);若惡意主體在訪問控制策略支持下完成相應(yīng)任務(wù)目標(biāo)，則說明訪問控制策略存在漏洞。本文將提供相應(yīng)的算法，對相應(yīng)的策略進(jìn)行輸出，實(shí)現(xiàn)了對訪問控制策略有效性的驗(yàn)證。

2 工作流管理系統(tǒng)訪問控制策略模型

2.1 工作流管理系統(tǒng)相關(guān)定義

定義1 事件。它是對工作流中原子任務(wù)的驅(qū)動，通過事件控制原子任務(wù)的啟動與終止。可表示為集合E={e1，e2，e3，…，en}。

定義2 任務(wù)。它是工作流的基本組成構(gòu)件。其中原子任務(wù)是工作流的最小單位。任務(wù)可用集合T={t1，t2，t3，…，tn}表示。

定義3 工作流。形式上定義為一個事務(wù)處理活動的自動化過程。

定義4 主體。它是任務(wù)的執(zhí)行者，安全工作流模型通過授予主體執(zhí)行任務(wù)的權(quán)限完成相應(yīng)任務(wù)。主體可使用集合A={a1，a2，a3，…，an}表示。

2.2 工作流管理系統(tǒng)訪問控制策略模型TRW

工作流訪問控制系統(tǒng)可用一個五元組〈A，D，r，w，t〉來表示。其中:A表示完成工作流任務(wù)的主體集;t為工作流任務(wù);D為命題邏輯變量，表示主體在完成工作流任務(wù)t過程中所涉及的客體，該客體可以是數(shù)據(jù)、數(shù)據(jù)間關(guān)系及主體與客體間的授權(quán)關(guān)系;r與w表示在完成工作流任務(wù)t過程中主體對客體的訪問權(quán)限。

根據(jù)以上定義，主體a∈A在完成工作流任務(wù)t過程中是否可以訪問d∈D可分別通過命題邏輯式r(d，{a}，t)和w(d，{a}，t)表示。

3 工作流管理系統(tǒng)訪問控制策略驗(yàn)證算法

驗(yàn)證算法通過檢驗(yàn)訪問控制策略對工作流任務(wù)完成的支持度對訪問控制策略進(jìn)行以下兩種模式的驗(yàn)證:

a)訪問控制策略可用性驗(yàn)證。用于驗(yàn)證訪問控制策略是否可以支持合法用戶完成相應(yīng)任務(wù)，以防止拒絕合法用戶對數(shù)據(jù)和資源訪問的策略的存在。在一個工作流內(nèi)，數(shù)據(jù)和資源的使用必須是在主體的調(diào)度下進(jìn)行，如果某個主體不能執(zhí)行某個任務(wù)，工作流就不能被完整地執(zhí)行，因此訪問控制策略的可用性的驗(yàn)證對工作流管理系統(tǒng)至關(guān)重要。

b)攻擊探測驗(yàn)證。驗(yàn)證在當(dāng)前訪問控制策略存在的條件下，惡意用戶是否可以通過協(xié)作完成相應(yīng)的任務(wù)，用于驗(yàn)證訪問控制策略對于惡意用戶訪問數(shù)據(jù)和資源的控制能力。

驗(yàn)證語言為可機(jī)讀語言，可表示待驗(yàn)證訪問控制策略與屬性。驗(yàn)證模型包含三部分，即訪問控制策略、實(shí)例化數(shù)據(jù)和屬性描述。

model::=〈policy〉[〈initializationStatement〉][〈propertySpecification〉]

策略用于描述待驗(yàn)證的工作流管理系統(tǒng)的訪問控制策略。實(shí)例化數(shù)據(jù)對訪問控制系統(tǒng)進(jìn)行實(shí)例化，描述了待驗(yàn)證的訪問控制系統(tǒng)的規(guī)模。屬性用于描述工作流任務(wù)。

3.1 訪問控制策略描述

以下采用新公司注冊申請審批工作流管理系統(tǒng)為例簡要介紹訪問控制策略描述方法。其工作流程如圖1所示。

某公司要進(jìn)行新公司登記注冊申請，首先到工商局領(lǐng)取表格，然后是技術(shù)監(jiān)督局辦理企業(yè)代碼，稅務(wù)局辦理稅務(wù)登記，其中稅務(wù)登記包括國稅和地稅并聯(lián)審批，最后返回工商局，由工商局將審理結(jié)果通知申請者，相應(yīng)的訪問控制策略描述如下:

AccessControlSystem ApplicationInformationSystem

Class Application Subject

Task T(t1，t2，t3，t4，t5)

Predicate Application (applicant:Subject， application:Application)，

ICAgency(principal:Subject，application:Application)，

TSAgency(principal:Subject，application:Application)，

NTAgency(principal:Subject，application:Application)，

LTAgency(principal:Subject，application:Application)，

Submittedreview(application:Application， principal:Subject)，

Result(application: Application， principal: Subject).

Application(a，b){

read:true;

Task:All;

write:Application(a，b)a=user;

Task:All;

}

ICAgency(a，b){

read:(ICAgency(a，b)a=user)|TSAgency(user，b)|NTAgency(user，b)|LTAgency(user，b)~Application(user，b)|;

Task:All;

write:ICAgency(a，b)a=user;

Task:t1;

}

TSAgency(a，b){

read:ICAgency(user，b)|(TSAgency(a，b)a=user)|NTAgency(user，b)|LTAgency(user，b)~Application(user，b);

Task:All;

write:TSAgency(a，b)a=user|ICAgency(user，b);

Task:t2;

}

NTAgency(a，b){

read:ICAgency(user，b)|TSAgency(user，b)|NTAgency(a，b)a=user |LTAgency(user，b)~Application(user，b);

Task:All;

write:(NTAgency(a，b)a=user)|TSAgency(user，b);

Task:t3;

}

LTAgency(a，b){

read:ICAgency(user，b)|TSAgency(user，b)|NTAgency(user，b)

|LTAency(a，b)a=user~Application(user，b);

Task:All;

write:(LTAgency(a，b)a=user)|TSAgency(user，b);

Task:t4;

}

Subreviewer(a，b，c){

read:~Application(user，b);

Task:All

write:Subreviewer(a，user，c)|Subreviewer(a，b，user);

Task:t2，t3，t4;

}

Submittedreview(a，b){

read:ICAgency(user，b)|TSAgency(user，b)|NTAgency(user，b)

|LTAgency(user，b)~Application(user，b);

Task:t2，t3，t4，t5;

write:user=b;

Task:t2，t3，t4，t5;

}

Result(a，b){

read:ICAgency(user，b)|TSAgency(user，b)|NTAgency(user，b);

|LTAgency(user，b)~Application(user，b);

Task:t2，t3，t4，t5;

write:user=b;

Task:t2，t3，t4，t5;

}

End

訪問控制策略描述以關(guān)鍵字AccessControlSystem開始，后面緊跟訪問控制系統(tǒng)的標(biāo)志名稱。標(biāo)志以字母為首，可包含字母、數(shù)字或下劃線，且大小寫敏感。

訪問控制系統(tǒng)標(biāo)志符下是訪問控制策略描述的主體部分，包含變量定義和訪問控制策略描述。變量定義了工作流任務(wù)完成過程中所涉及的主體與客體、主體與客體間的關(guān)系及工作流所包含的任務(wù)組成。訪問控制策略描述定義了工作流任務(wù)完成過程中主體對客體的訪問權(quán)限。

關(guān)鍵字Class用于定義工作流管理系統(tǒng)中所涉及的主體與客體類。類型標(biāo)志名使用大寫字母為首。

關(guān)鍵字Task用于定義工作流管理系統(tǒng)中的工作流任務(wù)組成，由集合T表示。

主體與客體的關(guān)系使用關(guān)鍵字Predicate定義，各主體與客體間關(guān)系都具有關(guān)系名及相應(yīng)的參數(shù)，且參數(shù)類型必須包含于Class所定義的范圍內(nèi)，參數(shù)名使用小寫字母開頭，如application(applicant:Subject，application: Application)關(guān)系application定義了類型為主體的申請者與類型為Application的申請表之間的歸屬關(guān)系。通過該定義，關(guān)系application建立了集合Subject與集合Application之間各元素的關(guān)系。對任意s∈Subject，a∈Application，application(s，a)都是一個命題變量，代表s是否是a的申請者。

訪問控制策略描述部分由一系列規(guī)則定義組成，每條規(guī)則以參數(shù)化的關(guān)系為首，并包含read和write關(guān)鍵字所定義的邏輯公式以及所對應(yīng)的工作流任務(wù)，表示工作流管理系統(tǒng)工作過程中，主客體關(guān)系的讀寫權(quán)限，即在相應(yīng)工作任務(wù)下，工作流執(zhí)行主體對定義的關(guān)系變量進(jìn)行讀取與書寫的權(quán)限。若規(guī)則中read與write定義缺失，則表明主體對該關(guān)系不具備讀寫?yīng)?quán)限。

3.2 實(shí)例化參數(shù)描述

上一節(jié)給出的訪問控制策略只是策略的模板，在執(zhí)行模型檢測之前，需要對模板進(jìn)行實(shí)例化。該工作使用Initialization-Statement進(jìn)行描述，語法如下:

〈InitializationStatement〉::=\"run for\"〈NumberClassPair〉

(\"，\"〈NumberClassPair〉)

當(dāng)Initialization-Statement執(zhí)行后，檢測工具為每一類賦予固定數(shù)量的元素。這些元素將對訪問控制策略部分中參數(shù)化的主客體關(guān)系進(jìn)行實(shí)例化。實(shí)例化后，具體的模型便建立起來，在此模型之上進(jìn)行模型檢測。如在訪問控制策略描述之后定義:

run for 3 Application，4 Subject

則檢測工具將分別賦予Application與Subject 3與4個元素，因此Application將實(shí)例化為{p1，p2，p3}，Subject將實(shí)例化為{s1，s2，s3，s4}，相應(yīng)的主客體關(guān)系將隨之建立。

3.3 驗(yàn)證屬性描述

實(shí)例化后，將對驗(yàn)證的屬性進(jìn)行描述。驗(yàn)證屬性描述語法如下:

check{Γ‖δ→A:ε}

Γ對δ、ε與A中所涉及的類變量進(jìn)行量化;δ是實(shí)現(xiàn)工作流任務(wù)ε的前提條件，ε定義所要完成的工作流任務(wù)，A定義了一系列合作完成工作流任務(wù)的主體。驗(yàn)證在前提δ下，是否存在訪問控制策略，使A完成工作流任務(wù)ε。

Γ中使用量詞E、A對類變量進(jìn)行定義;δ為命題邏輯變量，用于表示完成工作流任務(wù)ε，主體A所具有的權(quán)限狀態(tài);ε所定義的任務(wù)可以通過主體A對主客體邏輯關(guān)系命題邏輯變量的權(quán)限狀態(tài)表示，可以為簡單任務(wù)或?yàn)榍短兹蝿?wù)。簡單任務(wù)由兩種原子任務(wù)組合而成，分別使用{}和[ ]表示。如設(shè)L(D)由D中命題邏輯變量所構(gòu)成，l1∈L(D)，則{l1}表示通過訪問控制策略可以獲得對l1的寫權(quán)限，[l1]表示通過訪問控制策略可以獲得對l1的讀權(quán)限。

例如3.1節(jié)中，驗(yàn)證屬性如下:

check{E s1，s2:Subject，a:Application‖application(s1，a)→{s1}:{Subreviewer(a，s1，s2)}}

以上定義表示:是否存在訪問策略使s1，s2∈Subject，a∈Application在s1為a的申請者的情況下，可指定某一組織對其申請進(jìn)行審批。

3.4 驗(yàn)證算法

3.4.1 合法策略與滲透策略

對應(yīng)可用性驗(yàn)證和攻擊探測驗(yàn)證兩種檢測模式，策略分為兩類，即合法策略S和滲透策略S′。兩者的主要區(qū)別在于，合法策略是主體A在直接具有訪問權(quán)限的情況下，獲取權(quán)限且完成相應(yīng)的任務(wù)。該策略用于檢測訪問控制策略的可用性，即在現(xiàn)有訪問控制策略支持下，合作的主體A是否能完成工作流任務(wù)。滲透策略是主體A在執(zhí)行某一訪問動作時(shí)不直接具備訪問權(quán)限，但通過合作主體間的信息互通或多步動作，獲取相應(yīng)權(quán)限以完成某一工作流任務(wù)。該策略用于探測惡意主體對工作流管理系統(tǒng)的訪問，防止工作流管理系統(tǒng)所涉及信息的泄露。

3.4.2 遷移系統(tǒng)

本算法是建立在主體集A完成工作流任務(wù)狀態(tài)基礎(chǔ)上的，針對不同的工作流任務(wù)，任務(wù)狀態(tài)的變遷，通過主體集所需具備的訪問權(quán)限體現(xiàn)。因此，使用主體集權(quán)限表示各任務(wù)狀態(tài)，權(quán)限的變化意味著任務(wù)狀態(tài)的遷移。

本算法定義主體集A完成工作流任務(wù)所具備的權(quán)限狀態(tài)為PT，主體集A通過訪問控制策略提升自身所具備的權(quán)限狀態(tài)，直到完成所需完成的任務(wù)。權(quán)限狀態(tài)分為起始狀態(tài)Pinit，即為執(zhí)行訪問控制策略前所具有的權(quán)限狀態(tài)，與當(dāng)前權(quán)限狀態(tài)，即執(zhí)行訪問控制策略后，對應(yīng)各工作流任務(wù)所具備的權(quán)限狀態(tài)Pt。訪問控制策略分為兩類，即讀和寫。通過訪問控制策略可將主體集A的權(quán)限狀態(tài)逐步遷移到PT，這也相應(yīng)表明主體集A在訪問控制策略支持下完成了工作流任務(wù)。

主體集A對于命題邏輯變量D的訪問權(quán)限可使用如下變量表示。對于任意d∈D，t∈T，所對應(yīng)的訪問權(quán)限狀態(tài)描述為

wd:當(dāng)A當(dāng)前具備對d的寫權(quán)限時(shí)，wd為真。

rd:當(dāng)A當(dāng)前具備對d的讀權(quán)限時(shí)，rd為真。

根據(jù)以上定義，A在某一任務(wù)環(huán)節(jié)的權(quán)限狀態(tài)可使用二元組(Wd，Rd)表示，

W={d∈D|wd=T}，R={d∈D|rd=T}

圖2表示在訪問控制策略支持下，對命題邏輯變量d的訪問權(quán)限狀態(tài)遷移系統(tǒng)。每一次遷移都將影響A的權(quán)限狀態(tài)以完成相應(yīng)的任務(wù)，直到A完成所有工作流任務(wù)。為簡化起見，圖2僅描述主體集對單一變量的權(quán)限狀態(tài)遷移過程。

由圖2可知，狀態(tài)遷移中，對命題邏輯變量d的讀寫權(quán)限是不斷變化的，且符合一定的時(shí)序特性，不是單一的權(quán)限提升，這也體現(xiàn)了工作流管理系統(tǒng)中訪問權(quán)限與任務(wù)相對應(yīng)的時(shí)序變化。檢測過程將對所有符合任務(wù)權(quán)限狀態(tài)需求的狀態(tài)進(jìn)行檢測。

3.4.3 驗(yàn)證算法

本文中，檢測主體A從起始權(quán)限狀態(tài)Pinit到目標(biāo)權(quán)限狀態(tài)PT所需使用的策略的算法，采用逆向計(jì)算的方法，即從目標(biāo)權(quán)限狀態(tài)PT開始，逆向追尋達(dá)到此任務(wù)目標(biāo)權(quán)限狀態(tài)的起始權(quán)限狀態(tài)，并輸出相應(yīng)的策略。為便于描述這一過程，作出以下定義:

定義5 集合Pre-sets。對于任意a∈A，d∈D與給定的權(quán)限狀態(tài)Pt。

1)Pre，aw:=T，r:=T(Pt) 表示前權(quán)限狀態(tài)集，從該權(quán)限狀態(tài)集出發(fā)，存在主體a在已知許可對d進(jìn)行讀與寫操作的情況下，權(quán)限狀態(tài)遷移到Pt，即可用以下形式化定義:

{(W，R)|(W′，R′)∈Pt，W′=T，R′=T}

2)Pre，aw:=T，r:=⊥(Pt) 表示前權(quán)限狀態(tài)集，從該狀態(tài)集出發(fā)，存在主體a在已知許可對d進(jìn)行寫操作，但不可讀的情況下，權(quán)限狀態(tài)遷移到Pt，即可用以下形式化定義:

{(W，R)|(W′，R′)∈Pt，W′=T，R′=⊥}

3)Pre，aw:=⊥，r:=T(Pt) 表示前權(quán)限狀態(tài)集，從該狀態(tài)集出發(fā)，主體a在已知許可對d進(jìn)行讀操作，但不可寫的情況下，權(quán)限狀態(tài)遷移到Pt，即可用以下形式化定義:

{(W，R)|(W′，R′)∈Pt，W′=⊥，R′=T}

4)Pre，aw:=⊥，r:=⊥(Pt) 表示前權(quán)限狀態(tài)集，從該狀態(tài)集出發(fā)，主體a在已知不許可對d進(jìn)行讀寫操作的情況下，權(quán)限狀態(tài)遷移到Pt，即可用以下形式化定義:

{(W，R)|(W′，R′)∈Pt，W′=⊥，R′=⊥}

在檢測過程中，始終存儲(Pt，s)，即權(quán)限狀態(tài)Pt與策略。(Pt，s)表示使用策略s可將權(quán)限狀態(tài)Pt躍遷到權(quán)限狀態(tài)PT。當(dāng)Pt=PT，令s=skip，即策略為空。

逆向計(jì)算，即從(PT，skip)開始，算法核心是:給定(Pt，s)，根據(jù)訪問控制策略所定義的權(quán)限，添加((Pre，aw:=T，r:=T(Pt)，(w:=T，r:=T;s))，((Pre，aw:=T，r:=⊥(Pt)，(w:=T，r:=⊥;s))，((Pre，aw:=⊥，r:=T(Pt)，(w:=⊥，r:=T;s))，(Pre，aw:=⊥，r:=⊥(Pt)，(w:=⊥，r:=;s))。當(dāng)不在產(chǎn)生新的組合時(shí)，檢測停止，所有組合中，權(quán)限狀態(tài)集中包含起始權(quán)限狀態(tài)的策略便是檢測所需的。

對于攻擊探測模式中，策略的檢測，在計(jì)算Pre，aw:=T，r:=T(Pt)與Pre，aw:=⊥，r;=T(Pt)時(shí)，只需減除可讀的約束即可。

通過逆向計(jì)算的方法，計(jì)算Pinit到PT的可達(dá)性。在此過程中，將存儲檢測過程中的各權(quán)限狀態(tài)states_seen及到達(dá)各權(quán)限狀態(tài)的策略strategies。令A(yù)表示主體。提取策略的驗(yàn)證算法偽碼描述如下:

輸入:PT—目標(biāo)權(quán)限狀態(tài);Pinit—起始權(quán)限狀態(tài);D—命題變量集;A—執(zhí)行工作流主體;r，w—讀寫權(quán)限定義。

輸出:當(dāng)存在Pinit到PT的通路時(shí)，輸出相對應(yīng)的策略集。

1 strategies:=;

2 states_seen:=;

3 put(PT，skip;)in strategies;

4 repeat until strategies does not change{

5choose(Pt，st)∈ strategies;// for all pairs in strategies

6for each d∈D{

7

for each a ∈ A{

8

DWRPt:=Pre，aw:=T，r:=T(Pt);

9

if((DWRPt≠)∧(DWRPtstates_seen)){

10

states_seen:=states_seen ∪DWRPt;

11

dwrst:=\"set permission towards d to WR by a;\"+st;

12

strategies:=strategies ∪(DWRPt， dwrst);

13

if(Pinit∈DWRPt if (Pinit ∈DWRPt))

14

output dwrst;

15}

16DWPt:=Pre，aw:=T，r:=⊥(Pt);

17if ((DWPt≠)∧(DWPtstates_seen)){

18

states_seen:=states_seen ∪DWPt;

19

dwst:=\"set permission towards d to write True by a;\"+st;

20

strategies:=strategies ∪(DWPt，dwst);

21

if(Pinit∈DWPt)

22

output dwst;

23}

24DRPt=Pre，aw;=⊥，r:=T(Pt);

25if((DRPt≠)∧(DRPtstates_seen)){

26

states_seen:=states_seen ∪DRPt;

27

drst:=\"set permission towards d to read True by a;\"+st;

28

strategies:=strategies∪(DRPt，drst);

29

if(Pinit∈DRPt if (Pinit∈DRPt))

30

output drst;

31}

32DPt:=Pre，aw:=⊥，r:=⊥(Pt);

33if((DPt≠)∧(DPtstates_seen)){

34

states_seen:=states_seen∪DPt;

35

dst:=\"set permission towards d to none by a;\"+st;

36

strategies:=strategies∪(DPt，dst);

37

if(Pinit∈DPt)

38

output dst;

39}

40

}

41}

40 }

4 實(shí)驗(yàn)與分析

本驗(yàn)證算法通過Java進(jìn)行編寫與實(shí)現(xiàn)。算法的性能通過內(nèi)存占用量與時(shí)間消耗衡量。影響本算法的主要因素是:查詢內(nèi)容與d中變量的個數(shù)。

表1中，列舉了對2.1節(jié)中訪問控制策略的驗(yàn)證實(shí)例。采用Linux(kernel 2.6.10)操作系統(tǒng)，CPU采用Pentium M 1.6 GHz，內(nèi)存512 MB。

驗(yàn)證屬性描述如下:

Query1:

check{E s1，s2，s3:Subject，a:Application‖application(s1，a)ICAgency(s2，a)TSAgency(s3，a)→{s1}:{Subreviewer(a，s1，s2)}AND{Subreviewer(a，s2，s3)}}

Query2:

check{E s1，s2:Subject，a:Application‖ICAgency(s1，a)TSAgency(s2，a)→{s1}:{Subreviewer(a，s1，s2)}}

Query3:

check{E s1，s2:Subject，a:Application‖TSAgency(s1，a)(NTAgency(s2，a) →{s1}:{Subreviewer(a，s1，s2)}}

Query4:

check{E s1，s2，s3:Subject，a:Application‖TSAgency(s1，a)(NTAgency(s2，a)

or LTAgency(s3，a))→{s1}:{Subreviewer(a，s1，s2)} or {s1}:{Subreviewer(a，s1，s3)}}

Query5:

check{A s1，s2，s3:Subject，a:Application‖NTAgency(s1，a)LTAgency(s2，a)ICAgency(s3，a)→{s1}:{Subreviewer(a，s1，s3)}and {s2}:{Subreviewer(a，s2，s3)}}

性能如表1所示。

表1 訪問控制策略驗(yàn)證實(shí)驗(yàn)數(shù)據(jù)

queryassignment|D|memory usage/MBtime spent/ms

1application=3，agent=4941473 506

2application=2，agent=329138275

3application=1，agent=329161269

4application=2，agent=332179325

5application=5，agent=71121894 560

由實(shí)驗(yàn)可知，當(dāng)模型及查詢內(nèi)容復(fù)雜度變化時(shí)，內(nèi)存消耗量趨于穩(wěn)定，但時(shí)間消耗量顯著增大。對于針對同一驗(yàn)證內(nèi)容(query4)，對模型進(jìn)行規(guī)模上的調(diào)整。實(shí)驗(yàn)數(shù)據(jù)如表2所示。

表2 Query 4訪問控制策略驗(yàn)證試驗(yàn)數(shù)據(jù)

assignment|D|memory usage/MBtime spent/ms

application=2，subject=325157327

application=3，subject=4491551 399

application=3，subject=6751683 346

application=4，subject=811015529 980

application=6，subject=1017317881 083

實(shí)驗(yàn)數(shù)據(jù)表明，當(dāng)模型增大時(shí)，時(shí)間消耗量相對內(nèi)存消耗量變化較大。因此對模型檢測中，狀態(tài)空間的進(jìn)一步壓縮以縮短查詢所需時(shí)間，是下一步對該方法進(jìn)行改進(jìn)的方向。

5 結(jié)束語

本文在模型檢測的基礎(chǔ)上，建立了一種對工作流管理系統(tǒng)訪問控制策略進(jìn)行可用性及漏洞的驗(yàn)證算法。通過建立工作流管理系統(tǒng)訪問控制策略模型，并在此基礎(chǔ)上建立工作流任務(wù)權(quán)限狀態(tài)遷移系統(tǒng)，對訪問控制策略的可用性與漏洞進(jìn)行了驗(yàn)證。實(shí)驗(yàn)證明了該算法的可用性及有效性。

參考文獻(xiàn):

[1]MARTIN E. Automated test generation for access control policies[C]//Proc of Conference on Object-Oriented Programming Systems， Languages， and Applications. New York: Association for Computing Machinery， 2006:752-753.

[2]FISLER K， KRISHNAMURTHI S， MEYEROVICH L A， et al. Verification and change-impact analysis of access-control policies[C]//Proc of the 27th International Conference on Software Engineering. New York: Association for Computing Machinery， 2005:96-205.

[3]KNORR K. Dynamic access control through Petri net workflows[C]//Proc of the 16th Annual Computer Security Applications Conference. New York: IEEE Computer Society，2000: 159-167.

[4]KNORR K. Multilevel security and information flow in Petri net workflows[C]//Proc of the 9th International Conference on Telecommunication Systems-Modeling and Analysis， Special Session on Security Aspects of Telecommunication Systems.2001:9-20.

[5]JIANG Yi-xin， LIN Chuang， YIN Hao， et al. Security analysis of mandatory access control model[C]//Proc of IEEE International Conference on Systems， Man and Cybernetics. New York: Institute of Electrical and Electronics Engineers Inc， 2004: 5013-5018.

[6]ZHANG N， RYAN M， GUELEV D P. Evaluating access control policies through model checking[C]//Proc of the 8th Information Security Conference. Berlin: Springer-Verlag，2005:446-460.

[7]SCHAAD A， LOTZ V， SOHR K. A model checking approach to analysis organizational controls[C]//Proc of the 11th ACM Symposium on Access Control Models and Technologies. New York: Association for Computing Machinery，2006: 139-149.

[8]SCHAAD A， MOFFETT J. A lightweight approach to specification and analysis of role-based access control extensions[C]//Proc of ACM Symposium on Access Control Models and Technologies. New York: Association for Computing Machinery， 2002: 13-22.