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 Lamport's TLA to specify noninterference properties. In addition to providing a more intuitive definition of noninterference than previous attempts, this approach also supports analysis of systems that do contain covert channels to demonstrate limitations on their exploitations. In relating the definition of noninterference given here to prior definitions of noninterference, this paper discusses ways in which other definitionsof 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.

• Type: Conference
• Year: 1996
• Where: SP
• Authors: Todd Fine
• Keywords: Covert Channels, Lamport's TLA, MLS Systems, Security Privacy, SP 1996