操作系统安全_课件_第4章

《操作系统安全_课件_第4章》由会员分享，可在线阅读，更多相关《操作系统安全_课件_第4章（97页珍藏版）》请在金锄头文库上搜索。

1、第4章 安全模型,4.1 安全模型的作用和特点 4.2 形式化安全模型设计 4.3 状态机模型原理 4.4 主要安全模型介绍 4.5 本章小结 4.6 习题,在进行安全操作系统的设计和开发时，需要围绕着给定的安全策略进行。安全策略是对系统安全需求的形式化或者非形式化描述，安全需求则是从有关管理、保护和发布敏感信息的法律、规定和实施细则中导出的。一般来说，信息系统的安全需求主要包含机密性(confidentiality)、完整性(integrity)、可追究性(accountability)和可用性(availability)4个方面。所以基于系统安全策略的定义和内涵可将系统安全策略分为两大类:

2、 访问控制策略(access control policy)和访问支持策略(access supporting policy)。前者反映系统的机密性和完整性要求，它确立相应的访问控制规则，以控制对系统资源的访问；而后者反映系统的可追究性和可用性要求，它以支持访问控制策略的面貌出现。所谓一个系统是安全的，,就是指系统的实现达到了当初设计时所制定的安全策略。 安全策略模型指的是如何用形式化或者非形式化的方法来描述安全策略，也就是系统的安全需求。安全模型就是对安全策略所表达的安全需求的简单、抽象和无歧义的描述，它为安全策略和它的实现机制之间的关联提供了一种框架。安全模型描述了对某个安全策略需要用哪种

3、机制来满足；而模型的实现则描述了如何把特定的机制应用于系统中，从而实现某一特定安全策略所需的安全保护。 下面首先介绍安全模型的作用和特点，然后讨论在高安全等级操作系统中所要求的形式化模型设计的各个方面的内容，最后是对几个著名模型的介绍。,能否成功地获得高安全级别的系统，取决于对安全控制机制的设计和实施投入多少精力。但是，如果对系统的安全需求了解得不清楚，即使运用最好的软件技术，投入最大的精力，也很难达到安全要求的目的。安全模型的目的就在于明确地表达这些需求，为设计开发安全系统提供方针。 安全模型有以下几个特点: 它是精确的、无歧义的； 它是简易和抽象的，所以容易理解； 它是一般性的，只涉及安全

4、性质，而不过度地牵扯系统的功能或实现；,4.1 安全模型的作用和特点, 它是安全策略的显式表示。 安全模型一般分为两种: 形式化的安全模型和非形式化的安全模型。非形式化安全模型仅模拟系统的安全功能；形式化安全模型则使用数学模型，精确地描述安全性及其在系统中使用的情况。 图4-1给出了两种安全操作系统开发途径。 为了简明扼要，安全模型只须模拟系统中与安全相关的功能，省略掉系统中其他与安全无关的功能。这也是系统安全模型和形式化功能规范之间的差别，因为相比较而言，形式化功能规范包括了过多的与安全策略无关的系统功能特征。,图4-1 安全模型与安全操作系统开发过程,J.P.Anderson指出，要开发安

5、全系统首先必须建立系统的安全模型，完成安全系统的建模之后，再进行安全内核的设计和实现。 形式化安全策略模型设计要求人们不仅要建立深刻的模型设计理论，而且要发掘出具有坚实理论基础的实现方法。为了模型的形式化，必须遵循形式设计的过程及表达方式。 美国国防部的彩虹序列中的“对理解可信系统中安全模型的指导”,提出了指导实现的一般性步骤。下面对这些步骤进行分析。,4.2 形式化安全模型设计,1 确定对外部接口的要求。 2 确定内部要求。 3 为策略的执行设计操作规则。 4 确定什么是已知的。 5 论述一致性和正确性。 6 论述关联性。,在现有技术条件下，安全模型大都是以状态机模型作为模拟系统状态的手段，

6、通过对影响系统安全的各种变量和规则的描述和限制，来达到确保系统安全状态不变量的维持（意味着系统安全状态保持）的目的。 状态机模型最初受到欢迎，是由于它们用模仿操作系统和硬件执行过程的方法描述了计算机系统，它将一个系统描述为一个抽象的数学状态机器。 状态机模型在系统安全模型中得到了较为广泛的应用，它可以比较自如地模拟和处理与安全相关的各种变量和函数。,4.3 状态机模型原理,开发一个状态机安全模型包含确定模型的要素（变量、函数、规则等）和安全初始状态。 开发一个状态机模型需要采用如下特定的步骤。 1 定义安全相关的状态变量。 2 定义安全状态的条件。 3 定义状态转换函数。 4 检验函数是否维持

7、了安全状态。 5 定义初始状态。 6 依据安全状态的定义，证明初始状态安全。,1. 模型介绍 Bell-LaPadula模型（简称BLP模型）是D. Elliott Bell和Leonard J. LaPadula于1973年提出的一种适用于军事安全策略的计算机操作系统安全模型，它是最早、也是最常用的一种计算机多级安全模型之一。 在BLP模型中将主体定义为能够发起行为的实体，如进程；将客体定义为被动的主体行为承担者，如数据、文件等；将主体对客体的访问分为,4.4 主要安全模型介绍 4.4.1 Bell-LaPadula模型,r（只读）、w（读写）、a（只写）、x（执行）以及c（控制）等几种访问

8、模式，其中c（控制）是指该主体用来授予或撤销另一主体对某一客体的访问权限的能力。BLP模型的安全策略包括两部分: 自主安全策略和强制安全策略。自主安全策略使用一个访问矩阵表示，访问矩阵第i行第j列的元素Mij表示主体Si对客体Oj的所有允许的访问模式，主体只能按照在访问矩阵中被授予的对客体的访问权限对客体进行相应的访问。强制安全策略包括简单安全特性和*特性，系统对所有的主体和客体都分配一个访问类属性，包括主体和客体的密级和范畴，系统通过比较主体与客体的访问类属性控制主体对客体的访问。,BLP模型是一个状态机模型，它形式化地定义了系统、系统状态以及系统状态间的转换规则；定义了安全概念；制定了一组

9、安全特性，以此对系统状态和状态转换规则进行限制和约束，使得对于一个系统而言，如果它的初始状态是安全的，并且所经过的一系列规则转换都保持安全，那么可以证明该系统是安全的。,2. 模型元素 为了对访问控制机制进行形式化阐述，Bell-LaPadula模型从形式化的角度出发，对模型中涉及到的元素进行了数学形式上的定义。 1) 模型元素的含义 表4-1给出了BLP模型中定义的部分元素及相应的说明。 2) 系统状态表示 状态是系统中元素的表示形式，它由主体、客体、访问属性、访问矩阵以及标识主体和客体的访问类属性的函数组成。状态vV由一个有序的四元组(b,M,f,H)表示。, b (SOA)表示在某个特定

10、的状态下，哪些主体以何种访问属性访问哪些客体。 M表示访问矩阵。 fF表示访问类函数。 H表示当前的层次结构，即当前客体的树形结构。 3) 安全系统的定义 定义规则为函数: RVDV，对规则的解释为，给定一个请求和一个状态，规则决定系统产生的一个响应和下一状态。,3. 模型的几个重要公理 为了解释什么样的状态是一个安全状态，什么样的系统是一个安全系统，BLP模型制定了一组安全公理（特性）。 1) 简单安全性（simple-security property,ss-property） 状态v=(b,M,f,H)满足简单安全性。 2) *特性（*-property） 如前所述，S是S的一个子集，状

11、态v=(b,M,f,H)满足相对于S的*特性（记为*property rel S）。 3) 自主安全性（discretionary-security） 状态v=(b,M,f,H)满足自主安全性。,4) 兼容性公理（compatibility） 状态v=(b,M,f,H)满足兼容性。,4. 状态转换规则 如前所述，规则定义为函数: RVDV。规则保持系统安全状态，iff所有的(Rk,v)=(Dm,v*)，均有v是安全状态,v*也是安全状态。这就是说: (1) 规则保持简单安全性，即对所有的(Rk,v)=(Dm,v*)，均有v保持简单安全性,v*也保持简单安全性。 (2) 规则保持*特性，即对所有

12、的(Rk,v)=(Dm,v*)，均有v保持*-特性=v*也保持*-特性。 (3) 规则保持自主安全性，即对所有的(Rk,v)=(Dm,v*)，均有v保持自主安全性=v*也保持自主安全性。,模型共定义了11条安全状态转换规则。 规则1（R1）: 表示主体对客体请求“只读”访问get-read。 规则2（R2）: 表示主体对客体请求“只写”访问get-append。 规则3（R3）: 表示主体对客体请求“执行”访问get-execute。 规则4（R4）: 表示主体对客体请求“读写”访问get-write。 规则5（R5）: 表示主体释放对客体访问属性release-read/execute/wr

13、ite/append。 规则6（R6）: 表示授予另一主体对客体访问属性: give-read/execute/write/append。,规则7（R7）: 表示撤销另一主体对客体访问属性: rescind-read/execute/write/append。 规则8（R8）: 表示创建一客体（保持兼容性）create-object。 规则9（R9）: 表示删除一组客体delete-object-group。 规则10（R10）: 表示改变主体当前安全级change-subject-current-security-level。 规则11（R11）: 表示改变客体的安全级change-obje

14、ct-security-level。,5. 模型的几个重要定理 BLP模型为了证明系统为安全状态及转换规则保持安全状态，证明了10个重要的定理。 【定理4.1】对每一个初始状态z0，系统(R,D,W,z0)满足简单安全特性iff: 对每一个行为(Ri,Dj,(b*,M*,f*,H*),(b,M,f,H)，关系W()满足: 对任意(S,O,x)b*-b满足相对于f*的简单安全性（ssc rel f*）； 对任意(S,O,x)b不满足相对于f*的简单安全性的不在b*内。,【定理4.2】对每一个满足相对于S的*特性的初始状态z0，系统(R,D,W,z0)满足相对于S的*特性iff对每一个行为(Ri,

15、Dj,(b*,M*,f*,H*),(b,M,f,H)关系W()满足: 对任意的SS，有 O(b*-b)(S:a)f*o(O)f*o(S) O(b*-b)(S:w)f*o(O)=f*c(S) O(b*-b)(S:r)f*c(S)f*o(O) 对任意的SS，有 O(b*-b)(S:a)&f*o(O)f*c(S)=Ob*(S,a) O(b*-b)(S:w)&f*o(O)f*c(S)=Ob*(S,w) O(b*-b)(S:r)&f*o(O)f*c(S)=Ob*(S,r),【定理4.3】系统(R,D,W,z0)满足自主安全特性，iff z0满足自主安全特性并且对每一个行为(Ri,Dj,(b*,M*,f*

16、,H*),(b,M,f,H)，关系W满足: 对任意(Sj,Oj,x)b*-b=xM*ij； 对任意（Si,Oj,x)b*-b&xM*ij=(Si,Oj,x)b*）。 推论（基本安全公理）: 系统(R,D,W,z0)是一个安全系统，iff z0是一安全状态并且对于每一个行为（action），关系W满足定理4.1，定理4.2和定理4.3。,【定理4.4】假设关系W是一套保持简单安全性的规则并且z0满足简单安全性，则系统(R,D,W(w),z0)满足简单安全特性。 【定理4.5】假设关系W是一套保持*-特性的规则并且z0满足*-特性，则系统(R,D,W(w),z0)满足*特性。 【定理4.6】假设关系W是一套保持自主特性的规则并且z0满足自主特性，则系统(R,D,W(w),z0)满足自主安全特性。 【定理4.7】若v=(b,M,f,H)满足简单安全特性，并且(S,O,x)b，b*=b(S,O,x)，则v*=(b*,M,f,H)满足简单安全性，iff (x=e or x=a)or (x=r or x=w) and fs(S)fo(O),