BARF -- 二进制分析及逆向框架

2017-01-05 11:05:37来源:作者:Paper人点击

项目地址: https://github.com/programa-stic/barf-project/

在计算机科学和软件工程学科的众多领域中,从软件安全程序分析到逆向工程,二进制代码的分析是很关键的行为。而手动进行二进制分析是一个困难又耗时的任务,因此便有了一些给分析人员准备的自动化分析工具。然而,这些大多数工具具有若干技术和商业上的限制,限制了大部分学术和从业者社区的访问和使用。 BARF是一款二进制分析框架,旨在支持信息安全学科中常见的大量的二进制代码分析任务。它是一个可编写脚本的平台,支持从多种架构中提取指令,提供了从二进制翻译到中间表示,用于代码分析的插件和能与外部工具(如调试器)交互的可扩展框架, SMT 求解器以及一些指令工具等。

该框架主要用于辅助分析者,但它完全可以自动化。

BARF 项目包括了 BARF 和相关工具包。到目前为止,该项目由以下项目组成:

BARF : 跨平台开源二进制分析和逆向工程框架。 PyAsmJIT : 用于 Intel x86_64 和 ARM 架构的 JIT 编译器。 基于 BARF 的 工具: BARFgadgets : 在二进制程序中搜索,分类并校验 ROP 的小程序。 BARFcfg : 恢复二进制程序功能的控制流图。 BARFcg : 回复二进制程序函数的调用图。

更多相关信息参考:

BARF: A multiplatform open source Binary Analysis and Reverse engineering Framework (Whitepaper) [ en] BARFing Gadgets (ekoparty2014 presentation) [ es]

当前版本信息: v0.3

URL: https://github.com/programa-stic/barf-project/releases/tag/v0.3

Change Log: https://github.com/programa-stic/barf-project/blob/v0.3/CHANGELOG.md

所有包均在 Ubuntu 16.04 (x86_64) 进行测试

BARF

BARF 是用于二进制分析和逆向工程的 Python 包。支持以下特性:

加载不同类型的二进制程序( ELF, PE等) 支持 32 位和 64 位的 Intel x86 架构 支持 32 位的 ARM 架构 运行在中间语言( REIL),因此所有分析算法是与架构无关的 与 Z3和 CVC4SMT 求解器集成,这意味着你可以将代码片段表述为公式,并检查对它们的限制。

相关功能仍在开发中。

安装

BARF 需要以下依赖:

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.

在系统上安装 BARF:

sudo python setup.py install

本地用户安装:

$ sudo python setup.py install --user 快速入门

下面一个简单的例子显示了如何打开一个二进制文件,并打印每条指令的中间翻译(REIL)。

from barf import BARF# Open binary file.barf = BARF("examples/bin/x86/branch1")# Print assembly instruction.for addr, asm_instr, reil_instrs in barf.translate(): print("0x{addr:08x} {instr}".format(addr=addr, instr=asm_instr)) # Print REIL translation. for reil_instr in reil_instrs: print("{indent:11s} {instr}".format(indent="", instr=reil_instr))

我们还可以恢复 CFG 并保存到 .dot文件。

# Recover CFG.cfg = barf.recover_cfg()# Save CFG to a .dot file.cfg.save("branch1_cfg")

我们可以使用 SMT 解算器代码检测限制,比如以下代码:

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

你想知道必须分配什么值给内存位置 ebp-0x4, ebp-0x8, ebp-0xc,以便在执行代码后再 eax 寄存器获得一个特定的值。

首先,我们将指令添加到分析器组件.

from barf import BARF# Open ELF filebarf = BARF("examples/bin/x86/constraint1")# 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)

然后,我们为每个感兴趣的变量生成表达式。

# Get smt expression for eax and ebp registerseap = barf.code_analyzer.get_register_expr("eax") ebp = barf.code_analyzer.get_register_expr("ebp")# Get smt expressions for memory locations (each one of 4 bytes)a = barf.code_analyzer.get_memory_expr(ebp-0x8, 4) b = barf.code_analyzer.get_memory_expr(ebp-0xc, 4) c = barf.code_analyzer.get_memory_expr(ebp-0x4, 4)

并添加所需的限制。

# Set range for variablesbarf.code_analyzer.set_preconditions([a >= 2, a <= 100]) barf.code_analyzer.set_preconditions([b >= 2, b <= 100])# Set desired value for the resultbarf.code_analyzer.set_postcondition(c == 13)

最后,我们检查我们建立的限制是否得到解决。

# Check satisfiability.if barf.code_analyzer.check() == 'sat': print("SAT!") # Get concrete value for expressions. eax_val = barf.code_analyzer.get_expr_value(eax) 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("eax : 0x{0:%08x} ({0})".format(eax_val)) print("ebp : 0x{0:%08x} ({0})".format(ebp_val)) print(" a : 0x{0:%08x} ({0})".format(a_val)) print(" b : 0x{0:%08x} ({0})".format(b_val)) print(" c : 0x{0:%08x} ({0})".format(c_val))else: print("UNSAT!")

你可以在 examples目录看到更多的例子。

更多相关内容可参考项目的 GitHub

最新文章

123

最新摄影

微信扫一扫

第七城市微信公众平台