Insight: An open binary analysis framework

Abstract

We present Insight, a framework for binary program analysis and two tools provided with it: CFGRecovery and iii. Insight is intended to be a full environment for analyzing, interacting and verifying executable programs. Insight is able to translate x86, x86-64 and msp430 binary code to our intermediate representation and execute it symbolically in an abstract domain where each variable (register, memory cell) is substituted by a formula representing all its possible values along the current execution path. CFGRecovery aims at automatically rebuilding the program control flow based only on the executable file. It heavily relies on SMT solvers. iii provides an interactive and a (Python) programmable interface to a coherent set of features from the Insight framework. It behaves like a debugger except that the execution traces that are examined are symbolic and cover a collection of possible concrete executions at once. For example, iii allows to perform an interactive reconstruction of the CFG.