第6章-形式化方法与安全模型

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