（计算机软件与理论专业论文）信息流的语法标识及其属性算术验证的研究.pdf

本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独 立进行研究工作所取得的成果。除文中己注明引用的内容以外，本论 文不包含任何其他个人或集体已经发表或撰写过的作品成果，也不包 含为获得江苏大学或其他教育机构的学位或证书而使用过的材料。对 本文的研究做出重要贡献的个人和集体，均己在文中以明确方式标 明。本人完全意识到本声明的法律结果由本人承担。 学位论文作者签名：删 2 0 11 年6 月罗日 江苏大学硕士研究生毕业论文 学位论文版权使用授权书 学、中国科学技术信息研究所、国家图书馆、中国学术期 ) 电子杂志社有权保留本人所送交学位论文的复印件和电 以采用影印、缩印或其他复制手段保存论文。本人电子文 档的内容和纸质论文的内容相一致，允许论文被查阅和借阅，同时授 权中国科学技术信息研究所将本论文编入中国学位论文全文数据 库并向社会提供查询，授权中国学术期刊( 光盘版) 电子杂志社将 本论文编入中国优秀博硕士学位论文全文数据库并向社会提供查 询。论文的公布( 包括刊登) 授权江苏大学研究生处办理。 本学位论文属于不保密 学位论文作者签名：撇 沙1 1 年6 月e t 指导教师签名： 驯1 年6 月9 日 江苏大学硕士研究生毕业论文 摘要 为保证计算机系统中的信息机密性，自主访问控制和强制访问控制策略在计 算机多级安全系统中得到了广泛的应用。然而，实施了这两种策略的计算机系统 仍存在安全隐患，如安全系统中的隐通道问题。高安全级进程可以利用隐通道向 低安全级进程泄漏信息，对系统安全构成巨大威胁。因此，对高安全等级的安全 操作系统，各种安全标准都要求进行隐通道分析。 信息流控制方法是应用广泛的隐通道搜索方法，包括语法信息流分析方法和 语义信息流分析方法。传统的语法信息流分析方法均基于实施机密性安全策略的 信息流格模型，而格关系的传递特性使得该方法不能用来分析实施无传递性安全 策略的系统的安全性。无干扰分析方法是一种严谨的语义信息流分析方法，目前 主要采用“展开技术”对信息流安全属性进行验证，但是验证这些安全属性的“展 开方法 是可靠但并不是完备的，此外有一些安全属性不存在“展开条件”。 本文的主要研究内容包括： 1 针对格模型不能描述非传递安全性策略的问题，提出同时适用非传递性 和传递性安全策略的语法信息流分析方法。首先将信息流语义附加在每条语句之 后，然后定义一种称为信息流时序图的图结构来刻画信息流发生的时序关系，并 给出基于源程序的信息流时序图的构造方法。接着提出删除规则来删除信息流图 中多余的初始点、终止点和重复路径，并开发出一种基于时序图的隐蔽信息流的 标识算法。另外，针对并发程序的并发特性，提出了一种简化信息流时序图的方 法。在该方法下只要考虑并发进程之间特定的交互次序即可，而不需考虑所有可 能的交互方式。 2 针对验证前向可修正属性的“展开方法”不完备的问题，提出一种可靠 且完备的前向可修正属性验证方法。该方法根据前向可修正属性的特点，提出该 属性相应的确定型系统的双径双构造，在双径双构造结构上分析前向可修正属性 的性质，将前向可修正属性的验证归约为可达性问题，进一步给出该属性的验证 算法。当属性不成立时，算法可以给出使属性失效的反例，从而解决前向可修正 属性“展开方法”不完备性的问题。 3 针对验证广义不可推断属性的“展开方法”不完备的问题，提出一种可 靠且完备的广义不可推断属性的验证方法。该方法给出广义不可推断属性反例的 江苏大学硕士研究生毕业论文 定义，根据广义不可推断属性的特点，提出与该属性相应的确定型系统的单径双 构造，并基于图结构理论得出该属性最短反例的上近似计算。然后采用证伪技术， 通过逐步搜索长度递增的使广义不可推断属性失效的反例来完成验证过程，从而 解决广义不可推断属性“展开方法”不完备性的问题。进一步为提高验证方法的 时间效率和降低对内存空问的需求，将反例搜索和上近似计算归约为量化布尔公 式满足性求解问题，借助于高效的满足性求解程序完成属性的验证，实现验证过 程的符号化计算。 关键字：隐通道，语法信息流分析，无干扰，信息流安全属性，量化布尔公式， 符号化验证 i l a b s t r a c t t oe n s u r ec o n f i d e n t i a l i t yo fi n f o r m a t i o ni nc o m p u t e rs y s t e m s ，a u t o n o m ya c c e s s c o n t r o la n dm a n d a t o r ya c c e s sc o n t r o lp o l i c i e sh a v eb e e nw i d e l yu s e di nm u l t i - l e v e l c o m p u t e rs e c u r i t ys y s t e m h o w e v e r , e v e ni n as 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 dt h et w op o l i c i e s ，ah i g h - l e v e lp r o c e s sc a n l e a ki n f o r m a t i o nt oal o w - l e v e l p r o c e s sb yu s i n gc o n v e r tc h a n n e l b e c a u s ec o n v e r tc h a n n e lp o s e sah u g et h r e a t t o s y s t e ms e c u r i t y ，a l ls a f e t ys t a n d a r d sa r er e q u i r e m e n t sf o rc o v e r tc h a n n e la n a l y s i so f t h eh i g hs a f e t yl e v e ls e c u r eo p e r a t i n gs y s t e m i n f o r m a t i o nf l o wc o n t r o lm e t h o di sac o v e ac h a n n e ls e a r c hm e t h o d s ，i n c l u d i n g s y n t a c t i ci n f o r m a t i o nf l o wa n a l y s i s a n ds e m a n t i ci n f o r m a t i o nf l o wa n a l y s i s t h e t r a d i t i o n a ls y n t a c t i ci n f o r m a t i o nf l o wa n a l y s i si sb a s e do nt h el a t t i c em o d e ls u c ht h a t t h em e t h o dc a nn o tb eu s e dt oa n a l y z et h es e c u r i t yo fs y s t e m si m p l e m e n t i n gt h e s e c u r i t yp o l i c yn o ts a t i s f y i n gt r a n s i t i v i t y n o i n t e r f e r e n c ea n a l y s i s ，ar i g o r o u sm e t h o d o ft h es e m a n t i ci n f o r m a t i o nf l o wa n a l y s i s ，u s e st h e “u n w i n d i n gt h e o r e m t ov e i l f y t h ei n f o r m a t i o nf l o ws e c u r i t yp r o p e r t i e s h o w e v e r , “u n w i n d i n gt h e o r e m i sr e l i a b l e b u tn o tc o m p l e t e ，a n dt h e r e a r es o m ep r o p e r t i e sw h i c hh a v en o “u n w i n d i n g c o n d i t i o n s t h em a i nc o n t r i b u t i o no ft h i sp a p e rr e s t sw i t ht h ef o l l o w i n g ： 1 f o rt h el i m i t a t i o nt h a tl a t t i c em o d e li su n a b l et oa n a l y z et h es y s t e mw i t h s e c u r i t yp o l i c yn o ts a t i s f y i n gt r a n s i t i v i t y , w ep r o p o s ea n e wi n f o r m a t i o nf l o wa n a l y s i s a p p r o a c h f i r s t ，i n f o r m a t i o nf l o ws e m a n t i c si sa t t a c h e dt oe a c hs t a t e m e n to f a p r o g r a m l a n g u a g e t h e nag r a p hs t r u c t u r ec a l l e di n f o r m a t i o nf l o wt e m p o r a lr e l a t i o ni sd e f i n e d t od e s c r i b et h et e m p o r a lr e l a t i o no fi n f o r m a t i o nf l o wo c c u r r i n g ，a n dam e t h o do f c o n s t r u c t i n gt h eg r a p hs t r u c t u r ei sp r e s e n t e d b e s i d e s ，t h es i m p l i f i e dr u l e sa r eu s e dt o r e m o v et h er e d u n d a n ti n i t i a l p o i n t 、f i n a l p o i n to rr e p e a t e dp a t h ，a n db a s e do nt h e g r a p hs t r u c t u r eac o v e r ti n f o r m a t i o nf l o w i d e n t i f i c a t i o nm e t h o di sd e v e l o p e d i n a d d i t i o n ，f o rt h es t a t ee x p l o s i o no f t h eg r a p hs t r u c t u r eo fc o n c u r r e n tp r o g r a m ，w i t h o u t l o s i n ga n yi n f o r m a t i o nf l o was p e c i a lc o n c u r r e n to r d e r i sc o n s i d e r e d 2 f o rt h ei n c o m p l e t e n e s so ft h e “u n w i n d i n gt h e o r e m ”，p r e s e n tar e l i a b l ea n d c o m p l e t e v e r i f i c a t i o nm e t h o do ff o r w a r dc o r r e c t a b i l i t y a c c o r d i n g t ot h e c h a r a c t e r i s t i c so ff o r w a r dc o r r e c t a b i l i t y ，p r o p o s ead o u b l e p a t h d o u b l e s t r u c t u r eo f t h ed e t e r m i n i s t i cs y s t e ma n da n a l y s i st h en a t u r eo ft h ep r o p e r t y , t h e nr e d u c ef o r w a r d c o r r e c t a b i l i t yc h e c k i n gt ot h er e a c h a b i l i t yp r o b l e ma n dg i v e t h ea l g o r i t h mo ft h e p r o p e r t yv e r i f i c a t i o n t i l i sm e t h o di sc o m p l e t eb e c a u s e i tc a ng i v eac o u n t e r - e x a m p l e s w h e nas y s t e mf a i lt os a t i s f yt h ef o r w a r dc o r r e c t a b i l i t y 江苏大学硕士研究生毕业论文 3 f o rt h ei n c o m p l e t e n e s so ft h e “u n w i n d i n gt h e o r e m ”，p r e s e n tar e l i a b l ea n d c o m p l e t ev e r i f i c a t i o nm e t h o do fg e n e r a l i z e dn o n i n f e r e n c e f i r s t ，a f t e rg i v i n gt h e d e f i n i t i o no fc o u n t e r e x a m p l e so fg e n e r a l i z e dn o n i n f e r e n c ea n da n a l y z i n gi t s c h a r a c t e r i s t i c s ，w ep r e s e n ts i n g l e p a t h - d o u b l e s t r u c t u r eo f t h ed e t e r m i n i s t i cs y s t e mf o r t h ep r o p e r t y t h e n ，i no r d e rt og u a r a n t e et h ec o m p l e t e n e s so ft h ea p p r o a c h ，b a s e do n t h eg r a p hs t r u c t u r et h e o r y , w eg i v ea na p p r o x i m a t ec o m p u t a t i o no ft h es h o r t e s t c o u n t e r e x a m p l ea n dp r o p o s eaa p p r o a c hw h i c hv e r i f i e sg e n e r a l i z e dn o n i n f e r e n c eb y s e a r c h i n gf o rc o u n t e r e x a m p l e ss t e pb ys t e p f u r t h e ri no r d e rt oi n c r e a s et h ee f f i c i e n c y a n dr e d u c et h em e m o r yr e q u i r e m e n t ，t h es e a r c ho fc o u n t e r e x a m p l e sa n dc o m p u t a t i o n o ft h et h r e s h o l da r er e d u c e dt ot h eq u a n t i f i e db o o l e a nf o r m u l as a t i s f i a b i l i t yp r o b l e m t h e nas y m b o l i cv e r i f i c a t i o n p r o c e d u r ei se s t a b l i s h e db yaq u a n t i f i e db o o l e a n f o r m u l as o l v e r k e y w o r d ：c o v e r tc h a n n e l ，s y n t a c t i ci n f o r m a t i o nf l o wa n a l y s i s ，n o n i n t e r f e r e n c e ，i n f o r - m a t i o nf l o ws e c u r i t yp r o p e r t y ，q u a n t i f i e db o o l e a nf o r m u l a ，s y m b o l i cv e r i f i c a t i o n i v 江苏大学硕士研究生毕业论文 目录 第一章绪论一l 1 1 研究背景1 1 1 1 隐通道l 1 1 2 隐通道搜索方法2 1 2 研究现状4 1 3 研究内容及论文组织6 第二章相关的概念和定义9 2 1 安全策略9 2 2 信息流语义10 2 3 量化布尔公式1 2 第三章面向无传递性安全策略的语法信息流分析方法1 3 3 1 顺序程序中隐蔽信息流的标识13 3 1 1 信息流时序图l4 3 1 2 信息流时序图的构建算法1 7 3 1 - 3 信息流时序图的简化1 8 3 1 4 信息流的标识算法2 1 3 2 并发程序中隐蔽信息流的标识一2 2 3 2 1 信息流时序图的计算2 2 3 2 2 信息流的标识算法2 3 3 3 看寻例2 6 3 4 本章小结2 8 第四章前向可修正属性的算术验证2 9 4 1 前向可修正属性的描述2 9 4 1 1 状态转换系统模型2 9 4 1 2 前向可修正属性3 1 4 2 前向可修正属性的验证算法3 2 4 2 1 不确定型系统的确定型构造3 3 4 2 2 确定型系统的双径双构造3 4 4 2 3 前向可修正属性的验证方法3 5 4 3 示例3 7 4 4 本章小结3 9 第五章广义不可推断属性的算术验证4 0 5 1 广义不可推断属性的描述4 0 5 2 基于反例搜索的验证算法。4 1 5 3 算术验证的符号化计算4 5 5 3 1 状态转换系统模型的符号化表示4 6 5 3 2 反例搜索过程的符号化转换4 7 5 3 3 看专例4 8 v 江苏大学硕士研究生毕业论文 5 4 本章小结一：4 9 第六章实例分析一5 l 6 1 磁臂运动系统的描述5 1 6 2 前向可修正属性的验证5 3 6 3 广义不可推断属性的验证一5 4 6 4 本章小结5 6 第七章总结与展望5 7 7 1 总结5 7 7 2 展望5 8 参考文献5 9 墅i 【谢一6 3 发表论文6 4 v i 江苏大学硕士研究生毕业论文 1 1 研究背景 第一章绪论弗一早殖比 随着计算机技术的飞速发展，信息网络已经成为社会发展的重要保证。信息 网络涉及到国家的政府、军事、文化等诸多领域。这些信息其中有很多是敏感信 息，甚至是国家机密。然而保密信息在计算机中被窃取的例子却屡见不鲜，即使 像美国这样强国的军用系统亦不能幸免。因此，确保这些重要信息的机密性是很 多安全系统最基本最常见的安全性需求，如何防止重要数据的信息泄露是开发高 安全等级系统必须面对的问题。 访问控制是计算机系统常用的保护数据机密性的安全策略，它以某种途径显 示地管理着用户对所有资源的访问请求。根据系统既定的安全策略，访问控制对 每个资源的访问请求作出“许可”或“限制”的判断。它包括自主访问控制i l j 和强制访问控制【2 】，通过两者结合，可以有效地防止非法用户访问系统资源和合 法用户非法使用系统资源。然而，实施了访问控制策略的计算机系统仍存在安全 隐患，其中包括安全系统中的隐通道问题1 3 , 4 , 5 j 。 考察如下系统，高安全级的用户h i g h 可以通过在目录d i r 内创建或者删除 文件f i l e 给低安全级的用户l o w 传递信息。当h i g h 向空目录d 1 r 创建一个新 文件f i l e ，会导致用户l o w 删除目录d i r 的操作失败，此时h i 曲向l o w 传递 信息“o ”；反之，若h i 曲删除目录d i r 内全部的文件，则l o w 删除目录d i r 的操作就会成功，此时h i 曲向l o w 传递信息“1 。当h i 曲和l o w 之间有事先 约定的通信编码方式，那么h i 曲就能通过这种方式向l o w 传递任何可数字化的 信息。上述h i g l l 向l o w 传递信息的方式我们称为隐通道，隐通道能够突破访问 控制机制的约束，造成保密信息的泄露。 1 1 1 隐通道 隐通道的概念是b w l a m p s o n 于1 9 7 3 年在“论限制问题”一文中提出的f 6 j 。 他通过对程序限制问题的研究，分析了程序的调用与信息的传送，禁止程序在运 行期问向其它程序( 其调用程序除外) 传送信息，给出了对程序进行限制的规则。 如果程序向它的拥有者传送有关其调用程序的信息就属于信息泄漏。 江苏大学硕士研究生毕业论文 b w l a m p s o n 把信息泄漏的通道归纳为合法通道、存储通道、隐通道，并把隐通 道定义为，按常规根本不用于传送信息但却被用于泄漏信息的信息传送渠道。 1 9 7 5 年，s bl i p n e r 对隐通道做了进一步研究，根据通信双方传递信息所 采用的媒介不同，把隐通道分为存储隐通道和时间隐通道1 7 1 。存储通道涉及到 一个进程直接或者间接写入一个存储位置，此时有另外一个进程直接或者间接读 这个存储位置。一般来说，存储隐通道涉及到不同安全级可以共享某种数量有限 的资源( 如硬盘) 。而时间隐通道则指一个进程采用调节自己对系统资源( 如c p u ) 的使用，从而影响另外一个进程观察到的真实响应时问。随后，r k e m m e r e r 8 l 总结了隐通道的判断特征。他指出一个存储隐通道必须至少满足下列判断规则： ( 1 ) 发送方和接收方进程必须有权存取共享资源的同一属性。 ( 2 ) 发送方进程必须有办法改变该共享资源。 ( 3 ) 接收方进程必须有办法侦查该共享资源的改变。 ( 4 ) 必须存在某种机制，使发送方和接受方进程能启动隐蔽通信并正确给 事件排序。该机制可能足另一条较小带宽的隐通道。 如果满足条件( 1 ) ( 3 ) ，就要找出满足条件( 4 ) 的场景。如果可以找到 这样的场景，则表明系统存在存储隐通道。 同样，一个时间隐通道必须至少满足下列判断规则： ( 1 ) 发送方和接收方进程必须有权存取共享资源的同一属性。 ( 2 ) 发送方和接受方进程必须有权存取一个时间参照，比如实时时钟。 ( 3 ) 发送方进程必须能够调整接收方进程侦查共享属性的变化所用的响应 时间。 ( 4 ) 必须存在某种机制，使发送方和接收方进程能够启动隐蔽通信并正确 给事件排序。该机制可能是另一条较小宽带的隐通道。 对于p c 机来说，系统中至少处理器是共享的，因此系统中运行的各个进程 至少存在一个共享属性c p u 的响应时间。接收方进程通过监视时钟就能检测 到响应时间的变化。 1 1 2 隐通道搜索方法 隐通道的存在对信息系统的安全构成了巨大的威胁。因此，对高安全等级的 安全操作系统，各种标准都将隐通道分析作为一项评估条件。1 9 8 3 年，美国国 2 江苏大学硕士研究生毕业论文 防部在其发布的可信计算机系统评估准贝j j ( t c s e c ) 1 9 j 中，最早明确地提出隐通道 的问题，并规定在b 2 级及以上的高等级可信系统设计和开发过程中，必须进行 隐通道分析。t c s e c 标准将隐通道列入评估指标之后，1 9 9 9 年i s o 把可信计算 机系统评估准则c c 2 0 正式批准为国际标准，规定e a l 5 及以上安全级的安全软 件系统必须通过隐通道分析。另外，我国的g b 厂r 1 8 3 3 6 、欧洲的l s o i e c1 5 4 0 8 ， 加拿大的c t c p e c 等，也均把是否通过隐通道分析作为评估一个高等级安全系 统的硬性指标。 表1 - 1已有隐通道搜索方法的优缺点 分析法优点缺点 语法信l 、 可以用一种相对简单的方法自动 1 、 容易找i f ；错误的非法信息流( 需要额外通过手_ t 语义 息流分实现；分析米消除) ； 析法 2 、 既可用于项级形式化描述规范， 2 、 不适于非形式化说明： 也可以用于源代码分析；3 、不能帮助确定放置隐通道处理代码的t c b 位置； 3 、可以以逐步递增的方式用于单个4 、不适用于无传递性安全策略的系统。 函数和t c b 原语； 4 、在特定的规范描述( 或代码) 中， 不会遗漏任何可能导致隐通道的 信息流向。 共享资l 、可用于形式化或非形式化t c b 软1 、不能证明个别的t c b 原语( 或原语对) 是安全的( 也 源矩阵 硬件规范，也可用于t c b 源代码；就是说，不存在非法的信息流) ，这就导致系统中增加 法 2 、不用区分时间隐通道和存储隐通新的t c b 功能时分析更复杂； 道，原则上，它对两者都适用( 但2 、共享资源矩阵法可能会找出一些在信息流分析法中可 是，在搜索时间隐通道时不能提供以自动消除的隐通道； 一些特别的帮助) ； 3 、 虽然共享资源矩阵法可用来进行源代码分析，但是给 3 、对在矩阵中的内部t c b 变最不要t c b 源代码自动构造共享资源矩阵( 到目前为止，这是 求分配安全级别，凶此，消除了错最耗费时问和精力的工作) 的工具至今不存在，而对源 误的非法信息流的一个主要来源。代码手工使用该方法进行分析很容易出错。 无干扰1 、既可用于t c b 顶级形式化描述规1 、它可以基于形式化的t c b 项层描述，也可以基于源代 分析法 范也可用于源代码；码，但只能基于两者之一，而不能同时对这两者进行分 2 、可以避免发现假的非法信息流；析； 3 、 可增量地用于单个的t c b 函数字2 、对于较大规模的t c b 来说，手工使用无干扰分析法可能 和原语。不可行，而目前还没有适用于较大规模系统的自动化分 析- t 具； 3 、无干扰分析是“乐观的”，也就是说，它试图证明在t c b 描述或源代码中不出现十扰。 基于源可用于所有已经实现的系统，克服了 1 、代码量巨大，涉及的变量众多，程序流程复杂，即便在 代码搜有些系统缺少形式化项层说明的问题系统开发过程中遵循了良好的软件i t 程规范，依然很难 索方法 理解。 2 、重新设计系统或者部分修改设计牵涉很大。 隐通道的分析主要包括隐通道搜索、隐通道带宽的计算与测量、隐通道消除 江苏大学硕士研究生毕业论文 三方面。其中隐通道的搜索是隐通道分析中最为基础和最为重要的一环。目前， 国内外学者对隐通道的搜索问题作了大量的研究，提出了无干扰分析法【1 0 , 1 1 , 1 2 】、 语法信息流分析法【1 3 , 1 4 】、共享资源矩阵法1 1 5 , 1 6 , 1 7 j ，和源代码分析澍1 8 , 1 9 , 2 0 1 等。其 中无干扰分析法是基于无干扰模型提出的，它将信息流抽象成不同的状态然后对 状态转换的过程中进行隐通道分析；语法信息流分析法与无干扰分析法类似，它 能找出系统存在的存储隐通道，但不能检测出时间隐通道：共享资源矩阵分析法 在基于存储控制模型的基础提出的，它通过矩阵数据结构对共享资源进行隐通道 搜索；源代码分析法是直接针对系统源代码进行隐通道搜索的方法，但由于大型 系统的源代码复杂难懂，且需要手工操作分析源代码中的信息流，因此对分析人 员专业水平要求相当高。 上述的各种搜索方法都是从隐通道的某个侧而出发，揭示隐通道其中内在规 律，因此这些方法存在各自的优点和不足。上面表1 1 对主要的搜索方法进行总 结归纳。 1 2 研究现状 在所有的隐通道搜索方法中，语法信息流分析法易于进行自动分析并且不会 漏掉可能产生隐通道，而无干扰方法则是一种理论上严谨的形式化方法，它描述 系统实际运行转换过程，是一种动态的搜索方法且可以避免源代码分析方法和共 享资源矩阵法出现伪隐通道情况，因此语法信息流分析方法和无干扰分析方法一 直受到国内外研究者的广泛关注。 d o r o t h ye d e n n i n g 于1 9 7 6 年提出语法信息流分析法【2 1 】来对隐通道进行搜 索，随后s h i g e t ak u n i n o b u 、t a k e t o s h is a k u r a b a 和y i nl i u 等人在此基础上对语 法信息流分析法进行改进【2 2 ，2 3 ，2 4 1 。 语法信息流方法的基本思想可以概括为：首先引入一个基于格关系的信息流 模型，然后将信息流语义附加在每条语句之后，最后比较附加的信息流是否满足 信息流模型表示的安全策略。该方法的主要问题在于信息流合法性的判断均是建 立在一个格模型的基础上，而格关系满足传递性，这使得安全策略也满足传递性。 例如，如果a 到b 和b 到c 的信息流动是合法的，那么传递性保证a 到c 的信息流 动也是合法的。换句话讲，我们不需要考察a 到c 的信息流动的合法性。然而事 4 江苏大学硕士研究生毕业论文 实上有很多高安全系统的安全策略并不满足传递性，典型的如通道控制策略，而 传统的语法信息流分析方法无法解决具有非传递性安全策略的隐通道搜索问题 【2 5 l o 19 8 2 年g o g u e n 和m e s e g u e r 首次引入基于信息流分析的无干扰方法1 2 6 1 来控 制确定型系统中信息的直接流动和间接流动。该方法首先定义系统中合法的信息 流动，即无干扰，具体表现为系统中不存在高安全级用户的信息流动，当且仅当 低安全级用户不应当知道高安全级用户的任何动作。然后通过分析系统是否满足 无干扰属性来判断有无非法的信息流。接着在大量对无干扰方法进行研究过程中 发现，存在一些系统是安全的，但却不满足已有的无干扰属性，因此研究者们在 无干扰属性的基础上相继提出广义无干扰属性、不可推断属性、广义不可推断属 性、前向可修正属性和不可演绎属性等安全性质。 不可推断属性( n o i n f e r e n c e ) 是由o ，h e l l o r a n1 2 7 1 提出的，它的基本思想是分 离低级别安全动作和高级别安全动作，非形式地说，不可推断属性要求进程的迹 在删除所有高级别动作之后，仍是该进程的一个迹。 不可推断属性不仅保护进程的高级别输入动作，而且还保护进程的高级别输 出动作。然而，实际中存在一些系统只需保护进程高级别输入动作，对高级输出 动作不做要求。针对上述问题，m c l e a n 在不可推断属性的基础上提出广义不可 推断属性( g e n e r a l i z e dn o n i n f e r e n c e ) 1 2 8 】，它是一种仅保护高级别输入动作的信 息流属性。 广义不可推断属性只要求分离出高级别输入动作，即要求进程的迹在删除所 有高级别输入动作之后，仍然是该进程的迹。广义不可推断属性比不可推断属性 弱，是一种弱不可推断性。 广义无干扰属性( g e n e r a l i z e dn o n i n t e r f e r e n c e ) 是m c c u l l o u g h 提出的一种适 用不确定型系统的安全属性【2 9 ，3 0 】，它的主要思想是高级别输入动作的改变不能影 响低级别用户的观察结果，即任意插入或者删除高级别输入动作后，低级别用户 的观察结果是一样的。广义不可推断属性和广义无干扰都是高级别动作的改变不 能引起低级别用户的观察发生改变，但广义无干扰属性比广义不可推断属性强。 前向可修正属性( f o r w a r dc o r r e c t a b i l i t y ) 是由j o i l s o n 【3 l 】提出的，是一种可 复合的安全属性。前向可修正属性要求若两个子系统是安全的，则由两个子系统 复合而成的系统也应该是安全的。 5 江苏大学硕士研究生毕业论文 上述安全属性的强弱关系如图1 1 所示，安全属性所在的圆越在内部则表明 该属性越强。 图卜1 信息流安全属性之间的关系 引入上述安全属性的最终目的是确保多级安全系统中没有相应的非法信息 流，因此如何验证系统满足安全属性一直是一个重要的议题。传统的安全属性验 证方法称为“展开方法 1 3 引。该方法首先是要构造一个“展开定理 ，然后基于 该定理将信息流安全属性这一全局约束归约到仅仅涉及单步状态转换的局部条 件的验证。该技术建立了系统安全与单个状态转换命令之问的关系，因此称为“展 开方法”。但是“展开方法 存在一个问题，它是可靠的，但并不是完备的，这 里可靠性是指如果局部条件得到满足，则可推断出系统满足安全属性，不完备是 指如果局部条件没有得到满足，则不能推断出系统不满足安全属性。 除了“展开方法”，国内外学者对无干扰属性还开发了其它一些验证方法。 d e e p a kd s o u z a i 3 3 j 等将广义无干扰属性的验证问题转化为自动机的语言包含问 题，此外r o nv a nd e rm e y d e n a 和c h e n y iz h a n 9 1 3 4 1 将不可演绎属性的验证问题转 化为自动机的语言包含问题，但是和“展开方法”一样，该方法是不完备的。 r o nv a n 将确定型系统上无干扰属性的验证归约为可达问题，进而可以借助于可 达性检测技术完成验证。訾小超1 3 5 】等通过研究有限自动机的特性来分析确定型 系统是否满足无干扰属性。然而后两种方法并不适用于广义无干扰属性、不可推 断属性、广义不可推断属性和前向可修正属性等。 1 3 研究内容及论文组织 本文的研究目标包括两大方面：一是针对传统语法信息流分析方法只能解决 6 江苏大学硕士研究生毕业论文 传递性安全策略的问题，提出一种新的语法信息流分析方法，使之在适用于传递 性安全策略的同时也能描述非传递安全性策略的情况。二是针对信息流安全属性 已有的“展开方法 和自动机语言包含方法的不完备性，提出广义不可推断属性 和前向可修正属性可靠又完备的验证方法。 由于格关系的传递性保证了传统的语法信息流分析中，只要每一条语句是安 全的，那么这些语句组成的整体程序也是安全的。换句话讲，传统的语法信息流 分析方法只需考察每一条独立的语句即可。但是对于不满足传递性的安全策略而 言，仅仅考虑每一条语句是不够的。例如，如果口到b 和b 到c 的信息流动是合 法的，且口到b 的信息流动发生在b 到c 的信息流动之前，那么存在日到c 的信息 流动。此时我们需要判断口到c 的信息流动是否合法。因此我们要提出一个适用 非传递安全策略的信息流分析方法，不仅需要考察每一条语句，还需要从整个程 序语句的执行顺序上考察信息的传递闭包。 由于广义不可推断、前向可修正等信息流安全属性是由不同的研究者提出， 他们是在不同模型上对这些安全属性进行定义和分析。因此，有必要使用统一的 模型来描述信息流安全属性，有利于对这些安全属性间进行分析和比较，为后面 提出安全属性的验证方法提供理论基础。目前，已有安全属性的描述模型主要包 括状态转换系统模型、事件系统模型、进程代数模型、迹语义模型等。与其它模 型相比，状态转换系统模型具有以下优点：( 1 ) 在实际系统中，安全策略大多是 以状态转移规则的形式进行描述的，极少用事件轨迹集合的方法来表示，安全策 略容易形式化为相应状态机模型的状态转移条件。( 2 ) 状态机模型简明易懂， 有成熟的研究理论，多数的证明框架和工具都是在有限状态机的基础上进行研 究。( 3 ) 在状态机模型中，系统可以增加时间因素。而在基于事件轨迹模型和进 程代数模型增加时间因素是困难的。因此本文采用状态转换系统模型对信息流安 全属性进行定义和分析，并在此基础上提出广义不可推断属性和前向可修正属性 的验证方法。 下面给出本文具体的研究内容： ( 1 ) 根据程序语句附加的信息流域，提出一种可以用来描述程序中信息流 发生时序关系的图结构一信息流时序图，通过对此结构进行信息传递闭包计算， 进一步提出适用于无传递性安全策略的语法信息流标识算法。 ( 2 ) 将前向可修正属性以及广义不可推断属性的定义转换到状态转换系统 7 江苏大学硕士研究生毕业论文 模型上，然后分析得到两个属性的一些性质。 ( 3 ) 提出不确定性系统行为等价的确定型系统双径双构造结构，在此基础 上，将前向可修正属性的验证归约为可达性问题，并给出具体的前向可修正属性 验证算法。 ( 4 ) 开发一种可靠且完备的广义不可推断属性的验证方法，通过逐步搜索 长度递增的使广义不可推断属性失效的反例来完成验证过程。进一步将验证过程 归约为量化布尔公式满足性求解问题，实现验证过程的符号化计算，提高验证方 法的时问效率和降低对内存空间的需求。 ( 5 ) 利用己提出的前向可修正属性、广义不可推断属性的验证算法，以磁 臂运动系统为例，分析该系统是否存在不符合上述两种属性的非法信息流。 论文组织如下： 第一章概述隐通道问题的产生背景及研究现状，归纳概括了隐通道的分析方 法，明确本文的研究目标和内容。 第二章介绍安全策略、向量布尔公式的一些基本概念，给出机密性安全策略、 量化布尔公式以及程序不同语句的信息流语义的形式化定义。 第三章分析各种程序结构的信息流语义，构造各结构的信息流时序图，并对 时序图分别进行初始一终止点简化和路径简化。然后，提出适用于非传递性安全 策略的语法信息流分析方法，并通过一个例子来搜索被验证系统中可能存在的隐 通道。 第四章分析基于状态转换系统模型的前向可修正属性的性质，介绍前向可修 正属性验证方法的思想，并给出具体的算法描述。 第五章分析广义不可推断属性的性质，提出广义不可推断属性确定型系统上 的单径双构造运算，通过双构造的图结构理论得出属性最短