广义不可推断属性符号化算术验证的研究  

Symbolic Algorithmic Verification of Generalized Noninference

作　　者：周从华[1] 吴海玲[1] 鞠时光[1] 

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

出　　处：《计算机研究与发展》2012年第12期2591-2602,共12页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(61003288;61111130184;60773049);江苏省自然科学基金项目(BK2010192);教育部博士学科点专项科研基金项目(20093227110005)

摘　　要：多级安全系统中机密数据的泄漏本质上是信息的非法流动.广义不可推断属性刻画了不同安全级主体之间合法的信息流动.在系统应用之前,验证其满足广义不可推断属性,可以排除各种隐蔽数据泄漏,保护数据的机密性.传统的广义不可推断属性验证方法——"展开方法"——验证的仅仅是属性成立的一个充分非必要条件,因此是不完备的.基于证伪技术提出一种完备的广义不可推断属性验证方法,该方法通过逐步搜索长度递增的使广义不可推断属性失效的反例来完成验证过程.为确保搜索过程能正确终止,即方法的完备性,提出状态转换系统的双构造运算,并在此基础上基于图结构理论给出最短反例的上近似计算.进一步为提高验证方法的时间效率和降低对内存空间的需求,将反例搜索和上近似计算归约为量化布尔公式满足性求解问题,借助于高效的满足性求解程序完成属性的验证,实现了验证过程的符号化计算.最后通过一个磁臂隐通道的实例说明验证方法在实际的隐通道分析中的应用.In multi-level security systems the leakage of confidential data, is in essence, the illegal flow of information. Generalized noninference characterizes the legal information flow between subjects with different security levels. Before the security system is applied, verifying whether it satisfies generalized noninference can eliminate all kinds of hidden data leakage and protect the confidentiality of data. At present the traditional verification approach for generalized noninference, i. e. ＂unwinding＂, only checks a sufficient and non-neccessary condition making generalized noninference hold. Therefore the traditional approach is not complete. A complete verification approach for generalized noninference is proposed. It verifies generalized noninference by searching for counterexamples step by step. In order to guarantee the completeness of the approach, the double construction of finite state transition system is given, and based on the graph structure theory an approximate computation of the shortest counterexample is given. Further in order to increase the efficiency of the approach, the search of counterexamples and computation of the threshold are reduced to the quantified Boolean formula satisfiability problem. Then a symbolic verification procedure is established by a quantified Boolean formula solver. Finally, how to apply the approach to search for illegal information flow is explained by a case study of the disk-arm covert channel.

关 键 词：广义不可推断属性 信息流安全 量化布尔公式 多级安全系统 隐通道 

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