programa-stic/barf-projectBARF : A multiplatform 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 interoperation 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:
For more information, see:
Current status:
| Latest Release | v0.6.0 |
|---|---|
| URL | https://github.com/programa-stic/barf-project/releases/tag/v0.6.0 |
| Change Log | https://github.com/programa-stic/barf-project/blob/v0.6.0/CHANGELOG.md |
All packages were tested on Ubuntu 16.04 (x86_64).
BARF is a Python package for binary analysis and reverse engineering. It can:
ELF, PE, etc),It is currently under development.
BARF depends on the following SMT solvers:
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
sudo pip install pyasmjitsudo apt-get install graphvizThis is a very simple example which shows how to open a binary file and print each instruction with its translation to the intermediate language (REIL).
from barf import BARF
# Open binary file.
barf = BARF("examples/misc/samples/bin/branch4.x86")
# Print assembly instruction.
for addr, asm_instr, reil_instrs in barf.translate():
print("{:#x} {}".format(addr, asm_instr))
# Print REIL translation.
for reil_instr in reil_instrs:
print("\t{}".format(reil_instr))
We can also recover the CFG and save it to a .dot file.
# Recover CFG.
cfg = barf.recover_cfg()
# Save CFG to a .dot file.
cfg.save("branch4.x86_cfg")
We can check restrictions on code using a SMT solver. For instance, suppose you have the following code:
80483ed: 55 push ebp
80483ee: 89 e5 mov ebp,esp
80483f0: 83 ec 10 sub esp,0x10
80483f3: 8b 45 f8 mov eax,DWORD PTR [ebp-0x8]
80483f6: 8b 55 f4 mov edx,DWORD PTR [ebp-0xc]
80483f9: 01 d0 add eax,edx
80483fb: 83 c0 05 add eax,0x5
80483fe: 89 45 fc mov DWORD PTR [ebp-0x4],eax
8048401: 8b 45 fc mov eax,DWORD PTR [ebp-0x4]
8048404: c9 leave
8048405: c3 ret
And you want to know what values you have to assign to memory locations ebp-0x4, ebp-0x8 and ebp-0xc in order to obtain a specific value in eax register after executing the code.
First, we add the instructions to the analyzer component.
from barf import BARF
# Open ELF file
barf = BARF("examples/misc/samples/bin/constraint1.x86")
# Add instructions to analyze.
for addr, asm_instr, reil_instrs in barf.translate(0x80483ed, 0x8048401):
for reil_instr in reil_instrs:
barf.code_analyzer.add_instruction(reil_instr)
Then, we generate expressions for each variable of interest and add the desired restrictions on them.
ebp = barf.code_analyzer.get_register_expr("ebp", mode="post")
# Preconditions: set range for variable a and b
a = barf.code_analyzer.get_memory_expr(ebp-0x8, 4, mode="pre")
b = barf.code_analyzer.get_memory_expr(ebp-0xc, 4, mode="pre")
for constr in [a >= 2, a <= 100, b >= 2, b <= 100]:
barf.code_analyzer.add_constraint(constr)
# Postconditions: set desired value for the result
c = barf.code_analyzer.get_memory_expr(ebp-0x4, 4, mode="post")
for constr in [c >= 26, c <= 28]:
barf.code_analyzer.add_constraint(constr)
Finally, we check is the restrictions we establish can be resolved.
if barf.code_analyzer.check() == 'sat':
print("[+] Satisfiable! Possible assignments:")
# Get concrete value for expressions
a_val = barf.code_analyzer.get_expr_value(a)
b_val = barf.code_analyzer.get_expr_value(b)
c_val = barf.code_analyzer.get_expr_value(c)
# Print values
print("- a: {0:#010x} ({0})".format(a_val))
print("- b: {0:#010x} ({0})".format(b_val))
print("- c: {0:#010x} ({0})".format(c_val))
assert a_val + b_val + 5 == c_val
else:
print("[-] Unsatisfiable!")
You can see these and more examples in the examples directory.
The framework is divided in three main components: core, arch and analysis.
This component contains essential modules:
REIL: Provides definitions for the REIL language. It, also, implements an emulator and a parser.SMT: Provides means to interface with [Z3] and [CVC4] SMT solver. Also, it provides functionality to translate REIL instructions to SMT expressions.BI: The Binary Interface module is responsible for loading binary files for processing (it uses [PEFile] and [PyELFTools].)