| 广义不可推断属性符号化算术验证的研究 |
| |
| 引用本文： | 周从华,吴海玲,鞠时光. 广义不可推断属性符号化算术验证的研究[J]. 计算机研究与发展, 2012, 49(12): 2591-2602 |
| |
| 作者姓名： | 周从华 吴海玲 鞠时光 |
| |
| 作者单位： | 江苏大学计算机科学与通信工程学院 江苏镇江212013 |
| |
| 基金项目： | 国家自然科学基金项目，江苏省自然科学基金项目，教育部博士学科点专项科研基金项目 |
| |
| 摘 要： | ![]()
多级安全系统中机密数据的泄漏本质上是信息的非法流动.广义不可推断属性刻画了不同安全级主体之间合法的信息流动.在系统应用之前,验证其满足广义不可推断属性,可以排除各种隐蔽数据泄漏,保护数据的机密性.传统的广义不可推断属性验证方法——"展开方法"——验证的仅仅是属性成立的一个充分非必要条件,因此是不完备的.基于证伪技术提出一种完备的广义不可推断属性验证方法,该方法通过逐步搜索长度递增的使广义不可推断属性失效的反例来完成验证过程.为确保搜索过程能正确终止,即方法的完备性,提出状态转换系统的双构造运算,并在此基础上基于图结构理论给出最短反例的上近似计算.进一步为提高验证方法的时间效率和降低对内存空间的需求,将反例搜索和上近似计算归约为量化布尔公式满足性求解问题,借助于高效的满足性求解程序完成属性的验证,实现了验证过程的符号化计算.最后通过一个磁臂隐通道的实例说明验证方法在实际的隐通道分析中的应用.
|
| 关 键 词： | 广义不可推断属性 信息流安全 量化布尔公式 多级安全系统 隐通道 |
Symbolic Algorithmic Verification of Generalized Noninference |
| |
| Zhou Conghua , Wu Hailing , Ju Shiguang. Symbolic Algorithmic Verification of Generalized Noninference[J]. Journal of Computer Research and Development, 2012, 49(12): 2591-2602 |
| |
| Authors: | Zhou Conghua Wu Hailing Ju Shiguang |
| |
| Affiliation: | (School of Computer Science and Telecommunication Engineering, Jiangsu University, Zhenjiang, Jiangsu 212013) |
| |
| Abstract: | ![]()
|
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
