Information flow control for Java based on path conditions in dependence graphs
Christian Hammer, Jens Krinke, Gregor Snelting · 2006
Language-based information flow control (IFC) is a powerful tool to discover security leaks in software. Most current IFC approaches are however based on nonstandard 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