We present a static analysis that extracts from a program's source code a sound approximation of the most restrictive conditional confidentiality policy that the program obeys. To formalize conditional confidentiality policies, we present a modified definition of noninterference that depends on runtime information. We implement our analysis and experiment with the resulting tool on C programs. While we focus on using our analysis for policy extraction, the process can more generally be used for information flow analysis. Unlike traditional information flow analysis that simply states what flows are possible in a program, our tool also states what conditions must be satisfied by an execution for each flow to be enabled. Furthermore, our analysis is the first to handle interactive I/O while being compositional and flow sensitive.

23 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu