Sciweavers

Share
POPL
2006
ACM

Decidability and proof systems for language-based noninterference relations

11 years 2 days ago
Decidability and proof systems for language-based noninterference relations
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...
Mads Dam
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where POPL
Authors Mads Dam
Comments (0)
books