Defining noninterference in the temporal logic of actions

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