ARE: A System for Automated Reverse Engineering

Abstract:

Binary code analysis is a challenging problem, yet it is essential for many applications such as verification, security, and optimization. Thus BAE Systems lead the development of a system for finding inputs that steer program execution to reach areas of interest. At a high level, this system consists of dynamic tracing (e.g., via instrumentation plugins to Intel’s Pin), static analysis (e.g., via PREIL, our extension of Google’s Reverse Engineering Intermediate Language REIL), program databases (e.g., with taint queries for data stored via Apache’s HBase), constraint analysis (e.g., via COMET, our interface to SMT constraint solvers such as the Simple Theorem Prover STP), and a planner (e.g., to drive directed searches). Though we briefly describe the entire ARE system, our poster focuses on the impact of PREIL design decisions (to offer insights gained from evolving an existing language) and the implementation

of COMET (to share lessons learned from building Constraint Optimization, Management, Extension, and Translation layers over existing array and bit- vector solvers).
________
This material is based upon work supported by DARPA and AFRL under contract FA8750-12-C-0097. Approved for public release; distribution unlimited. Cleared for open publication on 3/22/2013.