# Conference Papers: On PDG-Based Noninterference and its Modular Proof

 [wasserrab09plas] Daniel Wasserrab, Denis Lohner, Gregor Snelting, On PDG-Based Noninterference and its Modular Proof, Proceedings of the 4th Workshop on Programming Languages and Analysis for Security, pp. 31--44, ACM, June 2009.

## Abstract

We present the first machine-checked correctness proof for information flow control (IFC) based on program dependence graphs (PDGs). IFC based on slicing and PDGs is flow-sensitive, context-sensitive, and object-sensitive; thus offering more precision than traditional approaches. While the method has been implemented and successfully applied to realistic Java programs, only a manual proof of a fundamental correctness property was available so far. he new proof is based on a new correctness proof for intraprocedural PDGs and program slices. Both proofs are formalized in Isabelle/HOL. They rely on abstract structures and properties instead of concrete syntax and definitions. Carrying the correctness proof over to any given language or dependence definition reduces to just showing that it fulfills the necessary preconditions, thus eliminating the need to develop another full proof. We instantiate the framework with both a simple while language and Java bytecode, as well as with three ifferent control dependence definitions. Thus we obtain $6$ IFC correctness proofs for the price of $1 {1\over 2}$.

## Download

 [PDF] [DOI]

## Authors at the institute

Department Head
Prof. Gregor Snelting
Former Staff Member
Dr.-Ing. Daniel Wasserrab
Dipl.-Inform. Denis Lohner

## Projects

 Project IFC for Mobile Components Quis-Custodiet