为保证计算机系统中的信息机密性,自主访问控制和强制访问控制策略在计算机多级安全系统中得到了广泛的应用。然而,实施了这两种策略的计算机系统仍存在安全隐患,如安全系统中的隐通道问题。高安全级进程可以利用隐通道向低安全级进程泄漏信息,对系统安全构成巨大威胁。因此,对高安全等级的安全操作系统,各种安全标准都要求进行隐通道分析。　　 信息流控制方法是应用广泛的隐通道搜索方法,包括语法信息流分析方法和语义信息流分析方法。传统的语法信息流分析方法均基于实施机密性安全策略的信息流格模型,而格关系的传递特性使得该方法不能用来分析实施无传递性安全策略的系统的安全性。无干扰分析方法是一种严谨的语义信息流分析方法,目前主要采用“展开技术”对信息流安全属性进行验证,但是验证这些安全属性的“展开方法”是可靠但并不是完备的,此外有一些安全属性不存在“展开条件”。　　 本文的主要研究内容包括:　　 1.针对格模型不能描述非传递安全性策略的问题,提出同时适用非传递性和传递性安全策略的语法信息流分析方法。首先将信息流语义附加在每条语句之后,然后定义一种称为信息流时序图的图结构来刻画信息流发生的时序关系,并给出基于源程序的信息流时序图的构造方法。接着提出删除规则来删除信息流图中多余的初始点、终止点和重复路径,并开发出一种基于时序图的隐蔽信息流的标识算法。另外,针对并发程序的并发特性,提出了一种简化信息流时序图的方法。在该方法下只要考虑并发进程之间特定的交互次序即可,而不需考虑所有可能的交互方式。　　 2.针对验证前向可修正属性的“展开方法”不完备的问题,提出一种可靠且完备的前向可修正属性验证方法。该方法根据前向可修正属性的特点,提出该属性相应的确定型系统的双径双构造,在双径双构造结构上分析前向可修正属性的性质,将前向可修正属性的验证归约为可达性问题,进一步给出该属性的验证算法。当属性不成立时,算法可以给出使属性失效的反例,从而解决前向可修正属性“展开方法”不完备性的问题。　　 3.针对验证广义不可推断属性的“展开方法”不完备的问题,提出一种可靠且完备的广义不可推断属性的验证方法。该方法给出广义不可推断属性反例的定义,根据广义不可推断属性的特点,提出与该属性相应的确定型系统的单径双构造,并基于图结构理论得出该属性最短反例的上近似计算。然后采用证伪技术,通过逐步搜索长度递增的使广义不可推断属性失效的反例来完成验证过程,从而解决广义不可推断属性“展开方法”不完备性的问题。进一步为提高验证方法的时间效率和降低对内存空间的需求,将反例搜索和上近似计算归约为量化布尔公式满足性求解问题,借助于高效的满足性求解程序完成属性的验证,实现验证过程的符号化计算。