前向可修正属性算术验证的研究

摘要：

目前验证前向可修正属性的"展开方法"是不完备的,即当"展开定理"的局部条件不满足时,不能判断出系统不满足前向可修正属性.为此,提出一种基于状态转换系统的前向可修正属性验证方法,该方法将前向可修正属性的验证归约为可达性问题,进而可借助可达性检测技术完成属性的验证.该方法是完备的,且当属性不成立时,可以给出使属性失效的反例,反例的给出对非法信息流的消除和控制具有直接的帮助.最后,通过磁臂隐通道的例子说明了方法的有效性和实用性.

关键词：前向可修正属性、信息流、无干扰、状态转换系统

所属期刊栏目：38

分类号：TP309(计算技术、计算机技术)

资助基金：国家自然科学基金60773049;江苏大学高级人才科研启动基金07JDG014;江苏省高校自然科学基金08KJD520015;教育部博士点基金20093227110005

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

页数：共6页

页码：97-102