Abstract by Sean Brown

Personal Infomation

Presenter's Name

Sean Brown

Degree Level


Abstract Infomation


Computer Science

Faculty Advisor

Eric Mercer


Detecting information flow via symbolic execution


Information flow detection is a very important feature of program verification. 
However, many simple program features (such as conditional branches and 
function calls) can obscure flow, causing many implicit information leaks to 
remain undetected.
Symbolic execution can capture these implicit leaks naturally by capturing 
sensitive values in path constraints.
This process can be improved further by using function and loop summaries to 
reduce the amount of time required to perform the symbolic execution.
This work presents a technique for detecting information leaks via symbolic 
execution with function summaries by propogating sensitive values through 
symbolic values and guarded expressions.