KIT | KIT-Bibliothek | Impressum | Datenschutz

Intransitive Noninterference in Dependence Graphs

Hammer, Christian; Krinke, Jens; Nodes, Frank


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.

Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2006
Sprache Englisch
Identifikator ISBN: 978-0-7695-3071-0
KITopen-ID: 1000017615
Erschienen in Proceedings of the Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, November 15 - 19, 2006, Paphos, Cyprus
Verlag IEEE Computer Society
Seiten 119 - 128
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page