Semantics for Interactive Sequential Systems and Non-Interference Properties

TitleSemantics for Interactive Sequential Systems and Non-Interference Properties
Publication TypeJournal Article
Year of Publication2011
AuthorsLee, MD, D'Argenio, PR
JournalCLEI Electron. J.
Volume14
Issue3
AbstractAn interactive system is a system that allows communication with the users. This communication is modeled through input and output actions. Input actions are controllable by a user of the system, while output actions are controllable by the system. Standard semantics for sequential system [1,2], are not suitable in this context because they do not distinguish between the different kinds of actions. Applying a similar approach to the one used in [2] we define semantics for interactive systems. In this setting, a particular semantic is associated with a "notion of observability". These notions of observability are used as parameters of a general definition of non-interference. We show that some previous versions of the non-interference property based on traces semantic, weak bisimulation and refinement, are actually instances of the observability-based non-interference property presented here. Moreover, this allows us to show some results in a general way and to provide a better understanding of the security properties.
URLhttp://www.clei.cl/cleiej/paper.php?id=228
PDF (Full text):