Information flow control (IFC) checks whether a program can leak secret
data to public ports, or whether critical computations can be influenced
from outside. But many IFC analyses are imprecise, as they are flow-insensitive,
context-insensitive, or object-insensitive; resulting in false alarms.
We argue that IFC must better exploit modern program analysis
technology, and present an approach based on program dependence graphs
(PDG). PDGs have been developed over the last 20 years as a standard
device to represent information flow in a program, and today can
handle realistic programs. In particular, our dependence graph generator
for full Java bytecode is used as the basis for an IFC implementation
which is more precise and needs less annotations than traditional
approaches.
We explain PDGs for sequential and multi-threaded
programs, and explain precision gains due to flow-, context-, and
object-sensitivity. We then augment PDGs with a lattice of security
levels and introduce the flow equations for IFC. We describe algorithms
for flow computation in detail and prove their correctness. We then
extend flow equations to handle declassification, and prove that
our algorithm respects monotonicity of release. Finally, examples
demonstrate that our implementation can check realistic sequential
programs in full Java bytecode.
