非传递广义无干扰属性符号化算术验证方法

广义无干扰属性规约了多级安全系统中具有传递性质的安全策略,而对于不满足传递性的策略则无法刻画.文中首先对广义无干扰属性进行扩展,提出了非传递广义无干扰属性的概念,进而可以规约无传递性的安全策略.文中提出了一种可符号化实现的非传递广义无干扰属性验证方法.该方法主要基于证伪和证真的基本验证策略,通过集成反例搜索和归纳证明完成属性的验证.该方法适用于广义无干扰属性,同时有效地解决了基于"展开定理"的证明方法的不完备性.进一步将反例搜索和归纳证明问题归约为布尔公式满足性求解问题,并借助于满足性求解程序完成验证过程的符号化计算.符号化计算通过对系统空间进行紧致表示,降低了对存储空间的需求,而且可以提高验证的时间效率.

基于Petri网的信息流安全属性的分析与验证

信息流安全属性的定义均基于不同的语义模型,很难作出比较,以Petri网作为描述安全系统的统一模型,在Petri网上定义四种常见的安全属性,并分析它们之间的逻辑关系。在信息流安全属性验证方面,传统的方法称为展开方法,该方法适用于确定型系统,而对于非确定型系统,该方法是可靠的,但不完备。进一步对Pe-tri网上已经定义的四种属性给出可靠完备的验证算法,并开发出相应的验证工具。最后通过实例说明了验证方法在搜索隐通道方面的应用。