其中，α是命令名，X1，…，Xk 是形式参数，每个opi 是以下 α X1 … Xk opi 原语操作之一： ①输入权限r到(Xs,Xo)中； ②从(Xs,Xo)中删除权限r； ③创建主体Xs； ④创建客体Xo； ⑤取消主体Xs； ⑥取消客体Xo。 r(r1, …, rm )是普通权限，s(s1, …, sm)和o(o1, …, om) 是1 至k 间的整数。
2011年8月9日星期二 12
信息安全系 张柱
第6章 形式化方法与安全模型
6.3.1 Lampson访问控制矩阵模型
系统中状态的改变取决于访问矩阵Ｍ的改变，独立的状态机构成 一个系统，因此访问矩阵也可称为系统的“状态保护”。 Lampson模型中访问控制矩阵如图：
主体 (Subjects) Sunny Clone Richard 客 体(Objects) file1 Own/Read/Write Read Read file2 Read Own/Read/Write Write file3 Write Read Own/Read/Write
2011年8月9日星期二
2
信息安全系 张柱
第6章 形式化方法与安全模型(8课时)
6.1 形式化方法
1.定义 所谓形式化方法，指的是使用特定的语言和推理来描述事物的 方法。相对而言，非形式化的方法则是以自然语言和基于人 们的常识来描述事物的方法。 使用形式化的表示方法，尤其是使用一套简单易懂的语义学符 号来描述事物之间的关系，可以大大提高描述安全策略的精 度，使用形式化的证明可以从理论上确保系统的安全策略能 够满足系统的安全需求。 2.通常，系统的不安全性源自于对用户安全需求的错误理解或源 自于系统的实现缺陷。 保证系统安全性的主要策略是，制定一个符合用户安全须由的 安全策略模型，该模型必须同时考虑安全策略和其在自动信 息系统中的实现过程。
2011年8月9日星期二 10
信息安全系 张柱
第6章 形式化方法与安全模型(8课时)
6.2 形式化安全模型
安全策略的主要方面反映在安全模型中包括策略的目标、策略 实施的场合和强度以及用户分类的粒度等。在将安全策略进 行形式化时，这些方面将反映在受控实体的安全属性上。 信息的策略是用来维护信息的安全属性供系统和用户使用，而 访问控制的策略限制系统中的主体对系统资源和资源所包含 的信息的访问。 访问控制属性可以根据其控制的内容进行分类： 不严格的访问控制属性，只和受控实体相关； 严格的访问控制属性则不仅与实体相关，还与其所包含的信息 相关。 大多数的安全策略是集中授权和分布式授权的混合体。
安全操作系统原理与技术
安徽理工大学计算机科学与工程学院 信息安全系 张柱 讲师
2011年8月9日星期二
第6章 形式化方法与安全模型
学习内容: ①了解什么是形式化方法 ②了解形式化安全模型 ③掌握基于访问控制矩阵的安全模型 ④掌握基于格的安全模型 ⑤了解其他安全模型 本章重点： 基于访问控制矩阵的安全模型、基于格的安全模型
主 体 Xs1 Xs2 Xs3 … 客体 Xs1 控制 Xs2 拥有/挂起/恢复 控制 控制 读/写 Xs3 Xo1 拥有 Xo2 拥有 扩展 写 Xo3 读/扩展 拥有 读
2011年8月9日星期二 7
信息安全系 张柱
第6章 形式化方法与安全模型(8课时)
6.1 形式化方法
除了得到形式化语义学的证明外，通过机器证明器的方法不大 可能获得太高的的安全级别保证。在这种情况下，一个公式 A是一系列公式集B的有效结果，当且仅当每个满足公式集B 的解释同样满足公式A。即不经过形式化语义学的证明，证 明器可能不够安全并且有可能接受错误的假设。 形式化语义学包括对公式功能的解释以及对系统的证明方法是 正确的相关证明。
2011年8月9日星期二
8
信息安全系 张柱
第6章 形式化方法与安全模型(8课时)
6.2 形式化安全模型
形式化模型，指的是用形式化的方法来描述如何实现系统的安 全要求，包括机密性、完整性和可用性。 一个安全的计算机系统可以分为如下几大部分：数据结构、进 程、用户信息、I/O设备以及被控实体的安全属性。 标识被控实体在设计一个安全模型中占据着重要地位，对于达 到TCSEC规定的B2级或以上安全级的系统来说，被控实体必 须包括所有的系统资源。系统包括显式被控实体和隐式被控 实体。 数据结构是一个数据仓库，包含标明系统内部状态的数据和值。 系统中进程可以利用系统事先明确定义的允许的操作来对这 些数据或值进行读或写访问。 一个最小的数据结构，同时也是显式被控实体的存储客体，存 储客体的安全属性可能包括安全级和用户访问权限。
end
2011年8月9日星期二
17
信息安全系 张柱
第6章 形式化方法与安全模型
6.3.3 HRU模型
在HRU模型中，将系统的保护基于三元组(S,O,P),其中，S 表示 系统当前的主体集，O表示当前系统的客体集，并且S包含 于O，p表示访问控制矩阵，此矩阵中，行表示主体，列表示 客体，P[S,O]是权限集R的一个子集，表示主体S对客体O拥 有的权限，HRU模型中的访问控制矩阵。
6.1 形式化方法
高层策略目标 外部接口需求 内部需求 操作规则 高层设计规范 低层设计规范 代码实现及硬件描述 正 确 性 依 赖
具体描述
2011年8月9日星期二
4
信息安全系 张柱
第6章 形式化方法与安全模型(8课时)
6.1 形式化方法
高层策略目标：用来指定设计和使用计算机系统来实现什么目 标； 外部接口需求：是将高层策略目标应用于计算机系统的外部接 口。 内部需求：用来约束系统实体或部件相互之间的关系。对安全 的形式化定义，通常包含内部需求和外部接口两个方面。 操作规则：用来解释内部需求是如何通过指定的访问检查和相 关的行为措施来保证内部需求的正确实施。 高层设计：用来指定系统部件或被控的实体的行为以及TCB接口 的复杂功能描述。 代码编写，涉及到硬件接口的代码，必须详细了解硬件接口规 范。
A[x,o]中为“拥有者” A[x,s]中为“控制” A[x,s]中的为“控制” A[x,o]中为“拥有者” A[x,s]中的为“控制” 或A[x,o]为“拥有者” A[x,o]中为“拥有者” A[x,o]中为r*
2011年8月9日星期二
15
信息安全系 张柱
第6章 形式化方法与安全模型 6.3 基于访问控制矩阵的安全模型 6.3.3 HRU模型 HRU模式是Graham-Denning模型的变体，在HRU模型中，基于 “命令”来描述对主客体的访问控制机制，其中每个命令含 有“条件”和“基本操作”。命令结构如下： command α (X1 , X 2 , L, X k ) if r1 in (X s1 , X o1 ) and
2011年8月9日星期二 14
信息安全系 张柱
第6章 形式化方法与安全模型
命令 创立目标o 创立主体s 删除目标o 删除主体s S对o读访问权 删除s对o的访问权r 给s授予对o的访问权r 转移对o的访问权r或r*给s 条件 －－ －－
6.3.2 Graham-Denning模型
作 用 在A中增加一个关于o的列， 在A[x,o]处放入“拥有者” 在A中增加一个关于s的行，在 A[x,s]处放入“控制” 删除o对应的列 删除s对应的行 将A[s,o]拷贝给x 从A[s,o]中去掉r 从A[s,o]中增加r 从A[s,o]中增加r或r*
2011年8月9日星期二
6
பைடு நூலகம்
信息安全系 张柱
第6章 形式化方法与安全模型(8课时)
6.1 形式化方法
机器证明依赖于使用机器化的证明器，“检查机”具有如下的 特性： ①接受输入； ②决定输出； ③如果成功，则该推测是该系列假设的有效结果。 证明器能够潜在的提升用户效率。在操作系统的安全策略模型 中，经常需要自动机的协助。典型地，对安全的定义包含许 多需求，这些需求通常以状态不变式和状态转换约束的形式 出现。 特别地，一个需求只处理几个状态元素，任何操作规则对这些 元素的细微的修改都会导致对需求的违反，因此，至多90% 的必需的引理都可能是非常重要的。
2011年8月9日星期二 5
信息安全系 张柱
第6章 形式化方法与安全模型(8课时)
6.1 形式化方法
高层目标指定的恰当性对设计一个计算机系统尤其重要，其是 否合适的判断标准是，能否抵御威胁并且可以加以实现。 系统的安全策略是否合适是使用该系统的组织的安全策略能否 成功实施的关键。如果一个系统的安全策略的实施能够达到 系统事先制定的安全目标，则该安全策略就是适当的。 有三种“形式化证明”方法： ①数学证明； ②机器证明； ③Hilbert证明。 数学证明依赖于使用数学语言来进行模型或范型的形式化，不 允许自动化。
r2 in (X s2 , X o2 ) and L rm in (X sm , X om ) then op1 , op 2 , L , op n end
2011年8月9日星期二 16
信息安全系 张柱
第6章 形式化方法与安全模型 或者，如果m为0，命令格式为：
6.3.3 HRU模型
command α (X1 , X 2 , L, X k ) op1 , op 2 , L , op n
2011年8月9日星期二
13
信息安全系 张柱
第6章 形式化方法与安全模型 6.3 基于访问控制矩阵的安全模型 6.3.2 Graham-Denning模型 在Graham-Denning模型中，对主体集合S、目标集合O、权利集 合R和访问控制矩阵A进行操作。矩阵中每个主体一行，每 个主体以及每个目标均有一列。一个主体对于另一个主体， 或者一个目标的权利利用矩阵元素的内容来表示。 对于每个目标，标明为“拥有者”的主体，有特殊的权利；对 于每个主体，标明为“控制者”的另一个主体，有特殊权利。 在Graham-Denning模型中，有八个基本的保护权，这些权利被 表示成主体能够发出的命令，作用于其他主体或目标。 ①创建目标； ⑤删除访问权； ②创立主体，删除目标，删除主体； ⑥转移访问权。 ③读访问权； 这些规则如图所示。 ④授予访问权；