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

• 作者: 刘志锋 吴海玲 周从华 陈松 鞠时光
• 来源期刊: 中国科学（信息科学）
• 关键词: 非传递广义无干扰属 性量化布尔公式 符号化验证 多级安全
• 年，卷（期）: 2011,（11）
• 所属期刊栏目: 论文
• 页码范围: 1310-1327
• 页数: 18页
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	鞠时光	江苏大学计算机科学与通信工程学院	159	1685	21.0	34.0
2	吴海玲	江苏大学计算机科学与通信工程学院	4	2	1.0	1.0
3	周从华	江苏大学计算机科学与通信工程学院	46	193	7.0	11.0
4	刘志锋	江苏大学计算机科学与通信工程学院	29	118	5.0	10.0
5	陈松	江苏大学计算机科学与通信工程学院	21	121	7.0	10.0