Precisely Measuring Quantitative Information Flow: 10K Lines of Code and Beyond

This paper considers the quantitative measurementof information flow through a program -- the degree of influence a program's inputs can have over a set of specified program variables. This definition has been proposed as a refinement of taint analysis in the detection of a class of security flaws in programs. Unfortunately, the precise information flow by this definition is difficult to compute, and prior work has sacrificed precision, scalability, and/or automation. In this paper, we show how to compute this information flow (specifically, channel capacity) in a highly precise and automatic manner, and scale to much larger programs than previously possible. We build on recent advances in symbolic execution and SAT solving, and propose further novel improvements as well. We discover two previously-unknown buffer overflows using our tool. Experimentally, we demonstrate that our approach scales to over 10K lines of real C code.