PyVEX

PyVEXはVEX IRのPythonバインディングです。

プロジェクトリンク

プロジェクトリポジトリ: https://github.com/angr/pyvex

ドキュメント: https://api.angr.io/projects/pyvex/en/latest/

PyVEXのインストール

PyVEXはpipでインストールできます:

pip install pyvex

PyVEXの使用

import pyvex
import archinfo

# translate an AMD64 basic block (of nops) at 0x400400 into VEX
irsb = pyvex.lift(b"\x90\x90\x90\x90\x90", 0x400400, archinfo.ArchAMD64())

# pretty-print the basic block
irsb.pp()

# this is the IR Expression of the jump target of the unconditional exit at the end of the basic block
print(irsb.next)

# this is the type of the unconditional exit (i.e., a call, ret, syscall, etc)
print(irsb.jumpkind)

# you can also pretty-print it
irsb.next.pp()

# iterate through each statement and print all the statements
for stmt in irsb.statements:
    stmt.pp()

# pretty-print the IR expression representing the data, and the *type* of that IR expression written by every store statement
import pyvex
for stmt in irsb.statements:
    if isinstance(stmt, pyvex.IRStmt.Store):
        print("Data:", end="")
        stmt.data.pp()
        print("")

        print("Type:", end="")
        print(stmt.data.result_type)
        print("")

# pretty-print the condition and jump target of every conditional exit from the basic block
for stmt in irsb.statements:
    if isinstance(stmt, pyvex.IRStmt.Exit):
        print("Condition:", end="")
        stmt.guard.pp()
        print("")

        print("Target:", end="")
        stmt.dst.pp()
        print("")

# these are the types of every temp in the IRSB
print(irsb.tyenv.types)

# here is one way to get the type of temp 0
print(irsb.tyenv.types[0])

これは基本ブロックの構文的表現であることに留意してください。つまり、そのブロックが何を意味するかを教えてくれますが、例えばストア命令によって実際にどのようなデータが書き込まれるかを言うためのコンテキストはありません。

VEX中間表現

多種多様なアーキテクチャを扱うには、中間表現上で解析を行うと便利です。 IRは、異なるアーキテクチャを扱う際のいくつかのアーキテクチャの違いを抽象化し、単一の解析をそれらすべてに対して実行できるようにします:

• レジスタ名。 レジスタの数と名前はアーキテクチャによって異なりますが、現代のCPU設計は共通のテーマに従っています: 各CPUにはいくつかの汎用レジスタ、スタックポインタを保持するレジスタ、条件フラグを格納するレジスタのセットなどが含まれます。IRは、異なるプラットフォーム上のレジスタへの一貫した抽象化されたインターフェースを提供します。具体的には、VEXはレジスタを別個のメモリ空間としてモデル化し、整数オフセットを持ちます（つまり、AMD64のraxはこのメモリ空間のアドレス16から格納されます）。
• メモリアクセス。 異なるアーキテクチャは異なる方法でメモリにアクセスします。例えば、ARMはリトルエンディアンモードとビッグエンディアンモードの両方でメモリにアクセスできます。IRはこれらの違いを抽象化しなければなりません。
• メモリセグメンテーション。 x86など一部のアーキテクチャは、特別なセグメントレジスタを使用したメモリセグメンテーションをサポートしています。IRはそのようなメモリアクセス機構を理解します。
• 命令の副作用。 ほとんどの命令には副作用があります。例えば、ARMのThumbモードでのほとんどの操作は条件フラグを更新し、スタックのプッシュ/ポップ命令はスタックポインタを更新します。これらの副作用を解析内でアドホックに追跡するのは正気の沙汰ではないので、IRはこれらの効果を明示的にします。

IRには多くの選択肢があります。バイナリコードのVEXへのリフティングが非常によくサポートされているため、私たちはVEXを使用しています。 VEXは、多数のターゲットマシン言語のアーキテクチャ非依存で副作用のない表現です。 これはマシンコードを、プログラム解析を容易にするように設計された表現に抽象化します。 この表現には5つの主要なオブジェクトクラスがあります:

• 式。 IR式は、計算された値または定数値を表します。これにはメモリロード、レジスタ読み取り、算術演算の結果が含まれます。
• 演算。 IR演算は、IR式の変更を記述します。これには整数演算、浮動小数点演算、ビット演算などが含まれます。IR式に適用されたIR演算は、結果としてIR式を生成します。
• 一時変数。 VEXは内部レジスタとして一時変数を使用します: IR式は使用の間に一時変数に格納されます。一時変数の内容はIR式を使用して取得できます。これらの一時変数には番号が付けられ、t0から始まります。これらの一時変数は強い型付けがされています（つまり、「64ビット整数」や「32ビット浮動小数点数」）。
• 文。 IR文は、メモリストアやレジスタ書き込みの効果など、ターゲットマシンの状態の変化をモデル化します。IR文は、必要とする値にIR式を使用します。例えば、メモリストアIR文は、書き込みのターゲットアドレスにIR式を使用し、内容に別のIR式を使用します。
• ブロック。 IRブロックはIR文の集合であり、ターゲットアーキテクチャにおける拡張基本ブロック（「IRスーパーブロック」または「IRSB」と呼ばれる）を表します。ブロックは複数の出口を持つことができます。基本ブロックの途中からの条件付き出口には、特別なExit IR文が使用されます。IR式は、ブロックの最後にある無条件出口のターゲットを表すために使用されます。

VEX IRは実際には、VEXリポジトリのlibvex_ir.hファイル（https://github.com/angr/vex/blob/dev/pub/libvex_ir.h）で非常によく文書化されています。面倒な人のために、頻繁にやり取りする可能性が高いVEXのいくつかの部分を詳しく説明します。まず、いくつかのIR式を紹介します:

IR式	評価される値	VEX出力例
Constant	定数値。	0x4:I32
Read Temp	VEX一時変数に格納された値。	RdTmp(t10)
Get Register	レジスタに格納された値。	GET:I32(16)
Load Memory	メモリアドレスに格納された値。アドレスは別のIR式で指定されます。	LDle:I32 / LDbe:I64
Operation	指定されたIR式の引数に適用された、指定されたIR演算の結果。	Add32
If-Then-Else	指定されたIR式が0と評価された場合、1つのIR式を返します。それ以外の場合は別のものを返します。	ITE
Helper Function	VEXは、特定のアーキテクチャの条件フラグレジスタの計算など、特定の操作にCヘルパー関数を使用します。これらの関数はIR式を返します。	function_name()

これらの式は次に、IR文で使用されます。以下は一般的なものです:

IR文	意味	VEX出力例
Write Temp	VEX一時変数を指定されたIR式の値に設定します。	WrTmp(t1) = (IR Expression)
Put Register	指定されたIR式の値でレジスタを更新します。	PUT(16) = (IR Expression)
Store Memory	IR式として与えられたメモリ内の場所を、同じくIR式として与えられた値で更新します。	STle(0x1000) = (IR Expression)
Exit	基本ブロックからの条件付き出口。ジャンプターゲットはIR式で指定されます。条件はIR式で指定されます。	if (condition) goto (Boring) 0x4000A00:I32

ARMでのIR変換の例を以下に示します。この例では、減算操作は5つのIR文からなる単一のIRブロックに変換され、それぞれが少なくとも1つのIR式を含んでいます（ただし、実際にはIRブロックは通常複数の命令で構成されます）。レジスタ名は、GET式とPUT文に与えられた数値インデックスに変換されます。 注意深い読者は、実際の減算がブロックの最初の4つのIR文でモデル化され、次の命令（この場合は0x59FC8に位置する）を指すようにプログラムカウンタをインクリメントすることが最後の文でモデル化されていることに気づくでしょう。

以下のARM命令:

subs R2, R2, #8

は、このVEX IRになります:

t0 = GET:I32(16)
t1 = 0x8:I32
t3 = Sub32(t0,t1)
PUT(16) = t3
PUT(68) = 0x59FC8:I32

素晴らしいですね！

PyVEXの引用

学術研究でPyVEXを使用する場合は、それが開発された論文を引用してください:

@article{shoshitaishvili2015firmalice,
  title={Firmalice - Automatic Detection of Authentication Bypass Vulnerabilities in Binary Firmware},
  author={Shoshitaishvili, Yan and Wang, Ruoyu and Hauser, Christophe and Kruegel, Christopher and Vigna, Giovanni},
  booktitle={NDSS},
  year={2015}
}