[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
BibTeX
Authors at the institute
Projects