GitHubじゃ!Pythonじゃ!

GitHubからPython関係の優良リポジトリを探したかったのじゃー、でも英語は出来ないから日本語で読むのじゃー、英語社会世知辛いのじゃー

programa-stic

barf-project – BARF:マルチプラットフォームのオープンソースバイナリ解析とリバースエンジニアリングフレームワーク

投稿日:

BARF:マルチプラットフォームのオープンソースバイナリ解析とリバースエンジニアリングフレームワーク

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

バイナリコードの分析は、ソフトウェアセキュリティとプログラム分析からリバースエンジニアリングに至るまで、コンピュータサイエンスおよびソフトウェアエンジニアリング分野の多くの分野で重要な活動です。 手作業によるバイナリ分析は困難で時間がかかる作業であり、人間の分析者を自動化または支援するソフトウェアツールがあります。 しかし、これらのツールのほとんどは、学術および実践者のコミュニティの大部分がアクセスと使用を制限するいくつかの技術的および商業上の制限があります。 BARFは、オープンソースのバイナリ分析フレームワークであり、情報セキュリティの分野で一般的な広範なバイナリコード分析タスクをサポートすることを目的としています。 これは、複数のアーキテクチャからバイナリ変換、中間表現への命令リフティング、コード解析プラグインのための拡張可能なフレームワーク、およびデバッガ、SMTソルバ、計装ツールなどの外部ツールとの相互運用をサポートするスクリプト可能なプラットフォームです。 このフレームワークは主に人手による分析のために設計されていますが、完全に自動化することもできます。

BARFプロジェクトには、 BARFと関連するツールとパッケージが含まれています。 これまでのところ、プロジェクトは以下の項目で構成されています。

  • BARF :マルチプラットフォームのオープンソースバイナリ解析とリバースエンジニアリングフレームワーク
  • PyAsmJIT :Intel x86_64およびARMアーキテクチャのJIT。
  • BARF上に構築されたツール:
    • BARFgadgets :バイナリプログラム内でROPガジェットを検索分類検証できます。
    • BARFcfg :バイナリプログラムの関数のコントロールフローグラフをリカバリできます。
    • BARFcg :バイナリプログラムの関数のコールグラフを復元できます。

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

  • BARF:マルチプラットフォームのオープンソースバイナリ分析とリバースエンジニアリングフレームワーク (ホワイトペーパー)[ en ]
  • BARFingガジェット (ekoparty2014プレゼンテーション)[ es ]

現在のステータス:

最新のリリース v0.5.0
URL https://github.com/programa-stic/barf-project/releases/tag/v0.5.0
ログの変更 https://github.com/programa-stic/barf-project/blob/v0.5.0/CHANGELOG.md

すべてのパッケージはUbuntu 16.04(x86_64)でテストされました。

BARF

BARFはバイナリ解析とリバースエンジニアリングのためのPythonパッケージです。 できる:

  • バイナリプログラムをさまざまな形式( ELFPEなど)で読み込み、
  • 32ビットと64ビットのIntel x86アーキテクチャをサポートしており、
  • 32ビットのARMアーキテクチャをサポートしており、
  • 中間言語( REIL )上で動作するため、すべての分析アルゴリズムはアーキテクチャに依存しないため、
  • これは、 Z3およびCVC4 SMTソルバーとの統合を備えています。つまり、コードの断片を数式として表現し、制約をチェックすることができます。

現在開発中です。

インストール

BARFは、次のSMTソルバーによって異なります。

  • Z3 :Microsoft Researchで開発中の高性能定理証明者。
  • CVC4 :充足可能性モジュロ理論(SMT)問題のための効率的なオープンソース自動定理証明器。

次のコマンドは、システムにBARFをインストールします。

$ sudo python setup.py install

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

$ sudo python setup.py install --user

ノート

  • 作業に必要なSMTソルバは1つだけです。 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

また、 ebp-0x8ebp-0x8 、およびebp-0xcをメモリ位置に割り当てる必要がある値を知りたい場合は、コード実行後にeaxレジスタ内の特定の値を取得する必要があります。

まず、アナライザコンポーネントに命令を追加します。

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ディレクトリに、これらの例やその他の例があります。

概要

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

コア

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

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

アーチ

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

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

分析

これまでのところ、このコンポーネントは、 コントロールフローグラフコールグラフコードアナライザの各モジュールで構成されています。 最初の2つは、それぞれCFGとCGリカバリの機能を提供します。 後者は、SMTソルバー関連の機能に対する高度なインターフェースです。

ツール

BARFgadgets

BARFgadgetsは、バイナリプログラム内でROPガジェットの検索分類 、および確認を可能にするBARFgadgets構築されたPythonスクリプトです。 検索ステージでは、バイナリ内のすべてのretjmp 、およびcall -initiatedガジェットが検索されます。 分類段階では、以前に見つかったガジェットを次のタイプに基づいて分類します。

  • ノーオペレーション、
  • 移動登録、
  • 負荷定数、
  • 算術演算/論理演算、
  • メモリをロードする、
  • ストアメモリ、
  • 算術/論理積、
  • 算術/論理ストア
  • 未定義。

これは命令エミュレーションによって行われます。 最後に、 検証段階では、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はバイナリプログラムの制御フローグラフを復元するためのBARFcfg構築された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はバイナリプログラムのコールグラフをリカバリできるBARFcg構築された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条項ライセンス。 詳細については、「 ライセンス 」を参照してください。







-programa-stic
-, , , , , ,

執筆者: