Proving concurrent noninterference

Andrei Popescu, Johannes Hölzl, Tobias Nipkow

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

8 Scopus citations

Abstract

We perform a formal analysis of compositionality techniques for proving possibilistic noninterference for a while language with parallel composition. We develop a uniform framework where we express a wide range of noninterference variants from the literature and compare them w.r.t. their contracts: the strength of the security properties they ensure weighed against the harshness of the syntactic conditions they enforce. This results in a simple implementable algorithm for proving that a program has a specific noninterference property, using only compositionality, which captures uniformly several security type-system results from the literature and suggests a further improved type system. All formalism and theorems have been mechanically verified in Isabelle/HOL.

Original languageEnglish
Title of host publicationCertified Programs and Proofs - Second International Conference, CPP 2012, Proceedings
Pages109-125
Number of pages17
DOIs
StatePublished - 2012
Event2nd International Conference on Certified Programs and Proofs, CPP 2012 - Kyoto, Japan
Duration: 13 Dec 201215 Dec 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7679 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference2nd International Conference on Certified Programs and Proofs, CPP 2012
Country/TerritoryJapan
CityKyoto
Period13/12/1215/12/12

Fingerprint

Dive into the research topics of 'Proving concurrent noninterference'. Together they form a unique fingerprint.

Cite this