HOME | DEUTSCH | IMPRESSUM | KIT

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

[wasserrab10verify]Daniel Wasserrab, Denis Lohner, Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing, 6th International Verification Workshop - VERIFY-2010, 2010.

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.

Download

  [PDF]

BibTeX

Authors at the institute

Former Staff Member
Dr.-Ing. Daniel Wasserrab
Dipl.-Inform. Denis Lohner

Projects

Project
Quis-Custodiet