Decidability and proof systems for language-based noninterference relations
2006 (English)In: SIGPLAN notices, ISSN 0362-1340, E-ISSN 1558-1160, Vol. 41, no 1, 67-78 p.Article in journal (Refereed) Published
Noninterference is the basic semantical condition used to account for confidentiality and integrity-related properties in programming languages. There appears to be an at least implicit belief in the programming languages community that partial approaches based on type systems or other static analysis techniques are necessary for noninterference analyses to be tractable. In this paper we show that this belief is not necessarily true. We focus on the notion of strong low bisimulation proposed by Sabelfeld and Sands. We show that, relative to a decidable expression theory, strong low bisimulation is decidable for a simple parallel while-language, and we give a sound and relatively complete proof system for deriving noninterference assertions. The completeness proof provides an effective proof search strategy. Moreover, we show that common alternative noninterference relations based on traces or input-output relations are undecidable. The first part of the paper is cast in terms of multi-level security. In the second part of the paper we generalize the setting to accommodate a form of intransitive interference. We discuss the model and show how the decidability and proof system results generalize to this richer setting.
Place, publisher, year, edition, pages
2006. Vol. 41, no 1, 67-78 p.
security, theory, verification, multi-level security, information flow, noninterference, language-based security, intransitive noninterference, secure information-flow, programs, confidentiality
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-15461DOI: 10.1145/1111320.1111044ISI: 000235615800008ScopusID: 2-s2.0-33745842281OAI: oai:DiVA.org:kth-15461DiVA: diva2:333502
QC 20100525 QC 201110052010-08-052010-08-052011-10-05Bibliographically approved