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

Symbolic algorithmic verification of intransitive generalized noninterference

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

Generalized noninterference can be used to formulate transitive security policies, but is unsuitable for intransitive security policies. We propose a new information flow security property, which we call intransitive generalized noninterference, that enables intransitive security policies to be specified formally. Next, we propose an algorithmic verification technique to check intransitive generalized noninterference. Our technique is based on the search for counterexamples and on the window induction proof, and can be used to verify generalized noninterference. We further demonstrate that the search of counterexamples and induction proof can be reduced to quantified Boolean satisfiability. This reduction enables us to use efficient quantified Boolean decision procedures to perform the check of intransitive generalized noninterference. It also reduces spatial requirement by representing the space compactly, and improves the efficiency of the verification procedure.