Information Flow Control with Program Dependence Graphs

Jens Krinke

In classic information flow control (IFC), noninterference guarantees that no information flows from secret input channels to public output channels. However, this notion turned out to be overly restrictive as many intuitively secure programs do allow some release and thus intransitive noninterference allows declassification. We developed a static analysis that allows intransitive noninterference based on Program Dependence Graph. In contrast to type systems that annotate variables, our approach annotates information sources and sinks. Our approach is flow- and context-sensitive and because it is based on an industrial strength Program Dependence Generator (CodeSurfer from GrammaTech), it allows IFC for realistic C programs.