Non-Interference for Deterministic Interactive Programs

David Clark, Sebastian Hunt

Research output: Chapter in Book/Report/Conference proceedingConference paper

21 Citations (Scopus)

Abstract

We consider the problem of defining an appropriate notion of non-interference (NI) for deterministic interactive programs. Previous work on the security of interactive programs by O'Neill, Clarkson and Chong (CSFW 2006) builds on earlier ideas due to Wittbold and Johnson (Symposium on Security and Privacy 1990), and argues for a notion of NI defined in terms of strategies modelling the behaviour of users. We show that, for deterministic interactive programs, it is not necessary to consider strategies and that a simple stream model of the users' behaviour is sufficient. The key technical result is that, for deterministic programs, stream-based NI implies the apparently more general strategy-based NI (in fact we consider a wider class of strategies than those of O'Neill et al). We give our results in terms of a simple notion of Input-Output Labelled Transition System, thus allowing application of the results to a large class of deterministic interactive programming languages.
Original languageEnglish
Title of host publicationUnknown
Place of PublicationBERLIN
PublisherSpringer
Pages50 - 66
Number of pages17
Volume5491 LNCS
ISBN (Print)978-3-642-01464-2
Publication statusPublished - 2009
Event5th International Workshop on Formal Aspects in Security and Trust - Malaga, Spain
Duration: 9 Oct 200810 Oct 2008

Publication series

NameFORMAL ASPECTS IN SECURITY AND TRUST

Conference

Conference5th International Workshop on Formal Aspects in Security and Trust
Country/TerritorySpain
CityMalaga
Period9/10/200810/10/2008

Fingerprint

Dive into the research topics of 'Non-Interference for Deterministic Interactive Programs'. Together they form a unique fingerprint.

Cite this