Defining Noninterference in the Temporal Logic of Actions

11 years 9 months ago
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.
Todd Fine
Added 07 Aug 2010
Updated 07 Aug 2010
Type Conference
Year 1996
Where SP
Authors Todd Fine
Comments (0)