%0 Journal Article
%T 前向可修正属性算术验证的研究
%A 吴海玲
%A 周从华
%A 鞠时光
%A 王基？
%J 计算机科学
%D 2011
%X 目前验证前向可修正属性的“展开方法”是不完备的，即当“展开定理”的局部条件不满足时，不能判断出系统不满足前向可修正属性。为此，提出一种基于状态转换系统的前向可修正属性验证方法，该方法将前向可修正属性的验证归约为可达性问题，进而可借助可达性检测技术完成属性的验证。该方法是完备的，且当属性不成立时，可以给出使属性失效的反例，反例的给出对非法信息流的消除和控制具有直接的帮助。最后，通过磁臂隐通道的例子说明了方法的有效性和实用性。
%K 前向可修正属性
%K 信息流
%K 无干扰
%K 状态转换系统
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=110321&flag=1