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