實(shí)用模型的自動(dòng)化形式驗(yàn)證＊

徐 亮，劉 宏

（1.湖南師范大學(xué) 數(shù)學(xué)與計(jì)算機(jī)科學(xué)學(xué)院，湖南 長(zhǎng)沙 410081；（2.高性能計(jì)算與隨機(jī)信息處理省部共建教育部重點(diǎn)實(shí)驗(yàn)室，湖南 長(zhǎng)沙 410081）

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

1）防止未授權(quán)用戶的修改；

2）防止授權(quán)用戶的不當(dāng)修改；

3）維護(hù)數(shù)據(jù)的內(nèi)部和外部一致性.

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

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

1 Biba實(shí)用模型

1.1 模型元素

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

定義1 （完整級(jí)之間的支配關(guān)系 ∝）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）稱為安全內(nèi)核系統(tǒng)的狀態(tài)，狀態(tài)全體的集合稱為狀態(tài)空間，記為V.安全內(nèi)核系統(tǒng)Σ被定義為一個(gè)五元組（V，ρ，R，D，v0），其中V稱為安全內(nèi)核系統(tǒng)Σ的狀態(tài)空間；ρ稱為安全內(nèi)核系統(tǒng)Σ的遷移規(guī)則集，它規(guī)定了從一個(gè)狀態(tài)向另一個(gè)狀態(tài)變遷的操作規(guī)程，規(guī)則被定義為函數(shù)：V×R→V×D；v0稱為初始狀態(tài).

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

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

1.2 模型不變量

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

1）簡(jiǎn)單完整性

一個(gè)主體能夠?qū)σ粋€(gè)客體進(jìn)行讀（Observe）操作，僅當(dāng)客體的完整級(jí)別支配主體的完整級(jí)別，即：

2）完整性＊－特性

一個(gè)主體能夠?qū)σ粋€(gè)客體進(jìn)行寫（Modify）操作，僅當(dāng)主體的完整級(jí)別支配客體的完整級(jí)別，即：

3）調(diào)用完整性

一個(gè)主體能夠?qū)σ粋€(gè)客體進(jìn)行執(zhí)行（Execute）操作，僅當(dāng)客體的完整級(jí)別支配主體的完整級(jí)別，即：

4）兼容性

2 模型規(guī)則

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

1）get＿read（s，o）

主體s對(duì)客體o進(jìn)行讀操作，表示為

2）get＿write（s，o）

主體s對(duì)客體o進(jìn)行寫操作，表示為 （g，s，o，）；

3）get＿execute（s，o）

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

4）release＿access（s，o）

主體s釋放對(duì)客體的操作，表示為 （r，s，o，x），其中x代表訪問(wèn)方式；

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

主體s1授予另一主體s2對(duì)客體o的訪問(wèn)屬性x，表示為（g，s1，s2，o，x）；

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

表示主體s1撤銷另一主體s2對(duì)客體o的訪問(wèn)屬性x，表示為 （r，s1，s2，o，x）；

7）create＿object（s，o）

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

8）delete＿object（s，o）

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

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

表示非可信主體s請(qǐng)求改變自己的完整級(jí)為（Lmin，Lmax），表示為 （ch，s，L）；

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

表示非可信主體s請(qǐng)求改變客體o的完整級(jí)為（Lmin，Lmax），表示為 （ch，s，o，（Lmin，Lmax））.

由于文章篇幅的原因，在本文中只給出了其中3個(gè)遷移關(guān)系的詳細(xì)描述和自動(dòng)化驗(yàn)證腳本.

2.1 get＿read（s，o）

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

2.2 create＿object（s，o）

執(zhí)行該操作時(shí)，如果訪問(wèn)類型不恰當(dāng)，則下一狀態(tài)保持原狀，決策輸出UNDEFINED；否則，檢驗(yàn)如下條件：（（L＿min，L＿max）在主體s的標(biāo)簽范圍內(nèi)，且s獲得創(chuàng)建o的授權(quán)）∨ （L＝L＿min＝L＿max在主體s的標(biāo)簽范圍內(nèi)，且存在o＇使得o＇∈H（o＇），且fo（o＇）∝L）∧（（s，o，ˉw）∈b），如果條件成立，決策輸出YES，下一個(gè)狀態(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í)行該操作時(shí)，如果訪問(wèn)類型不恰當(dāng)，則下一狀態(tài)保持原狀，決策輸出UNDEFINED；否則，檢驗(yàn)如下條件：（（?o∈O.（（s，o，ˉw∨ˉe）∈b?fo（o）∝fs（s））∧（（s，o，ˉr）∈b?fs（s）∝fo（o）））∧（Lmax≤fs（s）），如果條件成立，決策輸出 YES，下一個(gè)狀態(tài)變化如下：（f＊ ＝ （f∪ ｛s，（Lmin，Lmax）｝）－ ｛（s，a＿mins（s），v＿maxs（s））｝）∧ 其它分量不變；如果上述條件不成立，決策輸出NO，下一狀態(tài)保持原狀.

3 模型的Isabelle語(yǔ)言描述及其驗(yàn)證

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

3.1 模型的構(gòu)成元素

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

3.1.1 主體和客體

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

3.1.2 請(qǐng)求

請(qǐng)求是主體對(duì)客體要實(shí)施的操作類型.在模型中，主體對(duì)客體的操作被描述為Rules，每個(gè)Rules對(duì)應(yīng)不同的操作類型，請(qǐng)求實(shí)質(zhì)上是根據(jù)操作類型劃分的，請(qǐng)求作為Rules的輸入傳遞給Rules所需要的信息.

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

3.1.3 訪問(wèn)模式

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

3.1.4 Class、Category和SecurityLevel

每個(gè)IntegrityLevel類型的安全標(biāo)簽有Category和Sensitive兩個(gè)元素.Category表示完整性標(biāo)簽所屬的類別集合，Sensitive表完整性標(biāo)簽中的敏感級(jí)別.

dominates表示兩個(gè)完整性級(jí)別間存在支配關(guān)系，equals表示兩個(gè)完整性級(jí)別間存在相等的關(guān)系.

3.1.5 狀態(tài)

AccessTriple表示主體對(duì)客體的訪問(wèn)權(quán)限，即為訪問(wèn)矩陣的一項(xiàng).狀態(tài)States用記錄來(lái)表示，其中Subjects，Objects表示狀態(tài)中所包含的主客體集合；CAT表示狀態(tài)的當(dāng)前訪問(wèn)集合，AM表示狀態(tài)的訪問(wèn)矩陣；f＿s，a＿min，v＿max分別表示主體的最大安全級(jí)，最小可寫的安全級(jí)和最大可讀的安全級(jí)；Hier表示客體的層次結(jié)構(gòu).

3.2 安全狀態(tài)

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

簡(jiǎn)單完整性表示當(dāng)訪問(wèn)方式為讀時(shí)，要求客體的最大安全級(jí)必須控制主體的最大安全級(jí).

3.2.2 ＊－特性

當(dāng)主體對(duì)客體實(shí)施寫操作時(shí)，要求主體、客體的完整級(jí)滿足一定的要求以防止低完整級(jí)的信息向高完整級(jí)傳遞.

3.2.3 調(diào)用完整性

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

3.2.4 兼容性

該屬性提供同一結(jié)構(gòu)樹下不同客體的完整性標(biāo)簽間應(yīng)遵循的支配關(guān)系.

3.2.5 當(dāng)前訪問(wèn)集的控制

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

3.2.6 安全狀態(tài)

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

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

3.3.1 初始化操作

初始化時(shí)主、客體的集合都為空，當(dāng)前訪問(wèn)集合，訪問(wèn)矩陣都為空，客體的層次結(jié)構(gòu)樹為空樹.f＿s，a＿min，v＿max，L＿min，L＿max初 始 化 時(shí) 不 賦予任何值.

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

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

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

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

3.4.1 Get＿read

3.4.2 Create＿object

3.4.3 Change＿subject＿integrity＿level＿range constdefs

4 結(jié) 語(yǔ)

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

[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改進(jìn)模型在安全操作系統(tǒng)中的應(yīng)用[J].計(jì)算機(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] 張明西，韋俊銀，程裕強(qiáng)，等.具有歷史特征的Biba模型嚴(yán)格完整性策略[J].鄭州大學(xué)學(xué)報(bào)：理學(xué)版，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信息安全技術(shù)操作系統(tǒng)安全技術(shù)要求[S].北京：中國(guó)國(guó)家標(biāo)準(zhǔn)化管理委員會(huì)，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／.