Proving concurrent noninterference

Andrei Popescu, Johannes Hölzl, Tobias Nipkow

Publikation: Beitrag in Buch/Bericht/KonferenzbandKonferenzbeitragBegutachtung

8 Zitate (Scopus)

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.

OriginalspracheEnglisch
TitelCertified Programs and Proofs - Second International Conference, CPP 2012, Proceedings
Seiten109-125
Seitenumfang17
DOIs
PublikationsstatusVeröffentlicht - 2012
Veranstaltung2nd International Conference on Certified Programs and Proofs, CPP 2012 - Kyoto, Japan
Dauer: 13 Dez. 201215 Dez. 2012

Publikationsreihe

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

Konferenz

Konferenz2nd International Conference on Certified Programs and Proofs, CPP 2012
Land/GebietJapan
OrtKyoto
Zeitraum13/12/1215/12/12

Fingerprint

Untersuchen Sie die Forschungsthemen von „Proving concurrent noninterference“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren