课件7：第3-4节构建安全模型

13.4安全模型的构建本节将以构建一个基于访问矩阵-监控器的安全模型为例，说明安全模型的构建方法与步骤。访问矩阵-监控器安全模型是一种基于状态机的模型，有着广泛的应用，因此，所介绍的模型构建方法与思路对其他类型的安全模型也适用。23.4.1建模的方法步骤•下面要建立的安全模型是由访问矩阵与访问监控器组成的，访问矩阵反映了系统的安全状态。•保护系统可以抽象地用几个要素及其相互关系来描述：系统中包括主体集合与客体集合，主体包括用户或完成用户任务的进程，客体是指系统中所有可以被访问的对象。3•为了建立一个简洁的体现上述概念的安全模型，在安全模型中要尽量减少，甚至不包括那些与安全无关的功能与状态或其他因素。•模型中包括：安全状态变量（访问矩阵）和状态转换函数。4建立模型的步骤•（1）确定系统的安全策略，及其形式描述。•（2）定义系统的安全状态，确定访问矩阵•其他辅助安全变量，•指定变量初始值，定义初始状态。5•（3）定义安全状态不变式，它表明在安全状态中，状态变量值之间必须保持的关系；•（4）定义状态转换函数（或称操作命令），它描述了安全状态变量的值发生变化而引起的系统安全状态的变化。6•（5）证明转换函数能够维持系统安全状态，即证明转换函数在执行前与执行后系统都处于安全状态。•为了确保维持系统的安全状态，常常需要对转换函数增加约束条件。•（6）证明初始状态是安全的。7•如果能够证明该初始状态是安全的，然后证明所有的状态转换函数能够保持系统的安全状态，那么根据数学推理就可以保证，无论按什么顺序调用系统功能，系统将总是能够保持安全状态的。83.4.2.1安全策略的描述•策略（a）只有当某用户对某文件有访问关系时，该用户才能按规定的访问权对该文件进行访问；•策略（b）只有系统管理员才能够创建与删除用户和修改它们的安全属性与访问权限；9•策略（c）每个用户都有权创建与删除自己的文件，并可以赋予或修改它们的安全属性或访问权限。•策略（d）只有当某用户是某文件的主人时，该用户才有权把对该文件的访问权转授其他用户或撤消其他用户对自己文件的访问权。10•为了保证在系统中实施多级安全，我们在模型中增加了两条带有强制性的控制策略，这两条策略分别对应于BLP模型的简单安全性与*-特性：•策略（e）只有当用户的敏感级不低于文件的敏感级时，用户才可以阅读该文件或者执行该文件。•策略（f）只有当文件P的敏感级不低于文件o的敏感级时，读过文件o的用户才能够写文件P。11•为了在安全模型中体现安全策略的要求，需要给出安全策略的形式化描述，为此，首先从系统的需求分析者对策略的自然语言描述中抽象出一些概念，并把它们计算机术语化。表4-22反映了这种对应关系，但没有穷尽。•表符号栏内的“tA[s,o]”表示t为矩阵项A[s,o]中的某个访问权，SC表示安全类，是SecurityClass的缩写。12),...,(1kXXCkxx,...,1nopop,...,1nm,...,1),...,(1kXXCkxx,...,1nopop,...,1nm,...,1AOSQQQQm,,,...,,110AOSQm,,***2211mmQopopQopQ*iopiopAOSQQQQm,,,...,,110表3-7安全策略中的术语对照自然语言模型术语符号某用户某主体s用户集合主体集S某文件某客体o文件集合客体集O用户敏感级主体安全类SC(s)客体敏感级客体安全类SC(o)阅读读访问R写文件写访问W访问权访问权tA[s,o]有访问关系矩阵元素非空A[s,o]主人拥有者ownerA(s,o)……………….13•性质（a）仅当某主体对某客体有访问关系，该主体才能按规定的访问权访问该客体。•性质（b）仅当主体是系统管理员时才有权创建与删除主体和修改主体的安全属性与访问权限。•性质（c）每个主体都有权创建与删除自己的客体，并可以赋予或修改自己客体的安全属性或访问权限。14•性质（d）仅当某主体是某客体的拥有者时，该主体才有权把对该客体的访问权转授其他主体或撤消其他主体对自己客体的访问权。•性质（e）仅当某主体的安全类不低于某客体的安全类时，该主体才可以读该客体或执行该客体。•性质（f）仅当客体P的安全类不低于客体o的安全类时，读过客体o的主体s才能够写客体P。153.4.2.2实例模型的定义•下面根据上一小节介绍的安全策略的要求定义系统的安全模型，其中包括定义状态变量、安全状态（包括初态）和状态之间的转换函数。161、定义模型的状态变量•系统的状态由系统中所有的状态变量所决定，系统在某一时刻的状态由该时刻下所有状态变量的值决定的。•系统的安全状态则是由系统中所有与安全有关的状态变量所决定的。这些状态变量的值发生了变化，安全状态也就随着发生了变化。•为了使模型简洁，最重要的一点就是尽量减少模型所使用的安全状态变量的数量，与安全无关的变量尽量不列入模型中。17表3-8模型中的状态变量变量标识类型含义说明S集合主体集O集合客体集s变量某主体o变量某客体A[s,o]矩阵元素内含主体s对客体o的访问权A[S,O]是描述系统中访问控制关系的访问矩阵SC(s)数组元素主体s的安全类SC(S)是存放所有主体安全类的数组SC(o)数组元素客体o的安全类SC(O)是存放所有主体安全类的数组owner变量文件的拥有者或称文件主admin变量系统管理员Contents(o)字符串变量客体o的内容Lives变量当前活动主体该主体正在调用转移函数18•模型（也就是系统）的安全状态由表中这些状态变量的集合组成，可以表示为：•security_state={S,O,A[S,O],SC(s),SC(o),contents(o),live}•其中矩阵A[S,O]是最重要的状态变量，SC(s)与SC(o)可以认为它们分别是附着在矩阵A[S,O]中的一行与一列。由于主体也可能是受访问控制的对象，因此在矩阵的列中也包括所有主体。•contents和live状态变量是与安全相关的辅助状态变量19表3-9本模型中访问矩阵的结构示意S1…S6O1…O20SC机密无密机密无密S1机密R/w/e/ownS2秘密rS3机密S4绝密r/e/wS5秘密S6无密r/w202、定义安全状态不变式•安全状态不变式表明了系统对安全状态的要求，•其含义表示，不论系统的安全状态如何转换，如果安全不变式的要求仍能得到满足，那么系统总是处于安全状态。•安全不变式应该是简洁的，但却又应该是保证系统处于安全状态的最关键的和最低要求。•在任何状态下保证客体的读写与执行的安全性是最关键的，也是最低要求21表3-10模型的安全不变式后两条性质是最关键的，它们表明了安全状态下，主体、客体安全类之间应该保持的关系。系统是安全的，当且仅当对于所有的sS，oO有ifrA[s,o]oreA[s,o]thenSC(s)SC(o),ifrA[s,o]andwA[s,p]thenSC(p)SC(o).223、定义状态转换函数•作用：修改系统中的安全变量（如访问矩阵）的内容。由状态转换函数完成。•主体通过调用这些转换函数使模型从一个安全状态转换到另一个安全状态。•表4-26是根据安全策略的要求定义的部分状态转换函数;23表3-11状态转换函数函数名函数表示式作用创建主体Creat_subject(s,sc)在访问矩阵中增加一行，代表具有某安全类sc的主体s；删除主体Delete_subject(s)从矩阵中删除主体s所在行所有内容；创建客体Creat_object(s,o,sc)主体s在访问矩阵中增加一列，代表具有某安全类sc的客体o；删除客体Delete_object(o)从矩阵中删除客体o；设置访问权EntertintoA[s,o]把s对o的访问权t加入到矩阵元素A[s,o]中；修改客体安全类modify_SC(o,sc)把访问矩阵中客体o的安全类修改为指定的sc类。修改主体安全类modify_SC(s,sc)把访问矩阵中主体s的安全类修改为指定的sc类。转授权利confert（s,si,o）主体s把对o的访问权t授予si。撤消权利Revoket（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中24表3-12状态转换函数的描述•Function1create_subject(si,sc):/*sc是某具体安全类，如机密类，下同*/•iflives=’admin’andsiSandsiO•thencreatesubjectsi；•S’=SU{si}；/*S’,O’分别表示新状态下的主体集与客体集，下同*/•O’=OU{si}；•SC(si)=sc；•foralloO’A’[si,o]=；/*A’[s,o]表示新状态下的访问矩阵*/•end25•Function2create_object(s,f,sc)：•iffOandsS•thencreateobjectf；•SC(f)=sc；•O’=OU{f}；S’=S；•forallaS’A’[a,f]=；•enter‘own’intoA’[s,f]；•enter‘read’intoA’[s,f]；•enter‘write’intoA’[s,f]；•enter‘execute’intoA’[s,f]/*如果f是可执行文件的话*/•end26•function3entertintoA[s,o]：/*t表示某一具体访问权，如read,write,execute等*/•iflives=’admin’or‘own’inA[s,o]•thenO’=O；S’=S；•ifSC(s)SC(o)then•A’[s,o]=A[s,o]U{t}；•forall(s’,o’)(s,o)A’[S’,O’]=A[S,O]；•End•Function4confert（s,si,o）：•if‘own’inA[s,o]andtinA[s,o]•thenentertintoA[si,o]；•end27•上述各状态转换函数的主要作用是完成对状态变量值的修改，进而使得模型（或系统）的状态从当前状态变换为新状态。•需要强调的是这些函数都是原子型的，执行是不可中断的。如果状态需要发生变化，那么这种变化是在瞬间完成的，可以认为是不花费时间的。283.4.2.3实例模型的安全性分析•安全性分析包括两方面：•一是状态转换函数的正确性与安全性，•二是初始状态的确定及其安全性。•本小节将从“让人相信”的角度，用说明与解释的方式“证明”转换函数的安全性。291、状态转换函数的安全性分析•从数学角度讲，对于每个状态转换函数，如果要证明它是安全的，必须证明它满足以下定理：•对于任意状态转换函数，当且仅当在满足安全不变式的某个安全状态下执行该函数以后，系统仍能在新安全状态下满足安全不变式的要求，该转换函数才是安全的。30•在函数create_object(s,f,sc)中，s是创建客体f的主体，该函数的作用是s为自己创建一个具有sc安全类的客体f。•这里认为创建者就是文件的拥有者，并且可以对自己的文件拥有全部访问权（这也是实际系统中采用的方法）。•函数中的“forallaS’A’[a,f]=”语句是为了防止同时对其他主体授予对文件f的任何访问权，这样处理的目的是确保该转换函数的安全性。31•可以利用entertintoA[s,o]状态转换函数为其他主体设置对f的任何访问权，只要能够满足安全不变式就行。•为了防止低于f安全类的主体可以访问f的情况发生，所以函数中在把访问权t增加到A[s,o]中之前设置了条件限制，要求必须满足SC(s)SC(o)。32•状态转换函数create_subject(si,sc)的作用是在系统中增加一个具有sc安全类的新主体si