BYU

Abstract by Sean Brown

Personal Infomation


Presenter's Name

Sean Brown

Degree Level

Masters

Abstract Infomation


Department

Computer Science

Faculty Advisor

Eric Mercer

Title

Detecting information flow via symbolic execution

Abstract

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.