Sciweavers

PLDI
2009
ACM

On PDG-based noninterference and its modular proof

14 years 6 days ago
On PDG-based noninterference and its modular proof
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. The new proof is based on a new correctness proof for intraprocedural PDGs and program slices. Both proofs are ed 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 diff...
Daniel Wasserrab, Denis Lohner, Gregor Snelting
Added 19 May 2010
Updated 19 May 2010
Type Conference
Year 2009
Where PLDI
Authors Daniel Wasserrab, Denis Lohner, Gregor Snelting
Comments (0)