Defining noninterference in the temporal logic of actions
Defining noninterference in the temporal logic of actions
复制标题
定义行动的时间逻辑中的不干涉
DOI：
10.1109/secpri.1996.502665
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
T. Fine
中科院分区：
文献类型：
--
作者：
T. Fine
隐蔽通道是多级安全 (MLS) 系统的一个关键问题。由于其微妙性，需要使用形式化方法来分析 MLS 系统是否存在隐蔽通道。本文描述了一种使用 Abadi & Lamport (1993) 的动作时序逻辑 (TLA) 来指定非干扰属性的方法。除了提供比以前的尝试更直观的不干扰定义之外，该方法还支持对包含隐蔽通道的系统进行分析，以证明其利用的局限性。在将本文给出的不干扰定义与先前的不干扰定义联系起来时，本文讨论了在 TLA 中形式化其他不干扰定义的方法。最后，本文讨论了如何将先前的规范细化和组合工作应用于 TLA 提供的框架内的无干扰问题。
Covert channels are a critical concern for multilevel secure (MLS) systems. Due to their subtlety, it is desirable to use formal methods to analyze MLS systems for the presence of covert channels. This paper describes an approach for using Abadi & Lamport's (1993) temporal logic of actions (TLA) to specify noninterference properties. In addition to providing a more intuitive definition of noninterference than previous attempts, this approach also supports the analysis of systems that do contain covert channels to demonstrate limitations on their exploitations. In relating the definition of noninterference given in this paper to prior definitions of noninterference, this paper discusses ways in which other definitions of noninterference can be formalized in TLA, too. Finally, this paper discusses how prior work on specification refinement and composition might be applied to the noninterference problem within the framework provided by TLA.