-
题名广义不可推断属性符号化算术验证的研究
被引量：1
- 1
-
-
作者
周从华
吴海玲
鞠时光
-
机构
江苏大学计算机科学与通信工程学院
-
出处
《计算机研究与发展》
EI
CSCD
北大核心
2012年第12期2591-2602,共12页
-
基金
国家自然科学基金项目(61003288
61111130184
+2 种基金
60773049)
江苏省自然科学基金项目(BK2010192)
教育部博士学科点专项科研基金项目(20093227110005)
-
文摘
多级安全系统中机密数据的泄漏本质上是信息的非法流动.广义不可推断属性刻画了不同安全级主体之间合法的信息流动.在系统应用之前,验证其满足广义不可推断属性,可以排除各种隐蔽数据泄漏,保护数据的机密性.传统的广义不可推断属性验证方法——"展开方法"——验证的仅仅是属性成立的一个充分非必要条件,因此是不完备的.基于证伪技术提出一种完备的广义不可推断属性验证方法,该方法通过逐步搜索长度递增的使广义不可推断属性失效的反例来完成验证过程.为确保搜索过程能正确终止,即方法的完备性,提出状态转换系统的双构造运算,并在此基础上基于图结构理论给出最短反例的上近似计算.进一步为提高验证方法的时间效率和降低对内存空间的需求,将反例搜索和上近似计算归约为量化布尔公式满足性求解问题,借助于高效的满足性求解程序完成属性的验证,实现了验证过程的符号化计算.最后通过一个磁臂隐通道的实例说明验证方法在实际的隐通道分析中的应用.
-
关键词
广义不可推断属性
信息流安全
量化布尔公式
多级安全系统
隐通道
-
Keywords
generalized noninference
information flow security
quantified Boolean formula
multilevel security system
covert channel
-
分类号
TP309.2
[自动化与计算机技术—计算机系统结构]
TP309.7
[自动化与计算机技术—计算机科学与技术]
-
