《第6章形式化方法与安全模型ppt课件.ppt》由会员分享，可在线阅读，更多相关《第6章形式化方法与安全模型ppt课件.ppt（46页珍藏版）》请在三一办公上搜索。
1、2023/1/11,安全操作系统原理与技术,安徽理工大学计算机科学与工程学院信息安全系张柱 讲师,2023/1/11,2,第6章 形式化方法与安全模型,学习内容:了解什么是形式化方法了解形式化安全模型掌握基于访问控制矩阵的安全模型掌握基于格的安全模型了解其他安全模型本章重点：基于访问控制矩阵的安全模型、基于格的安全模型,2023/1/11,3,第6章 形式化方法与安全模型(8课时)6.1 形式化方法,1.定义所谓形式化方法，指的是使用特定的语言和推理来描述事物的方法。相对而言，非形式化的方法则是以自然语言和基于人们的常识来描述事物的方法。使用形式化的表示方法，尤其是使用一套简单易懂的语义学符号
2、来描述事物之间的关系，可以大大提高描述安全策略的精度，使用形式化的证明可以从理论上确保系统的安全策略能够满足系统的安全需求。2.通常，系统的不安全性源自于对用户安全需求的错误理解或源自于系统的实现缺陷。保证系统安全性的主要策略是，制定一个符合用户安全须由的安全策略模型，该模型必须同时考虑安全策略和其在自动信息系统中的实现过程。,2023/1/11,4,第6章 形式化方法与安全模型(8课时)6.1 形式化方法,安全策略模型应由如下两个子模型组成：对安全的定义和一套操作的规则。为了说明形式化方法在安全系统的建立过程中所起的角色，有必要来对建立一个安全自动信息系统开发的各个阶段进行详细的描述，如图。
3、,2023/1/11,5,第6章 形式化方法与安全模型(8课时)6.1 形式化方法,高层策略目标：用来指定设计和使用计算机系统来实现什么目标；外部接口需求：是将高层策略目标应用于计算机系统的外部接口。内部需求：用来约束系统实体或部件相互之间的关系。对安全的形式化定义，通常包含内部需求和外部接口两个方面。操作规则：用来解释内部需求是如何通过指定的访问检查和相关的行为措施来保证内部需求的正确实施。高层设计：用来指定系统部件或被控的实体的行为以及TCB接口的复杂功能描述。代码编写，涉及到硬件接口的代码，必须详细了解硬件接口规范。,2023/1/11,6,第6章 形式化方法与安全模型(8课时)6.1
4、形式化方法,高层目标指定的恰当性对设计一个计算机系统尤其重要，其是否合适的判断标准是，能否抵御威胁并且可以加以实现。系统的安全策略是否合适是使用该系统的组织的安全策略能否成功实施的关键。如果一个系统的安全策略的实施能够达到系统事先制定的安全目标，则该安全策略就是适当的。有三种“形式化证明”方法：数学证明；机器证明；Hilbert证明。数学证明依赖于使用数学语言来进行模型或范型的形式化，不允许自动化。,2023/1/11,7,第6章 形式化方法与安全模型(8课时)6.1 形式化方法,机器证明依赖于使用机器化的证明器，“检查机”具有如下的特性：接受输入；决定输出；如果成功，则该推测是该系列假设的有
5、效结果。证明器能够潜在的提升用户效率。在操作系统的安全策略模型中，经常需要自动机的协助。典型地，对安全的定义包含许多需求，这些需求通常以状态不变式和状态转换约束的形式出现。特别地，一个需求只处理几个状态元素，任何操作规则对这些元素的细微的修改都会导致对需求的违反，因此，至多90%的必需的引理都可能是非常重要的。,2023/1/11,8,第6章 形式化方法与安全模型(8课时)6.1 形式化方法,除了得到形式化语义学的证明外，通过机器证明器的方法不大可能获得太高的的安全级别保证。在这种情况下，一个公式A是一系列公式集B的有效结果，当且仅当每个满足公式集B的解释同样满足公式A。即不经过形式化语义学的
6、证明，证明器可能不够安全并且有可能接受错误的假设。形式化语义学包括对公式功能的解释以及对系统的证明方法是正确的相关证明。,2023/1/11,9,第6章 形式化方法与安全模型(8课时)6.2 形式化安全模型,形式化模型，指的是用形式化的方法来描述如何实现系统的安全要求，包括机密性、完整性和可用性。一个安全的计算机系统可以分为如下几大部分：数据结构、进程、用户信息、I/O设备以及被控实体的安全属性。标识被控实体在设计一个安全模型中占据着重要地位，对于达到TCSEC规定的B2级或以上安全级的系统来说，被控实体必须包括所有的系统资源。系统包括显式被控实体和隐式被控实体。数据结构是一个数据仓库，包含标
7、明系统内部状态的数据和值。系统中进程可以利用系统事先明确定义的允许的操作来对这些数据或值进行读或写访问。一个最小的数据结构，同时也是显式被控实体的存储客体，存储客体的安全属性可能包括安全级和用户访问权限。,2023/1/11,10,第6章 形式化方法与安全模型(8课时)6.2 形式化安全模型,在包含安全级的模型中，在最小化的情况下，存储客体具有唯一的安全级，存储客体可能被组合起来形成多级数据结构，其中每个客体被赋予自己的安全级。进程可创建、删除存储客体及其他进程以及与它们交互，还可以与I/O设备交互。显式被控进程称为“主体”。通常具有多种与它关联的安全属性，可能包括安全级、硬件安全属性。在支持
8、角色的程序中，系统用户可履行制定角色的职责，一个用户可以拥有多个角色，一个角色也可以包含多个用户。用户与系统设备的交互行为在模型中体现对I/O设备的约束。外部策略要求系统只有允许授权用户才能访问相应的I/O设备。I/O设备封装在TCB软件内，并被看作是被动实体。安全属性可以显式地与显式受控实体相关联，还有一些与系统环境相关的安全属性。,2023/1/11,11,第6章 形式化方法与安全模型(8课时)6.2 形式化安全模型,安全策略的主要方面反映在安全模型中包括策略的目标、策略实施的场合和强度以及用户分类的粒度等。在将安全策略进行形式化时，这些方面将反映在受控实体的安全属性上。信息的策略是用来维
9、护信息的安全属性供系统和用户使用，而访问控制的策略限制系统中的主体对系统资源和资源所包含的信息的访问。访问控制属性可以根据其控制的内容进行分类：不严格的访问控制属性，只和受控实体相关；严格的访问控制属性则不仅与实体相关，还与其所包含的信息相关。大多数的安全策略是集中授权和分布式授权的混合体。,2023/1/11,12,第6章 形式化方法与安全模型 6.3 基于访问控制矩阵的安全模型,6.3.1 Lampson访问控制矩阵模型利用状态机模型来形式化描述对客体访问的安全模型大多数是Lampson访问控制矩阵模型的变体。在此模型中，客体被视为存储器，访问控制检查不基于存储在此容器内的值，而是基于系统
10、的状态，系统状态中与安全相关的要素概括在个访问矩阵中。Lampson模型中，系统的状态是由一个三元组(S,O,M)来决定，其中：S：表示系统中主体的集合，也是系统正在运行的程序集合；O：系统中客体的集合，客体是指主体行为的对象，即主体行为的直接承担者。M：表示二维访问矩阵，主体用行表示，客体用列表示，主、客体的交叉点表示主体对客体所拥有的访问权限。,2023/1/11,13,第6章 形式化方法与安全模型 6.3.1 Lampson访问控制矩阵模型,系统中状态的改变取决于访问矩阵的改变，独立的状态机构成一个系统，因此访问矩阵也可称为系统的“状态保护”。Lampson模型中访问控制矩阵如图：,20
11、23/1/11,14,第6章 形式化方法与安全模型 6.3 基于访问控制矩阵的安全模型,6.3.2 Graham-Denning模型在Graham-Denning模型中，对主体集合S、目标集合O、权利集合R和访问控制矩阵A进行操作。矩阵中每个主体一行，每个主体以及每个目标均有一列。一个主体对于另一个主体，或者一个目标的权利利用矩阵元素的内容来表示。对于每个目标，标明为“拥有者”的主体，有特殊的权利；对于每个主体，标明为“控制者”的另一个主体，有特殊权利。在Graham-Denning模型中，有八个基本的保护权，这些权利被表示成主体能够发出的命令，作用于其他主体或目标。创建目标；创立主体，删除目
12、标，删除主体；读访问权；授予访问权；,删除访问权；转移访问权。这些规则如图所示。,2023/1/11,15,第6章 形式化方法与安全模型 6.3.2 Graham-Denning模型,2023/1/11,16,第6章 形式化方法与安全模型 6.3 基于访问控制矩阵的安全模型,6.3.3 HRU模型HRU模式是Graham-Denning模型的变体，在HRU模型中，基于“命令”来描述对主客体的访问控制机制，其中每个命令含有“条件”和“基本操作”。命令结构如下：,2023/1/11,17,第6章 形式化方法与安全模型 6.3.3 HRU模型,或者，如果m为0，命令格式为：,其中，是命令名，X1，X
13、k 是形式参数，每个opi 是以下原语操作之一：输入权限r到(Xs,Xo)中；从(Xs,Xo)中删除权限r；创建主体Xs；创建客体Xo；取消主体Xs；取消客体Xo。r(r1,rm)是普通权限，s(s1,sm)和o(o1,om)是1 至k 间的整数。,2023/1/11,18,第6章 形式化方法与安全模型 6.3.3 HRU模型,在HRU模型中，将系统的保护基于三元组(S,O,P),其中，S 表示系统当前的主体集，O表示当前系统的客体集，并且S包含于O，p表示访问控制矩阵，此矩阵中，行表示主体，列表示客体，PS,O是权限集R的一个子集，表示主体S对客体O拥有的权限，HRU模型中的访问控制矩阵。,
14、2023/1/11,19,第6章 形式化方法与安全模型 6.3.3 HRU模型,在HRU模型中，创建CREATE、授予CONFER和撤销REMOVE命令如下：1.创建(CREATE)进程可能创建客体，进程拥有对自己创建的客体的拥有权，表示如下：command CREATE(process,file)create object fileenter own into(process,file)end,2023/1/11,20,第6章 形式化方法与安全模型 6.3.3 HRU模型,2.授予(CONFER)文件的拥有者可以授予除“拥有”权限以外的任何权限给任何一个其他主体，表示如下：command C
15、ONFER(owner,friend,file)if own in(owner,file)then enter r into(friend,file)end此处，r表示读、写和执行等权限,2023/1/11,21,第6章 形式化方法与安全模型 6.3.3 HRU模型,3.撤销(REMOVE)文件的拥有者可以撤销任何一个其他主体赋予此文件的权限，表示如下：command REMOVE(owner,exfriend,file)if own in(owner,file)and r in(exfriend,file)then delete r from(exfriend,file)end,2023/1
16、/11,22,第6章 形式化方法与安全模型 6.3.3 HRU模型,Harrison等得出两个重要结论对保护系统的设计者有重要影响。第一个结论适用于限定每条命令只包含一个操作时的情况。可以判定一个给定的保护系统，从访问控制矩阵的某一给定的初始配置出发，能否允许一给定的用户获得对一个给定目标的给定的访问权。如果不限定每条命令只含一项操作，则一个给定的保护系统是否可参照一给定的权利问题是“不可”判定的。,2023/1/11,23,第6章 形式化方法与安全模型(8课时)6.4 基于格的安全模型,6.4.1 Bell-LaPadula模型BLP模型是1973年创立的一种模拟符合军事安全策略的计算机操作
17、模型，也是最常使用的一种计算机多级安全模型。BLP模型是一种状态机模型，它形式化地定义了系统、系统状态以及系统状态间的转换规则，定义了安全的概念，并制定了一组安全特性，以此对系统状态和状态转换规则进行限制和约束，使得对一个系统，如果它的初始状态是安全的，并且经过一系列的规则都保持安全性，则可以证明该系统是安全的。,2023/1/11,24,第6章 形式化方法与安全模型(8课时)6.4.1 Bell-LaPadula模型,1.系统状态的表示状态是系统中元素的表示，它由主体、客体、访问属性、访问矩阵以及标识主体和客体的访问类属性的函数组成。状态vV由一个有序的四元组(b,M,f,H)所表示，其中：
18、标识在某个特定的状态下，哪些主体以何种访问属性访问哪些客体，其中S是主体集，O为客体集，A=r,w,a,e是访问属性集；M：表示访问矩阵，其中元素 表示主体Si对客体Oj具有的访问权限；fF：表示访问类函数，记作f=(fs,fo,fc),其中fs表示主体的安全级函数；fc表示主体当前拥有的安全级函数；fo表示客体的安全级函数。H：是客体间的层次关系,即当前客体的树形结构，OjH(O)表示在此树形结构中，Oj为叶子节点，O为父节点。,2023/1/11,25,第6章 形式化方法与安全模型(8课时)6.4.1 Bell-LaPadula模型,元素H在(其中PO表示O的幂子集)中，iff：OiOj
19、H(Oi)H(Oj)=不存在集合O1,O2,Ow使得对每个r，1r w，有Or+1H(Or)，且Ow+1O12.安全系统的定义定义规则：RVDV含义：给定一个请求和一个状态，规则决定系统产生一个响应和下一个状态。其中R为请求集，V为状态集，D为判定集yes,no,error,?，yes表示请求被执行，no表示请求被拒绝，error表示有多个规则适用于该请求-状态对，?表示规则不能处理该请求。,2023/1/11,26,第6章 形式化方法与安全模型(8课时)6.4.1 Bell-LaPadula模型,设 是相对于R,D,V的一组规则集，关系 定义为(Rk,Dm,v*,v)iff Dm?，并且存在
20、唯一的i，1is，使得(Dm,v*)；而系统 定义为(x,y,z)(R,D,W,z0)，iff：对每个tT,(xt,yt,zt,zt-1)W，其中z0为初始状态。系统(R,D,W,z0)是一个安全系统，iff：系统的每个状态(z0,z1,zn)均为为安全状态。,2023/1/11,27,第6章 形式化方法与安全模型(8课时)6.4.1 Bell-LaPadula模型,3.模型几个重要的公理简单安全性：状态v=(b,M,f,H)满足简单安全性，对所有：其中，符号表示前者支配后者，即b(S:x1,x2,xn)表示b中主体S对其具有访问权限xi(1in)的所有客体集合。*-特性：S是S的一个子集，状
21、态v=(b,M,f,H)，满足相对于S的*-特性，记为*-property rel S，iff对所有的,2023/1/11,28,第6章 形式化方法与安全模型(8课时)6.4.1 Bell-LaPadula模型,自主安全性：状态v=(b,M,f,H)，满足自主安全特性，iff：对于所有的.兼容性公理：状态v(b,M,f,H)满足兼容性，iff：对所有的oO，有：,2023/1/11,29,第6章 形式化方法与安全模型(8课时)6.4.1 Bell-LaPadula模型,4.状态转换规则规则定义为,：RVDV。规则保持系统安全状态，iff：对所有的(Rk,v)=(Dm,v*),有v是安全状态，则
22、v*是安全状态，即：规则保持简单安全性：即对所有的(Rk,v)=(Dm,v*)，有v保持简单安全性，则v*也保持安全性。规则保持*-特性：即对所有的(Rk,v)=(Dm,v*)，有v保持*-特性，则v*也保持*-特性。规则保持自主安全性：即对所有的(Rk,v)=(Dm,v*)，有v保持自主安全性，则v*也自主安全性。,2023/1/11,30,第6章 形式化方法与安全模型(8课时)6.4.1 Bell-LaPadula模型,5.模型的几个重要定理定理1：对于每个初始状态z0，系统(R,D,W,z0)满足简单安全特性，iff：对每个行为(Ri,Dj,(b*,M*,f*,H*),(b,M,f,H)
23、，关系W()满足：对任意(S,O,x)b*-b满足相对于f*的简单安全性；对任意(S,O,x)b不满足相对于f*的简单安全性的不在b*内。定理2：对每个满足相对于S的*-特性的初始状态z0，系统(R,D,W,z0)满足相对于S的*-特性，iff：对每个行为(Ri,Dj,(b*,M*,f*,H*),(b,M,f,H)，关系W()满足：对任意SS，有：,2023/1/11,31,第6章 形式化方法与安全模型(8课时)6.4.1 Bell-LaPadula模型,对任意SS，有：定理3：系统(R,D,W,z0)满足自主安全特性，iff：z0满足自主安全性，并且对每个行为(Ri,Dj,(b*,M*,f*
24、,H*),(b,M,f,H)，关系W()满足：对任意对任意,2023/1/11,32,第6章 形式化方法与安全模型(8课时)6.4.1 Bell-LaPadula模型,推论(基本安全公理)：系统(R,D,W,z0)是一个安全系统，iff：z0是一个安全状态，并且对于每个动作，关系W满足定理1，定理2和定理3。定理4：假设关系W是一套保持简单安全特性的规则并且满足简单安全性，则系统(R,D,W(),z0)满足简单安全特性。定理5：假设关系W是一套保持*-特性，并且z0满足*-特性，则系统(R,D,W(),z0)满足*-特性。定理6：假设关系W是一套保持自主特性，并且z0满足自主特性，则系统(R,
25、D,W(),z0)满足简单自主特性。,2023/1/11,33,第6章 形式化方法与安全模型(8课时)6.4.1 Bell-LaPadula模型,定理7：若v=(b,M,f,H)满足简单安全特性，并且，则v*=(b*,M,f,H)满足简单安全性，iff：(x=e or x=a)or(x=r or x=w)and fs(S)fo(O)定理8：若v=(b,M,f,H)满足相对于 的*-特性，并且对任意的 并且,b*=b(S,O,x)，则v*=(b*,M,f,H)满足相对于S的*-特性，iff：if x=a then fo(O)fc(S)if x=w then fo(O)=fc(S)if x=r t
26、hen fc(S)fo(O),2023/1/11,34,第6章 形式化方法与安全模型(8课时)6.4.1 Bell-LaPadula模型,定理9：若v=(b,M,f,H)满足自主安全特性，并且，则v*=(b*,M,f,H)满足自主安全性，iff：xMij定理10：设为规则，且(Rk,v)=(Dm,v*),其中v=(b,M,f,H)，v*(b*,M*,f*,H*)，则有：如果，且f*=f，则规则保持简单安全性；如果，且f*=f，则规则保持*-特性；如果，且对任意的i、j，f有，则保持自主安全性；如果，且f*=f，且对任意的i、j，有，则保持安全状态。,2023/1/11,35,第6章 形式化方法
27、与安全模型(8课时)6.4.1 Bell-LaPadula模型,6.对BLP模型的争论1)McLean的+-特性及其基本安全定理McLean的基础：给定一个已知为不安全的假定系统，通过“基本安全定理”能够证明该不安全的系统是安全的。定义1：状态(b,M,f)满足+-特性，当且仅当对每个主体sS，下列条件成立：也就是说，+-特性对主体S和客体O成立，当且仅当主体S的安全级别支配客体O的安全级别。状态满足+-特性，当且仅当对于每个三元组(S,O,x)，主体S和客体O都保持+-特性。,2023/1/11,36,第6章 形式化方法与安全模型(8课时)6.4.1 Bell-LaPadula模型,定理11
28、(McLean)：对任何一个安全状态z0，系统(R,D,W,z0)相对于 满足+-特性，iff：对任一行为(Ri,Dj,(b,a,f)(b,a,f)，关系W()满足(对任意sS)：对任意(S,O,x)b-b满足相对于S的+-特性；对任意(S,O,x)b不满足相对于S的+-特性的不在b内。定理12(McLean基本安全定理)：系统(R,D,W,z0)是一个安全系统，iff：z0是安全的，且关系W()满足定理1、定理2和定理11中的条件。,2023/1/11,37,第6章 形式化方法与安全模型(8课时)6.4.1 Bell-LaPadula模型,2)McLean的系统Z以及更多的问题系统Z具有弱宁
29、静特性，并且以此支持一个动作，当某一主体对任意客体请求任意类型的访问时，系统首先将所有主体和客体降到最低安全级别，然后在访问控制矩阵中添加访问权限，并允许访问。定理13：如果z0是一个安全状态，而且W中的每个动作都满足替代版的简单安全条件、*-特性和自主安全特性，那么系统(R,D,W,z0)就是一个安全系统。实例，系统Z中有两个安全级别HIGH和LOW，HIGHLOW。初始状态有一个主体s和一个客体o，在初始状态下fsc(s)LOW且foc(o)=HIGH，as,o=w,且b(S,O,w)。当S对O请求读取时，规则将系统转换到一个状态，在该状态下foc(o)=LOW,(s,o,r)b,as,o
30、=r,w。但是由于(s,o,r)b-b且fsc(s)foc(o),就产生了非法访问。,2023/1/11,38,第6章 形式化方法与安全模型(8课时)6.4 基于格的安全模型,6.4.2 D.Denning模型1.概述信息流模型是访问控制模型的变形，这类模型不检查主体对客体的存取，而试图从一个客体到另一个客体的信息传输过程，根据两个客体的安全属性决定操作是否进行。信息流分析能够保证操作系统模型在对敏感信息存取时不会将数据泄露给所调用的模块。,2023/1/11,39,第6章 形式化方法与安全模型(8课时)6.4.2 D.Denning模型,2.格结构有界格是一个有限的偏序集，有最小上界和最大下
31、界操作符的数学结构，关系(S,+,*)是格，必须具有如下性质：(S,)是一个偏序集；S是有限的；S有下界L，对于S中的所有A，有LA；+是S上的最小上界操作符；*是S上的最大下界操作符。,2023/1/11,40,第6章 形式化方法与安全模型(8课时)6.4.2 D.Denning模型,3.典型的格结构例如线性优先权格，描述了n个类之间的线性次序，对所有i,j0,n-1,i+j=max(i,j),i*j=min(i,j),L=0,H=n-1。当n=2时，非机密为0，机密为1。当n=4时，可用于普通军事安全问题，非机密为0，机密为1，秘密为2，绝密为3。,2023/1/11,41,第6章 形式化
32、方法与安全模型(8课时)6.4.2 D.Denning模型,例如：描述了2n(n=3)个子集之间的包含关系，箭头代表所有权关系。该图推广到任何的n值，且可以用于有如下特性的系统：信息只能流向与出发点的类至少有相同的所有权的类。,2023/1/11,42,第6章 形式化方法与安全模型(8课时)6.4.2 D.Denning模型,假定程序有m个输入参数x1,x2,xm和n个输出参数y1,y2,yn，使得每个输出参数只决定于某些输入。所有权格可以从X=x1,x2,xm的子集构造。和每个输入xi相联系的类是氮元素集合#xi=xi，且与每个输出相联系的类是集合#yj=xi|xiy是允许的。当且仅当b至少
33、具备a的性质时，客体a的信息才允许流入客体b。令(A,C)和(A,C)是安全类，其中A和A是安全级，C和C是范畴，则：(A,C)(A,C)当且仅当AA,(A,C)+(A,C)=(max(A,A),CC)(A,C)*(A,C)=(min(A,A),CC)L=(0,)=(不保密,)，H=(3,X)=(绝密,X)可见，格模型是BLP模型的扩展。,2023/1/11,43,第6章 形式化方法与安全模型(8课时)6.4.2 D.Denning模型,4.信息流格模型中的信息状态和策略描述系统的信息状态由系统中每个客体的值和安全类描述构成。客体可以是一种逻辑结构，或物理结构。一个流可以用(S,)表示，其中S
34、是安全类的集合，说明两个类之间可容许的流动的一个流关系。每个存储客体x被指定一个安全类，表示为#x。用#x#y表示流策略允许从客体x到客体y的流。客体的类可以不变，也可以改变，采用不变类或静态连接时，在x存在期间，客体的类保持不变；采用可变类或动态连接时，客体的类随着它的内容而变化。给定客体x和y，iff：#x#y，根据流策略从x到y的流是许可的，若y有可变类，则在这个流之后的#y就是它的类。在多级安全的信息流策略中，允许信息在一类之中或向上一级类流动，但不允许向下或向无关的类流动。,2023/1/11,44,第6章 形式化方法与安全模型(8课时)6.4.2 D.Denning模型,对安全类#
35、x和#y，关系#x#y意味着类#x的信息低于或等于#y类的信息。因此，iff：#x#y，类#x的信息才可以允许流入类#y。假定安全类是有限个，并且流关系具有自反性(#x#x)、传递性(若#x#y和#y#z，则#x#z)和反对称性(若#x#y和#y#x，则#x=#y)。则可以假定(S,)是格。因此，对于任意两个类，只有唯一的上界和下界，如果(S,)不是格，则可以将它变形为格，需要添加新的必要的类，并且保证不改变原来的类之间的流。,2023/1/11,45,第6章 形式化方法与安全模型(8课时)6.4.2 D.Denning模型,对安全类#x和#y，关系#x#y意味着类#x的信息低于或等于#y类的信息。因此，iff：#x#y，类#x的信息才可以允许流入类#y。假定安全类是有限个，并且流关系具有自反性(#x#x)、传递性(若#x#y和#y#z，则#x#z)和反对称性(若#x#y和#y#x，则#x=#y)。则可以假定(S,)是格。因此，对于任意两个类，只有唯一的上界和下界，如果(S,)不是格，则可以将它变形为格，需要添加新的必要的类，并且保证不改变原来的类之间的流。,2023/1/11,安全操作系统原理与技术,谢谢大家！,
