Holmes: Binary Analysis Integration Through Datalog

We need tools and techniques for program analysis that address the unique problems
faced when analyzing compiled code. During compilation, the compiler strips
away source code information, such as control
ow, types, and variable locations. As
a result, analysis of compiled code faces a number of unique challenges. Previous work
has proposed techniques to perform an individual analysis in isolation. However, previous
work has not focused on the co-dependencies between these individual analysis.
For example, value set analysis requires control
ow analysis, which in turn requires
value set analysis. We need techniques that can handle such co-dependencies in order
to eeffectively check higher-level security properties.
In this thesis we propose using a logic-language based approach to encode codependent
analysis and build a tool called Holmes based on our approach to demonstrate
our ideas on real code. We demonstrate novel techniques for extending Datalog
semantics to eefficiently and effeffectively reason about real binary code. Our approach
allows one to elegantly encode the co-dependence between value-set and control-
ow
analysis described above. We demonstrate Holmes and our approach by encoding
real-world co-dependent analysis, and showing that Holmes can act as a framework to
eeffectively check higher-level properties, such as use-after-free, on real compiled code.