Towards a Flow- and Path-Sensitive Information Flow Analysis: Technical Report
This addresses security issues in programming by enabling more precise control of information flow for developers, though it is incremental as it builds on existing type systems.
The paper tackles the problem of improving static information flow analysis by developing a flow- and path-sensitive method that uses fixed labels, showing it is strictly more precise than classic flow-sensitive type systems and enforces noninterference without run-time mechanisms.
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.