一个非确定系统的不干扰模型

摘要

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