10.1184/R1/7571519.v1
Matthew Maurer
Matthew
Maurer
Holmes: Binary Analysis Integration Through Datalog
Carnegie Mellon University
2018
alias analysis
binary analysis
datalog
program analysis
type recovery
2018-10-01 00:00:00
Thesis
https://kilthub.cmu.edu/articles/thesis/Holmes_Binary_Analysis_Integration_Through_Datalog/7571519
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.