欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
多级安全系统中机密数据的泄漏本质上是信息的非法流动．广义不可推断属性刻画了不同安全级主体之间合法的信息流动．在系统应用之前，验证其满足广义不可推断属性，可以排除各种隐蔽数据泄漏，保护数据的机密性．传统的广义不可推断属性验证方法——“展开方法”——验证的仅仅是属性成立的一个充分非必要条件，因此是不完备的．基于证伪技术提出一种完备的广义不可推断属性验证方法，该方法通过逐步搜索长度递增的使广义不可推断属性失效的反例来完成验证过程．为确保搜索过程能正确终止，即方法的完备性，提出状态转换系统的双构造运算，并在此基础上基于图结构理论给出最短反例的上近似计算．进一步为提高验证方法的时间效率和降低对内存空间的需求，将反例搜索和上近似计算归约为量化布尔公式满足性求解问题，借助于高效的满足性求解程序完成属性的验证，实现了验证过程的符号化计算．最后通过一个磁臂隐通道的实例说明验证方法在实际的隐通道分析中的应用．
英文摘要：
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.
同期刊论文项目
同项目期刊论文
期刊信息
位置：