基于Ｐｅｔｒｉ網的混合安全策略建模與驗證

摘要:提出了一種基于有色Petri網的建模方法，在系統的Petri網模型中可以對中國墻策略進行分析和驗證。給出了基于有色Petri網的混合安全策略的形式化定義;并通過一個系統實例闡述了如何利用該方法對系統的混合安全性進行分析和驗證。無論是在系統的設計階段還是實現階段，該方法都能夠有效地提升系統的混合安全性。

關鍵詞:中國墻策略; 有色Petri網; 模型; 安全; 驗證

中圖分類號:TP309文獻標志碼:A

文章編號:1001－3695(2008)02－0509－03

安全性是信息系統的重要方面。幾乎所有的機構都不會將它們的安全目標僅僅局限于單一的保密性或完整性之上，更多的需求是保密性和完整性兼顧的策略。中國墻模型[1]是一種同等考慮保密性與完整性的安全策略模型。該策略模型主要解決商業中的利益沖突問題，其重要性等同于Bell－LaPadula模型[2]在軍事中的意義。Petri網作為一個形式化工具，非常適合用來描述離散的進程，并且能用來有效地分析系統的并發#65380;異步和不確定行為。在近期的研究中，Petri網已經被用來驗證安全需求[3]#65380;工作流的定義[4， 5]以及強制訪問控制的安全分析[6]。

在一個應用了中國墻策略的復雜商業進程中，策略是很難被驗證的。因此本文詳細闡述了如何在中國墻策略下對信息流進行系統地分析和驗證。

1中國墻策略和有色Petri網

1.1中國墻策略

中國墻策略的主要目的是解決商業中的利益沖突問題。因此，該策略通常用于股票交易或者投資公司的經濟活動等環境中。

定義1數據庫的客體是指某家公司相關的信息條目。

定義2公司數據集(CD)包含了與某家公司相關的若干客體。

定義3利益沖突(COI)類包含了若干相互競爭的公司的數據集。

圖1展示了符合上述定義的數據庫中客體的組織結構。假設張三有權訪問美洲銀行的公司數據集(CD)中的客體，那么因為花旗銀行的公司數據集和美洲銀行的公司數據集在同一個COI類中，所以張三不能獲得訪問花旗銀行CD中的客體的權限。因此，這種數據庫結構就能規避利益沖突的威脅。

實際上，公司有些數據是可以公開的。中國墻策略將數據分為無害(sanitized)數據和有害(unsanitized)數據。另外，假設張三“曾經訪問”過美洲銀行CD中的客體，他也應該不能獲得訪問在同一個COI類中的花旗銀行CD中客體的權限;否則，也會引起利益沖突。為了避免這種沖突的發生，以下規則應運而生，其中PR(s)表示s曾經讀取過的客體集合。

規則1CW－簡單安全條件。s能讀取o，當且僅當以下任一條件滿足:

a)存在一個o′，它是s曾經訪問過的客體，并且CD(o′)=CD(o);b)對于所有的客體o′，o′∈PR(s) COI(o′) ≠ COI(o);c)o是無害客體。

最初PR(s) =，并且假定最初的一個讀請求總是被允許的。對于主體寫客體的權限，有如下規則，以避免客體成為信息通道，使得主體能間接獲得信息。

規則2CW－*－屬性。主體s能寫客體o，當且僅當以下兩個條件同時滿足:CW－簡單安全條件允許s讀o;對于所有有害客體o′，s能讀取o′ CD(o′) = CD(o)。

對于中國墻策略的CPN模型，控制庫所的引入代替了訪問控制矩陣的概念。訪問控制矩陣需要集中存儲，而每個控制庫所與一個主體相關聯，可以分布式的部署。因此，在分布式的環境下，控制庫所比訪問控制矩陣更易于實現。

3實例分析

本文展示了如何通過上文中的定義以及覆蓋圖來分析一個系統或進程。是一份投資報告的準備過程。

3.1進程實例

假設張三和李四是同一個投資公司的分析師，并且李四是經理。進程實例是關于該投資公司中一份投資報告的準備過程。圖3顯示了該進程相應的CPN模型。

第一個變遷(主體)t1，張三根據他從infodb2中讀取的信息創建了一份投資報告的草稿p3。然后經理李四(t2)審閱了這份投資報告的草稿并提出了修改意見p4。最后，張三(t3)根據草稿p3和修改意見p4完成了投資報告的最終稿p5。并且，p6是張三的控制庫所，而p7是李四的控制庫所。

Infodb1由李四所提供咨詢的公司資料組成;infodb2由張三所提供咨詢的公司資料組成。圖4顯示了infodb1和infodb2中的內容，以及COI類。每個COI類中只有兩個元素，是為了減少問題的復雜性。李四所使用的infodb1包括匯豐銀行(顏色“b”)和沃爾沃公司(顏色“e”)的資料。張三所使用的infodb2包括花旗銀行(顏色“a”)和福特公司(顏色“s”)的資料。

3. 2形式化分析

現在，中國墻策略將作為這個系統的基本安全策略。

李四為匯豐銀行和沃爾沃公司(分別具有顏色“b”和“e”)提供咨詢，對于他來說沒有利益沖突，因為這兩個公司屬于不同的COI類。同樣，張三也沒有利益沖突(圖4)。形式化的分析如下:

通過形式化分析，可以確定各個托肯的顏色，并且可以發現潛在的利益沖突。

對于這個簡單的實例，各個托肯的顏色是比較容易確定的。但是對于復雜的系統或進程來說，則會非常困難。對于在這些復雜情況下的自動分析，覆蓋圖將會是一個有力的工具。

3.3覆蓋圖

對應于圖3中CPN模型的覆蓋圖顯示在圖5中。各個托肯都進行了顏色標注。

圖5中，這個覆蓋圖由19個節點構成，表示了CPN模型的可能標志。由于篇幅的限制，圖5并不是一個完整的覆蓋圖。節點的條目表示了由數據庫所p3#65380;p4和p5中的對應托肯顏色構成的標志。節點中括號內的條目表示了控制庫所p6和p7的標志。例如，節點11表示，一個顏色為a的托肯在p3中;一個顏色為e的托肯在p4中;一個顏色為a的托肯在p6中;兩個托肯在p7中，顏色分別為a和e。箭頭表示變遷的發生。例如，變遷t2的發生將標志2改變到標志4(也將標志2改變到標志5， …， 11)。由于篇幅限制，并不是所有的箭頭都有標注。有兩種類型的箭頭，即實線的和虛線的。實線箭頭表示“有效的”標志改變，即，變遷的發生不違反第2章中定義的那些公理;相反，虛線箭頭表示對公理的違反，例如:

a)從節點2指向節點4的箭頭違反了公理2，因為李四讀取了顏色為a和b的托肯，而這兩種顏色在同一個COI類中。

b)從節點2指向節點7的箭頭違反了公理6，因為創建一個顏色為b的托肯需要李四的控制庫所中有一個顏色為b的托肯。c)從節點2指向節點10的箭頭既違反了公理2也違反了公理6。

對圖5的分析可以發現，從起始標志(節點1)到可能的結束標志(節點12~19)可以找到一條有效路徑。這條路徑是1—2—5—13。這條路徑要求各托肯的顏色為:p3={a}，p4={a}，p5={a}，p6={a，a，a}，p7={a，e}。當然，還可以找到其他有效路徑。

4結束語

本文提出了一種利用有色Petri網為中國墻策略建模和驗證的方法。通過引入控制庫所的概念，給出了基于有色Petri網的中國墻策略的形式化定義;然后利用一個實例闡述了如何通過基于CPN的形式化定義和覆蓋圖分析來驗證中國墻策略的系統行為。

對于復雜的大型實際系統來說，CPN模型會有非常多的節點，使得無法手工完成分析工作。因此，開發自動分析和驗證安全策略的工具是筆者今后的研究方向。另外，利用Petri網處理無干擾策略和策略復合也是今后的研究內容。

參考文獻:

[1]BREWERD，NASH M. The Chinese wall security policy[C]//Proc of the 1989 IEEE Symposium on Security and Privacy. Oakland，Cali－fornia: IEEE Computer Society Press， 1989:206－214.

[2]BELL D，LAPADULA L. The bell－lapadula model[J].Journal of Computer Security， 1996， 4(2，3):239－263.

[3]AHMED T，TRIPATHI A R. Static verification of security requirements in role based CSCW systems[C]//Proc of ACM Symposium on Access Control Models and Technologies. New York: ACM Press， 2003:196－203.

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

[5]KNORR K. Multilevel security and information flow in Petri net workflows[C]//Proc of the 9th International Conference on Telecommunication Systems， Modeling and Analysis. Dallas， Texas: IEEE Computer Society， 2001:9－20.

[6]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. Hague， Netherlands: IEEE Computer Society， 2004:5013－5018.

[7]PETRI C A. Kommunikation mit automaten[D].Bonn:Institutfür Instrumentelle Mathematik der Universitt Bonn， 1962.

[8]MURATA T. Petri nets: properties， analysis and applications[J].Proceedings of the IEEE， 1989，77(4):541－580.

[9]JENSEN K. An introduction to the theoretical aspects of coloured Petri nets:a decade of concurrency[C]//Lecture Notes in Computer Science.1994:230－272.

“本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文”