KIT | KIT-Bibliothek | Impressum | Datenschutz

Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing

Wasserrab, Daniel; Lohner, Dennis

Abstract:
We present a machine-checked correctness proof for information flow noninterference based on interprocedural slicing. It reuses a correctness proof of the context-sensitive interprocedural slicing algorithm of Horwitz, Reps, and Binkley. The underlying slicing framework is modular in the programming language used; by instantiating this framework the correctness proofs hold for the respective language, without reproving anything in the correctness proofs for slicing and noninterference. We present instantiations with two different languages to show the applicability of the framework, and thus a verified noninterference algorithm for these languages. The formalization and proofs are conducted in the proof assistant Isabelle/HOL.


Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Jahr 2010
Sprache Englisch
Identifikator KITopen-ID: 1000027776
Erschienen in 6th International Verification Workshop - VERIFY-2010, Edinburgh, July 20-21, 2010
Projektinformation KASTEL I (BMBF, 01BY1172 / 16BY1172)
Externe Relationen Siehe auch
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page