  This paper investigates a flow- and path-sensitive static information flow
analysis. Compared with security type systems with fixed labels, it has been
shown that flow-sensitive type systems accept more secure programs. We show
that an information flow analysis with fixed labels can be both flow- and
path-sensitive. The novel analysis has two major components: 1) a
general-purpose program transformation that removes false dataflow dependencies
in a program that confuse a fixed-label type system, and 2) a fixed-label type
system that allows security types to depend on path conditions. We formally
prove that the proposed analysis enforces a rigorous security property:
noninterference. Moreover, we show that the analysis is strictly more precise
than a classic flow-sensitive type system, and it allows sound control of
information flow in the presence of mutable variables without resorting to
run-time mechanisms.
