基于不干扰理论的信道控制策略及其自动化验证方法

摘要

通过研究信道与那些向其输入信息或从其获得信息的信息域之间直接或间接的干扰关系,来定义信道的语义和作用.明确描述和严格控制系统模块和进程之间的信息通道,有利于最大限度地保障模块或进程的完整性和可控性.所提出的信道控制策略正是基于上述目的.而针对信道控制策略复杂而不便于手工验证的特点,提出了基于通信顺序进程(CSP)的系统和策略描述方法以及基于FDR2的系统信息流策略自动化验证方法.该方法能够在少量的人工参与的情况下有效地分析信道控制策略,发现大部分存储隐蔽通道.