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

Symbolic algorithmic verification of intransitive generalized noninterference

作　　者：周从华[1] 刘志锋[1] 吴海玲[1] 陈松[1] 鞠时光[1] 

机构地区：[1]江苏大学计算机科学与通信工程学院,镇江212013

出　　处：《中国科学：信息科学》2011年第11期1310-1327,共18页Scientia Sinica(Informationis)

基　　金：国家自然科学基金(批准号:60773049;61003288);江苏省自然科学基金(批准号:BK2010192);江苏大学高级人才科研启动基金(批准号:07JDG014);江苏省高校自然科学基金(批准号:08KJD520015)资助项目

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

关 键 词：非传递广义无干扰属性 量化布尔公式 符号化验证 多级安全 

分 类 号：TP309.2[自动化与计算机技术—计算机系统结构]