实用模型的自动化形式验证＊

徐 亮，刘 宏

（1.湖南师范大学 数学与计算机科学学院，湖南 长沙 410081；（2.高性能计算与随机信息处理省部共建教育部重点实验室，湖南 长沙 410081）

安全操作系统的完整性指的是数据或数据源的可信性.“完整性”经常在阻止不恰当及未授权的改变时涉及到.信息源与它的精确性和可信性以及人们对该信息的信任程度有关.完整性的可信性方面对于系统的正常运作至关重要.完整性的目标有3个[1]：

1）防止未授权用户的修改；

2）防止授权用户的不当修改；

3）维护数据的内部和外部一致性.

常见的完整性模型有Biba模型[2]、Clark－Wilson模 型[3]、DTE 模 型[4]、Sutherland 模 型[5]以 及Biba改进模型[6－7]等.DTE模型和Sutherland模型只是其中的某些特性可以达到完整性保护的目的，而并不是作为完整性模型提出的；Clark－Wilson模型没有用形式化的语言来描述；Biba模型是专门为完整性保护提出的，使用了严格的形式化语言来描述，可以有效保护系统数据的完整性，但降低了系统的可用性；Biba改进模型对传统的Biba模型进行了改进并给出了具有形式化语言的描述，符合GB／T20272－2006[8]中对结构化保护级安全策略模型开发要求，但在该模型中并没有对模型的正确性给出自动化的形式证明，同时，其主客体完整性的基本操作也相对简单.

在操作系统的形式化验证工作中，微软的SLAM[9]主要是对C语言进行模型检测；NICTA的L4.Verified[10－11]则只针对seL4微内核进行了从规范到代码的验证分析，都没有严格意义上对某一具体安全策略模型进行验证.本文针对安全策略模型中的完整性模型，为模型引入了多安全标签，以及适合实际系统的安全模型操作规则共十条，并在此基础上，采用定理证明的方法[12－13]，将组成模型的各元素、操作规则和不变式用Isabelle[14]定理证明器能接受的完全形式化的语言进行描述，并对其进行正确性的自动化证明，从而满足GB／T20272－2006中关于最高等级安全操作系统——访问验证保护级操作系统研发中对形式化安全策略模型的要求.

1 Biba实用模型

1.1 模型元素

S＝ ｛s1，s2，…，sn｝表示主体的集合，在操作系统里通常代表进程；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为执行方式，不能看也不能修改客体；B＝｛b｜b∈（S×O×A）｝表示当前访问状态，指状态机模型中，当前状态中所包含的主体对客体的所有访问情况的集合，在系统中则是处在激活状态下的进程对被动实体的访问的全体；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｝，其中li＝ （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）称为安全内核系统的状态，状态全体的集合称为状态空间，记为V.安全内核系统Σ被定义为一个五元组（V，ρ，R，D，v0），其中V称为安全内核系统Σ的状态空间；ρ称为安全内核系统Σ的迁移规则集，它规定了从一个状态向另一个状态变迁的操作规程，规则被定义为函数：V×R→V×D；v0称为初始状态.

定义3 设Σ＝ （VΣ，ρΣ，RΣ，DΣ，v0），C是VΣ的子集，CT是VΣ×VΣ的子集，我们称v是关于C的一个安全状态，如果v∈C；一个规则ρj关于C和CT是安全的，如果ρj满足以下两个条件：

1）如果v∈C，且ρj（v，Rm）＝ （v＊，Dk），则v＊∈C，表示v的后继状态，而且如果∃x∈S∪O，使得f＊（x）≠f（x），那么s∈α（x）∪ ｛x｝；

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

我们称系统Σ是关于C和CT的一个安全系统，如果ρΣ的每一个规则关于C和CT都是安全的，而且v0是关于C的一个安全状态.C和CT是由系统的安全策略所决定的，C就是满足安全策略的状态，因此我们也称C是系统的不变量；称CT是系统的限制性条件，它们规定了系统状态迁移时必须满足的限制性条件.

1.2 模型不变量

为了保证系统的完整性，模型制定了严格完整特性，也即该模型应该保持的不变量，它包括：

1）简单完整性

一个主体能够对一个客体进行读（Observe）操作，仅当客体的完整级别支配主体的完整级别，即：

2）完整性＊－特性

一个主体能够对一个客体进行写（Modify）操作，仅当主体的完整级别支配客体的完整级别，即：

3）调用完整性

一个主体能够对一个客体进行执行（Execute）操作，仅当客体的完整级别支配主体的完整级别，即：

4）兼容性

2 模型规则

为了满足实际系统的操作需要，本文给出了模型必须满足的10条安全迁移规则如下：

1）get＿read（s，o）

主体s对客体o进行读操作，表示为

2）get＿write（s，o）

主体s对客体o进行写操作，表示为 （g，s，o，）；

3）get＿execute（s，o）

主体s对客体o进行执行操作，表示为 （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）

执行该操作时，如果访问类型不恰当，则下一状态保持原状，决策输出UNDEFINED；否则，检验如下条件：（（s，¯r）∈M（o））∧fs（s）∝fo（o）∧（s具有对o的¯r访问特权），如果条件成立，决策输出YES，下一个状态变化如下：（b＊＝b∪｛s，o，¯r｝）∧其它分量不变；如果上述条件不成立，决策输出NO，下一状态保持原状.

2.2 create＿object（s，o）

执行该操作时，如果访问类型不恰当，则下一状态保持原状，决策输出UNDEFINED；否则，检验如下条件：（（L＿min，L＿max）在主体s的标签范围内，且s获得创建o的授权）∨ （L＝L＿min＝L＿max在主体s的标签范围内，且存在o＇使得o＇∈H（o＇），且fo（o＇）∝L）∧（（s，o，¯w）∈b），如果条件成立，决策输出YES，下一个状态变化如下：（f＊＝f∪ ｛（o，L）∨ （o，L＿min，L＿max）｝）∧ （H＊ ＝H∪ ｛（o＇，o）｝）∧ 其它分量不变；如果上述条件不成立，决策输出NO，下一状态保持原状.

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

执行该操作时，如果访问类型不恰当，则下一状态保持原状，决策输出UNDEFINED；否则，检验如下条件：（（∀o∈O.（（s，o，¯w∨¯e）∈b⇒fo（o）∝fs（s））∧（（s，o，¯r）∈b⇒fs（s）∝fo（o）））∧（Lmax≤fs（s）），如果条件成立，决策输出 YES，下一个状态变化如下：（f＊ ＝ （f∪ ｛s，（Lmin，Lmax）｝）－ ｛（s，a＿mins（s），v＿maxs（s））｝）∧ 其它分量不变；如果上述条件不成立，决策输出NO，下一状态保持原状.

3 模型的Isabelle语言描述及其验证

模型的形式化描述和验证过程，是在基于Linux内核的Ubuntu操作系统下进行的.采用的验证工具是Isabelle／Isar形式化验证工具.Isabelle是一个适用于多种逻辑形式的通用系统，具体定位为一个“通用定理证明环境”，而Isabelle／HOL则是Isabelle实例化Church的经典简单逻辑类型高阶逻辑后形成的交互式定理证明器.

3.1 模型的构成元素

Biba实用模型的构成元素，包括主体、客体、请求和决策.状态是一个 （b，f，M，H）四元组，主、客体具有完整性标签，标签又是由安全级别和类别构成的.

3.1.1 主体和客体

系统将客体分为主体和其他客体.形式化的主体和客体描述都是抽象的数据类型，有待于系统实现时将其实例化.

3.1.2 请求

请求是主体对客体要实施的操作类型.在模型中，主体对客体的操作被描述为Rules，每个Rules对应不同的操作类型，请求实质上是根据操作类型划分的，请求作为Rules的输入传递给Rules所需要的信息.

请求的类型分为获取访问权限，释放访问权限，授予访问权限，撤销访问权限，创建客体，删除客体，改变安全级.

3.1.3 访问模式

访问模式的类型分为只读、写和执行.

3.1.4 Class、Category和SecurityLevel

每个IntegrityLevel类型的安全标签有Category和Sensitive两个元素.Category表示完整性标签所属的类别集合，Sensitive表完整性标签中的敏感级别.

dominates表示两个完整性级别间存在支配关系，equals表示两个完整性级别间存在相等的关系.

3.1.5 状态

AccessTriple表示主体对客体的访问权限，即为访问矩阵的一项.状态States用记录来表示，其中Subjects，Objects表示状态中所包含的主客体集合；CAT表示状态的当前访问集合，AM表示状态的访问矩阵；f＿s，a＿min，v＿max分别表示主体的最大安全级，最小可写的安全级和最大可读的安全级；Hier表示客体的层次结构.

3.2 安全状态

3.2.1 简单安全状态

简单完整性表示当访问方式为读时，要求客体的最大安全级必须控制主体的最大安全级.

3.2.2 ＊－特性

当主体对客体实施写操作时，要求主体、客体的完整级满足一定的要求以防止低完整级的信息向高完整级传递.

3.2.3 调用完整性

表示主体对客体进行执行操作时，主体的完整级要支配客体的完整级.

3.2.4 兼容性

该属性提供同一结构树下不同客体的完整性标签间应遵循的支配关系.

3.2.5 当前访问集的控制

该属性要求当前访问集中的客体一定包含在当前状态的客体集合中.

3.2.6 安全状态

安全状态即为满足上述5条性质的状态.

3.3 安全状态的初始化

3.3.1 初始化操作

初始化时主、客体的集合都为空，当前访问集合，访问矩阵都为空，客体的层次结构树为空树.f＿s，a＿min，v＿max，L＿min，L＿max初 始 化 时 不 赋予任何值.

3.3.2 安全状态的初始化

要求状态初始化满足安全要求.

3.4 BLP模型的状态迁移规则及其安全证明脚本

系统要始终保持在安全状态运行，除了初始状态要满足安全要求以外，系统的所有迁移规则也必须满足安全要求，也即由安全状态经过任意一条迁移规则以后到达的状态仍然是安全状态.接下来就是对系统中各条迁移规则的安全性自动化证明脚本.

3.4.1 Get＿read

3.4.2 Create＿object

3.4.3 Change＿subject＿integrity＿level＿range constdefs

4 结 语

本文以研究设计符合GB／T20272－2006中对最高等级安全操作系统——访问验证保护级安全操作系统要求的完全形式化的安全策略模型为目标，提出了一种具有实际可行性的Biba模型，并详细定义了模型的不变量和安全迁移规则，使得该模型能够满足系统实际操作的需要.于此同时，我们还以定理证明工具Isabelle为依托，对模型的安全状态、安全性质、初始化状态进行完全形式化的描述，参照文中对3条迁移规则的具体描述和验证方法，可以给出全部11条安全迁移规则的自动化正确性验证脚本，从而完成了对模型的自动化形式验证工作.

[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].计算机工程，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信息安全技术操作系统安全技术要求[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／.