Change search
ReferencesLink to record
Permanent link

Direct link
Decidability and proof systems for language-based noninterference relations
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5432-6442
2006 (English)In: SIGPLAN notices, ISSN 0362-1340, E-ISSN 1558-1160, Vol. 41, no 1, 67-78 p.Article in journal (Refereed) Published
Abstract [en]

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.
Keyword [en]
security, theory, verification, multi-level security, information flow, noninterference, language-based security, intransitive noninterference, secure information-flow, programs, confidentiality
National Category
Computer and Information Science
URN: urn:nbn:se:kth:diva-15461DOI: 10.1145/1111320.1111044ISI: 000235615800008ScopusID: 2-s2.0-33745842281OAI: diva2:333502
QC 20100525 QC 20111005Available from: 2010-08-05 Created: 2010-08-05 Last updated: 2011-10-05Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Dam, Mads
By organisation
Theoretical Computer Science, TCS
In the same journal
SIGPLAN notices
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 42 hits
ReferencesLink to record
Permanent link

Direct link