Konferenzartikel: 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.


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}$.


  [PDF]   [DOI]


Institutsinterne Autoren

Prof. Gregor Snelting
Ehemalige Mitarbeiter
Dr.-Ing. Daniel Wasserrab
Dipl.-Inform. Denis Lohner


IFC for Mobile Components