Abstract by Sean Brown
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
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.