BARF : バイナリ解析とリバースエンジニアリングフレームワーク

バイナリコードの解析は、ソフトウェアセキュリティ、プログラム解析、リバースエンジニアリングなど、コンピュータ科学およびソフトウェア工学の多くの分野において重要な活動です。手動でのバイナリ解析は困難で時間のかかる作業であり、それを自動化または支援するソフトウェアツールが存在します。しかし、これらのツールの多くには技術的・商業的な制約があり、学界や実務家コミュニティの大部分がアクセスして使用することが制限されています。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 (ホワイトペーパー) [en]
BARFing Gadgets (ekoparty2014 プレゼンテーション) [es]

現在のステータス:

最新リリース	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

BARF は、バイナリ解析およびリバースエンジニアリングのためのPythonパッケージです。以下のことが可能です:

さまざまな形式 (ELF、PE など) のバイナリプログラムをロードできます。
Intel x86 アーキテクチャ (32ビットおよび64ビット) をサポートします。
ARM アーキテクチャ (32ビット) をサポートします。
中間言語 (REIL) で動作するため、すべての解析アルゴリズムはアーキテクチャに依存しません。
Z3 および CVC4 SMTソルバと統合されており、コードの断片を数式として表現し、それらに対して制約を確認できます。

現在 開発中 です。

インストール

BARF は以下の SMTソルバに依存します:

Z3 : Microsoft Research で開発されている高性能な定理証明器。
CVC4 : SMT (Satisfiability Modulo Theories) 問題のための効率的なオープンソース自動定理証明器。

以下のコマンドで BARF をシステムにインストールします:

$ sudo python setup.py install

ローカルにインストールすることもできます:

$ sudo python setup.py install --user

注意事項

動作には1つの SMTソルバのみ必要です。Z3 と CVC4 のどちらかを選択するか、両方をインストールしても構いません。
一部のテストを実行するには、PyAsmJIT を事前にインストールする必要があります: sudo pip install pyasmjit
Graphviz のインストールが必要な場合があります: sudo 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!")

これらの例やその他の例は、例ディレクトリにあります。

概要

フレームワークは、コア、アーキテクチャ、解析の3つの主要コンポーネントに分かれています。

コア

このコンポーネントには、以下の必須モジュールが含まれています:

REIL: REIL言語の定義を提供します。また、エミュレータ と パーサ を実装しています。
SMT: Z3 および CVC4 SMTソルバとのインターフェースを提供します。また、REIL命令をSMT式に変換する機能も提供します。
BI: Binary Interface モジュールは、処理のためにバイナリファイルをロードする責任を持ちます (PEFile および PyELFTools を使用)。

アーキテクチャ

サポートされている各アーキテクチャはサブコンポーネントとして提供され、以下のモジュールが含まれています。

Architecture: アーキテクチャの説明（レジスタ、メモリアドレスサイズなど）。
Translator: サポートされている各命令のREILへの変換を提供します。
Disassembler: 逆アセンブル機能を提供します (Capstone を使用)。
Parser: 命令を文字列からオブジェクト形式に変換します。

解析

現在、このコンポーネントは 制御フローグラフ、コールグラフ、コードアナライザ のモジュールで構成されています。最初の2つは、それぞれCFGおよびCGの復元機能を提供します。後者は、SMTソルバ関連機能への高レベルインターフェースです。

ツール

BARFgadgets

BARFgadgets は、BARF上に構築されたPythonスクリプトで、バイナリプログラム内のROPガジェットを検索、分類、検証します。検索段階では、バイナリ内の ret、jmp、call で終わるすべてのガジェットを見つけます。分類段階では、以前に見つかったガジェットを以下のタイプに分類します:

無操作 (No-Operation),
レジスタ移動 (Move Register),
定数ロード (Load Constant),
算術論理演算 (Arithmetic/Logical Operation),
メモリロード (Load Memory),
メモリストア (Store Memory),
算術論理ロード (Arithmetic/Logical Load),
算術論理ストア (Arithmetic/Logical Store),
未定義 (Undefined).

これは命令エミュレーションによって行われます。最後に、検証段階では、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

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

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

PyAsmJIT は、x86_64/ARM アセンブリコードの生成と実行のためのPythonパッケージです。

このパッケージは、x86_64/ARM から REIL への BARF 命令変換をテストするために開発されました。主なアイデアは、コードの断片をネイティブに実行できるようにすることです。次に、同じ断片を REIL に変換して REIL VM で実行します。最後に、両方の最終コンテキスト（ネイティブ実行で得られたものとエミュレーションで得られたもの）を比較して差異を確認します。

詳細については、PyAsmJIT を参照してください。

ライセンス

BSD 2-Clause License。詳細については、LICENSE を参照してください。

barf-project

人気