信息流安全属性算术验证的研究

多级安全系统中，机密数据的泄漏本质上是信息的非法流动。信息流安全属性刻画了不同安全级主体之间合法的信息流动。在系统应用之前，验证其满足信息流安全属性，可以排除各种隐蔽数据泄漏，保护数据的机密性。传统的安全属性验证方法验证的仅仅是属性成立的一个充分非必要条件，且仅适用于部分属性。本项目旨在面向多级安全系统，研究一种完备的、标准的且可符号化计算的信息流安全属性验证方法。主要内容包括：以反例搜索和归纳证明为主要技术手段，研究基于证伪和证真方法的验证安全属性的基本策略；从信息流安全属性定义模式的共性出发，研究一种标准化的方式来定义反例，计算最短反例的上界，以及构造归纳证明中的不变量；研制一套算法将反例搜索和归纳证明问题归约为布尔公式满足性求解问题，并借助于满足性求解程序完成验证过程的符号化计算。符号化计算不仅可以提高验证的效率，而且通过对系统空间进行紧致表示，降低了对存储空间的需求。

多级安全系统中，机密数据的泄漏本质上是信息的非法流动。信息流安全属性刻画了不同安全级主体之间合法的信息流动。在系统应用之前，验证其满足信息流安全属性，可以排除各种隐蔽数据泄漏，保护数据的机密性。传统的安全属性验证方法验证的仅仅是属性成立的一个充分非必要条件，且仅适用于部分属性。本项目面向多级安全系统，从算术验证的完备性、状态空间约简、非法信息流的搜索三个方面对信息安全属性的验证进行了系统的研究。.首先对无干扰、广义无干扰、多域无干扰、非传递无干扰、广义不可推断五个属性提出了一种完备的验证方法。基本的验证思想是以反例搜索和归纳证明为主要技术手段，研究了一种标准化的方式来定义反例，计算最短反例的上界，以及构造归纳证明中的不变量。完备算法的提出有效解决了信息流安全属性的特征刻画和验证问题。.其次针对验证大规模多级安全系统时出现的状态空间爆炸问题，在状态空间约简方面提出了三种有效的约简技术：1）研制了一套算法将反例搜索和归纳证明问题归约为布尔公式满足性求解问题，进而借助于满足性求解程序完成验证过程的符号化计算。符号化计算不仅可以提高验证的效率，而且通过对系统空间进行紧致表示，降低了对存储空间的需求；2）对马尔科夫链、马尔科夫决策过程、概率时间自动机三种模型，分别提出了基于局部空间的信息流属性的验证方法，包括局部空间上信息流安全属性的定义与正确性证明、限制搜索深度情况下的验证算法。这种方法的主要优势在于无需遍历与所验证属性无关的状态空间，从而达到约简状态空间的目的；3）对刻画信息流安全属性的逻辑系统概率认知逻辑与概率实时认知逻辑，分别提出了二值和三值抽象技术，实现了等价状态的合并，使得信息流安全属性的验证可以在由等价状态形成的空间上完成。.最后，以Petri网作为形式化建模工具,给出了Petri网中隐蔽信息流存在的判定条件。提出了该条件成立的两种网结构，进而可以在语法层次上预先判断隐蔽信息流的存在性，并使由此类结构引起的隐蔽信息流在系统的设计阶段得以避免。开发了一种基于Petri网可达图的隐蔽信息流存在性判定算法，算法遵循无干扰方法的思想，但是避免了无干扰方法中等价状态的区分和展开定理的使．另外，算法采用深度优先搜索的策略，避免了Petri网全局可达图的构造。对复杂的安全系统，分析了子系统的各种组合运算对隐蔽信息流存在性的影响，降低了大规模系统分析的复杂度。