Intransitive Noninterference in Dependence Graphs

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. In this paper we define a static analysis that allows intransitive noninterference in combination with context- sensitive analysis for Java bytecode programs. In contrast to type systems that annotate variables, our approach annotates information sources and sinks. To the best of our knowledge this is the first IFC technique which is flow-, context-, and object- sensitive. It allows IFC for realistic languages like Java or C and offers a mechanism for declassification to accommodate some information leakage for cases where traditional noninterference is too restrictive.