（计算机应用技术专业论文）多级安全系统中主体间信息感知机理的研究.pdf

江苏走荦硕士研究生毕业论文 摘要 由于计算机互联网络的国际化、社会化、开放化、个性化等特点，使得它在 向人们提供信息资源共享和技术共享的同时，也带来了不安全的隐患，其中就包 括隐通道问题。 低安全级进程可以通过自身和周围环境的变化来计算和推理出高安全级进 程的信息，这种隐蔽信息传递方法是一种逻辑操作，可以绕过安全模型的检验。 隐通道的这一特点，决定了传统的隐通道分析方法，即在语法分析基础上展丌的 基于系统顶级描述或源代码的分析，无法从根本上解决隐通道问题。论文提出了 一种基于操作语义的信息感知判定算法，该算法能够搜索出基于计算和推理实现 的隐蔽信息传递。具体的工作包括： 形式化地定义出隐通道的各种要素，将信息传导机制描述为抽象机，分 析了主体间通过共享客体属性的变化进行信息传递的机理，并提出一种信 息感知模型来刻画这种机理。 利用标记转换系统描述高、低安全级主体对共享客体的访问，并在此基 础上依据标记转换系统中的状态变迁提出了两个主体问的感知型信息传导 存在性判定算法。并通过实例说明低安全级主体如何通过感知获取高安全 级主体的信息。 将信息感知判定算法从两个主体构成的系统推广到由多主体构成的系 统。首先分析了多主体系统中影响信息感知的主要因素：访问顺序、访问 类型、访问属性。然后根据第三方主体产生的影响，将多主体对共享客体 的访问划分成独立的访问序列段，对每一序列段分别调用两个主体间的感 知判定算法。 对于一个可信计算机系统，在实现时能完全满足安全模型，则隐通道只发生 传导方法为感知型的场合，这样我们获得一个重要的性质，即我们进行隐通道分 析时，不需对所有的信息传导进行语法分析，关键的是找出感知型的信息传导， 对其进行语义分析，从而使得隐通道分析的工作量大大下降，进而从理论上指导 开发新的隐通道搜索方法。 关键词：隐通道，信息安全，感知模型，结构化操作语义 江苏大学硕士研究生毕业论文 a b s t r a c t d u et ot h ei n t e r n a t i o n a li n t e r n e tc o m m u n i t y , o p e n p e r s o n a l i z e df e a t u r e s 。m a d ei t t ot h es h a r i n go fi n f o r m a t i o nr e s o u r c e sa n dt e c h n o l o g ys h a r i n gw i t hp e o p l ea tt h e s a d i et i m e 。i n s e c u r i t yh a sb r o u g h tt h eh i d d e nd a n g e r sw h i c hi n c l u d ec o v e r tc h a n n e l s p r o c e s sw i t hl o ws e c u r i t yl e v e la p p e r c e i v e st h ei n f o r m a t i o nf r o mp r o c e s sw i t h h i g h e rs e c u r i t yl e v e lv i ai t ss t a t u st m n s f e ra n de n v i r o n m e n tc h a n g e s t h em e t h o du s e d b yc o v e r tc h a n n e l st os e n dm e s s a g ei sp e r c e p t i o n a l i t sak i n do fl o g i co p e r a t i o n ，s oi t n e e d n tp a s st h ei n s p e c t i o no fs e c u r i t ym o d e l t h i sc h a r a c t e ro fc o v e r tc h a n n e lm a k e s t h et r a d i t i o n a lc o v e r tc h a n n e la n a l y s i sm e t h o d w h i c hb a s e do nt o pl e v e ls p e c i f i c a t i o no r s o u r c ec o d e ，n o tf i n dt h i sk i n do fc o v e rc h a n n e l s w h e r e a sa na l g o r i t h mf o rt h e e x i s t e n c eo fi n f o r m a t i o na w a r e n e s sb a s e do ns t r u c t e do p e r a t i o n a ls e m a n t i c sp r o p o s e d i nt h i sp a p e r , c o u l ds o l v et h i sk i n do fp r o b l e me f f e c t i v e l y t h ec o n c r e t ew o r k so ft h i s d i s s e r t a t i o nc a nb es u m m a r i z e df o l l o wa s ： t h i sp a d e l f o r m a l l yd e f i n e de v e r yf a c t o r so fc o v e r tc h a r m e la n dp r e s e n t e d i n f o r m a t i o nt r a n s f e rm e c h a n i s m 勰a u t o m a t o n , a n da n a l y z e dt h em e c h a n i s mo f i n f o r m a t i o nt r a n s f e ra m o n gs u b j e c t sc h a n g i n gv a l u e so fs h a r e do b j e c ta t t r i b u t e s ，a n d p r e s e n t e dak i n do f i n f o r m a t i o na w a r e n e s sm o d e lt od e s c r i b et h i sm e c h a n i s m b a s e do nl a b e lt r a n s f o r m a t i o ns y s t e mt od e s c r i b ea c c e s s0 b i e c tb ys u b j e c t w i t hh i g ha n dl o w e rs e c u r i t yl e v e lr e s p e c t i v e l y a na l g o r i t h mf o rt h ee x i s t e n c eo f i n f o r m a t i o na w a r e n e s sw a sg i v e n h o ws u b j e c tw i t hl o ws e c u r i t yl e v e ic a nd e d u c e i n f o r m a t i o nf r o ms u b j e c tw i t hh i g h e rs e c u r i t yl e v e li si l l n s t r a t e db ya ni n s t a n c e a l g o r i t h mf o rt h ee x i s t e n c eo fi n f o r m a t i o na w a r e n e s si nt w o s u b j e c ts y s t e m e x p a n d e di n t oa l g o r i t h mi nm u l t i s u b j e c ts y s t e m f i r s t l y ，t h ek e yf a c t o r so fw h i c h i m p a c t e dt h ei n f o r m a t i o na w a r e n e s sw e r ea n a l y z e d , s u c ha st h es e q u e n c eo fa c c e s s o b j e c t ，t h et y p eo fa c c e s so b j e c t , t h ea t t r i b u t eo fa c c e s so b j e c t t h e na c c o r d i n gt o i m p a c tc a u s e db yt h et h i r ds u b j e c t ，s e q u e n c eo fm u l t i s u b j e c ta c c e s so b j e c tw e r e d e r i d e di n t os o m ei n d e p e n d e n ts e q u e n c e s ，a n da l g o r i t h mf o rt h ee x i s t e n c eo f i n f o r m a t i o na w a r e n e s si nt w o s u b j e c ts v s t e mw a sc a l l e db ye v e r yi n d e p e n d e n t s e q u e n c eo f a c c e s so b j e c t t h i sp a p e ra s s u m e st h a tat r u s t e dc o m p u t e rs y s t e mf u l f i l l e ds e c u r i t ym o d e l e n t i r e l ya f t e ri m p l e m e n t a t i o n t h a ti st os a y c o v e r tc h a n n e l se m e r g e do ns c e n a r i oo f i n f o r m a t i o na w a r e n e s so n l y s oa l li m p o r t a n tc h a r a c t e r i s t i ci sc o n c l u d e d ，i e t h e k e y s t o n eo fc o v e r tc h a n n e la n a l y s i sl i e s i ni d e n t i f yt h es c e n a r i oo fi n f o r m a t i o n a w a r e n e s si n s t e a do fc o n d u c tg r a m m a t i c a la n a l y s i sf o ra l li n f o r m a t i o nt r a n s f e r m e c h a n i s m k e yw o r d s ：c o v e r tc h a n n e l 。i n f o r m a t i o ns e c u r i t y , a w a r e n e s sm o d e l 。s t r u c t u r e d o p e r a t i o n a ls e m a n t i c s n 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校保 留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借 阅。本人授权江苏大学可以将本学位论文的全部内容或部分内容编入有关数据库 进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。 本学位论文属于 保密口，在 年解密后适用本授权书。 不保密囹。 学位论文作者签名多晦译 叼年l ，月芦 指导教师签名： ) 年z 月扩同 7 江苏大学硕士研究生毕业论文 第一章绪论 二十一世纪是信息的社会，信息已成为国家政治、军事、经济活动以及人们 日常生活必不可少的一项要素。随着当今社会对信息的依赖程度越来越高，信息 安全对整个社会的正常运转以及各种军事行动的有效实施的重要性也随之提高， 信息安全技术已逐步成为信息技术的重要支撑技术。 目前信息安全面临的威胁，有来系统自外部的，比如黑客病毒等；也有来自 系统内部的，比如隐通道。隐通道存在于多级安全系统中，即使系统已经实旌了 强制存取控制，在一个或多个特洛伊木马程序的帮助下，高安全级进程仍然可以 利用隐通道来向低安全级进程泄漏信息，且这种泄漏过程往往不被系统的存取控 制机制所检测，对系统安全构成了一定的威胁。1 9 8 3 年，美国国防部在其发布 的可信计算机系统评估准则( t c s e c ) 中，规定在b 2 级及以上的高等级可信系统 设计和开发过程中，必须进行隐通道分析。t c s e c 标准将隐通道列入评估指标之 后，1 9 9 9 年i s o 把可信计算机系统评估准则c c 2 0 正式批准为国际标准，规定 e a l 5 及以上安全级的安全软件系统必须通过隐通道分析。另外，我国的 g b t 1 8 3 3 6 、欧洲的i s o ! e c1 5 4 0 8 ，加拿大的c t c p e c 等，也均把是否通过隐通 道分析作为评估一个高等级安全系统的硬性指标。 1 。1 研究背景及意义 隐通道是指系统的一个用户在安全模型的监控下，通过违反系统安全策略 的方式传送信息给另一用户的机制。一般它通过系统原本不用于数据传送的资源 来传送信息，并且这种通信方式往往难以被系统的安全机制所检测和控制。 计算机、数学、通讯等方面的相关学者对隐通道分析进行了广泛地研究， 主要工作集中在隐通道的定义、搜索、审计和消除四个方面”1 。其中，隐通道搜 索是最关键也最困难的一环，这个方面始终是国际上的研究热点。 为了保证一个可信计算机系统的安全性，我们必须对其进行隐通道的搜索。 一类是完全依赖顶级描述规范的隐通道标识方法，如d e n n i n g 等提出的信息流分 析法0 1 ，可用来寻找安全操作系统中的隐通道。并在此基础上开发了诸如m i t r e 流分析器“1 、g y p s y 流分析器”3 等一些分析工具。 但这种完全依赖顶级描述规范来进行分析是不精确的。因为这类分析不能 标识出所有可能出现在实现代码中的隐通道。在实践中，实现代码和形式化规范 之间总是有差别的。这些代码包括性能监控、审计、调试以及其它和安全有关的 代码。他们之中有可能导致潜在的隐通道。更关键的是，在实际情况中，很少有 江苏大学硕士研究生毕业论文 程序员愿意写详细而准确的系统项级描述，有的系统甚至根本就没有这方面的工 作，因此这类方法很难被软件开发团体所接受。 另一类是面向源代码的隐通道标识，1 9 8 2 年g o g u e n 等提出的无于扰分析 法”1 ；1 9 8 3 年k e 嘲e r e r 提出共享资源矩阵法”1 ，以及1 9 9 0 年提出的隐蔽流树法 ”1 等。这些基于源代码的搜索方法，在代码量巨大、共享变量众多的场合，作 业的空自j 、时问复杂度过高，即便在系统开发过程中遵循了良好的软件工程舰范， 依然很难实现。而且这种方法属系统实现后的分析，不便于重新设计系统或者部 分修改设计以消除或限制隐通道。 更重要的是，面向源代码或者系统顶级描述的隐通道搜索方法，均是建立在 对程序结构分析的基础上。在系统运行中，低安全级主体完全可以通过对自身状 态及系统环境的变化进行推理，从而实现从高安全级主体向低安全级主体的信息 传递。我们把这一类信息传递称为感知型的信息传导，其依赖于系统运行环境下 的语义解释，是无法通过对程序结构的分析来发现的。面向源代码或者系统顶级 描述的隐通道标识方法因为未考虑系统的运行环境，所以不能从根本上解决隐通 道的搜索问题。 目前，国内关于隐通道的研究仍处于起步阶段，公开发表的文献及相关研究 成果很少。而西方国家是禁止对中国出售e a l 5 级以上的商安全等级软件系统产 品的。所以我国要拥有高安全等级软件系统，必须走独立自主地开发道路。本论 文的目的就是要自主地进行隐通道分析的研究，以打破国外对我们的技术封锁。 1 2 隐通道概述 隐通道的概念最仞是由l a m p s o n 于1 9 7 3 年提出的。他在论文“a n o t eo n t h e c o n f i n e m e n t p r o b l e m ”。1 中这样定义隐通道：“如果一个通道既不是设计用于通 信，也不是用于传递信息，则称该通道为隐通道”。迄今为止，从隐通道问题提出 到现在的三十几年里，国际上的信息安全专家进行了广泛的研究，各类系统中的 隐通道问题不断被发掘并加以分析，隐通道概念的内涵也逐步清晰，分清了它和 泄露信道( 1 e a k a g ec h a n n e l ) 的区别。 1 9 8 3 年，美国国防都发布的第一个计算机安全产品评估标准“”( 通常 简称t c s e 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 nc r i t e r i a 或者橘皮书) 给隐通 道下的定义是：“隐通道是允许进程以危害系统安全策略的方式传递信息的通 道”，也就是说，隐通道与系统的安全策略应该有关系，较为全面地刻画了隐通 道的内涵，显示了隐通道与不同的访问策略之间的关系。 江苏太擘硕士研究生毕业论丈 1 2 1 隐通道的工作原理 依据目| ；i 的认识，隐通道的工作原理“”是安全系统中具有较高安全级的主体 z 。，使用事先约定好的编码方式，通过更改某个共享客体0 f 的属性q 专4 并 使具有较低、或不可比安全级的主体z l 观察到这种变化，来传送违反系统安全 策略的信息，见图1 1 。 图1 1 隐通道的工作原理 需要指出的是，图1 1 中的实线箭头所标识的操作都是合法的，即能通过安 全模型的验证，但两次合法的操作却导致了一次非法的信息流动，如图卜l 中虚 线箭头所示。 1 2 2 隐通道的成因 正如在t c s e c 等安全标准中所做的那样，我们将一个可信计算机系统分成若 干个有序的安全等级厶，岛，厶，其中厶 k l ，1 f r , f ，胛。对每一级的可 信系统用自然语占确定了一组安全约束条件“4 ”1 。 定义l 安全策略旯 我们把用自然语言对某一给定的可信系统所描述的安全约束条件的集合称 为该系统的安全策略z 。 每一安全策略对应着一个安全约束条件的集合： 九( 厶) 2 这里l 表示系统的安全等级，p 表示安全约束条件。 公理l 当两个不同等级的可信系统满足 ) 时刻，主体z 2 对客体d 进行操作，则z 2 与z i 通过共 享客体d 形成了一个信息通道，如图2 1 所示。 江苏大擘硕士研究生毕业论文 通道元c i 图2 1两个通道元共享一个客体从而构成一个信息通道 在安全模型m 的监控下，在 时刻通道元c i 中，主体z 1 对共享客体d 进行 操作，从而将信息厶由主体z l 传送到共享客体0 ；在f 2 时刻通道元g 中，主体z 2 对共享客体0 进行操作，从而将信息，2 由主体z 2 传送到共享客体0 ，则z 2 与z 1 通过共享客体d 形成了一个信息通道。 2 2 2 信息通道的构成 下面详细分析两个不同安全级主体z 1 ，z 2 的通道元c i ，c 2 以及具有安全级别的 客体d ，在b l p 安全模型下是否有可能构成一条信息通道( 见图2 2 ) 。以下讨论 假设在安全级t ( c ，s ) 具有相同的部门级s 条件下进行。 | i 、 、 ， 、 图2 2b l p 模型下的信息通道 江苏走学硕士研究生毕业论文 1 当l ( z t ) l ( z 2 ) 时，此时主体互安全级高于客体d 低，所以2 ；只 能对客体d 执行读操作：而主体乞安全级别低于客体0 ，所以z 2 只能对客体。执 行写操作，即 z f ：r ( d ) m ( b l p ) z 2 ：形( d ) 芒m ( b l p ) z l ：胄( o ) 芒m ( b l p ) z 2 ：( d ) m ( b l p ) 此时z i ：月( d ) 一z 2 ：( d ) 构成一条信息通道。 3 当( z 1 ) 三( d ) 三( z 2 ) 时，此时，在b l p 安全模型下，主体五，乙都只能 对客体。执行读操作，即 z l ：r ( o ) m ( b l p ) z 2 ：矿( d ) 芒m ( b l p ) z l ：r ( d ) m ( b l p ) z 2 ：缈( 芒m ( b l p ) 此时，五：r ( d ) 啼z 2 ：露( o ) 构成信息通道。 4 当( z 1 ) ( o ) 2 三( z 2 ) 时，客体d 的安全级别比主体z 1 z 2 都高，此时z i ，z 2 都只能对客体执行w 操作。 五：r ( o ) 仨m ( b l p ) 乙：w ( o ) m ( b l p ) z i ：r ( o ) 芒m ( b l p ) z 2 ：( d ) m ( b l p ) 1 4 江苏大擘硕士研究生毕业论文 此时，z l ：矽( d ) 斗z 2 ：矿( d ) g j r 戎n , g i $ g g 。 2 3 信息感知模型的建立 假设系统有两个用户一高安全用户h i g h 和低安全l o w 以及一个共享客体 ( 打印机) ，在某个时刻，l o w 用户请求打印机失败，此时l o w 用户根据自己的 请求失败，可以推出h i g h 用户正在使用打印机。从而h i g h 用户可以根据是否占 用打印机向l o w 用户发送信息0 或者l 。从这个例子我们不难发现，低安全级用 户可以通过对共享客体的变化属性进行计算或推理来获取高安全级用户的信息。 本文把这种信息传递方式称为感知。 本小节我们主要讨论两个主体和一个客体构成的系统中，感知发生的机理和 场景。在系统运行中，z l 与z 2 对客体0 的访问顺序不是任意的，会受到某种访 问调度算法的约束，本文用表示这种约束。不失一般性我们假设客体0 的属性 数目为胁屯表示第个属性，p 表示每个属性的值域，且是有限的。 在一个通道元中主体对客体的访问是一个动态的过程，我们用标记转换系统 来刻画这种动态行为。 【定义2 5 】通道元状态机 i 殳c ( z ，o ，a ) 为一通道元，标记转换系统k = ( s ，s o ，艿) 刻画了c 的动态行 为( l ，称为c 的通道元状态机) ，这里， s = s t a t e z x s t a t e o 是有限状态的集合； s o = ( z ( ) ，0 ( d 0 ) ) 是仞始状态； = z ( a ) 是操作的集合； j ：s x - - + s是状态转换关系，满足： v s ，j s ，v 口e ，s a ( s ，盯) 当且仅当 ( o e z ( r ) 一a ，( s 上z ) = z ( 口) 。( ，( s s z ) ) 且s 0 0 = j 工o ) 或者 ( c r e a ，y ( s 毒z ) = z ( 口) ，( ，( sj ，z ) ) ，叩( j 山d ) = d ( ) ，( 玎( s 上。) ) ( s 上z 表面；s 中主体的状态，j k 表示s 中客体的状态) 。 l s 江苏大擘硕士研究生毕业论更 对于通道元c ( z ，d ，a ) ，约定c ( s ) = s ，c ( d ) = 0 ，c ( a ) = a ；对于通道元状态 机k = ( s ，南，d ) ，约定k ( s ) = s ，厶，) = ，0 ( ) = ，厶( 6 ) = 6 。 【定义2 6 1 可视属性设c l ( d ) = c 2 ( d ) ，我们称客体d 的属性6 j 是可视的当且 仅当在通道元状态机k , g j e 体q ( z ) 访问了属性匆，在通道元状态机乇中主体 c 2 ( z ) 访问了属性6 j 。 主体z t 通过对共享客体的可视属性进行计算、推理柬获取主体z 2i n 信, g t ， 我们把这种信息传递方式称为感知，形式化定义如下： 【定义2 7l 主体z 1 对z 2 的感知o ( z 2 与z 1 ) 是一个八元组 ( 丁，巧，正，s , v ，1 2 ，丫) ，其中， t = t o ，厶 为刻画事件发生顺序的相对时间序列的集合，且满足 岛 f 2 5 互= 纸，气：， t ，为刻画主体五对共享客体访问顺序的相对时间序 列的集合，且满足 幺 龟； e = ，f 2 ，f ) 量r ，为刻画主体z 2 对共享客体访问顺序的相对时间序 列的集合，且满足f ，i 屯 气，r = 7 ：u 正，五n 疋= a ； s = ， ，晶是一个状态序列，其中置= ( z i ( ) ，0 ( 0 3 ，z 2 ( ) ) ( o i 疗) ， 这罩五( z 。) ，z 2 ( z ，) 分别表示主体z l ，z 2 在f 。时刻的状态，o ( o 。) 表示客体 o 在f 时刻的状态。 v = 岛，以 为可视属性的集合，且对于v 6 9 v ，存在气7 i 使得主体 z i 利用传导方法在气时刻访问了可视属性6 9 ，存在l 疋使得主体z 2 利用传导方法在时刻访问了可视属性。 1 6 江苏走擘项士研究生毕业论文 ，l = 嚣， ( 叩( 气) 山。，) ，其中叩( 气) 山。表示在时刻客体0 的可视属 性的值，这里叩( ) 山。可以为j 表示属性6 9 在气时刻没有被主体z l 访问； l = u 臻， ( 玎( 气) k ，气) ，其中叩( ) j ，。表示在- 时刻客体0 的可视属 性的值，这罩叩( d ，) j ，。可以为上表示属性唣在时刻没有被主体z 2 访问； 丫是集合上的一个计算和推理过程，且丫( ，) n 厶a ，这里： ( 蹿( 吼) 山。，t ) t ( ，眇) 当且仅当由，( 叩( q ) 上。，气) 形成的共享客体访问顺 序满足约束。 访口j 时刻共享客体的可视属性访问的宅体 f 0 r ( 0 0 ) - ，r ( 0 0 ) z 1 叩( d 1 ) - ，玎( d 1 ) 上，z 1 乞 r ( o z ) , 1 1 ，i ( 0 2 ) 工，z 2 屯 叩( 0 3 ) 山 ，玎( d 3 ) 山，z 2 厶一i 叩( o 。一1 ) 上l ，r l ( o n 1 ) 山，z 2 叩( d 。) 上l ，7 ( d 。) 上，z 1 图2 3 发生感知的操作序列 我们可使用如图2 3 所示的操作序列来分析其发生感知的过程。 在飞，k ，t 时刻，主体z 1 利用传导方法仇操作客体d 的可视属性矿，并 获取客体d 的信息= u 。l ；8 9 f ( 叩( 气) j ，。，气) ； 1 7 江苏大擘硕士研究生毕业论文 在，气，t t , 时刻，主体互利用传导方法仍操作客体d 的可视属性矿，并 获取客体。的信息，2 = u 礞， ( 可( q ) j ，) ) ； 主体z 1 利用对共享客体的访问约束，在获取的信息，l 的基础上进行推 导和计算，从而获得厶中的某个信息。 2 4 信息感知与隐通道 以下讨论均假设在安全级l ( c ，s ) 具有相同的部门级s 条件下进行。在2 2 2 小节中我们已经讨论在b l p 模型下可能的信息通道有：当( z 1 ) ( z 2 ) 时，信息通道 z l ：r ( o ) jz 2 ：缈( d ) ；当三( z 1 ) ( d ) ( z 2 ) ， 信息通道 z 1 ：r ( d ) 。z 2 ：r ( d ) ；当工( z 1 ) ( d ) l ( z 2 ) 时，信息通道 z l ：缈( d ) 斗z 2 ：( o ) 。下面对这4 种信息通道讨论在何种情况可能会产生信息 感知，从而找出在b l p 模型下，信息感知发生的必要条件。 1 当( z 1 ) t 2 ，低安全级主体z 1 对客体d 进行w 操作，然后高安全级主体z 2 来对 江苏走擘硕士研究生毕业论文 客体。进行r 操作，根据感知的定义，此时低安全级主体五无法推出高安全级 主体的信息；若 上( z 2 ) ，此时z l ：r ( d ) 一z 2 ：矿( d ) 构成一条信息通道。 赆图2 5 。 ， i 、 、 、 图2 ，5 信息通道z i ：胄( d ) 专z 2 ：( o ) 我们设高安全主体z l 对客体。的r 操作在 时刻发生，低安全主体乙对客 体d 的w 操作在，2 发生，若，i t 2 ，高安全级主体z l 来对客体0 进 行r 操作，然后低安全级主体z 2 对客体d 进行w 操作，z l 来对客体d 进行r 操 作没有使共享客体的属性发生变化，因而低安全级主体z 对客体。进行w 操作 的过程中无法推出高安全级主体z 1 的信息。 3 当三( z 1 ) 三( d ) 上( z 2 ) ，此时，互：r ( d ) _ z 2 ：r ( 构成信息通道。下 面分两种情况来讨论： 1 9 江苏走学硕士研究生毕业论文 ( 1 ) 当l ( z z ) ，2 ，此时低安全级主体z 1 对客体0 进行r 操作， 然后高安全级主体z 2 来对客体。进行r 操作，根据感知的定义，此时低 安全级主体乞无法推出高安全级主体z 1 的信息：若 三( s ) 时，信息通道如下图2 7 所示 图2 7 信息通道z 1 ：r ( d ) 寸z 2 ：r ( o ) 、 ， 、 ， 、 、 ， ， 江苏大学硕士研究生毕业论文 我们设高安全级主体五对客体d 的r 操作在f i 时刻发生，z 2 对客 体0 的r 操作在f 2 发生，若 1 2 时，此时高安全级主体z 1 来 对客体d 进行r 操作，然后低安全级主体z 2 对客体d 进行r 操作，z l 对客体0 进行r 操作不能改变客体0 的属性，而低安全级主体z ，对客 体0 进行r 操作的过程就不能够推理或者计算出高安全级主体z 的操 作，此时不可能发生信息感知。 4 当l ( z 1 ) 表示在状态盯下 计算表达式e 所得的值。 【定义3 3 】 ( 1 ) e v a l ( e ，仃 = 口是一个规则，其中o r 为值； ( 2 ) ( j ，盯 _ 0 ：盯是一个规则，表示从组态( 5 ，玎) 出发，执行一定的语句 后，到达组态( s ，盯 。当s 为空语句时，上式右端为p ； ( 3 ) 有限多个规则的并和交仍是规则； ( 4 ) 若和是规则，则 二l ( 3 2 1 ) ，2 也是规则。表示若成立，则吩也成立： ( 5 ) 在一个具体的s o s 中，若某规则r 恒成立，且不为( 3 2 1 ) 形式，则r 称为公理。若有类如式( 3 2 1 ) 的规则成立，则称为推理。 【定义3 4 】三元组 称为是一个转换三元组，其中c 是全体可能 江苏走擘硕士研究生毕业论文 的组态的集合，t 是全体终结组态的集合，r 是全体公理和推理的集合，简称公 理集合。 终结组态是指形式为 的组态，或这样的组态 ，对它们不存在 使得 一 ( 3 2 2 ) 成立，并且s j 。 3 1 2 2s l 语言的结构化操作语义 现在以微型语占s l 为例，说明如何用s o s 来描述，下面是s l 的语法的b n f 形式： ：= i i l s l 【i p l ； ：= ：= a 表达式 ：= i f t i l e n e l s e f i ：部惋l e d o o d 下面各部分是s o s 描述部分： 1 语法范畴 变量集v ，元素) 【，y ，z ； a 表达式集e ，元素e l ，e 2 , e 3 ，e ； b 表达式集b ，元素t m e ，脚s e ，b l ，b 2 ，b 3 ； 语句集s ，元素为s ，t l l ，v 2 静态语义 ( 1 ) h ：= e 卜s & 卜t ( 2 了赢面 丽 ( 4 ) 卜蔽卜t 卜占；z 卜。 注：h 表示s 是一个合法的语言成分，用卜表示：若s 表示一个合 法的语言成分，则t 也是一个合法的语言成分。 3 动态语义 江苏大学硕士研究生毕业论文 l l j ( 2 ) 寸 ( 3 ) 一一兰兰坐堕! 三三竺坚 、 f 4 1 一一 ! 兰生三垒：! ! ! 型! ! 专 f 5 ) 一旦堕! 生! 兰竺丝一 、7 ( 6 ) ! 堡! 三生2 三丝丝 、 焉i 暑淼t 如果我们把触发信息流动的命令看成是给定计算机语言的程序，把信息传导 的机制描述成抽象机，那么就可以把操作语义引入信息传导的描述中，对信息在 信息传导抽象机中的运行状况进行准确地描述。在此基础上，我们就能够以操作 语义为工具，研究分类建立信息传导机制及其操作语义模型、并讨论各类信息传 导机制抽象机在不同语境下的操作语义。 3 2 两个主体间的感知判定算法 z t ，z 2 分别为c i ，c 2 中的主体，c t ( 0 ) = c 2 ( o ) 。据感知的定义，z i 对z 2 的感知足z l 通过对z i ，z 2 共同操作的客体属性进行计算和推导而实现的，因此客 体中没有被z i 操作的属性对感知的产生是不起作用的。对于作用于客体d 的每 一个操作v 盯o ( y ) ，函数屯： 1 ，脚 ) 呻2 忆4 表示操作盯改变的属性集合。 在存在共享客体的两个通道元中主体对客体的访问是交互进行的，我们以 p l o t k i n 结构化操作语义中的组合语义为基础，定义信息通道状态机来描述这个 交互过程。 【定义3 5 1 信息通道状态机 用标记转换系统l = ( s ，s o ，艿) 来刻画z 1 ，z 2 对客体d 的并发访问，并把称 为信息通道状态机，这黾， 江苏大擘硕士研究生毕业论交 s = s t a t e z 1x s t a t e o x s t a t e z j ； = ( z l ( 白) ，o ( 0 0 ) ，z 2 ( ) ) 是初始状态： = z 。( x ) u z 2 ( x ) 是操作的集合； 8 ：s x e 寸s 是状态转换关系，v s ，j s ，v o ，s = 艿( 5 ，盯) 当且仅当下 面两个条件中的一个成立： a e z l ( x ) s 上z l u d = 毛( 艿) 山z i u d ，a ) a s 0 2 2 = s l z 2 ，这晕s 上z i u d 表示在s 下主体z l 和客体d 的状态，s 山。表示在s 下主体z 2 的状态。 o - e z 2 ( x ) j j ，z 2 u d = k ( 回。山乙u 0 ，o r ) a s 屯= s 山z l 设= q ，吒，o r ，是中长度为v