項目地址：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 和 CVC4 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-0x4，ebp-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
本文由 Seebug Paper 發布，如需轉載請注明來源。本文地址：http://www.bjnorthway.com/169/
暫無評論