A Multi-platform open source Binary Analysis and Reverse engineering Framework.
The analysis of binary code is a crucial activity in many areas of the computer sciences and software engineering disciplines ranging from software security and program analysis to reverse engineering.
Manual binary analysis is a difficult and time-consuming task and there are software tools that seek to automate or assist human analysts. However, most of these tools have several technical and commercial restrictions that limit access and use by a large portion of the academic and practitioner communities.
BARF is an open source binary analysis framework that aims to support a wide range of binary code analysis tasks that are common in the information security discipline. It is a scriptable platform that supports instruction lifting from multiple architectures, binary translation to an intermediate representation, an extensible framework for code analysis plugins and inter operation with external tools such as debuggers, SMT solvers and instrumentation tools. The framework is designed primarily for human-assisted analysis but it can be fully automated.
The BARF project includes BARF and related tools and packages. So far the project is composed of the following items:
BARF : A multiplatform open source Binary Analysis and Reverse engineering Framework
PyAsmJIT : A JIT for the Intel x86_64 and ARM architecture.
Tools built upon BARF:BARFgadgets : Lets you search, classify and verify ROP gadgets inside a binary program.
BARFcfg : Lets you recover the control-flow graph of the functions of a binary program.
BARFcg : Lets you recover the call graph of the functions of a binary program.
BARFBARF is a Python package for binary analysis and reverse engineering. It can:
Load binary programs in different formats (ELF, PE, etc),
It supports the Intel x86 architecture for 32 and 64 bits,
It supports the ARM architecture for 32 bits,
It operates on an intermediate language (REIL) thus all analysis algorithm are architecture-agnostic,
It has integration with Z3 and CVC4 SMT solvers which means that you can express fragments of code as formulae and check restrictions on them.
It is currently under development.
BARF depends on the following SMT solvers:
Z3 : A high-performance theorem prover being developed at Microsoft Research.
CVC4 : An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
The following command installs BARF on your system:
$ sudo python setup.py install
You can also install it locally:
$ sudo python setup.py install --user
NotesOnly one SMT solver is needed in order to work. You may choose between Z3 and CVC4 or install both. You can use the barf-install-solver.sh script which downloads and install both solver.
To run some tests you need to install PyAsmJIT first.