计算机软硬件系统已广泛应用于商业以及安全至关重要的领域,这些系统一旦出错,将给人类带来不可估量的损失。模型检测是目前一种比较有效的验证系统正确性和可靠性的方法。模型检测主要通过遍历有限状态机来检验时态逻辑公式的正确性,然而在实际应用中,并发系统的状态空间随着并发分量的增加呈指数级增长,即状态空间爆炸问题,因此约简状态空间对提高模型检测的效率至关重要。论文研究了两种状态空间约简技术来缓解状态爆炸问题。对高等级的安全操作系统,目前各种标准都要求对其进行隐通道分析。1985年,美国国防部发布了橘皮书TCSEC明确规定,在对B2级以上的高等级安全操作系统进行评估时,必须要进行隐通道分析。我国国家标准GB/T 18336-2001和GB17859-1999都有类似的规定。因此隐通道的搜索对提高操作系统的安全等级至关重要。论文探讨了如何借助于模型检测技术完成一类特殊隐通道的搜索,以及信息流安全属性的验证。具体来讲,论文的工作包括以下几个方面：1.CTL的渐增模型检测技术目前模型检测算法大致可以分为两类：符号化的全局检测算法和局部检测算法。全局检测算法的优点在于利用二叉决策图对状态空间进行紧致表示,缺点是需要计算不可达的状态空间。局部检测算法的优点在于状态的产生是由需求驱动的,缺点是对状态空间的表示是显式的。因此有效结合这两种方法可以缓解状态空间爆炸问题。论文提出一种CTL渐增模型检测技术,基本思想是：给定一个有限状态转换系统,利用基于二叉决策图的符号化技术逐步计算它的可达状态空间,并在可达状态空间内搜索CTL公式成立的证据或者失效的反例。定义了CTL的限界语义,并证明了限界语义是对无界语义的逼近,保证了方法的正确性。给出了限界语义下CTL算子的不动点刻画,保证了符号化技术可以实施的前提。实验结果表明,与符号化的全局方法和显式的局部方法相比,该方法可以有效缓解状态空间爆炸问题,在一定程度上拓展了可检测的系统的规模。2.概率实时时态认知逻辑模型检测中的抽象技术概率实时时态认知逻辑在传统的时态逻辑的基础上融入概率、实时和知识,因此可以表示与这些因素相关的重要属性。抽象技术是目前比较成功地缓解状态空间爆炸的技术。本文对概率实时时态认知逻辑模型检测中的抽象技术进行了系统地研究。主要工作有：1)对概率实时时态认知逻辑中的实时部分,采用抽象离散时钟赋值隐式构造概率实时解释系统状态空间的时钟区域,从而得到概率实时解释系统状态空间的有限形式；对于认知算子,给出了两个抽象状态关于智体认知等价的定义,这样就可以把满足该定义中约束的抽象状态进行合并,使其成为一个等价类,从而进一步简化概率实时解释系统的状态空间。2)利用上面给出的抽象技术,从概率实时解释系统的原始模型推演出了对应的抽象模型,给出了抽象模型上概率实时时态认知逻辑的语义,并证明了抽象模型是原始模型的上近似。3.推理通道的搜索论文挖掘了一类特殊的隐通道(称为推理通道),在该通道中信息转移是一个逻辑过程,依赖于系统的运行环境,因此已有的隐通道标识方法无法搜索推理通道。本文基于程序的动态行为,将程序视为一个有限状态机,利用状态的演化过程来捕捉推理通道发生的特征,并在此基础上设计了推理通道的标识方法。具体工作包括两个方面：1)首先对由两个主体和一个客体组成的系统,利用有限状态机刻画两个主体对客体交互执行的操作,并在此基础上演绎出以某个变量为载体发生推理通道的操作序列的特征,进一步利用线性时态逻辑LTL刻画了这种特征,使得可以借助于模型检测技术完成推理通道的标识。2)对由多个主体与一个客体组成的系统,首先从访问序列、访问变量、访问方式三个方面分析了第三方主体的行为对推理通道的影响,得出了第三方主体行为不破坏推理通道发生的条件。依据该条件可将访问序列分解成多个独立的序列。对于每个独立的序列借助于模型检测技术进行推理通道的标识。4.隐通道的本质是非法信息流,非传递无干扰属性刻画了一类非法信息流,验证安全系统满足非传递无干扰属性可以确保系统中没有此类信息流。目前对非传递无干扰属性还没有有效的验证方法,论文提出了一种符号化的算术方法来验证非传递无干扰。验证方法的可靠性和完备性依赖于完全界的计算,完全界必须满足：系统不满足非传递无干扰,则一定存在长度不超过界的反例。我们基于图结构理论给出了最小完全界的上近似计算。鉴于近年来,命题公式的满足性求解程序在软硬件分析方面获得了成功地运用,进一步将反例搜索和完全界的计算归约为命题公式的满足性求解问题,实现了验证过程的符号化计算,进而为大规模多级安全系统的验证提供了一种有效的途径。