On PDG-based noninterference and its modular proof
Daniel Wasserrab, Denis Lohner, Gregor Snelting · 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.