安全模型的构建(OS).doc

1 安全模型的构建本节将以构建一个基于访问矩阵-监控器的安全模型为例，说明安全模型的构建方法与步骤。访问矩阵-监控器安全模型是一种基于状态机的模型，有着广泛的应用，因此，所介绍的模型构建方法与思路对其他类型的安全模型也适用。1.1 建模的方法步骤下面要建立的安全模型是由访问矩阵与访问监控器组成的，访问矩阵反映了系统的安全状态。保护系统可以抽象地用几个要素及其相互关系来描述：系统中包括主体集合与客体集合，主体包括用户或完成用户任务的进程，客体是指系统中所有可以被访问的对象，例如，文件、库表、记录、字段、程序变量、存储区或存储单元、字节甚至比特位都可能属于需要受到保护的对象。访问矩阵中存放着主体与客体的安全属性和主体对客体的访问关系与访问权限（如果主体与客体对应的矩阵元素为空，则两者之间没有访问关系）。我们假定模型采用的自主访问控制原则是，一个主体对另一个主体可以有控制权（如父进程对子进程），可以把自己对某客体的访问权限转授给另一个主体，也可以从某主体收回（删除）某些权利，主体还可以修改对自己所属客体的访问权。系统中除了访问矩阵外还有其他一些与系统安全控制有关的变量。改变这些变量的值或者修改访问矩阵中的内容（安全属性、访问关系、访问权限、增删主、客体等）都会使系统安全状态发生变化。访问监控器可以看成为一个状态机，是系统访问控制的执行者和访问矩阵与安全变量的管理者、控制者与修改者。系统安全状态的变化可以理解为由监控器调用的状态转换函数完成的。为了建立一个简洁的体现上述概念的安全模型，在安全模型中要尽量减少，甚至不包括那些与安全无关的功能与状态或其他因素。让模型中只包括与安全有关的安全状态变量（访问矩阵本身可以看成为一个大的数组变量）和状态转换函数，就可以做到既使安全模型反映系统的行为，又达到简化安全模型的目的。利用访问矩阵-监控器安全模型证明（或说明）系统的安全性，需要在模型中定义或证明以下内容：（1）分析系统的安全需求，确定系统的安全策略，并给出其形式描述。（2）根据安全策略定义系统的安全状态，主要是确定访问矩阵中的内容，包括主体、客体的安全属性、访问关系与访问权限等内容。需要的话，还可以包括一些其他辅助安全变量，然后为这些变量指定初始值，定义初始状态。（3）定义安全状态不变式，它表明在安全状态中，状态变量值之间必须保持的关系；（4）定义状态转换函数（或称操作命令），它描述了安全状态变量的值发生变化而引起的系统安全状态的变化。状态转换函数实际上就是4.1.1.3定义的命令或其扩展。（5）证明转换函数能够维持系统安全状态，即证明转换函数在执行前与执行后系统都处于安全状态。为了确保维持系统的安全状态，常常需要对转换函数增加约束条件。（6）用安全状态的定义证明初始状态是安全的。如果能够证明该初始状态是安全的，然后证明所有的状态转换函数能够保持系统的安全状态，那么根据数学推理就可以保证，无论按什么顺序调用系统功能，系统将总是能够保持安全状态的。1.2 模型构建实例下面以在自主访问控制下实施部分强制访问控制策略的系统为背景，给出一个简单的基于访问矩阵-监控器概念的多级安全模型，并以此为例说明安全模型的一种构建过程和定义方法。构建过程可以分为3大步，首先确定系统的安全策略，然后根据安全策略要求定义安全模型的各个基本要素，最后再证明在状态转移函数的作用下，安全模型能够保持安全状态不变。由于访问矩阵-监控器模型属于状态机类安全模型，而此类安全模型是一种应用非常广泛的模型，因此，本节介绍的模型建立方法有普遍的参考意义。下面首先给出安全策略的描述1.2.1 安全策略的描述不失一般性，在我们所研究的模型中，假定访问的目标是文件，对这些目标的自主访问控制策略都体现在访问矩阵中。我们可以把其中的主要控制策略归纳为以下几条，先用自然语言表述如下：策略（a）只有当某用户对某文件有访问关系时，该用户才能按规定的访问权对该文件进行访问；策略（b）只有系统管理员才能够创建与删除用户和修改它们的安全属性和访问权限；策略（c）每个用户都有权创建与删除自己的文件，并可以赋予或修改它们的安全属性或访问权限。策略（d）只有当某用户是某文件的主人时，该用户才有权把对该文件的访问权转授其他用户或撤消其他用户对自己文件的访问权。为了保证在系统中实施多级安全，我们在模型中增加了两条带有强制性的控制策略，这两条策略分别对应于BLP模型的简单安全性与*-特性：策略（e）只有当用户的敏感级不低于文件的敏感级时，用户才可以阅读该文件或者执行该文件。策略（f）只有当文件P的敏感级不低于文件o的敏感级时，读过文件o的用户才能够写文件P。 为了在安全模型中体现安全策略的要求，需要给出安全策略的形式化描述，为此，首先从系统的需求分析者对策略的自然语言描述中抽象出一些概念，并把它们计算机术语化。表4-22反映了这种对应关系，但没有穷尽。表符号栏内的“tAs, o”表示t为矩阵项As, o中的某个访问权，SC表示安全类，是Security Class的缩写。 表4-22 安全策略中的术语对照 自然语言 模型术语 符号 某用户某主体s 用户集合主体集S 某文件某客体o 文件集合客体集O 用户敏感级 主体安全类 SC(s) 客体敏感级 客体安全类 SC(o) 阅读读访问R 写文件写访问W 访问权 访问权 tAs, o 有访问关系矩阵元素非空 As, of 主人 拥有者 ownerA(s, o) .根据对一些术语的抽象，上述策略可以略加形式化地表述为如下的模型的安全性质：性质（a）仅当某主体对某客体有访问关系，该主体才能按规定的访问权访问该客体。性质（b）仅当主体是系统管理员时才有权创建与删除主体和修改主体的安全属性与访问权限。性质（c）每个主体都有权创建与删除自己的客体，并可以赋予或修改自己客体的安全属性或访问权限。性质（d）仅当某主体是某客体的拥有者时，该主体才有权把对该客体的访问权转授其他主体或撤消其他主体对自己客体的访问权。性质（e）仅当某主体的安全类不低于某客体的安全类时，该主体才可以读该客体或执行该客体。性质（f）仅当客体P的安全类不低于客体o的安全类时，读过客体o的主体s才能够写客体P。 上述安全策略是根据对保护系统的总的访问控制原则，反映了对系统的总安全要求。是设计安全模型的总依据。1.2.2 实例模型的定义下面根据上一小节介绍的安全策略的要求定义系统的安全模型，其中包括定义状态变量、安全状态（包括初态）和状态之间的转换函数。1、定义模型的状态变量系统的状态由系统中所有的状态变量所决定，系统在某一时刻的状态由该时刻下所有状态变量的值决定的。系统的安全状态则是由系统中所有与安全有关的状态变量所决定的。这些状态变量的值发生了变化，安全状态也就随着发生了变化。为了使模型简洁，最重要的一点就是尽量减少模型所使用的安全状态变量的数量，与安全无关的变量尽量不列入模型中。模型中的状态变量需要结合系统的安全功能和安全策略的要求来确定。表4-23是模型中将要使用的与安全有关状态变量。 表4-23 模型中的状态变量 变量标识 类型含义 说明 S 集合 主体集 O 集合 客体集 s 变量 某主体 o 变量 某客体 As,o矩阵元素内含主体s对客体o的访问权AS,O是描述系统中访问控制关系的访问矩阵 SC(s)数组元素主体s的安全类SC(S)是存放所有主体安全类的数组 SC(o)数组元素客体o的安全类SC(O)是存放所有主体安全类的数组 owner变量文件的拥有者或称文件主 admin变量系统管理员Contents(o)字符串变量客体o的内容Lives变量当前活动主体该主体正在调用转移函数请注意，contents和live状态变量在上述几个性质中没有直接涉及到，它们是与安全相关的辅助状态变量，其作用后面将可以看到。模型（也就是系统）的安全状态由表中这些状态变量的集合组成，可以表示为： security_state=S, O, AS,O, SC(S), SC(O), contents(O), lives其中矩阵AS,O是最重要的状态变量，SC(s)与SC(o)可以认为它们分别是附着在矩阵AS,O中的一行与一列。由于主体也可能是受访问控制的对象，因此在矩阵的列中也包括所有主体。表4-24给出了本模型中访问矩阵的结构示意。安全类所在的行与列内容分别表示对应行和对应列上的主体的安全类SC(s)和客体的安全类SC(o)的值，我们把它称之为主体与客体的安全属性。表中矩阵元素中的内容的含义为：own表示拥有者，r表示读访问权，w表示写访问权，e表示执行权。当某矩阵元素为空时，表示该元素对应的主体与对应的客体之间无访问关系，如果该元素的内容中包括null（即使还可能包括其他访问权），则表示对应的主体与客体之间随有访问关系，但主体对客体没有访问权。 表4-24 本模型中访问矩阵的结构示意S1S6O1O20SC机密无密机密无密S1机密R/w/e /ownS2秘密rS3机密S4绝密r/e/ wS5秘密S6无密r /w 2、定义安全状态不变式安全状态不变式表明了系统对安全状态的要求，安全状态的定义就是根据上述6个安全策略的要求，把它们抽象为数学上的一个安全不变式。该安全不变式的含义表示，不论系统的安全状态如何转换，如果安全不变式的要求仍能得到满足，那么系统总是处于安全状态。安全不变式应该是简洁的，但却又应该是保证系统处于安全状态的最关键的和最低要求。在任何状态下保证客体的读写与执行的安全性是最关键的，也是最低要求，在上述6条性质中，前四条性质是一种约束性规定，它们对主体对客体的控制或访问操作做了限制；后两条性质是为了保持主体对客体访问操作中信息的安全，规定了主体与客体或客体之间的安全类要求，用以保证信息流按规定的方向流动。对于确定系统的安全状态而言，后两条性质是最关键的，它们表明了安全状态下，主体、客体安全类之间应该保持的关系。因此可给出如表4-25所示的安全不变式。其他策略中的安全性要求，可以在相应的状态转换函数中体现。 表4-25 模型的安全不变式 安全不变式系统是安全的，当且仅当对于所有的sS，oO有if r As, o or eAs, o then SC(s) SC(o),if r As, o and wAs, p then SC(p) SC(o).安全不变式的定义是直观地根据原始策略给出的，并不能表明我们对原始策略的理解与表达是正确的。为了使人相信安全不变式与策略的要求是一一对应的，应尽量使策略的描述简洁。为了达到利用模型进行系统安全性证明的目的，使策略简洁化非常重要。在上述安全性质中，后面两条是核心条款，前两条定义了主体对客体或另一个主体是否有访问权（读、写）或权利的转授权。有了这两条，说明访问矩阵是非空的，在初态时已经为系统定义了访问关系，使得系统中只有具有访问关系的主体与客体或主体与主体之间才能实施访问。第二条不变式会引起系统中权利的转移，这是一个不安全因素，后面将给出约束条件。初态中如果访问矩阵为空，则使后面两条不变式中的操作无法执行，因而也不会破坏系统的安全性。一般而言，安全策略对系统的实用性并不附加任何限制。 3、定义状态转换函数在实际系统中，由于经常需要进行增加或删除用户或文件，修改用户的访问权限和文件的安全属性等操作，这些操作都会改变系统的安全状态。系统把这些操作功能作为系统服务提供给主体调用，调用的结果是改变系统中的安全变量（如访问矩阵）的内容。对应到模型上来，完成这些操作的任务由状态转换函数完成。主体通过调用这些转换函数使模型从一个安全状态转换到另一个安全状态。函数中的参数由主体描述，在状态发生变化之前，系统必须对参数进行有效性校验。表4-26是根据安全策略的要求定义的部分状态转换函数，这些函数在模型中都要都要使用到。 表4-26 状态转换函数函数名函数表示式 作用创建主体Creat_subject (s, sc)在访问矩阵中增加一行，代表具有某安全类sc的主体s；删除主体Delete_subject(s)从矩阵中删除主体s所在行所有内容；创建客体Creat_object (s, o, sc)主体s在访问矩阵中增加一列，代表具有某安全类sc的客体o ；删除客体Delete_object(o)从矩阵中删除客体o；设置访问权Enter t into As, o把s对o的访问权t加入到矩阵元素As, o中；修改客体安全类modify_SC (o, sc)把访问矩阵中客体o的安全类修改为指定的sc类。修改主体安全类modify_SC (s, sc)把访问矩阵中主体s的安全类修改为指定的sc类。转授权利confer t（s, si, o）主体s把对o的访问权t授予si。撤消权利Revoke t（s, si, o）主体s撤消si对o的访问权t写客体Write_object (o, date)把数据date写入客体o中读客体copy_object (from, to)把客体from的内容拷贝到客体to中附加数据Append_object (o, date)把数据date附加到客体o中表4-27中给出了Creat_subject (s, sc)、Creat_object (s, f, sc)、Enter t into As, o、confer t（s, s1, o）几个转换函数的稍微详细的描述，其他函数的描述读者可自己参照给出。 表4-27 状态转换函数的描述Function1 creat_subject (si, sc) : /* sc是某具体安全类，如机密类 ，下同*/ if lives=admin and siS and si O then creat subject si ； S=SUsi ；/* S,O分别表示新状态下的主体集与客体集，下同 */ O=O U si； SC(si) =sc； for all oO Asi, o=f；/* As,o表示新状态下的访问矩阵*/ endFunction2 creat_object(s,f,sc)： if fO and sS then creat object f； SC (f) =sc； O=O U f ；S=S； for all aS Aa, f =f； enter own into As, f ； enter read into As, f ； enter write into As, f ； enter excute into As, f /* 如果f是可执行文件的话 */ endfunction3 enter t into As, o：/* t表示某一具体访问权，如read,write,excute等*/if lives=admin or own in As, o then O=O；S=S； if SC(s) SC(o) then As, o= A s, o U t； for all (s,o) (s, o) As, o= A s, o；EndFunction4 confer t（s, si, o）： if own in As, o and t in As, o then enter t into Asi, o； end上述各状态转换函数的主要作用是完成对状态变量值的修改，进而使得模型（或系统）的状态从当前状态变换为新状态。需要强调的是这些函数都是原子型的，执行是不可中断的。如果状态需要发生变化，那么这种变化是在瞬间完成的，可以认为是不花费时间的。在多道程序系统中，要特别注意异步进程对状态转换的影响。在各个函数中只给出了相关状态的变化，凡是在函数中未涉及的状态的内容都将保持不变。从这一点来说，不能把这些函数完全看成为计算机程序，而应理解为描述系统状态转换前后状态变量之间的关系为好。对于函数creat_subject (si, sc)，其作用是创建一个新主体（用户）。函数中限定在不存在重名的主体与客体的情况下，只能由系统管理员admin创建，创建后设置该用户的安全类，并且不允许该用户访问任何客体。该主体所能访问的客体要么由自己创建新的客体，要么等别的主体转授对自己客体的访问权。对于函数creat_object(s,f,sc)，其作用是由主体s创建具有安全类sc的客体（文件）f。创建f后，把f的安全类设为sc，并不允许其他任何主体对f有访问权。但是对于创建者自己自动可以对f具有读、写、拥有、执行权（如果是可执行文件的话）。对于函数enter t into As, o，其作用是向主体s赋予对客体o的访问权t。函数限定只有admin或客体的拥有者才有权向矩阵元素As, o中添加访问权。本函数与上两个函数不同，不改变主体与客体的数量。对于函数confer t（s, si, o），其作用是主体s向si转授自己对客体o的访问权t。函数限定只有客体的拥有者且拥有者对o有t访问权的情况下，才允许权利t的转让。1.2.3 实例模型的安全性分析本应给出各个状态转换函数的安全性证明，但这种证明是比较冗繁的，并且需要一定的数学基础，同时也超出了本书的要求。安全性分析包括两方面，一是状态转换函数的正确性与安全性，二是初始状态的确定及其安全性。本小节将从“让人相信”的角度，用说明与解释的方式“证明”转换函数的安全性。只要状态转换函数的构造是简单的和易于理解的，那么通过解释与说明就更容易“让人相信”。另外，还要对定义的各种初始状态的安全性进行适当的分析。1、状态转换函数的安全性分析从数学角度讲，对于每个状态转换函数，如果要证明它是安全的，必须证明它满足以下定理：对于任意状态转换函数，当且仅当在满足安全不变式的某个安全状态下执行该函数以后，系统仍能在新安全状态下满足安全不变式的要求，该转换函数才是安全的。下面对上面给出的几个状态转换函数的安全性进行分析。在函数creat_object(s,f,sc)中，s是创建客体f的主体，该函数的作用是s为自己创建一个具有sc安全类的客体f。我们这里认为创建者就是文件的拥有者，并且可以对自己的文件拥有全部访问权（这也是实际系统中采用的方法）。函数中的“for all aS Aa, f =f”语句是为了防止同时对其他主体授予对文件f的任何访问权，这样处理的目的是确保该转换函数的安全性。因为在本函数执行后，其他转换函数执行之前，系统中虽然增加了一个客体，但除了文件的拥有者外，其他任何主体都不能对该文件进行任何访问，因此就不会发生访问权被偷窃或信息泄漏的问题。而且这样处理，可以使模型的安全性证明方法具有更大的灵活性，还可以使函数变得更加简洁。为了使其他主体能够访问新客体文件f，可以利用enter t into As, o状态转换函数为其他主体设置对f的任何访问权，只要能够满足安全不变式就行。为了防止低于f安全类的主体可以访问f的情况发生，所以函数中在把访问权t增加到As,o中之前设置了条件限制，要求必须满足SC(s) SC(o)。有了这一条限制后，就可以保证执行该状态转换函数后，系统仍能满足安全不变式的要求，即仍然能够保持系统在新状态下的安全性。状态转换函数creat_subject(si, sc)的作用是在系统中增加一个具有sc安全类的新主体si，并且限制只允许系统管理员admin才可以创建新的用户。为了保证该函数执行后不影响系统的安全性，对新主体不设置对任何客体的任何访问权。新主体对系统中客体的访问权，可以通过enter函数设置，该函数上面刚讨论过。enter函数的执行可以保持安全不变式的成立。状态转换函数confer t（s, si, o）的作用是主体s把对自己的客体o的访问权t转授给另一主体si。函数中的转授条件是own in As, o and SC(s) SC(si) and t in As, o，其含义为s必须是客体o的拥有者和si的安全级不低于s的安全级，并且s对o有访问权t。如果不设置SC(s) SC(si)的限制，就有可能将访问权授予低于o的安全级的主体对o进行访问，这将破坏安全不变式的要求。由于条件SC(s) SC(si)保证了接收访问权的主体si的安全类不低于s的安全类，因此，防止了信息的泄漏问题，保证系统处于安全状态。2、模型的初始状态及其安全性分析正确地定义模型的（也就是系统的）初始状态，确保其安全性，对于模型所有状态下的安全性都是非常关键的。因为在证明了转换函数的安全性之后，如果能够保证模型的初态是安全的，那么就可以保证在任何状态下执行状态转换函数后，模型仍是安全的。初始状态是模型中所有状态变量的初始值的集合，模型的初始安全状态则是由模型中与安全密切相关的状态变量所决定，在我们的模型中这些变量最主要的就是访问矩阵AS,O，此外还包括其他一些辅助安全变量如contents,lives等。在矩阵A中包括了所有的主体与客体、它们的安全属性、主体对客体的访问关系与访问权限等安全信息，对于contents和lives而言，在模型的初态中，由于还没有进行任何状态转换操作，所以它们的内容都是空的，因此，模型的初始状态主要由访问矩阵的初始状态决定。我们可以分析访问矩阵的三种初始状态下的安全性。（1）访问矩阵初始为空这种情况意味着主体集与客体集都为空，相互之间更不存在任何访问关系，因而模型中不存在泄漏信息的可能。很显然这种初始状态肯定是满足安全不变式的要求的。在这种初态下，第一个可执行的状态转换函数应该是创建主体(create_subject)，接着就可以执行创建目标的函数(create_object)了，然后其他函数也都可以开始执行了。一旦执行创建主体的函数后，模型的初态就转换到另一个状态。这种初态可以定义为： S= f ，O= f，SC(S) = f，SC(O) = f，AS，O= f这里AS，O= f 表示所有的矩阵项都为空，SC(S) = f，SC(O) = f表示所有的主体与所有的客体的安全类都是空的。（2）初始时访问矩阵中只含主体这种初态是符合实际情况的，因为新系统安装后，系统管理员往往是首先是在系统中注册用户。由于此时系统中不存在客体，矩阵中的访问关系（即矩阵元素内）是空的，因此系统也一定处于安全状态。这种初始状态可描述为： S f ，O=S， for all sS, oO， As，o= f（3）初始时只允许主体访问自己的客体这种初态也是比较符合实际情况的。系统管理员在把每个用户注册到系统内后，可以允许每个用户只创建自己的文件、设置它们的安全类和对它们的访问权限,不允许他们互相之间转授访问权。在初态下，各个主体只能访问各自的客体，不存在相互访问的问题，因而也就不存在信息泄漏问题，系统也就处于安全状态了。这种初态可以描述为： S f ，O f， For all sS，oO SC(s)=scs , SC(o)=sco As，o= f , when s is not owner of o; As，o= r,e,w, own , when s is owner of o其中SC(s)=scs , SC(o)=sco分别表示主体s与客体o的初始安全类。1.2.4 模型的安全约束条件前面所定义的系统安全的概念完全体现在所定义的安全不变式中，对于系统在任何时刻下的状态，可以根据安全不变式是否能够得到保持来判断系统在此状态下是否安全的，而不必要考虑在此状态的前一个或前一些状态是否是安全的。显然，这样定义安全的概念，是无法保证系统在状态发生连续转换的情况下的安全性。这就是说，一个安全不变式不能描述我们对模型（即系统）所要求的全部安全性质。因此，需要对安全定义进行扩充，使它不仅能够体现单个状态下安全性的要求，而且能够体现两个连续状态转换过程中状态变量之间也满足安全关系。在修正的模型中，为了描述状态转换的性质，对模型的安全定义增加了一些约束条件。为了保证模型状态转换的安全性，必须保证每个函数都满足约束条件的要求。约束条件与安全不变式之间的差别是，约束条件是对转换前后的两个相继状态间变量值之间必须满足的条件。可以这样说，安全不变式是在状态变量取值已经确定下来后，对该状态下变量之间的关系的限定，而约束条件则是系统从一个状态变换到另一个状态的过程中对两个相继状态中变量值间的限制要求。约束条件是从防止不安全的状态转换、限制主体执行某种操作和对信息的安全控制等方面考虑建立的。下面就从这三个方面介绍增加约束条件的方法。1、对不安全转换的约束在实际系统中，一般都允许用户修改文件的安全类。假设在模型中提供了以下定义的修改客体的安全类的函数modify_SC (o, sc)： function5 modify_SC (o, sc) SC(o)=sc；稍微注意分析，就可以发现这样定义的转换函数是很不安全的，因为它可以对客体的安全类进行任意的修改。假定一个秘密级的主体把某机密文件的安全类修改为秘密级的，那么该主体就有权阅读原本他无权阅读的文件。产生该问题的原因是，最初给出的全系统的安全策略中没有对如何修改安全类给出具体要求。因此需要在安全策略中增加性质(g)：性质(g)：任何客体的安全类不能降低。把这条性质可以表述为以下数学形式：约束（a）：for all oO SC(o) SC(o)该约束条件表明新状态下的客体o的安全类必须不低于前一状态下该客体的安全类。一个函数是安全的，它不仅要满足约束条件，还要满足安全不变式的要求。根据这个约束条件，修改安全类的函数可重写如下： function5 modify_SC (o, sc) if sc SC(o) and own in Alives, o SC(o)=sc；在修改后的函数中，只允许客体的拥有者才能够修改自己客体的安全类。由于有了条件sc SC(o)的限制，修改后的客体安全类不会低于修改前的安全类。因此，修改后的这个函数可以满足约束条件的要求。2、对主体的约束转换函数的操作的内容与对象不同，所涉及的对象与内容的敏感程度也不同，对它们的调用应该受到严格的限制。例如，遵照自主访问控制的原则，允许一个主体向另一个主体转授访问权。但是如果对此不加限制，系统中将会出现权利的转授不受限制的情况，这将严重影响系统的安全性。防止这种情况出现的方法是，对主体调用函数进行限制。在前面给出的性质(d)就是控制对访问权的转授的，根据这个性质可以给出以下约束： 约束（2）：for all oO if own not in Alives, o then for all sS，As,o= As,o在该约束中，条件own not in Alives, o表示当前正在调用函数的主体（lives）不是客体o的拥有者。如果该条件成立，该主体将不能修改矩阵中任何元素，保持新状态中的矩阵元素与原状态下的矩阵元素的内容相同（即As,o= As,o）。我们在前面定义的函数function4 confer t（s, si, o）可以满足这一限制条件，但该函数本身没有满足安全不变式的要求，因为在调用enter函数时没有限定si的安全类不能低于客体的安全类。好在在函数enter中有这样的控制条件，可以避免不符合安全要求的权利转授问题的发生。函数function3 enter t into As, o也满足该约束条件的限制。在设计约束条件时，要尽量使条件一般化，不要在约束条件中涉及到特殊操作的特殊要求，否则将使约束条件复杂化。更有可能因考虑了特殊要求而遗漏了对其他情况的限制，反而造成不能限制违反安全情况的发生。3、对信息访问的限制如果就单纯的访问矩阵-监控器模型而言，一般只控制是否允许主体去访问客体，如果通过访问控制机制的核查，那么主体对客体内容（信息）的修改则不受任何限制。由于安全模型的目的是把安全策略的主要思想形式化，主要是验证安全策略的正确性与可靠性，并不十分注重于实现的细节方面，因此，在信息系统设计的初期阶段，这种用模型描述系统的安全性质还是可以接受的。但我们这里给出的安全策略中的性质（e）和（f）中，实质上对信息流的控制提出了要求，在两个安全不变式中已经体现了对读与写信息流的控制。但这种控制仅仅表达了主体对客体可能的读写操作，但并没有考虑主体是否实际对客体进行了读写操作，模型中还缺少对实际读写操作的限制。下面这条性质（h）是对模型中的写操作进行控制。性质（h）：仅当某主体对某客体具有写访问权时，该主体才可以修改该客体的内容。对于模型的这条性质，可以用以下约束来描述：约束（3）：for all oO if w not in Alives, o then contents(o)=contents(o)根据这条约束，我们可以给出转换函数Write_object(o, date)的定义：function6 Write_ object (o, date) if oO and w in Alives, o and SC(lives) SC(o) then write data into contents(o)条件w in Alives, o限制了正在进行写操作的主体必须对客体o具有写访问权，否则就不允许对o进行写入；条件SC(lives) SC(o)表示正在执行写操作的主体的安全类必须不低于客体o的安全类，这是为了满足性质（f）的部分要求的。让我们重新考虑一下性质（f）。第二个安全不变式已经定义了在安全状态下，安全变量之间需要保持的安全关系。但该不变式中没有考虑主体是否实际把从客体o读出的数据写入到客体p，模型中还缺少对这种类型的读写操作的限制。下面是对这种从一个客体读数据，并同时把这些数据写入另一个客体的情况的约束条件：约束（4）：for all oO and pO and o,p is opened by lives if r in Alives, o and w in Alives, p and SC(o) SC(p) then contents(p)=contents(p)该约束条件中，正在对两个客体分别执行读与写操作的主体lives，如果对客体o没有读权，或者对客体p没有写权，或者客体o的安全级高于客体p的安全级，那么就不允许向p写入数据，即p的内容保持不变。该约束条件对于某个主体lives同时打开o与p两个文件的情况下，试图从其中一个文件读出，并同时写入另一个文件的操作可以发挥作用。但是如果一个用户把从一个文件o读出的数据先存入到某个缓冲区后关闭该文件，然后再打开另一个文件p，并把缓冲区中的内容写入到p中，那么对于这种情况，该约束条件是不起作用的。因此，还没有一种一般性的方法，它能够给出一种约束，防止对客体内容进行非法的读并将读出的内容非法转移到其他客体的情况的发生。如果在系统实现时特别加以注意（如做一些相关记录），是可以发现一个主体同时打开多个文件，并对它们进行关联操作，例如从其中一个文件读出，而向另一个文件写入的情况。以上情况说明该约束条件的使用还是有漏洞存在的，因为知道这种奥妙的程序员可以在编程时故意避开本约束的约束。根据该约束条件，我们可以给出状态转换函数copy_object (from, to)的如下描述：function7 copy_object (from, to) if fromO and toO and from, to is opened by lives then if r in Alives, from and w in Alives, to and SC(from) SC(to) then contents(to)=contents(from)在该函数中，只有对客体from有读权和对客体to有写权的主体，并且客体from的安全级不高于客体to的安全级，才允许从from拷贝数据到客体to。由于约束（4）不能有效地约束非法的读然后转移的情况，即存在着安全的漏洞，使得系统难以处理许多非法的读的情况。如在实际系统中，除文件外，还有其他客体，如缓冲池、全局计数器等是可以由所有主体修改的。如何区分对这些客体的读访问是合法的读还是违法安全要求的是非常困难的，需要对可能发生这种情况的所有函数进行逐一分析。系统中也需要进行一些读写关联的历史记录，判断是否存在非法的读与写的操作。2 安全模型的应用模型是一种描述系统中研究者所关心的主要特性或行为的形式化表示方法，信息安全模型则是描述信息系统中信息安全特性的形式化方法。本节将要介绍信息安全模型的特点与应用。2.1 安全模型的特点与用途 一、安全模型的特点设计一个安全信息系统需要对该系统所要采用的安全机制有一个清晰全面的理解与描述。虽然用自然语言的方式在很多情况下可以把安全需求说清楚，但仍可能造成用户、设计者与实现者之间在理解上的不一致的问题。安全模型的目的就是为了精确描述信息系统的安全需要，为此，安全模型需要具备以下特点：它是精确的和无二义性的。它是简单的、抽象的和易于理解的。它仅涉及系统的安全性质，不过分限制系统的功能及其实现。它能够清晰表达系统的安全策略。为了使安全模型简单，在建立模型的时候，可以仅考虑对系统的安全需求，不必考虑系统的功能需求。应该避免使模型包含许多与安全无关的系统功能，是建立安全模型的原则之一。应该注意，不要一味追求模型的简单性而忽视必要的安全细节，否则将会使结果模型达不到预期的作用。一个好的模型应该是易于理解的，既可以用自然语言描述，也可以用形式化语言描述，对模型的描述只需要几页纸或很短的时间就可以表达清楚。完全的数学描述虽然严密但往往使人难于理解，完全的自然语言描述又会使人很难相信模型的精确性。因此，在对模型进行描述的时候应该适当的折中，在能够用数学语言简洁描述的地方就应该尽量采用形式描述，尤其涉及对安全策略的表达上；如果有的安全要求用自然语言就能很精确的表达出来，就可以用自然语言或半形式化语言去过渡，不要一味追求完全的数学描述。这种描述策略可以说是“以数学描述为主，用自然语言过渡”。安全模型的最基本作用是表达信息系统的安全策略，如果模型与所要求的安全策略之间没有明显的对应关系，或者模型的描述含糊不清，就很难使人相信模型体现了安全策略的要求。由于目前还无法从数学上证明用自然语言描述的安全策略与抽象的安全模型之间的一一对应关系，所以如果能够通过符合常理的解释或推断让人相信就很好了。因此，设计良好模型的关键是让模型与策略之间有着清晰的对应关系。为了满足数学的完备性，模型有时还需要附加一些与安全策略不完全对应的性质，例如它总是要包括一些约束条件、和在用自然语言描述的原始策略中没有明确提出来的附加性质。 二、安全模型的用途信息系统的开发（如操作系统、应用系统等）可以分为规范开发与非规范开发两大类，其中非规范开发是指不需要借助安全模型和形式化验证技术去开发信息系统的过程，而规范开发则是以安全模型为基础，对系统的安全需求尽可能地进行形式化描述，再对形式描述进行论证、证明或实验，在确保系统的安全设计没有漏洞之后，然后按照安全模型的要求去实现信息系统的安全功能。很显然，非规范的开发方式很难保证系统没有安全漏洞，而采用安全模型则可以从理论上证明系统是否存在安全缺陷。安全模型可以帮助系统的设计者尽可能精确地描述系统的安全功能，堵住所有的安全漏洞。安全模型必须在不限制系统功能的条件下，满足安全需求。由于使用安全模型的手段要求必须证明或能使人信服地说明，该安全模型能够在满足安全策略的情况下获得相应的安全性质。如果在系统的实现过程中，能够完全遵照安全模型的描述进行实现，那么基于这种安全模型而实现的系统将不会有安全漏洞。从形式模型到系统安全功能的实现之间还存在很大跨度，需要通过形式描述把安全模型的功能细化。对安全模型的形式描述可粗可细。如果粗一点（体现为中高层与顶层形式描述），形式描述与实现之间的跨度仍然很大，需要辅助以非形式的说明进行补充。如果细一点（体现为中底层形式描述），则会使形式描述过于冗繁而难以验证。为了减少模型与实现之间的跨度，可以采用多级形式描述的办法解决。通过采用逐级加细的形式化描述的方法，可以有效地减少模型与实现之间的间隙。即使如此，目前为止的形式验证技术还不能完全消除在最底描述层与实现层之间仍需要非形式的解释或论证。这就可能产生系统的实现与安全模型之间的不一致问题，进而形成系统的安全漏洞。对于已有的信息系统，虽然也可以利用安全模型对其安全功能进行描述与分析，但是由于旧系统大多数都是非规范方法开发的，其安全机制分散在系统的各个模块中，很难进行安全改造。或者说，把不安全的旧系统改造成安全的新系统几乎是不可能的。所以费很大力气为旧系统建立安全模型的意义不是很大。当然，如果一个信息系统需要通过较高安全级别的认证，利用安全模型对其安全性进行理论分析还是十分必要的。 2.2 模型的类型从安全控制的观点，安全模型可以划分为访问控制、信息流控制以及混合控制三大类；从处理信息的多安全级的能力来讲，安全模型可以划分为单级与多级两大类。从状态机概念而言可以分为状态机模型和非状态机模型。第一种分类是从原理上，因而也就是从本质上对安全模型进行了合理分类；而多级与单级安全模型类型则是从模型的处理能力上进行分类，并没有引入新的模型类型，即使是访问监控器模型也可以用于支持多级安全；至于状态机模型的概念具有普遍性分类意义，因为任何一个系统的执行过程都可以看成为状态变化过程，而操作命令则是导致状态变化的动力，因而它们被称为状态转换函数。访问控制模型与信息流模型都可以用状态机与状态转换的概念进行解释。非状态机模型并不流行，这里不想涉及。下面仅按第一类分类法对各种模型作一些简单介绍。 1、访问控制类模型访问控制类模型主要是4.1节中介绍的访问矩阵模型，由于访问矩阵模型经常需要和访问监控器联用，因此有时也把它们成为访问矩阵-监控器模型。在访问矩阵模型中，访问矩阵本身是模型的核心数据结构，它的行表示系统的各个主体，它的列表示各个客体，由于主体有时也是受控制的对象（如父进程对子进程的控制、一个主体向另一个主体的转授访问权等），所以主体也作为客体之一。矩阵的体积是可伸缩的，它随系统中主体与客体的数量的增加而增大，随主、客体数量的减少而减小。访问矩阵表达了系统中存在的访问关系和允许的访问权限，矩阵某时刻下的内容代表了该时刻系统的安全状态。该模型可以很好地描述自主访问控制机制的规则，主、客体的安全属性、主体对客体的访问权限等信息都可以被修改，修改操作是直接对矩阵进行的，对矩阵内容的任何修改都导致系统安全状态的变化。监控器则是依据访问矩阵实施对主体访问客体的访问控制的，凡是矩阵中存在的访问关系的，而且又具备所请求的访问权，那么就允许一个主体对另一个客体的访问请求，否则就不允许。对矩阵的修改操作也是在监控器的监控下完成的。这种模型的最大优点是它的直观性以及与实际系统的直接对应关系。许多实际系统都是以矩阵模型为基础实现的，只不过对矩阵的实现方法有所不同。为了减少矩阵体积，有的采用按行存储矩阵，有的采用按列存储方式实现矩阵。访问矩阵有广泛的应用，尤其是对保护系统安全性的理论研究。例如，著名的获取-授予（take-grant）模型（简称TG模型）也是基于访问矩阵的，利用该模型可以从理论上解决权利的转授是否会引起敏感信息的泄漏问题。 2、信息流控制类模型访问矩阵模型的最大缺点是，访问监控器只根据访问矩阵决定是否允许用户对它的文件（客体）进行访问，一旦允许访问，至于用户如何对其客体进行操作，则不在进行监控。例如，用户是否向一个低安全级的文件写入了高安全级的信息，在访问矩阵模型中对此是不加控制的。另外，访问控制模型无法控制间接泄漏的信息流，这一点在4.2节的开头部分已经做了说明。而所有这些问题可以在信息流控制模型中可以得到较好地解决。信息流控制模型是根据信息流控制策略建立起来的，主要用于描述客体能够存储的信息的安全类和客体安全类