论文部分内容阅读
提出系统动作对信息域的不干扰概念，并在此基础上将不干扰模型推广到非确定系统．由于基于系统动作的不干扰概念简化了系统动作序列的提取操作，该模型的单步展开条件具有简洁的形式并易于理解和使用．推广后的不干扰模型不仅能够验证静态信息流策略，还可以验证各种动态信息流策略．最后设计了一个基于动态标记的访问控制模型，并在该模型中定义了读、写、执行等操作的具体语义，然后利用不干扰模型对其安全性进行了形式化验证．