[hammer06isola] | Christian Hammer, Jens Krinke, Frank Nodes, Intransitive Noninterference in Dependence Graphs, 2nd International Symposium on Leveraging Application of Formal Methods,
Verification and Validation (ISoLA 2006), pp. 119--128, November 2006.
|
Abstract
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 contextsensitive 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 objectsensitive.
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.
Download
BibTeX
Authors at the institute
Projects