KIT | KIT-Bibliothek | Impressum | Datenschutz

Information Flow Control for Java Based on Path Conditions in Dependence Graphs

Hammer, Christian; Krinke, Jens; Snelting, Gregor


Language-based information flow control (IFC) is a powerful tool to discover security leaks in software. Most current IFC approaches are however based on non-standard type systems. Type-based IFC is elegant, but not precise and can lead to false alarms. We present a more precise approach to IFC which exploits active research in static program analysis. Our IFC approach is based on path conditions in program dependence graphs (PDGs). PDGs are a sophisticated and powerful analysis device, and today can handle realistic programs in full C or Java. We first recapitulate a theorem connecting the classical notion of noninterference to PDGs.
We then introduce path conditions in Java PDGs. Path conditions are necessary conditions for information flow; today path conditions can be generated and solved for realistic programs. We show how path conditions can produce witnesses for security leaks.
The approach has been implemented for full Java and augmented with classical security level lattices. Examples and case studies demonstrate the feasibility and power of the method.

Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2006
Sprache Englisch
Identifikator KITopen-ID: 1000017616
Erschienen in Proceedings of the IEEE International Symposium on Secure Software Engineering (ISSSE 2006)
Verlag IEEE Computer Society
Seiten 87 - 96
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page