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 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 different control dependence definitions. Thus we obtain 6 IFC correctness proofs for the price of 1 1/2.