UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Precisely quantifying software information flow Enescu, Mihai Adrian


A common attack point in a program is the input exposed to the user. The adversary crafts a malicious input that alters some internal state of the program, in order to acquire sensitive data, or gain control of the program's execution. One can say that the input exerts a degree of influence over specific program outputs. Although a low degree of influence does not guarantee the program's resistance to attacks, previous work has argued that a greater degree of influence tends to provide an adversary with an easier avenue of attack, indicating a potential security vulnerability. Quantitative information flow is a framework that has been used to detect a class of security flaws in programs, by measuring an attacker's influence. Programs may be considered as communication channels between program inputs and outputs, and information-theoretic definitions of information leakage may be used in order to measure the degree of influence which a program's inputs can have over its outputs, if the inputs are allowed to vary. Unfortunately, the precise information flow measured by this definition is difficult to compute, and prior work has sacrificed precision, scalability, and/or automation. In this thesis, I 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. I present a tool, nsqflow, that is built on recent advances in symbolic execution and SAT solving. I use this tool to discover two previously-unknown buffer overflows. Experimentally, I demonstrate that this approach can scale to over 10K lines of real C code, including code that is typically difficult for program analysis tools to analyze, such as code using pointers.

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivatives 4.0 International