一種計算機系統安全模型驗證方法
2023-06-27 01:01:06
專利名稱：一種計算機系統安全模型驗證方法
技術領域：
本發明屬於作業系統安全技術領域，具體涉及一種計算機系統安全模型驗證方法。
背景技術：
隨著計算機技術和通信技術的迅速發展以及用戶需求的不斷增加，計算機作業系統作為各類應用的底層軟體，人們對其依賴程度越來越高。然而，人們在享受計算技術以及隨之伴生的網絡通信技術帶來的強大功能以及便利的同時，也面臨著日益嚴峻的信息安全形勢。在系統設計階段引入安全模型，可以從根源上杜絕因設計缺陷而留給黑客們的可乘之機，因此如何驗證計算機系統所採用的安全模型是否正確就成為目前計算機安全領域的研究熱點。而形式化技術更因為其能對模型的正確性加以證明而得到了重點的關注 (參考發明名稱基於模型轉換的協議正確性驗證和測試方法，專利號ZL 200510002613. X的專利技術文獻，以及發明名稱一種規範驅動的網格工作流描述和驗證方法，專利號 ZL200510027785. 2)。一般來說，對安全模型進行屬性驗證主要分為兩個步驟第一步先將安全模型和待驗證屬性用一種形式化語言抽象成特定輸入模型；第二步則對輸入模型進行分析，驗證屬性與模型之間的一致性。目前出現的安全模型驗證方法(參考發明名稱用於驗證電路的模型檢測中的模型抽象方法及其系統，申請號200910083790. 3的專利技術文獻)可以分為以下幾類第一類採用可視化約束或圖形變換等技術來描述安全模型和待驗證屬性，再利用專門開發的驗證工具進行驗證。這種方法利用人對直觀圖像的敏銳性，以可視化視圖的方式將安全模型的行為呈現出來，然而，該方法對安全模型的描述能力有限，驗證不同的屬性就需要重新建模，工作量很大，此外驗證算法的效率低下也阻礙了該方法的普及。第二類方法利用模型檢測器的輸入語言對安全模型建模，再通過模型檢測器進行驗證。這種方法試圖利用成熟的模型檢測自動化分析工具對安全模型進行分析，然而它的建模方式全憑驗證人員手工完成，這要求對模型檢測技術非常熟悉，否則稍微的疏忽都會導致構造的模型發生狀態爆炸的問題。第三類方法利用開發人員熟悉的UML語言對安全模型進行描述， 這種方法目前只能構造安全模型的靜態結構，無法反映安全模型的動態屬性，而其當前所採用的驗證工具也缺乏對安全模型的時序行為進行判定。考慮到安全模型設計、驗證在計算機軟體工程中的的實際應用背景，安全模型的驗證方法應該選取軟體開發人員所熟悉的模型描述方法，並採用具有一定自動化程度的形式化工具，建立相應的安全模型驗證方法，我們在第三類的方法上更進一步，提出了一種計算機系統安全模型驗證方法。
發明內容
本發明的目的在於提供一種基於UML描述語言與模型檢測技術的計算機系統安全模型驗證方法。針對計算機系統安全模型的靜態結構與動態行為，分別引入UML語言的類圖和狀態機圖對計算機系統安全模型進行描述，之後利用模型轉換工具將UML圖轉換為模型檢測器的輸入模型，由模型檢測器判斷該模型對安全需求、屬性的滿足性。從而實現安全策略模型與基本安全屬性、需求之間的一致性形式化驗證。本發明的技術方案為—種計算機系統安全模型驗證方法，其步驟為DUML建模模塊採用UML描述語言描述計算機系統安全模型的動、靜態屬性，得到計算機系統安全模型的UML模型；2)將待驗證安全屬性用預定的形式化驗證工具所採用的數理邏輯公式進行描述；3) UML模型轉換模塊將該UML模型轉換為該預定形式化驗證工具所能處理的輸入模型；4)該預定形式化驗證工具對該輸入模型進行狀態遍歷，並計算2)中得到的公式在每個狀態上的滿足性，輸出驗證結果。所述UML模型包括訪問發起機構和仲裁機構；所述訪問發起機構採用UML描述語言的一狀態機圖描述所述計算機系統安全模型中主體對客體提出訪問要求；所述仲裁機構採用UML描述語言的一狀態機圖依據所述計算機系統安全模型的安全策略來對所述計算機系統安全模型中主體提出的訪問要求進行仲裁。所述訪問發起機構採用UML描述語言的一狀態機圖描述所述計算機系統安全模型中主體對客體提出訪問要求的方法為所述訪問發起機構首先經初始化確定主體s客體 O的安全級別以及主體對客體的訪問方式a ；然後向將訪問申請(S，O, a)交由所述訪問仲裁機構進行仲裁，若批准，則實施狀態遷移，進入下一個系統狀態，而無論申請成功與否，都會進入第二次申請，如此循環。所述仲裁機構採用UML描述語言的一狀態機圖依據所述計算機系統安全模型的安全策略來對所述計算機系統安全模型中主體提出的訪問要求進行仲裁的方法為所述仲裁機構接到所述訪問發起機構的訪問申請後，依據計算機系統安全模型的訪問控制規則對申請進行仲裁，並將結果返回給該訪問申請機構；所述訪問控制規則由該仲裁機構狀態機圖中的狀態轉換的守衛條件實現。所述狀態機圖中所涉及到的計算機系統安全模型的元素、屬性由各自所對應的類圖描述；所述類圖用於保存對應狀態機圖中各個狀態的屬性並定義可能的行為。所述訪問發起機構的類圖保存了安全模型中所有與主、客體相關的屬性，以及安全模型的各種敏感級，主體讀過的客體的最高讀敏感級reacLlevel、主體寫過的客體的最高寫敏感級write_level，以及讀申請動作和寫申請動作。所述安全模型為DBLP模型；所述DBLP模型中各種敏感級包括最小可寫敏感級 a_mins、最大可讀敏感級、客體最大敏感級標籤L_min。、客體最小敏感級標籤L_max。 和當前訪問客體的敏感級標籤level。。所述訪問仲裁機構的類圖保存了請求批准動作、請求非法動作和仲裁結束動作。所述預定的形式化驗證工具為模型檢測器；所述模型檢測器為基於線性時態邏輯的模型檢測器。所述UML模型轉換模塊利用形式化的語義轉換算法將該UML模型轉換為所述模型檢測器所能處理的輸入模型。本發明結合計算機系統安全模型一般採用自動機模型的特點，將安全模型分為三個部分安全狀態集合、安全狀態遷移集合以及狀態遷移條件。安全狀態集合主要包含了一個安全模型中所有能夠到達的狀態。狀態遷移集合表示模型所允許的系統從一個安全狀態遷移到另一個安全狀態的過程。狀態遷移條件則用來表明發生狀態遷移所必須滿足的約束條件。本發明將這三部分都用UML語言進行描述，既考慮到了計算機系統安全模型的靜態結構、層次等問題，也可以處理計算機系統安全模型的動態特性，如在讀寫操作過程中導致的安全屬性的違反。本發明方法的框架圖如圖1所示。本發明方法包含了三個層次計算機系統安全模型的UML描述、UML模型轉換和基於模型檢測技術的模型驗證。計算機系統安全模型的UML描述需要將計算機系統安全模型中所有的狀態、對狀態遷移的約束用UML語言重新構造；UML模型轉換則負責將UML圖形轉化為模型檢測器所能接受的輸入模型；最後使用模型檢測器探索所有可能的安全狀態遷移序列，以發現是否存在違反安全屬性的狀態存在。本發明的具體步驟如下步驟A 計算機系統安全模型的UML建模描述，通過對計算機系統安全模型中安全狀態等抽象數據的實例化，利用UML的類圖、等靜態視圖對安全模型加以描述；此外，為了描述安全模型的動態特性，引入UML狀態機圖，並構建安全模型進行訪問仲裁的場景以描述計算機系統安全模型動態屬性。步驟B:待驗證安全屬性的形式化描述，根據模型檢測器所採用的描述方式，將待驗證安全屬性描述為時序邏輯公式。步驟C =UML模型轉換，對UML模型的語義和模型檢測器輸入語言的語義進行關聯分析，得到模型轉換的執行算法；步驟D 安全模型屬性分析，利用已得到的待驗證安全屬性的時態邏輯公式和由轉換算法得到的安全模型作為模型檢測器的輸入，對模型的屬性滿足性進行分析。模型檢測器會遍歷計算機系統安全模型所有的狀態以檢查是否存在有違反待驗證屬性的情況。步驟E 結果輸出，利用以上步驟可以對計算機系統安全模型是否滿足待驗證的安全屬性進行驗證。如果輸出結果顯示不滿足，該方法會給出違反屬性的具體執行路徑；如果輸出結果顯示滿足，則該安全模型滿足該安全屬性。本發明的積極效果本發明採用了軟體開發人員所熟知的UML語言進行安全模型的建模，可以使開發人員在系統設計階段及時地對所採用的安全模型進行形式化的驗證，而無需附加的學習成本。此外，由於採用了模型檢測作為驗證手段，和現有方法相比，不僅自動化程度有所提高， 安全模型的驗證能力有了明顯改善，而且可以驗證安全模型在自身結構上的缺陷，同時還可以驗證對於時序屬性的違反情況。
圖1示出了基於UML與模型檢測的安全模型驗證方法的主要框架；圖2示出了主體訪問客體的安全狀態遷移模式圖3示出了訪問發起機構的狀態機圖的建模；圖4示出了仲裁機構的狀態機圖的建模；圖5示出了兩個狀態機圖的類圖建模。
具體實施例方式本發明的輸入是計算機系統安全模型與待驗證的安全屬性。輸入信息分為兩部分，一部分來源於將在開發中實施或已經實施的計算機系統安全模型，它可以來自任何一個需要安全增強的計算機軟體系統及設備，如主機、伺服器、入侵檢測系統、路由器、防火牆等等。對這些設備上的安全機制經過形式化抽象、提取後得到的輸入模型都可作為本發明的輸入信息。另一部分來源於對這些系統、設備的安全需求或應滿足的安全屬性，如機密性、數據完整性等。以上信息要求完整全面，信息越完整，驗證結果越準確。通過對輸入信息的層層處理和分析，最後得到滿足性判定結果，如不滿足則給出違反屬性的執行路徑。下面給出詳細過程。步驟A 計算機系統安全模型的UML建模描述。UML建模模塊對計算機系統安全模型的UML建模，是通過UML視圖的形式全面地描述安全模型的動、靜態屬性。在安全策略模型中，系統的安全狀態通常由主體、客體和訪問方式來表述。典型的計算機系統安全模型，如BLP模型是將系統狀態描述為ν e V，V為系統狀態集合，V = (b，K，f)，其中^(Sxow)表示在某個特定的狀態下，哪些主體以何種訪問方式訪問哪些客體，S是主體集，0為客體集，A = {read, write, append, execute}是訪問操作集合；K表示訪問控制矩陣，通常由訪問控制規則得到；f = (level (s), Ievelc(S), Ievel(O)),表示主客體敏感標記函數，level (χ)表示對象χ的敏感級(安全級別)， levelc(x)表示對象χ的當前敏感級，χ既可能是主體也可能是客體。由於通常情況下安全模型都是高度抽象的，沒有對系統狀態等數據的基數作出限定，而模型檢測中有限狀態機的規模卻是固定的，因此本發明方法中，客戶端採用一個UML狀態機圖來表示模型中主體對客體提出訪問要求，稱為訪問發起機構，而伺服器端用另一個UML狀態機圖依據安全模型的安全策略來對主體提出的訪問要求來進行仲裁，稱為仲裁機構，狀態機圖中所涉及到的安全模型的元素、屬性由各自所對應的類圖描述。這種建模方法使得對安全模型動態特性進行描述成為可能。訪問發起機構和仲裁機構的狀態機圖、以及二者對應的類圖的建模具體步驟如下1)訪問發起機構的狀態機圖建模。訪問發起機構用於再現主體對訪問權限的申請過程先經初始化以獲得自身的安全級別，然後隨即獲取要訪問的客體以及訪問操作，即確定主體s客體ο的安全級別以及主體對客體的訪問方式a ；接著向仲裁機構發出信號，將訪問申請(s，0，a)交由訪問仲裁機構仲裁，若批准，則實施狀態遷移，進入下一個系統狀態，而無論申請成功與否，都會進入第二次申請，兩次申請的客體及申請權限都可能不一樣，如此循環。為了便於描述，我們以BLP 模型的一種改進模型一DBLP模型為待驗證安全模型，待驗證的安全屬性為驗證DBLP模型是否滿足機密性。圖3給出了訪問發起機構狀態機圖的實例，它是對DBLP安全模型中訪問發起過程的模擬。由於DBLP在於保護系統的機密性，所以我們在建模實例中發起了兩次申請先進行讀申請再進行寫申請，視待驗證模型的安全要求不同，對權限的申請順序可以靈活調整和增減。2)仲裁機構的狀態機圖建模仲裁機構用於依據模型的安全策略描述以及訪問控制矩陣K對訪問發起機構提出的申請進行仲裁。仲裁機構在接到訪問發起機構的訪問申請後，依據安全模型訪問控制規則對申請進行仲裁，並將結果返回給訪問申請機構。訪問控制規則由仲裁機構狀態機圖中的狀態轉換的守衛條件實現。圖4給出了 DBLP安全模型的仲裁機構狀態機圖示例，圖中方括號內的邏輯公式是UML狀態機圖的狀態轉換守衛條件，也就是DBLP模型的訪問控制規則。不同的安全模型所對應的守衛條件可能不一樣。3)類圖建模類圖用於保存對應狀態機圖中各個狀態的屬性並定義可能的行為。我們將系統當前的安全狀態ν保存在訪問發起機構的類圖中的屬性欄中。圖5給出了 DBLP安全模型的類圖實例，左側為DBLP模型訪問發起機構的類圖，保存了包括主體最小可寫敏感級a_mins 和最大可讀敏感級；客體最大最小敏感級標籤L_min。和Ljnax。；當前訪問客體的敏感級標籤level。；主體讀/寫過的客體的最高讀/寫敏感級read_level、Write_level。定義的動作有讀申請ReqRead和寫申請ReqWrite。右側為訪問仲裁機構的類圖，僅定義了三個動作請求批准verified、請求非法hvalid和仲裁結束done。步驟B 待驗證安全屬性的形式化描述。待驗證安全屬性的形式化描述，是將待驗證安全屬性用形式化驗證工具所採用的數理邏輯公式描述。本發明方法採用了模型檢測器作為形式化驗證安全模型的工具，模型檢測技術是基於時態邏輯的，時態邏輯分為兩種線性時態邏輯(LTL)和計算樹時態邏輯。 由於我們使用的模型檢測器SPIN基於線性時態邏輯，所以我們採用了 LTL公式從信息流的角度來描述待驗證安全屬性。我們以機密性為例。機密性的目標是為了防止非可信主體將高機密級別的信息洩露給低機密級別的主體。雖然機密性要求任何由高等級向低等級的信息流都不能出現，這其中也包括了隱通道在內，但是，一般來說，安全策略模型旨在控制各類顯式非法信息在非可信主體與客體間傳遞，隱通道並不在其考慮範圍內。因此，我們可以用線性時態邏輯描述機密性要求如下定義readlike =OXS- {True，False}，判斷主體s是否以只讀操作訪問客體o，如果是則返回True，否則為False ；writelike =OXS- {True, False}，判斷主體s是否以只寫操作訪問客體o，如果是則返回True，否則為False ；記s為非可信主體，O(S)表示主體s所訪問過的客體集合，levelc(o)表示客體ο 當前安全敏感標記。那麼，機密性要求表示如下
^do1，O2 e O(j) · {readlike(ox) -> Qwritelikeip2 ))八 Ievelc (o2 ) ^ Ievelc (O1)步驟C:UML模型轉換。為了使用現有模型檢測工具對安全模型進行屬性驗證，UML模型轉換模塊需要將UML視圖(包括狀態機圖和相應的類圖)翻譯為模型檢測器所能接受的輸入模型。由於我們採用了模型檢測器SPIN對我們構建的安全策略模型的UML模型進行安全屬性的驗證。我們需要將UML圖翻譯為SPIN的輸入語言PROMELA。UML的模型轉換原理，是利用形式化的語義轉換算法，採用PROMELA的進程原語表示UML狀態機圖，類圖則通過PROMELA 語言中的自定義數據結構實現。(參見文獻Alexander Knapp and Stephan Merz. Model Checkingand Code Generation for UML State Machines and Collaborations[R]. In Dominik Haneberg, Gerhard Schellhorn, and Wolfgang Reif, editors, Proc.5th ffsh. Tools for System Design andVerifixation, pages 59-64. Technical Report 2002-11, Institut fiir Informatik, Universitat Augsburg, 2002.)步驟D :安全模型屬性分析。安全模型屬性分析，即利用模型檢測工具對已經由UML模型轉化而來的安全模型進行狀態遍歷，並計算在每個狀態上步驟B中得到的LTL公式的滿足性。如果在遍歷過程中LTL公式恆為真，則模型滿足屬性；若存在使得公式為假的狀態，則模型不滿足屬性。步驟E 結果輸出。利用以上步驟可以得到安全模型對待驗證安全屬性的滿足情況，結果輸出或者給出「滿足」信息，或者給出安全模型中存在的違反該屬性的狀態遷移路徑。該遷移路徑即是模型漏洞的理論再現，可以利用對採用該安全模型的實際系統進行漏洞測試及滲透性測
試ο儘管為說明目的公開了本發明的具體實施例和附圖，其目的在於幫助理解本發明的內容並據以實施，但是本領域的技術人員可以理解在不脫離本發明及所附的權利要求的精神和範圍內，各種替換、變化和修改都是可能的。因此，本發明不應局限於最佳實施例和附圖所公開的內容，本發明要求保護的範圍以權利要求書界定的範圍為準。
權利要求
1.一種計算機系統安全模型驗證方法，其步驟為DUML建模模塊採用UML描述語言描述計算機系統安全模型的動、靜態屬性，得到計算機系統安全模型的UML模型；2)將待驗證安全屬性用預定的形式化驗證工具所採用的數理邏輯公式進行描述；3)UML模型轉換模塊將該UML模型轉換為該預定形式化驗證工具所能處理的輸入模型；4)該預定形式化驗證工具對該輸入模型進行狀態遍歷，並計算幻中得到的公式在每個狀態上的滿足性，輸出驗證結果。
2.如權利要求1所述的方法，其特徵在於所述UML模型包括訪問發起機構和仲裁機構； 所述訪問發起機構採用UML描述語言的一狀態機圖描述所述計算機系統安全模型中主體對客體提出訪問要求；所述仲裁機構採用UML描述語言的一狀態機圖依據所述計算機系統安全模型的安全策略來對所述計算機系統安全模型中主體提出的訪問要求進行仲裁。
3.如權利要求2所述的方法，其特徵在於所述訪問發起機構採用UML描述語言的一狀態機圖描述所述計算機系統安全模型中主體對客體提出訪問要求的方法為所述訪問發起機構首先經初始化確定主體s客體ο的安全級別以及主體對客體的訪問方式a ；然後向將訪問申請(s，0，a)交由所述訪問仲裁機構進行仲裁，若批准，則實施狀態遷移，進入下一個系統狀態，而無論申請成功與否，都會進入第二次申請，如此循環。
4.如權利要求2所述的方法，其特徵在於所述仲裁機構採用UML描述語言的一狀態機圖依據所述計算機系統安全模型的安全策略來對所述計算機系統安全模型中主體提出的訪問要求進行仲裁的方法為所述仲裁機構接到所述訪問發起機構的訪問申請後，依據計算機系統安全模型的訪問控制規則對申請進行仲裁，並將結果返回給該訪問申請機構；所述訪問控制規則由該仲裁機構狀態機圖中的狀態轉換的守衛條件實現。
5.如權利要求2所述的方法，其特徵在於所述狀態機圖中所涉及到的計算機系統安全模型的元素、屬性由各自所對應的類圖描述；所述類圖用於保存對應狀態機圖中各個狀態的屬性並定義可能的行為。
6.如權利要求5所述的方法，其特徵在於所述訪問發起機構的類圖保存了安全模型中所有與主、客體相關的屬性，以及安全模型的各種敏感級，主體讀過的客體的最高讀敏感級 reacLlevel、主體寫過的客體的最高寫敏感級write_level，以及讀申請動作和寫申請動作。
7.如權利要求6所述的方法，其特徵在於所述安全模型為DBLP模型；所述DBLP模型中各種敏感級包括最小可寫敏感級a_mins、最大可讀敏感級、客體最大敏感級標籤 L_min。、客體最小敏感級標籤L_maX。和當前訪問客體的敏感級標籤level。。
8.如權利要求5所述的方法，其特徵在於所述訪問仲裁機構的類圖保存了請求批准動作、請求非法動作和仲裁結束動作。
9.如權利要求1所述的方法，其特徵在於所述預定的形式化驗證工具為模型檢測器； 所述模型檢測器為基於線性時態邏輯的模型檢測器。
10.如權利要求9所述的方法，其特徵在於所述UML模型轉換模塊利用形式化的語義轉換算法將該UML模型轉換為所述模型檢測器所能處理的輸入模型。
全文摘要
本發明公開了一種計算機系統安全模型驗證方法，屬於作業系統安全技術領域，本發明的方法為1)ML建模模塊採用UML描述語言描述計算機系統安全模型的動、靜態屬性，得到計算機系統安全模型的UML模型；2)將待驗證安全屬性用預定的形式化驗證工具所採用的數理邏輯公式進行描述；3)UML模型轉換模塊將該UML模型轉換為該預定形式化驗證工具所能處理的輸入模型；4)該預定形式化驗證工具對該輸入模型進行狀態遍歷，並計算2)中得到的公式在每個狀態上的滿足性，輸出驗證結果。本發明提高了驗證的自動化程度和驗證能力，同時可以驗證安全模型在自身結構上的缺陷以及對於時序屬性的違反情況。
文檔編號G06F21/00GK102194061SQ201010116868
公開日2011年9月21日 申請日期2010年3月2日 優先權日2010年3月2日
發明者馮登國, 張陽, 程亮 申請人:中國科學院軟體研究所