项目地址: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),因此所有分析算法是与架构无关的
  • Z3CVC4 SMT 求解器集成,这意味着你可以将代码片段表述为公式,并检查对它们的限制。

相关功能仍在开发中。

安装

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-0x4ebp-0x8,ebp-0xc ,以便在执行代码后再 eax 寄存器获得一个特定的值。

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

from barf import BARF

# Open ELF file
barf = 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 registers
eap = 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 variables
barf.code_analyzer.set_preconditions([a >= 2, a <= 100])
barf.code_analyzer.set_preconditions([b >= 2, b <= 100])

# Set desired value for the result
barf.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


Paper 本文由 Seebug Paper 发布,如需转载请注明来源。本文地址:https://paper.seebug.org/169/