基于不干扰理论的隔离语义描述及隔离策略的自动化验证方法研究

隔离有助于阻止信息泄露或被篡改、错误或失败被传递等.利用不干扰理论给出了隔离的精确语义,以利于分析和制定系统的隔离策略;利用通信顺序进程CSP来定义上述隔离语义,并给出一个系统满足给定隔离策略的判定断言,以利于借助形式化验证工具FDR2来实现系统内隔离策略的自动化验证.以基于虚拟机的文件服务监控器为例,展示了如何利用CSP来建模一个系统及其隔离策略以及如何利用FDR2来验证该系统模型满足给定的隔离策略.