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

摘要：

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

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

所属期刊栏目：49

分类号：TP309.2;TP309.7(计算技术、计算机技术)

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

在线出版日期：2013-01-21（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：2591-2602