barf project
1.0.0
バイナリコードの分析は、ソフトウェアセキュリティやプログラム分析からリバースエンジニアリングまで、コンピューターサイエンスやソフトウェアエンジニアリング分野の多くの分野で重要なアクティビティです。手動のバイナリ分析は困難で時間のかかるタスクであり、人間のアナリストを自動化または支援しようとするソフトウェアツールがあります。ただし、これらのツールのほとんどには、学術および開業医コミュニティの大部分がアクセスと使用を制限するいくつかの技術的および商業的制限があります。 Barfは、情報セキュリティ分野で一般的な幅広いバイナリコード分析タスクをサポートすることを目的とするオープンソースのバイナリ分析フレームワークです。これは、複数のアーキテクチャからの命令リフティング、中間表現へのバイナリ変換、コード分析プラグインの拡張可能なフレームワーク、デバッガー、SMTソルバー、計装ツールなどの外部ツールとの相互操作をサポートするスクリプト可能なプラットフォームです。フレームワークは主に人間支援分析用に設計されていますが、完全に自動化できます。
BARFプロジェクトには、 Barfおよび関連するツールとパッケージが含まれます。これまでのところ、プロジェクトは次の項目で構成されています。
詳細については、次を参照してください。
現在のステータス：
| 最新リリース | V0.6.0 |
|---|---|
| URL | https://github.com/programa-stic/barf-project/releases/tag/v0.6.0 |
| ログを変更します | https://github.com/programa-stic/barf-project/blob/v0.6.0/changelog.md |
すべてのパッケージは、Ubuntu 16.04（x86_64）でテストされました。
Barfは、バイナリ分析とリバースエンジニアリング用のPythonパッケージです。できる：
ELF 、 PEなど）でバイナリプログラムをロードし、現在開発中です。
BARFは、次のSMTソルバーに依存します。
次のコマンドは、システムにbarfをインストールします。
$ sudo python setup.py installローカルにインストールすることもできます。
$ sudo python setup.py install --usersudo pip install pyasmjitsudo apt-get install graphvizする必要がある場合がありますこれは、バイナリファイルを開き、中間言語（ 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 ))また、CFGを回復して、 .dotファイルに保存することもできます。
# Recover CFG.
cfg = barf . recover_cfg ()
# Save CFG to a .dot file.
cfg . save ( "branch4.x86_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
また、コードを実行した後、 eaxレジスタで特定の値を取得するために、メモリロケーションebp-0x4 、 ebp-0x8 、およびebp-0xcに割り当てなければならない値を知りたいと思います。
まず、アナライザーコンポーネントに手順を追加します。
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 )次に、関心のある変数ごとに式を生成し、それらに目的の制限を追加します。
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 )最後に、私たちが確立できる制限を解決できることを確認します。
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!" )これらの例とその他の例をExamples Directoryに見ることができます。
フレームワークは、コア、アーチ、分析の3つの主要なコンポーネントに分割されています。
このコンポーネントには必須モジュールが含まれています。
REIL ：Reil言語の定義を提供します。また、エミュレータとパーサーを実装します。SMT ：Z3およびCVC4 SMTソルバーとインターフェイスする手段を提供します。また、reilの指示をSMT式に変換する機能を提供します。BI ：バイナリインターフェイスモジュールは、処理にバイナリファイルをロードする責任があります（PefileとPyelfToolsを使用します。） サポートされている各アーキテクチャは、次のモジュールを含むサブコンポーネントとして提供されます。
Architecture ：アーキテクチャ、つまり、レジスタ、メモリアドレスサイズについて説明します。Translator ：サポートされている指示ごとに翻訳者をReilに提供します。Disassembler ：機能性の分解を提供します（キャップストーンを使用します。）Parser ：命令を文字列からオブジェクトフォームに変換します。 これまでのところ、このコンポーネントはモジュールで構成されています：コントロールフローグラフ、コールグラフ、コードアナライザー。最初の2つは、それぞれCFGとCGの回復の機能を提供します。後者は、SMTソルバー関連の機能への高レベルのインターフェイスです。
BARFgadgets 、Barf上に構築されたPythonスクリプトで、バイナリプログラム内でROPガジェットを検索、分類、確認できます。検索段階では、バイナリ内のすべてのret 、 jmp 、およびcallエンドガジェットが見つかります。分類段階は、以前に見つかったガジェットを次のタイプに従って分類します。
これは、命令エミュレーションを通じて行われます。最後に、検証段階は、SMTソルバーを使用して、第2段階で各ガジェットに割り当てられたセマンティックを検証することで構成されています。
usage: BARFgadgets [-h] [--version] [--bdepth BDEPTH] [--idepth IDEPTH] [-u]
[-c] [-v] [-o OUTPUT] [-t] [--sort {addr,depth}] [--color]
[--show-binary] [--show-classification] [--show-invalid]
[--summary SUMMARY] [-r {8,16,32,64}]
filename
Tool for finding, classifying and verifying ROP gadgets.
positional arguments:
filename Binary file name.
optional arguments:
-h, --help show this help message and exit
--version Display version.
--bdepth BDEPTH Gadget depth in number of bytes.
--idepth IDEPTH Gadget depth in number of instructions.
-u, --unique Remove duplicate gadgets (in all steps).
-c, --classify Run gadgets classification.
-v, --verify Run gadgets verification (includes classification).
-o OUTPUT, --output OUTPUT
Save output to file.
-t, --time Print time of each processing step.
--sort {addr,depth} Sort gadgets by address or depth (number of
instructions) in ascending order.
--color Format gadgets with ANSI color sequences, for output
in a 256-color terminal or console.
--show-binary Show binary code for each gadget.
--show-classification
Show classification for each gadget.
--show-invalid Show invalid gadget, i.e., gadgets that were
classified but did not pass the verification process.
--summary SUMMARY Save summary to file.
-r {8,16,32,64} Filter verified gadgets by operands register size.
詳細については、Readmeを参照してください。
BARFcfg 、バイナリプログラムのコントロールフローグラフを回復できるBarf上に構築されたPythonスクリプトです。
usage: BARFcfg [-h] [-s SYMBOL_FILE] [-f {txt,pdf,png,dot}] [-t]
[-d OUTPUT_DIR] [-b] [--show-reil]
[--immediate-format {hex,dec}] [-a | -r RECOVER]
filename
Tool for recovering CFG of a binary.
positional arguments:
filename Binary file name.
optional arguments:
-h, --help show this help message and exit
-s SYMBOL_FILE, --symbol-file SYMBOL_FILE
Load symbols from file.
-f {txt,pdf,png,dot}, --format {txt,pdf,png,dot}
Output format.
-t, --time Print process time.
-d OUTPUT_DIR, --output-dir OUTPUT_DIR
Output directory.
-b, --brief Brief output.
--show-reil Show REIL translation.
--immediate-format {hex,dec}
Output format.
-a, --recover-all Recover all functions.
-r RECOVER, --recover RECOVER
Recover specified functions by address (comma
separated).
BARFcgは、Barf上に構築されたPythonスクリプトで、バイナリプログラムのコールグラフを回復できるようになります。
usage: BARFcg [-h] [-s SYMBOL_FILE] [-f {pdf,png,dot}] [-t] [-a | -r RECOVER]
filename
Tool for recovering CG of a binary.
positional arguments:
filename Binary file name.
optional arguments:
-h, --help show this help message and exit
-s SYMBOL_FILE, --symbol-file SYMBOL_FILE
Load symbols from file.
-f {pdf,png,dot}, --format {pdf,png,dot}
Output format.
-t, --time Print process time.
-a, --recover-all Recover all functions.
-r RECOVER, --recover RECOVER
Recover specified functions by address (comma
separated).
Pyasmjitは、X86_64/ARMアセンブリコードの生成と実行用のPythonパッケージです。
このパッケージは、X86_64/ARMからREILへのバーフ命令翻訳をテストするために開発されました。主なアイデアは、コードの断片をネイティブに実行できることです。次に、同じフラグメントがReilに翻訳され、Reil VMで実行されます。最後に、両方の最終コンテキスト（ネイティブ実行を通じて得られたものとエミュレーションから得られたもの）は、違いについて比較されます。
詳細については、pyasmjitを参照してください。
BSD 2-Clauseライセンス。詳細については、ライセンスを参照してください。
