Towards a Flow- and Path-Sensitive Information Flow Analysis: Technical Report

TL;DR

This paper presents a novel static information flow analysis that is both flow- and path-sensitive, improving precision over traditional fixed-label type systems while ensuring noninterference without runtime checks.

Contribution

It introduces a program transformation and a fixed-label type system with path-dependent security types, enhancing flow- and path-sensitivity in static analysis.

Findings

Proves the analysis enforces noninterference.

Demonstrates increased precision over classic flow-sensitive type systems.

Allows sound control of information flow with mutable variables.

Abstract

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.