（计算机应用技术专业论文）基于有限状态自动机的动态信息流监控研究与分析.pdf

江苏大学硕士学位论文 摘要 随着国家、社会对计算机和网络技术的依赖程度日益增长，信息安全问题越 来越重要。访问控制机制是保护信息机密性、完整性的重要手段，但即使实施了 强制访问控制机制的信息系统中仍然会发生高安全级信息向低安全级用户泄漏 的隐通道问题，对于这类问题主要通过信息流控制来解决。 动态信息流控制技术处于起步阶段，它解决了静态信息流监控技术不能根据 实时的情况进行相应的改变，手工工作量巨大，容易误判不安全信息流通道和不 能灵活面对各种系统的问题。然而，现有的动态信息流监控技术还不能监控到复 杂的不安全信息流的通道。 针对上述问题，本文主要研究的内容包括： ( 1 ) 在分析动态信息流监控技术和有限状态自动机监控技术的基础上，为解决 现有的动态信息流监控技术不能监控因系统状态变化引起的隐通道的问题，本文 根据动态分析的需求对有限状态自动机做出改善，使得有限状态自动机获得了较 好的适应性，并以改善后的有限状态自动机为工具提出了一种对信息流的动态监 控方法。该方法在保持原有动态信息流监控技术的优点的基础上，能够实现对此 类隐通道流进行监控，并能根据被监控系统的安全要求，对隐通道进行妥善的处 理。 ( 2 ) 通过详细介绍将该方法运用到s e l i n u x 系统的各步骤，提供具体实施本监 控方法的过程。这一运用结果也为仿真验证本方法有效性而提供一个实际系统的 环境。 ( 3 _ ) 在实际系统中检验本论文所提出的方法。在含有已知不安全信息流的仿真 环境中，用本文所改进的方法对实际系统进行监控，通过实验结果以验证该方法 的正确性和有效性。 本文所提出的一种基于有限状态自动机的动态信息流方法可以有效的阻止 不安全信息流对系统的危害，并能够根据不安全信息流的危害程度对其进行相应 的处理。 关键词：信息流，动态监控，有限状态自动机，s e l i n u x 江苏大学硕士学位论文 a b s t r a c t n o w a d a y s ，d u et oo u rc o u n t r ya n ds o c i e t yw i d e s p r e a dd e p e n d e n c eo nc o m p u t e r a n dn e t w o r kt e c h n o l o g y , i n f o r m a t i o ns e c u r i t yi sm o r ea n dm o r ev a l u e d s m n d f d s e c u r i t ym e c h a n i s m ss u c ha sa c c e s sc o n t r o l f i ee s s e n t i a lc o m p o n e n t sf o rp r o t e c t i n g t h ec o n f i d e n t i a l i t ya n di n t e g r i t yo fd a t a b u te v e ni nas e c u r es y s t e mw h i c hh a sb e e n i m p l e m e n t e dm a n d a t o r ya c c e s sc o n t r o lm e c h a n i s m ，ah i g h - l e v e lp r o c e s sc a ns i g n a l i n f o r m a t i o nt oal o w l e v e lp r o c e s sb yu s i n gc o v e r tc h a n n e l i n f o r m a t i o nf l o wc o n t r o l c a np r o v i d es u c hg u a r a n t e e s a l t h o u g ha tt h ei n i t i a ls t a g e ，d y n a m i ci n f o r m a t i o nf l o wc o n t r o ls o l v e st h es t a t i c i n f o r m a t i o nt h ep r o b l e m st h a tf l o wc o n t r o lt e c h n o l o g yc a n n o tb ec o n d u c t e da c c o r d i n g t ot h ec o r r e s p o n d i n gr e a l t i m ec h a n g e si nt h ew o r k l o a do fah u g em a n u a l ，e a s yt o m i s j u d g et h es a f ec h a n n e l so fi n f o r m a t i o nf l o wa n dc a n n o tb ef l e x i b l et of a c et h e p r o b l e m so fv a r i o u ss y s t e m s h o w e v e r , t h ee x i s t i n gd y n a m i ci n f o r m a t i o nf l o wc o n t r o l t e c h n o l o g yc a n n o tc o n t r o lt h ei n f o r m a t i o nf l o wi nt h ec o v e rc h a n n e l s o nt h e s e i s s u e s ，t h i sa r t i c l ec o v e r s ：b a s e do nt h ea n a l y s i s o fd y n a m i c i n f o r m a t i o nf l o wc o n t r o lt e c h n o l o g ya n df i n i t es t a t em a c h i n e ，i no r d e rt os o l v et h e p r o b l e mt h a td y n a m i ci n f o r m a t i o nf l o wc o n t r o lt e c h n o l o g yc a n n o tc o n t r o lt h e i n f o r m a t i o nf l o wi nt h ec o v e rc h a n n e l s a c c o r d i n gt ot h ed y n a m i ci n f o r m a t i o nf l o w c o n t r o l sn e e d s ，i m p r o v e m e n t sa r em a d et om a k ef i n i t es t a t em a c h i n eab e t t e r a d a p t a t i o n a sat o o l ，t h i sa r t i c l ep r e s e n t sam e t h o dt ow a t c ht h ei n f o r m a t i o nf l o wi n t h ec o v e rc h a n n e l ( 1 ) n em e t h o dw h i c hm a i n t a i n st h ea d v a n t a g e so fd y n a m i ci n f o r m a t i o nf l o wc a n w a t c ht h ei n f o r m a t i o nf l o wi nt h ec o v e rc h a n n e la n dh a n d l e sp r o p e r l yt h eu n s a f e c h a n n e lb a s e do nt h es y s t e ms e c u r i t yr e q u i r e m e n t s ( 2 ) u s i n gt h em e t h o ds t e pb ys t e po nt h es e l i n u xs y s t e mp r o v i d eaw a yt o i m p l e m e n tt h em e t h o d ，t h i ss i m u l a t i o nr e s u l tc a nt h ee f f e c t i v e n e s so ft h i sm e t h o dt o p r o v i d ear e a ls y s t e me n v i r o n m e n t ( 3 ) t e s t i n gt h em e t h o dp r o p o s e di nt h ea r t i c l ei nt h er e a ls y s t e m i nt h es y s t e m w h i c hh a sc o v e rc h a n n e l s ，b yu s i n gt h em e t h o dt ow a t c ht h ei n f o r m a t i o nf l o w , t h e e x p e r i m e n tr e s u l tc a ns h o wt h ec o r r e c t n e s sa n de f f e c t i v e n e s s t h i sa r t i c l ep r o p o s e daf i n i t es t a t em a c h i n eb a s e do nd y n a m i ci n f o r m a t i o nf l o w m e t h o dw h i c hc a ne f f e c t i v e l yp r e v e n tt h eu n s a f ei n f o r m a t i o nf l o wa n dh a n d l e p r o p e r l yt h ec o v e rc h a n n e l k e y w o r d s ：i n f o r m a t i o nf l o w , d y n a m i cc o n t r o l ，6 i t es t a t em a c h i n e ，s e l i n u x 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定， 同意学校保留并向国家有关部门或机构送交论文的复印件和电子版， 允许论文被查阅和借阅。本人授权江苏大学可以将本学位论文的全部 内容或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫 描等复制手段保存和汇编本学位论文。 本学位论文属于 保密口，在年解密后适用本授权书。 不保密西 学位论文作者签名：阄墅 蜥6 月1 e l弁 签7 币 可 师 月 教 导 三 雒 年 于 。似 独创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独 立进行研究工作所取得的成果。除文中已经注明引用的内容以外，本 论文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本 文的研究做出重要贡献的个人和集体，均已在文中以明确方式标明。 本人完全意识到本声明的法律结果由本人承担。 黟目 p 臼 辄q 姑 月 作 年姗辑 位 乳 剿 醐 江苏大学硕士学位论文 1 1 研究背景 第一章绪论 很多信息系统( 如操作系统、数据库系统等) 都有保密性的安全要求。系统的 保密性在很大程度上直接决定了系统的安全性，发现和阻止机密信息( 或其它重 要信息) 的扩散是信息安全研究和实践经常遇到的问题n 1 。 访问控制是系统中使用最为广泛的安全机制。它控制系统中的主体( 如用户、 进程等) 对系统中的客体( 如文件) 的访问( 读、写、执行、删除、追加等访问方式 的组合) ，一般涉及自主访问控制( d i s c r e t i o n a r y a c c e s s c o n t r o l ，d a c ) t 2 】和强制访 问控$ 1 j ( m a n d a t o r y a c c e s s c o n t r o l ，m a c ) t 3 1 。美国国防部已经把d a c 和m a c 作 为标准写入了“可信计算机系统评估准则 ( t r u s t e dc o m p u t e rs y s t e me v a l u a t i o n c f i m f i a ，t c s e c ) 嗍。 在自主访问控制机制下，客体的拥有者可以按照自己的意愿精确指定系统中 的其它主体对其文件的访问权限。使用访问控制矩阵表示主体和客体之间的关 系，矩阵的每一行表示一个主体，每一列表示一个受保护的客体，矩阵中的元素 表示主体对客体的访问权限。为了提高效率，控制矩阵在系统中采用稀疏矩阵、 访问控制表( a c c e s sc o n t r o ll i s t ，a c l ) 、能力表的数据形式存储。d a c 的控制是 自主的，在为用户提供很大灵活性的同时也缺少高等级安全要求的高安全性。因 此，在系统内进行自主访问控制的同时，还需要利用强制访问控制加强系统的安 全性。用户使用d a c 防止其他用户入侵自己的文件，而m a c 则使用户不能通 过意外事件或故意的误操作逃避安全控制。 使用强制访问控制可以防止特洛伊木马从系统内部引起的攻击。例如实施 b l p 模型的系统中，在机密安全级上运行的进程中的特洛伊木马试图把机密性信 息写入一个公开文件，系统的引用监视器可以立即检测出这个非法访问请求，因 为它违反了“上写下读 的访问控制规则。即使特洛伊木马能运行，它也无法取 走信息。 虽然强制访问控制可以阻止特洛伊木马直接泄露信息，但是不能够阻止它通 过系统的“副作用间接泄露机密信息。在强制访问控制机制中，一般只把用来 江苏大学硕士学位论文 存放信息的单元看作是客体，而文件锁、设备忙标志、时钟发生器等机制不会被 考虑。两个藏有特洛伊木马的进程可以通过这些系统机制绕过强制访问控制而肆 意地进行信息交流。这种允许进程可以危害系统安全策略的方式传输信息的通信 信道称为隐通道 4 ( c o v e r tc h a n n e l ) 。 1 2 国内外研究现状 从信息流的角度来看，系统中的信息流可分为两种信息流：安全的信息流和 不安全的信息流。安全的信息流的形成是由一个主体在符合安全规则要求的情况 下向另一个主体传递信息；反之，不安全信息流的形成是由一个主体在“违背” 安全规则要求的情况下向另一个主体传递信息。根据“违背 安全规则的方式不 同，不安全信息流又可以分为：直接的违背安全规则的明显不安全信息流，这种 信息流容易被监控，通过安全机制中访问控制技术就可以加以控制；间接的违背 安全规则的隐含的不安全信息流，这种不安全信息流难以控制，后者也称为隐通 道，目前关于隐通道的研究主要是通过信息流控制方法来解决： 静态信息流控制技术主要包括：静态信息流分析法【5 】，共享资源矩阵法【6 】， 无干扰分析法川，基于源代码搜索法【8 】等。这些方法可以在信息系统运行前，对 系统进行安全检测，但是各个方法存在不同程度的缺陷：静态信息流分析法容易 误判不安全信息流；共享资源矩阵法则不能证明单个t c b 原语是安全的，而且 增加新的t c b 功能时候会使得分析更复杂；无干扰分析法对于较大规模的t c b 来说，手工使用无干扰分析法不大可行；基于源代码搜索方法代码量巨大，涉及 的变量众多，程序流程复杂，即便在系统开发过程中遵循了良好的软件工程规范， 依然很难理解。 动态信息流控制技术处于起步阶段，主要技术包括：类型系统法【9 1 ，程序逻 辑法【1 0 】和有限自动机法【1 1 1 。动态信息流监控技术的出现解决了静态信息流监控 技术不能根据实时情况进行相应的改变，容易误判不安全信息流，手工工作量巨 大和难以理解的问题。动态信息流监控技术实现在线监控。终端用户可以自定义 安全类别，能随着每次信息系统执行而运行监控。因此终端用户可以根据自己的 需要去修改流策略，实现了以用户为中心的人性化思想。然而，动态信息流监控 技术主要是面对程序进程分析和监控而提出的，虽然l e 用自动机监视系统的信 2 江苏犬学硕士学位论文 息流去监控系统中信息流的流动【1 1 】【1 2 1 ，但至今动态信息流仍旧无法检测低密用 户通过感知系统状态改变而获得信息的隐通道。 1 3 论文的研究目的 信息流分析的技术已经成功地应用于计算机系统的安全分析，以及安全协议 的形式化分析中。由于计算机系统和安全协议所受到的攻击而导致的信息泄露都 可以看作是信息在不同用户、进程、主体之间的流动，因此信息流分析的方法是 信息安全分析中较为本质的一种方法。 信息流分析法分为静态分析和动态分析两种，由于静态分析只在编译阶段实 现，所以不能根据实时的情况进行相应的改变，而动态分析比静态分析更加以用 户为中心，实现在线监控。终端用户可以自定义安全类别，能随着每次信息系统 执行而运行监控。终端用户可以根据自己的需要去修改流策略。因此，动态分析 得到了更多的关注和发展。 在实际系统中，系统运行可以用状态转移形式进行描述，系统的当前操作可 以被描述为从一个状态转换到另一个状态。有限状态自动机作为能够较好的描述 状态转移的技术而被广为应用。 因此，本文利用有限状态自动机为工具改进了动态信息流监控的方法，不仅 能够实时动态的监控系统中的信息流，找出不安全的信息流，对其做出安全处理， 而且克服了原有动态信息流的缺点，从而使信息系统的机密性得到保证。 1 4 论文的组织结构 本文主要分为六章，其主要内容概要如下： 第一章绪论。该部分主要介绍了课题的研究背景和意义，指出了静态信息 流分析和动态信息流分析两种分析方法的主要研究工作和其中的不足之处，根据 其不足之处引出本文的研究目的，最后阐述了本文的主要工作和论文的组织结 构。 第二章信息流及其分析方法与技术。从明显的不安全信息流和隐含的不安 全信息流两个角度阐述了各自的主要研究工作，指出了现有的对不安全信息流监 控方法的不足之处。 3 江苏大学硕士学位论文 第三章有限状态自动机。本章介绍了现有的有限状态自动机的描述、分类、 定义和在监控系统信息流方面的应用。 第四章基于有限状态自动机的动态信息流分析方法。本章提出基于有限状 态自动机的动态信息流分析的方法，介绍了将系统形式化的方法和有限状态自动 机监控原理，并给出了实现该有限状态自动机监控机制的方法。 第五章基于有限状态自动机动态信息流分析法在s e l i n u x 中的应用。通过 详细介绍将该方法运用到s e l i n u x 系统的各步骤，提供具体实施本监控方法的过 程。这一运用结果也为仿真验证本方法有效性而提供一个实际系统的环境。 第六章仿真实验与分析。为了证明本文提出的基于有限状态自动机的动态 信息流分析法的有效性和可行性，本章设计了一个实验环境，在真实的系统环境 下模拟真实用户操作形成隐通道，利用第五章实现的有限状态自动机监控系统对 目标系统进行监控。用实验结果说明方法可行有效。 第七章总结和展望。总结全文工作，并对下一步工作进行展望。 4 江苏大学硕士学位论文 第二章信息流及其分析方法与技术 信息流监控中，不安全信息流的搜索定位一直是难点，怎样快捷、准确的寻 找到不安全信息流成了各国学者共同的课题。本章首先介绍信息流等基本概念， 然后分析现有的主要的不安全信息流搜索定位方法与技术。 2 1 信息流原理 “i n f o r m a t i o nf l o w ：t h el o g i co fd i s t r i b u t e ds y s t e m s 的作者j o nb a r w i s e 和 j e r r ys e l i g r n a n 写此书的目的是提取出理解信息流动最根本的东西，而不只是为 了通信。b a r w i s e s e l i g m a n 提出了两个问题：什么信息在系统中流动? 为什么它 会流动? 书中用“l o c a ll o g i c s ( 局部逻辑) ”表征第一个问题，而用“i n f o r m a t i o n c h a n n e l ( 信息通道) ”的观点回答第二个问题。一个系统的局部逻辑是支持信息在 系统内流动的规则的模型，而信息通道是支撑这种信息流动的连接系统的模型。 信息流理论又称通道理论( c h a n n e l t h e o r y ) ，以区别于s h a n n o n 的信息论。 书中介绍了信息流的4 个原理。 第一原理：信息流来自分布式系统中的规则。所谓“分布一是指系统用某种 方法分为若干部分，因而信息从一部分流向另一部分。由于系统中出现的规律性 以某种方式把系统各部分联系起来，因此允许了信息的流动。 第二原理：信息流的重要之处是同时包括了类型( t y p e ) 和个性( p a r t i c u l a r ) 。 对于信息理论，不能忽略个性或实例( i n s t a n c e ) ，因为个性携带了信息，它们 携带的信息是以类型的形式出现的。书中用t o k e n 表示携带信息的个性或实例， 是指被分类的东西；而类型是指用来分类的东西。 第三原理：分布式系统中某些组件的信息依靠连接之间的规则携带了其他组 件的信息。 分类及其相关的理论提供了一种方法对这些规则建模。用理论的约束和信息 射，可以获取信息流有关组件的基本原理。 第四原理：一个给定的分布式系统的规则与利用信息通道对其进行分析有 关。 5 江苏大学硕士学位论文 把系统分析成为一个通道取决于与语境有关的角度和标准。这样一个通道可 以由一个理论家明确描述出来或者可以隐含在该系统的用户的判断中。 以上4 个原理给出了信息流理论的框架。 2 2 明显的不安全信息流 明显的不安全信息流是由于违反了安全策略的规定进行传输信息而产生的 信息流。对于这些不安全信息流只需对其进行访问控制，发现此类信息流就采取 禁止传递的方法来防止不安全信息流。访问控制涉及自主访问控制( d i s c r e t i o n a r y a c c e s sc o n t r o l ，d a c ) 2 】和强制访问控制( m a n d a t o r y 觚e s sc o n t r o l ，m a c ) t 3 1 。 在自主访问控制机制下，客体的拥有者可以按照自己的意愿精确指定系统中 的其它主体对其文件的访问权限。使用访问控制矩阵表示主体和客体之间的关 系，矩阵的每一行表示一个主体，每一列表示一个受保护的客体，矩阵中的元素 表示主体对客体的访问权限。为了提高效率，控制矩阵在系统中采用稀疏矩阵、 访问控制表( a c c e s sc o n t r o ll i s t ，a c l ) 、能力表的数据形式存储。d a c 的控制是 自主的，在为用户提供很大灵活性的同时也缺少高等级安全要求的高安全性。因 此，在系统内进行自主访问控制的同时，还需要利用强制访问控制加强系统的安 全性。用户使用d a c 防止其他用户入侵自己的文件，而m a c 则使用户不能通 过意外事件或故意的误操作逃避安全控制。 在强制访问控制机制下，系统内的每个客体都赋予相应的安全属性，这些安 全属性并不是由客体的拥有者设置，而是由管理部门或系统自动地根据严格的规 则执行。同样，系统内的主体也被赋予一个安全属性以表示他对机密性客体的访 问许可级别。当一个主体访问客体时，系统内的“引用监视器”( r e f e r e n c em o n i t o r ) 通过比较主、客体相应的安全属性，从而确定是否允许主体对客体的访问。常见 的m a c 策略模型有保护机密性的b e l l l a p a d u l a 模型( 简称b l p 模型) 1 3 】【1 4 】和 保护完整性的b i b a 模型【1 5 】。前者规定当且仅当主体的机密性属性不低于客体的 机密性属性时才允许主体对客体拥有读权限，当且仅当主体的机密性属性不高于 客体的机密性属性时才允许主体对客体拥有写权限，即“不向下写，不向上读”； 后者正好相反，规定“不向上写，不向下读 ，即主体要想读客体，其完整性属 性不高于客体的完整性属性，主体要想写客体，其完整性属性不低于客体的完整 6 江苏大学硕士学位论文 性属性。 使用强制访问控制可以防止特洛伊木马从系统内部引起的攻击。例如实施 b l p 模型的系统中，在机密安全级上运行的进程中的特洛伊木马试图把机密性信 息写入一个公开文件，系统的引用监视器可以立即检测出这个非法访问请求，因 为它违反了“上写下读 的访问控制规则。即使特洛伊木马能运行，它也无法取 走信息。 虽然强制访问控制可以阻止特洛伊木马直接泄露信息，但是不能够阻止它通 过系统的“副作用 间接泄露机密信息。例如，假设一个目录d i r 与主体a 的 安全属性相同，当且仅当目录为空时a 才能删除d i r 。另一主体b 通过在目录 d i r 中删除文件使目录为空，或者创建文件使得目录非空。于是主体b 就可以 每次通过在目录d i r 中创建删除文件向主体a 发送一个比特的信息。 在强制访问控制机制中，一般只把用来存放信息的单元看作是客体，而文件 锁、设备忙标志、时钟发生器等机制不会被考虑。两个藏有特洛伊木马的进程可 以通过这些系统机制绕过强制访问控制而肆意地进行信息交流。这种允许进程可 以危害系统安全策略的方式传输信息的通信信道称为揪_ t 4 l ( c o v e r tc h a n n e l ) 。 2 3 隐含的不安全信息流 隐含的不安全信息流即隐通道。隐通道是指系统的一个用户通过违反系统安 全策略的方式传送信息给另一用户的机制。它往往通过系统原本不用于数据传送 的系统资源来传送信息，并且这种通信方式往往不被系统的存取控制机制所检测 和控制。1 9 9 0 年，t s a i g l i g o r 和c h a n d e r s e k a r a n t l 6 】针对安全模型中的多级强制存 取策略以及这些策略在各种实际状况中的解释，提出了隐通道的一般定义：给定 一个安全策略模型m 及其解释，似) ，似) 中的任何两个主体，佤) 和， ) 间的 潜在通信是隐蔽的，当且仅当m 的相应主体s 。和最的通信在m 中是非法的。 与信息安全研究领域的另一个热点信息隐藏不同，在隐通道研究里，安全规 则不允许两个主体互相通信，但它们采取了某种方法，绕开了存取控制机制的监 控，通过某些共享的资源，每次传递很少位的信息；而在信息隐藏研究里，通信 双方允许对话，只不过通话内容要经过审查，且限定在某个特定的主题上，其要 7 江苏大学硕士学位论文 点在于用某种看不出来的方式将非法数据加载在合法内容上，以逃避系统进行的 检查，一个典型的例子是将一副图片文件中每像素的低两位用于表示秘密数据。 隐通道可以用多种方式分类，可以基于其使用的机制、基于它们出现的抽象 级别、或发送者和接收者的本质。 传统上基于隐通道的实施机制将隐通道分为时间隐通道和存储隐通道。由一 个主体直接或间接地写某共享属性，另一主体直接或间接地读这一共享属性的 值，通过这一属性值的变化而传递信息构成的隐通道称为存储隐通道。一个主体 通过调整它自己对系统资源( 如c p u 时间) 的占用时间，而影响了另一个主体的 实际响应时间，从而发送信息给另一主体构成的隐通道称为时间隐通道。这里的 “时间 是一个相对概念，为构成时间隐通道所需时钟所必需的是接收方能观察 到事件发生的顺序，并且发送方能够改变这种顺序。 k e m m e r e r t l 7 】曾指出构成存储隐通道和时间隐通道所必须满足的最小条件。 存储隐通道须满足如下最小条件： 1 ) 发送和接收过程必须对共享资源的同一属性进行存取； 2 ) 必须存在某些方法，借之发送过程能够迫使共享属性改变； 3 ) 必须存在某些方法，借之接收过程能够感知这一改变； 4 ) 必须存在某些机制初始化发送和接收过程的通讯，且能正确地编排这些 事件。这可能是另一具有更小带宽的信道。 时间隐通道须满足如下最小条件： 1 ) 发送和接收过程必须对共享资源的同一属性进行存取； 2 ) 发送和接收过程必须对一个时间参照物进行存取，例如一个实时时钟； 3 ) 发送方必须能调整接收方的响应时间以探测共享属性的变化； 4 ) 必须存在某些机制初始化有序化这一过程。 在时间隐通道中隐含了发送方或接收方改变共享属性以实现隐通道的能力。 按这种分类方法，有时候同一隐通道机制既可以属于存储隐通道，也可以属 于时间隐通道。例如w r a y t l 8 】讨论过的磁臂隐通道，大多数情况下，一些存储资 源的值，例如磁臂位置寄存器，和一些临时行为相关，例如搜索时间。这样涉及 到磁臂操作的隐通道很明显既属于时间隐通道，也属于存储隐通道。 依据目前的认识，隐通道的工作原理是安全系统中具有较高安全级的主体 8 江苏大学硕士学位论文 s h ，使用事先约定好的编码方式，通过更改某个共享客体o i 的属性a j 并使具有 较低、或不可比安全级的主体s l 观察到这种变化，从而传送违反系统安全策略 的信息，见图2 1 存储隐通道中的共享客体是文件等非时间性资源【1 9 l 。 图2 1 隐通道的工作原理 需要指出的是，图2 1 中的实线箭头所标识的操作都是合法的，即能通过安 全模型的验证，但两次合法的操作却导致了一次非法的信息流动，如图2 1 中虚 线箭头所示。 2 4 隐通道的搜索法 2 4 1 隐通道静态搜索法 彻底搜索隐通道，即隐通道标识的工作是隐通道分析中最为困难的一环。其 困难性体现在理论和工程实践两个方面：( 1 ) 理论上仍然不够成熟，缺乏严谨且 行之有效的方法；( 2 ) 实际中工作量庞大，手工分析容易出错，缺乏行之有效的 自动工具。目前，主流的静态隐通道标识具有代表性的方法为：( 1 ) 语法信息流 法；( 2 供享资源矩阵法；( 3 ) 无干扰分析法。 2 4 1 1 语法信息流分析法 语法信息流分析法( i i 曲咖a t i o nf l o w a n a l y s i s ，i f a ) 由d e n n i n gd e 提出【5 1 ， 其特点是从每一条实现语句中导出信息流语义，从导出的语义中判断非法流。分 析从系统调用函数开始，找出信息流并检验是否违反信息流规则，直到函数中的 9 江苏大学硕士学位论文 每个表达式被分析过，并把每一对变量之间的信息流写作一个流语句；然后用信 息流规则加以检验，找出非法流，标记为隐通道。该方法假定每个变量或客体要 么显式、要么隐式地带有特定安全级标签或存取类。如果没有这种标签，就强行 指定安全级，这样做可能会导致伪非法流，因为有的变量不可能具有固定的安全 级【5 1 。该方法的优点是搜索彻底，不会漏过非法流。缺点是工作量极其巨大，特 别是由于强行指定安全级，导致大量伪非法流，需要用很多额外的工作来消除， 实际上该方法仅具有理论意义。 2 4 1 2 共享资源矩阵法 共享资源矩阵法( s h a r e dr e s o u r c em a t r i x ，s r m ) 由k e m m e r e rr a 提t bt 6 ， 该法曾成功用于几个项目( 如u n i x2 和d g u x ) 。其设计思想是系统中因存在共 享资源而产生隐通道，如果找出所有用于读写的系统资源和操作，经过分析就容 易找到隐通道。具体实现方法是建立一个表示系统资源与系统操作之间读写关系 的矩阵，行项是系统资源及其属性，列项是系统的操作原语。矩阵的每一项表示 给定操作原语是否读或写对应的系统资源，并分析该矩阵。该方法的优点是具有 广泛的适用性，不但可以用于代码分析，还可以用于规范分析甚至模型和机器代 码分析。缺点是构造共享资源矩阵工作量大，没有有效的构造工具，也不能证明 单独一个原语是否安全。 2 4 1 3 无干扰分析法 在f e i e r t a 9 2 0 11 2 1 】等人工作的基础上，g o g u e n 和m e s e g u e r l 2 2 】引入无干扰方法， 它的本质是一个用户不应当知道他不支配的其他用户的任何动作，他们将可信计 算基t c b 视为一个状态机，并定义了两个用户进程之间的无干扰概念。假设状 态机有一个初始状态，称一个用户进程与另一个用户进程是无干扰的，如果从初 始状态开始，删除第1 个进程所有的输入( 等价于从来没有这些输入) ，第2 个进 程的输入没有发生任何变化。可以证明，进程之间无干扰具有以下性质网：如 果一个进程的输入不能影响另一进程的输出，则不可能从第1 个进程向第2 个进 程传输信息。 在实际检验无干扰时，必须应用下面g o g u e n 和m e s e g u e l 【2 5 】给出的定理：进 江苏大学硕士学位论文 程x 与进程y 无干扰，当且仅当对于x 的任何输入，都使当前状态迁移到一个】，一 等价状态。 该方法的主要优点是：( 1 ) 可以同时应用于形式化顶层规范和源代码；( 2 ) 可以 避免标识伪非法流；( 3 ) 可以增量分析单个的t c b 函数和原语。 该方法的主要缺点是：( 1 ) n - - j 以基于形式化的t c b 顶级描述，也可以基于源代 码，但只能基于两者之一，而不能同时对这两者进行分析；( 2 ) 对于较大规模的 t c b 来说，手工使用无干扰分析法不大可行；( 3 ) 无干扰分析是”乐观的”，也就 是说，它假定在t c b 描述或源代码中不出现干扰 2 4 2 动态隐通道搜索法 主流的动态隐通道标识方法：( 1 ) 类型系统；( 2 ) 程序逻辑；( 3 ) 基于自动机的 方法。 2 0 0 0 年，s c h n e i d e r 等提出了可实施的安全策略的概念【2 3 1 ，他认为可以在目 标系统运行时检查其安全性质。此后，b a u e r 等研究了实施安全策略可用的安全 自动机 2 4 1 。f o n g 用跟踪程序运行的历史检查系统的安全性【矧。k 用自动机监视 系统的信息流【1 1 】【1 2 1 。s h r o f f 在监视系统信息时分析了系统中信息之间的动态依赖 2 6 1o 这些方法的优点是摆脱以往静态分析只在编译阶段实现，所以不能根据实时 的情况进行相应的改变的尴尬。动态分析比静态分析更加以用户为中心，实现在 线监控。终端用户可以自定义安全类别，能随着每次信息系统执行而运行监控。 因此终端用户可以根据自己的需要去修改流策略。 缺点是这些方法都为寻找源代码中的隐通道，无法检测低密用户通过感知系 统状态改变而获得信息的隐通道。 2 5 小结 为了快捷、准确的寻找到不安全信息流，各种方法先后被提出，然而在对系 统中隐含的不安全信息流搜索定位的各种方法始终有所不足，动态信息流分析法 比静态信息流分析法更加以用户为中心，实现在线监控，但不能检测低密用户通 过感知系统状态改变而获得信息的隐通道。 江苏大学硕士学位论文 有限状态自动机能够很好的描述系统状态间的转移，从而刻画系统间信息流 的流动，从而用以解决动态信息流分析法的问题。下一章将介绍有限状态自动机。 江苏大学硕士学位论文 第三章有限状态自动机 有限状态自动机( f i n i t e s t a t ea u t o m a t a ，f s 舢简称有限自动机，是具有离散输 入输出系统的数学模型，有着广泛的应用。它具有任意有限数量的内部格局或状 态，用此来记忆过去输入的有关信息，根据当前的输入可确定下一步的状态和行 为。一个有限自动机等价于一个状态转换图。而在实际系统中，系统都是以状态 转移形式进行描述的，系统的当前操作可以被描述为状态的转移，因而可以用有 限状态自动机来描述系统的状态之间的转移，下面介绍有限状态自动机的基本理 论。 3 1 有限状态自动机的描述 一个有限状态自动机可以表示成一个状态转换刚2 7 1 。状态转换图是一个有向 图，图中的一个结点表示一个状态，一条边( 或弧) 表示一个转换关系。 对于任何有限状态自动机m ( q ，万，吼，) ，均可以用有向图g m 来描述， g m 的结点集为q ，对于任何q i q 与工，若万( 留，功= q ，q j q ，则从g m 的结点吼引出一条有向弧至结点q j ，弧上标注输入字符x ，若8 ( q i ，矽= a ，则 g m 中不作处理。例如，现有一个有限状态自动机m ( q ，万，吼，f ) ，其中 q = q 0 ，q l ，q 2 ，q 3 ，输入字母表= 口，6 ) ，初始状态为q o ，接受状态集f - q 3 ， 转换函数为： 万( ，口) = q l ，a ( q o ，6 ) = q 2 ，艿( q 1 ，口) = q 3 ，万( 吼，功= 呸， 万( 吼，口) = q 2 ，万( 仍，6 ) = q 3 ，万( 吼，口) = f 2 j ，万( 仍，6 ) = f 2 j 。 则状态转换图g m 的结点集为 ，嚷，q 2 ，吼 ，对于m 的转换8 ( q o ，口) = 吼，g m 中从结点引出一条有向弧至儡，弧上标注字符a ，对于转换万( 色，口) = f 2 j ，g m 中不作处理，其它转换类似，重复此过程，直至将有限自动机m 中的转换全部 处理完毕，最终形成状态转换图g m ，如图3 1 所示。特别地，为明确有限自动 机m 的初始状态与接受状态，状态转换图g m 中将引出一条无出发点的有向 江苏大学硕士学位论文 弧指向结点，将所有接受状态的圆圈表示为双圈。 b 图3 1 有限状态自动机的状态转换图g l i 有限状态自动机读入一个字符序列时，它从初始状态q n 开始，从一个状态转 换到另一个状态，当有限状态自动机读到最后一个字符时，有限状态自动机产生 一个输出，如果有限状态自动机处于一个接受状态，则有限状态自动机输出“接 受 ，称该字符序列为有限状态自动机接受，否则有限状态自动机输出“拒绝 。 如图3 1 中描述的有限状态自动机m ，对于字符序列a a ，则m 从出发，对于 第一个字符a ，m 将状态从转换到吼，对于第二个字符a ，m 的状态从吼转换 到q 3 ，由于第二个字符a 为最后一个字符，而且此时自动机m 处于接受状态， 故字符序列a a 为自动机m 所接受。通常将有限状态自动机能接受的所有字符序 列集称为有限状态自动机识别的语言【2 8 1 。 3 2 确定型和不确定型( 随机型) 有限状态自动机 确定的有限状态自动机d f a ( d e t e r m i n i s t i cf i n i t ea u t o m a t a ) 与不确定的有限 状态自动机n f a ( n o n d e t e r m i n i s t i c f i n i t e a u t o m a t a ) ：之_ f n q 的区别是显而易见的。第 一，d f a 的每一个状态对于一个输入字符总是转换至一个唯一的后继状态，而 n f a 中的状态对于一个输入字符可以有多个后继状态。第二，在d f a 的字母表 中不包含空字符占，而在n f a 的状态转换图中，可以存在一条标注空字符占的箭 弧。 江苏大学硕士学位论文 一般地说，不确定的有限状态自动机n f a 有着较强的描述能力，它在理论 上有重要的意义，而确定的有限状态自动机d f a 则更容易用计算机程序实现。 可以证明，任何一个n f a 都可以等价转换为一个d f a 2 9 。通常采用子集构造法 【3 9 】将n f a 转换成等价的d f a ，算法描述如表3 1 所示。 表3 1 子集构造算法 在子集构造算法中涉及到两种运算：6 - c l o s u r e - 与m o v e 。对于吼q ，q 为 n f a 的状态集，s - c l o s u r e ( 呸) 表示n f a 中从状态呸通过空字符可以到达的所 有状态的集合，且级e - c l o s u r e ( q i ) ，对于s q ，6 - c l o s u r e ( s ) 表示集合s 中 每个元素的s - c l o s u r e 的并集。m o ，e ( t ，口) 表示t 中所有状态通过输入字符a 可 以到达的状态的集合。 3 3 有限状态自动机的形式化定义 有限状态自动机是一个数学的概念，是描述和资源极其有限的计算机的模型 a o l o 一个有限状态自动机有若干部分，它有一个状态集和根据输入符号从一个状 态到另一个状态的规则，有一个输入字母表，指明所有允许的输入符号，它还有 一个起始状态和一个接受状态集。形式化定义将一个有限自动机描述成一张含以 下五部分的表：状态集、输入字母表、动作规则、起始状态和接受状态集，通常 将这个表称为有限自动机的五元组。 定义3 1 有限状态自动机是一个五元组( q ，艿，吼，f ) 3 1 】，其中 江苏大学硕士学位论文 ( 1 ) q 是一个有穷集合，称为状态集，它的每一个元素称为一个状态。 ( 力是一个有穷集合，称为字母表，它的每一个元素称为一个输入字符。 ( 3 ) 万：q x - - 9 , q 是状态转换函数。 ( 4 ) q o q 是起始状态。 ( 5 ) f q 是接受状态集。 在定义3 1 的第3 条中，q x 表示集合q 与集合的笛卡尔积，万： q x 专q 表示艿是一个函数，其定义域为q ，值域为q 。 根据形式化定义3 1 ，有限状态自动机可以认为是由一个带有读头的有限控 制器和一条写有有限字符的输入带组成，读头从左向右移动，每当读头从带上读 到一个字符，便引起控制状态的改变，同时读头右移一个符号位。控制器包括有 限种状态，状态与状态之间存在着一种转换关系。每当在某个状态，读入一个字 符时，便使状态改变成另一个状态，称为状态转换，而改变后的状态则称为后继 状态。状态转换包括如下几种情况：转换到它自身，即保持原状态；转换的后继 状态只有一个；转换的后继状态有多个。如果一个有限自动机，每次转换后的后 继状态都是唯一的，则称它为确定的有限状态自动机d f a ，若转换的后继状态 不是唯一的，则称它为不确定的有