徐 亮，劉 宏

（1.湖南師范大學 數學與計算機科學學院，湖南 長沙 410081；（2.高性能計算與隨機信息處理省部共建教育部重點實驗室，湖南 長沙 410081）

安全操作系統(tǒng)的完整性指的是數據或數據源的可信性.“完整性”經常在阻止不恰當及未授權的改變時涉及到.信息源與它的精確性和可信性以及人們對該信息的信任程度有關.完整性的可信性方面對于系統(tǒng)的正常運作至關重要.完整性的目標有3個[1]：

1）防止未授權用戶的修改；

2）防止授權用戶的不當修改；

3）維護數據的內部和外部一致性.

常見的完整性模型有Biba模型[2]、Clark－Wilson模 型[3]、DTE 模 型[4]、Sutherland 模 型[5]以 及Biba改進模型[6－7]等.DTE模型和Sutherland模型只是其中的某些特性可以達到完整性保護的目的，而并不是作為完整性模型提出的；Clark－Wilson模型沒有用形式化的語言來描述；Biba模型是專門為完整性保護提出的，使用了嚴格的形式化語言來描述，可以有效保護系統(tǒng)數據的完整性，但降低了系統(tǒng)的可用性；Biba改進模型對傳統(tǒng)的Biba模型進行了改進并給出了具有形式化語言的描述，符合GB／T20272－2006[8]中對結構化保護級安全策略模型開發(fā)要求，但在該模型中并沒有對模型的正確性給出自動化的形式證明，同時，其主客體完整性的基本操作也相對簡單.

在操作系統(tǒng)的形式化驗證工作中，微軟的SLAM[9]主要是對C語言進行模型檢測；NICTA的L4.Verified[10－11]則只針對seL4微內核進行了從規(guī)范到代碼的驗證分析，都沒有嚴格意義上對某一具體安全策略模型進行驗證.本文針對安全策略模型中的完整性模型，為模型引入了多安全標簽，以及適合實際系統(tǒng)的安全模型操作規(guī)則共十條，并在此基礎上，采用定理證明的方法[12－13]，將組成模型的各元素、操作規(guī)則和不變式用Isabelle[14]定理證明器能接受的完全形式化的語言進行描述，并對其進行正確性的自動化證明，從而滿足GB／T20272－2006中關于最高等級安全操作系統(tǒng)——訪問驗證保護級操作系統(tǒng)研發(fā)中對形式化安全策略模型的要求.

1 Biba實用模型

1.1 模型元素

S＝ ｛s1，s2，…，sn｝表示主體的集合，在操作系統(tǒng)里通常代表進程；S＇?S表示服從完整性性質的主體集合；S－S＇表示非可信主體集合；O＝ ｛o1，o2，…，om｝表示客體集合，如文件、目錄、設備等；C＝ ｛c1，c2，…，cq｝表示等級分類，同時也表示主、客體的完整性級別，其中c1＞c2＞···＞cq；K＝｛k1，k2，…，kr｝表 示 非 等 級 類 別；L＝ ｛（c1，K1），（c2，K2），…，（cq，Kq）｝表示完整性標記，其中 ?1≤i≤q，ci∈C，Ki?K；表示訪問模式，ˉr為讀方式，能看但不能修改客體，ˉw為寫方式，既能看又能修改客體，ˉe為執(zhí)行方式，不能看也不能修改客體；B＝｛b｜b∈（S×O×A）｝表示當前訪問狀態(tài)，指狀態(tài)機模型中，當前狀態(tài)中所包含的主體對客體的所有訪問情況的集合，在系統(tǒng)中則是處在激活狀態(tài)下的進程對被動實體的訪問的全體；R＝｛g，r，ge，de，ch｝ 表 示 請 求；D＝ ｛yes，no，dc，undef｝表示安全策略所做的決策，分別表示請求被認可、拒絕、不關心和不恰當被拒絕；敏感級函數f＝ （fs，a＿mins，v＿maxs，L＿mino，L＿maxo），其中fs為主體的當前安全標簽函數，a＿mins為主體的最小可寫標簽，v＿maxs為主體的最大可讀標簽，L＿mino為客體的最小標簽，L＿maxo為客體的最大標簽，當客體的最大和最小標簽相等時，我們稱客體具有單一安全標簽，用fo表示；P（α）表示α的冪集；H：O→P（O）表示分級結構，從客體集到客體集的冪集的一個函數，如果o1≠o2，那么H（o1）∩H（o2）＝? ，并且，不存在集合 ｛o1，o2，…，om｝，使得or＋1∈H（or），r＝1，2，…，m，且om＋1＝o1；M：O→P（S×A）表示訪問許可函數.

定義1 （完整級之間的支配關系 ∝）L＝｛l1，l2，…，lq｝，其中l(wèi)i＝ （ci，Ki），ci∈C，Ki?K，（li，lj）∈∝≡li∝lj≡ （ci，Ki）∝ （cj，Kj）?ci≤cj∧Ki?Kj.

定義2v＝ （b，f，H，M，S，O）稱為安全內核系統(tǒng)的狀態(tài)，狀態(tài)全體的集合稱為狀態(tài)空間，記為V.安全內核系統(tǒng)Σ被定義為一個五元組（V，ρ，R，D，v0），其中V稱為安全內核系統(tǒng)Σ的狀態(tài)空間；ρ稱為安全內核系統(tǒng)Σ的遷移規(guī)則集，它規(guī)定了從一個狀態(tài)向另一個狀態(tài)變遷的操作規(guī)程，規(guī)則被定義為函數：V×R→V×D；v0稱為初始狀態(tài).

定義3 設Σ＝ （VΣ，ρΣ，RΣ，DΣ，v0），C是VΣ的子集，CT是VΣ×VΣ的子集，我們稱v是關于C的一個安全狀態(tài)，如果v∈C；一個規(guī)則ρj關于C和CT是安全的，如果ρj滿足以下兩個條件：

1）如果v∈C，且ρj（v，Rm）＝ （v＊，Dk），則v＊∈C，表示v的后繼狀態(tài)，而且如果?x∈S∪O，使得f＊（x）≠f（x），那么s∈α（x）∪ ｛x｝；

2）若ρj（v，Rm）＝ （v＊，Dk），則 （v，v＊）∈CT.

我們稱系統(tǒng)Σ是關于C和CT的一個安全系統(tǒng)，如果ρΣ的每一個規(guī)則關于C和CT都是安全的，而且v0是關于C的一個安全狀態(tài).C和CT是由系統(tǒng)的安全策略所決定的，C就是滿足安全策略的狀態(tài)，因此我們也稱C是系統(tǒng)的不變量；稱CT是系統(tǒng)的限制性條件，它們規(guī)定了系統(tǒng)狀態(tài)遷移時必須滿足的限制性條件.

1.2 模型不變量

為了保證系統(tǒng)的完整性，模型制定了嚴格完整特性，也即該模型應該保持的不變量，它包括：

1）簡單完整性

一個主體能夠對一個客體進行讀（Observe）操作，僅當客體的完整級別支配主體的完整級別，即：

2）完整性＊－特性

一個主體能夠對一個客體進行寫（Modify）操作，僅當主體的完整級別支配客體的完整級別，即：

3）調用完整性

一個主體能夠對一個客體進行執(zhí)行（Execute）操作，僅當客體的完整級別支配主體的完整級別，即：

4）兼容性

2 模型規(guī)則

為了滿足實際系統(tǒng)的操作需要，本文給出了模型必須滿足的10條安全遷移規(guī)則如下：

1）get＿read（s，o）

主體s對客體o進行讀操作，表示為

2）get＿write（s，o）

主體s對客體o進行寫操作，表示為 （g，s，o，）；

3）get＿execute（s，o）

主體s對客體o進行執(zhí)行操作，表示為 （g，s，o，）；

4）release＿access（s，o）

主體s釋放對客體的操作，表示為 （r，s，o，x），其中x代表訪問方式；

5）give＿access（s1，s2，o）

主體s1授予另一主體s2對客體o的訪問屬性x，表示為（g，s1，s2，o，x）；

6）rescind＿access（s1，s2，o）

表示主體s1撤銷另一主體s2對客體o的訪問屬性x，表示為 （r，s1，s2，o，x）；

7）create＿object（s，o）

表示主體s請求生成具有標簽范圍為（L＿min，L＿max） 的 客 體o，表 示 為 （ge，s，o，L＿min，L＿max）；

8）delete＿object（s，o）

表示主體s請求刪除具有標簽范圍為（L＿min，L＿max） 的 客 體o，表 示 為 （de，s，o，L＿min，L＿max）；

9）change＿subject＿integrity＿level＿range（s，（Lmin，Lmax））

表示非可信主體s請求改變自己的完整級為（Lmin，Lmax），表示為 （ch，s，L）；

10）change＿object＿integrity＿level＿range（s，o，（Lmin，Lmax））

表示非可信主體s請求改變客體o的完整級為（Lmin，Lmax），表示為 （ch，s，o，（Lmin，Lmax））.

由于文章篇幅的原因，在本文中只給出了其中3個遷移關系的詳細描述和自動化驗證腳本.

2.1 get＿read（s，o）

執(zhí)行該操作時，如果訪問類型不恰當，則下一狀態(tài)保持原狀，決策輸出UNDEFINED；否則，檢驗如下條件：（（s，ˉr）∈M（o））∧fs（s）∝fo（o）∧（s具有對o的ˉr訪問特權），如果條件成立，決策輸出YES，下一個狀態(tài)變化如下：（b＊＝b∪｛s，o，ˉr｝）∧其它分量不變；如果上述條件不成立，決策輸出NO，下一狀態(tài)保持原狀.

2.2 create＿object（s，o）

執(zhí)行該操作時，如果訪問類型不恰當，則下一狀態(tài)保持原狀，決策輸出UNDEFINED；否則，檢驗如下條件：（（L＿min，L＿max）在主體s的標簽范圍內，且s獲得創(chuàng)建o的授權）∨ （L＝L＿min＝L＿max在主體s的標簽范圍內，且存在o＇使得o＇∈H（o＇），且fo（o＇）∝L）∧（（s，o，ˉw）∈b），如果條件成立，決策輸出YES，下一個狀態(tài)變化如下：（f＊＝f∪ ｛（o，L）∨ （o，L＿min，L＿max）｝）∧ （H＊ ＝H∪ ｛（o＇，o）｝）∧ 其它分量不變；如果上述條件不成立，決策輸出NO，下一狀態(tài)保持原狀.

2.3 change＿subject＿integrity＿level＿range （s，（Lmin ，Lmax ））

執(zhí)行該操作時，如果訪問類型不恰當，則下一狀態(tài)保持原狀，決策輸出UNDEFINED；否則，檢驗如下條件：（（?o∈O.（（s，o，ˉw∨ˉe）∈b?fo（o）∝fs（s））∧（（s，o，ˉr）∈b?fs（s）∝fo（o）））∧（Lmax≤fs（s）），如果條件成立，決策輸出 YES，下一個狀態(tài)變化如下：（f＊ ＝ （f∪ ｛s，（Lmin，Lmax）｝）－ ｛（s，a＿mins（s），v＿maxs（s））｝）∧ 其它分量不變；如果上述條件不成立，決策輸出NO，下一狀態(tài)保持原狀.

3 模型的Isabelle語言描述及其驗證

模型的形式化描述和驗證過程，是在基于Linux內核的Ubuntu操作系統(tǒng)下進行的.采用的驗證工具是Isabelle／Isar形式化驗證工具.Isabelle是一個適用于多種邏輯形式的通用系統(tǒng)，具體定位為一個“通用定理證明環(huán)境”，而Isabelle／HOL則是Isabelle實例化Church的經典簡單邏輯類型高階邏輯后形成的交互式定理證明器.

3.1 模型的構成元素

Biba實用模型的構成元素，包括主體、客體、請求和決策.狀態(tài)是一個 （b，f，M，H）四元組，主、客體具有完整性標簽，標簽又是由安全級別和類別構成的.

3.1.1 主體和客體

系統(tǒng)將客體分為主體和其他客體.形式化的主體和客體描述都是抽象的數據類型，有待于系統(tǒng)實現時將其實例化.

3.1.2 請求

請求是主體對客體要實施的操作類型.在模型中，主體對客體的操作被描述為Rules，每個Rules對應不同的操作類型，請求實質上是根據操作類型劃分的，請求作為Rules的輸入傳遞給Rules所需要的信息.

請求的類型分為獲取訪問權限，釋放訪問權限，授予訪問權限，撤銷訪問權限，創(chuàng)建客體，刪除客體，改變安全級.

3.1.3 訪問模式

訪問模式的類型分為只讀、寫和執(zhí)行.

3.1.4 Class、Category和SecurityLevel

每個IntegrityLevel類型的安全標簽有Category和Sensitive兩個元素.Category表示完整性標簽所屬的類別集合，Sensitive表完整性標簽中的敏感級別.

dominates表示兩個完整性級別間存在支配關系，equals表示兩個完整性級別間存在相等的關系.

3.1.5 狀態(tài)

AccessTriple表示主體對客體的訪問權限，即為訪問矩陣的一項.狀態(tài)States用記錄來表示，其中Subjects，Objects表示狀態(tài)中所包含的主客體集合；CAT表示狀態(tài)的當前訪問集合，AM表示狀態(tài)的訪問矩陣；f＿s，a＿min，v＿max分別表示主體的最大安全級，最小可寫的安全級和最大可讀的安全級；Hier表示客體的層次結構.

3.2 安全狀態(tài)

3.2.1 簡單安全狀態(tài)

簡單完整性表示當訪問方式為讀時，要求客體的最大安全級必須控制主體的最大安全級.

3.2.2 ＊－特性

當主體對客體實施寫操作時，要求主體、客體的完整級滿足一定的要求以防止低完整級的信息向高完整級傳遞.

3.2.3 調用完整性

表示主體對客體進行執(zhí)行操作時，主體的完整級要支配客體的完整級.

3.2.4 兼容性

該屬性提供同一結構樹下不同客體的完整性標簽間應遵循的支配關系.

3.2.5 當前訪問集的控制

該屬性要求當前訪問集中的客體一定包含在當前狀態(tài)的客體集合中.

3.2.6 安全狀態(tài)

安全狀態(tài)即為滿足上述5條性質的狀態(tài).

3.3 安全狀態(tài)的初始化

3.3.1 初始化操作

初始化時主、客體的集合都為空，當前訪問集合，訪問矩陣都為空，客體的層次結構樹為空樹.f＿s，a＿min，v＿max，L＿min，L＿max初 始 化 時 不 賦予任何值.

3.3.2 安全狀態(tài)的初始化

要求狀態(tài)初始化滿足安全要求.

3.4 BLP模型的狀態(tài)遷移規(guī)則及其安全證明腳本

系統(tǒng)要始終保持在安全狀態(tài)運行，除了初始狀態(tài)要滿足安全要求以外，系統(tǒng)的所有遷移規(guī)則也必須滿足安全要求，也即由安全狀態(tài)經過任意一條遷移規(guī)則以后到達的狀態(tài)仍然是安全狀態(tài).接下來就是對系統(tǒng)中各條遷移規(guī)則的安全性自動化證明腳本.

3.4.1 Get＿read

3.4.2 Create＿object

3.4.3 Change＿subject＿integrity＿level＿range constdefs

4 結 語

本文以研究設計符合GB／T20272－2006中對最高等級安全操作系統(tǒng)——訪問驗證保護級安全操作系統(tǒng)要求的完全形式化的安全策略模型為目標，提出了一種具有實際可行性的Biba模型，并詳細定義了模型的不變量和安全遷移規(guī)則，使得該模型能夠滿足系統(tǒng)實際操作的需要.于此同時，我們還以定理證明工具Isabelle為依托，對模型的安全狀態(tài)、安全性質、初始化狀態(tài)進行完全形式化的描述，參照文中對3條遷移規(guī)則的具體描述和驗證方法，可以給出全部11條安全遷移規(guī)則的自動化正確性驗證腳本，從而完成了對模型的自動化形式驗證工作.

[1] BISHOP M.Computer security：art and science[M].Boston：Addison Wesley，2003：3－6.

[2] BIBA K J.Integrity considerations for secure computer systems[R].Washington：US Air Force Electronic System Division，1977.

[3] CLARK D D，WILSON D R.A comparison of commercial and military computer security policies[C]／／Proceedings of IEEE Symposium Security and Privacy.Oakland：IEEE，1987：184－195.

[4] BADGER L，STERNE D F，SHERMAN D L，etal.A domain and type enforcement UNIX prototype[C]／／Proceedings of the Fifth USENIX UNIX Security Symposium.Utah：USENIX，1996：127－140.

[5] SUTHERLAND D.A model of information[C]／／Proceedings of the 9th National Computer Security Conference.Gaithersburg：U.S.Government Printing Office，1986：126－132.

[6] 郭榮春，劉文清，徐寧，等.Biba改進模型在安全操作系統(tǒng)中的應用[J].計算機工程，2012，38（13）：96－98.GUO Rong－chun，LIU Wen－qing，XU Ning，etal.Application of improved Biba model in security operating system[J].Computer Engineering，2012，38（13）：96－98.（In Chinese）

[7] 張明西，韋俊銀，程裕強，等.具有歷史特征的Biba模型嚴格完整性策略[J].鄭州大學學報：理學版，2011，43（1）：85－89.ZHANG Ming－xi，WEI Jun－yin，CHENG Yu－qiang，etal.Strict integrity policy of Biba model with historical characteristics[J].J Zhenzhou Univ：Nat Sci Ed，2011，43（1）：85－89.（In Chinese）

[8] GB／T 20272－2006信息安全技術操作系統(tǒng)安全技術要求[S].北京：中國國家標準化管理委員會，2006.GB／T 20272－2006Information Security Technology－Security Techniques Requirement for Operating System[S].Beijing：China National Standardization Management Committee，2006.（In Chinese）

[9] SLAM [EB／OL].（2012－07－14）[2012－08－12].http：／／research.microsoft.com／en－us／projects／slam／.

[10] KEVIN E，GERWIN K，RAFAL K.Formalising a high－performance microkernel[C]／／Proceedings of Workshop on Verified Software：Theories，Tools，and Experiments.Seattle：Springer，2006：1－7.

[11] GERWIN K，MICHAEL N，KEVIN E，etal.Verifying a high－performance micro－kernel[R].Baltimore：7th Annual High－Confidence Software and Systems Conference，2007.

[12] GENESERETH M R，NILSSON N J.Logical foundations of artificial intelligence [M].California：Morgan Kaufmann，1987：87－90.

[13] DAVIS M，LOGEMANN G，LOVELAND D.A machine program for theorem proving[J].Communications of the ACM，1962，5（7）：394－397.

[14] ISABELLE[OL].（2012－07－12）[2012－08－12].http：／／www.cl.cam.ac.uk／research／hvg／isabelle／.