Information Flow Control for Java Based on Dependence Graphs

Jens Krinke


Abstract

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 15 years of
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.