SKILL: シンボリック実行ツール — エキスパート解析プレイブック

AI LOAD INSTRUCTION: angr、Z3、Unicorn Engineを使用したエキスパートレベルのシンボリック実行技法。CTFチャレンジの自動化、制約ソルバーパターン、関数フック、SimProcedureの置き換え、エミュレーションベースのアンパックをカバーします。ベースモデルは状態初期化の誤りまたはlibc関数のフック漏れにより、壊れたangrスクリプトを生成することが多いです。

0. 関連ルーティング

• anti-debugging-techniques アンチデバッグチェックをシンボリック的にバイパスする必要がある場合
• code-obfuscation-deobfuscation シンボリック実行を難読化解除に使用する場合
• vm-and-bytecode-reverse angrをカスタムVMチャレンジに適用する場合

高度なリファレンス

以下が必要な場合、ANGR_COOKBOOK.mdもロードしてください:

• CTFチャレンジの一般的なパターン向け15以上の即座に使えるangrスクリプトパターン
• scanf、printf、malloc、strcmpのフックテンプレート
• シンボリックファイル入力、stdin、argvパターン
• パス爆発管理の最適化トリック

どのツールを使用するか

シナリオ	最適なツール	理由
純粋な数学/方程式系	Z3	直接的な制約解法、バイナリ不要
制御フロー付きバイナリ	angr	パス探索、制約の自動管理
特定のコード領域をエミュレート	Unicorn	高速、シンボリックオーバーヘッドなし、アンパックに適切
複雑なバイナリ+カスタムVM	angr + Unicorn (コンボ)	制御フローはangr、VMハンドラはUnicorn
カーネル/ファームウェアコード	Qiling	OS認識を伴う完全なシステムエミュレーション

---

1. ANGR — コアコンセプト

1.1 パイプライン

Project(binary)
  → Factory.entry_state() / blank_state(addr=)
    → SimulationManager(state)
      → explore(find=target, avoid=bad)
        → found[0].solver.eval(symbolic_var)

1.2 基本的なセットアップ

import angr
import claripy

proj = angr.Project('./challenge', auto_load_libs=False)

# エントリー状態: プログラムエントリーポイントから開始
state = proj.factory.entry_state()

# ブランク状態: 任意のアドレスから開始
state = proj.factory.blank_state(addr=0x401000)

# 完全初期化状態: コマンドラインargs付き
state = proj.factory.full_init_state(args=['./challenge', arg1_sym])

simgr = proj.factory.simulation_manager(state)
simgr.explore(find=0x401234, avoid=[0x401300])

if simgr.found:
    found = simgr.found[0]
    solution = found.solver.eval(symbolic_input, cast_to=bytes)
    print(f"Solution: {solution}")

1.3 シンボリック変数 (claripy)

# ビットベクトル (固定サイズ整数)
sym_input = claripy.BVS("input", 64)        # 64ビットシンボリック
sym_byte = claripy.BVS("byte", 8)           # 8ビットシンボリック
sym_buf = claripy.BVS("buffer", 8 * 32)     # 32バイトバッファ

# 具体的なビットベクトル
concrete = claripy.BVV(0x41, 8)             # 具体値 0x41

# 制約
state.solver.add(sym_input > 0)
state.solver.add(sym_input < 100)
state.solver.add(sym_byte >= 0x20)           # 印字可能ASCII
state.solver.add(sym_byte <= 0x7e)

# 評価
value = state.solver.eval(sym_input)
all_values = state.solver.eval_upto(sym_input, 10)  # 最大10個の解

1.4 シンボリックstdin

flag_len = 32
sym_stdin = claripy.BVS("stdin", 8 * flag_len)

state = proj.factory.entry_state(stdin=sym_stdin)

# 印字可能ASCIIに制約
for i in range(flag_len):
    byte = sym_stdin.get_byte(i)
    state.solver.add(byte >= 0x20)
    state.solver.add(byte <= 0x7e)

1.5 関数フック

# アドレスでフック (元のコードのN バイトをスキップ)
@proj.hook(0x401100, length=5)
def skip_check(state):
    state.regs.eax = 1  # 成功を強制

# SimProcedure: ライブラリ関数を置き換え
class MyStrcmp(angr.SimProcedure):
    def run(self, s1, s2):
        return claripy.If(
            self.state.memory.load(s1, 32) == self.state.memory.load(s2, 32),
            claripy.BVV(0, 32),
            claripy.BVV(1, 32)
        )

proj.hook_symbol('strcmp', MyStrcmp())

# 一般的な問題のある関数をフック
proj.hook_symbol('printf', angr.SIM_PROCEDURES['libc']['printf']())
proj.hook_symbol('scanf', angr.SIM_PROCEDURES['libc']['scanf']())
proj.hook_symbol('puts', angr.SIM_PROCEDURES['libc']['puts']())

1.6 メモリ操作

# メモリ読取 (シンボリック対応)
data = state.memory.load(addr, size)          # BVを返す
data_concrete = state.solver.eval(data, cast_to=bytes)

# メモリ書込
state.memory.store(addr, claripy.BVV(0x41, 8))
state.memory.store(addr, sym_buf)

# レジスタ読取/書込
rax = state.regs.rax
state.regs.rdi = claripy.BVV(0x1000, 64)

---

2. Z3 制約ソルバー

2.1 コアAPI

from z3 import *

# ソート
x = BitVec('x', 32)    # 32ビットビットベクトル
y = Int('y')             # 任意精度整数
b = Bool('b')            # ブール値

# ソルバー
s = Solver()
s.add(x + y == 42)
s.add(x > 0)
s.add(y > 0)

if s.check() == sat:
    m = s.model()
    print(f"x = {m[x]}, y = {m[y]}")

2.2 一般的なCTFパターン

# シリアルキー検証: 各文字が制約を満たす
key = [BitVec(f'k{i}', 8) for i in range(16)]
s = Solver()
for k in key:
    s.add(k >= 0x30, k <= 0x7a)  # 英数字的な範囲

# XORキー復元
plaintext = b"known_plaintext"
ciphertext = b"\x12\x34..."
key_byte = BitVec('key', 8)
s = Solver()
for p, c in zip(plaintext, ciphertext):
    s.add(p ^ key_byte == c)

# 連立一次方程式 (モジュラー)
a, b, c = BitVecs('a b c', 32)
s = Solver()
s.add(3*a + 5*b + 7*c == 0x12345678)
s.add(2*a + 4*b + 6*c == 0xDEADBEEF)
s.add(a ^ b ^ c == 0xCAFEBABE)

2.3 最適化

from z3 import Optimize

opt = Optimize()
x = BitVec('x', 32)
opt.add(x > 0)
opt.add(x < 1000)
opt.minimize(x)  # 最小値を検索
opt.check()
print(opt.model())

---

3. UNICORN ENGINE — コードエミュレーション

3.1 基本的なセットアップ

from unicorn import *
from unicorn.x86_const import *
from capstone import Cs, CS_ARCH_X86, CS_MODE_64

mu = Uc(UC_ARCH_X86, UC_MODE_64)

CODE_ADDR = 0x400000
STACK_ADDR = 0x7fff0000
STACK_SIZE = 0x10000

mu.mem_map(CODE_ADDR, 0x10000)
mu.mem_map(STACK_ADDR, STACK_SIZE)

mu.mem_write(CODE_ADDR, code_bytes)
mu.reg_write(UC_X86_REG_RSP, STACK_ADDR + STACK_SIZE - 0x1000)
mu.reg_write(UC_X86_REG_RBP, STACK_ADDR + STACK_SIZE - 0x1000)

mu.emu_start(CODE_ADDR, CODE_ADDR + len(code_bytes))

result = mu.reg_read(UC_X86_REG_RAX)

3.2 メモリおよび命令のフック

# メモリアクセスのフック
def hook_mem(uc, access, address, size, value, user_data):
    if access == UC_MEM_WRITE:
        print(f"Write {value:#x} to {address:#x}")
    elif access == UC_MEM_READ:
        print(f"Read from {address:#x}")

mu.hook_add(UC_HOOK_MEM_READ | UC_HOOK_MEM_WRITE, hook_mem)

# 特定命令のフック (トレーシング用)
def hook_code(uc, address, size, user_data):
    code = uc.mem_read(address, size)
    md = Cs(CS_ARCH_X86, CS_MODE_64)
    for insn in md.disasm(bytes(code), address):
        print(f"  {insn.address:#x}: {insn.mnemonic} {insn.op_str}")

mu.hook_add(UC_HOOK_CODE, hook_code)

3.3 ユースケース

ユースケース	アプローチ
シェルコードのアンパック	シェルコードをマップ、エミュレート、デコード済みペイロードをダンプ
文字列の復号化	復号化関数をエミュレート、制御された入力を使用
短いキーのブルートフォース	エミュレーションをループ、異なるキー入力を試す
難読化関数の解析	関数をエミュレート、レジスタ/メモリの状態を観察
ファームウェアコードエミュレーション	ファームウェアメモリレイアウトをマップ、ルーチンをエミュレート

---

4. ANGR探索戦略

4.1 find/avoid

simgr.explore(
    find=lambda s: b"Correct" in s.posix.dumps(1),   # stdoutに「Correct」を含む
    avoid=lambda s: b"Wrong" in s.posix.dumps(1)      # 「Wrong」出力を回避
)

4.2 パス爆発の管理

戦略	実装
入力スペースを制約	制約を追加 (印字可能、長さ制限)
行き止まりパスを回避	既知の失敗アドレスにavoid=を使用
複雑な関数をフック	簡略化されたSimProcedureで置き換え
ループの繰り返しを制限	state.options.add(angr.options.LAZY_SOLVES)
Veritestingを使用	simgr.explore(..., technique=angr.exploration_techniques.Veritesting())
BFSの代わりにDFS	simgr.use_technique(angr.exploration_techniques.DFS())
パスあたりのタイムアウト	simgr.explore(..., num_find=1) +タイムアウトラッパー

4.3 具体値とシンボリックのハイブリッド

state = proj.factory.entry_state(
    add_options={angr.options.UNICORN}  # 具体領域にUnicornを使用
)

これにより実行が劇的に高速化されます: 具体的なコードはUnicornでネイティブに実行され、シンボリック変数が関与している場合のみシンボリックに切り替わります。

---

5. 実用的なワークフロー

5.1 CTFバイナリ解法ワークフロー

1. 静的解析: 入力方法、成功/失敗条件を特定
   └─ 「Correct」/「Wrong」文字列を検索 → xrefアドレスを取得

2. ツールを選択:
   ├─ 純粋な数学 (バイナリ不要) → Z3
   ├─ 小さなバイナリ、明確な成功/失敗 → angrの探索
   └─ 特定の関数をエミュレート → Unicorn

3. シンボリック入力をセットアップ:
   ├─ stdin → claripy.BVS + entry_state(stdin=)
   ├─ argv → full_init_state(args=[...])
   ├─ ファイル入力 → SimFile
   └─ 特定のメモリ → state.memory.store(addr, sym)

4. 問題のある関数をフック:
   ├─ printf/puts → SimProcedureまたはno-op
   ├─ scanf → カスタムハンドラ
   ├─ time/random → 具体値を返す
   └─ アンチデバッグ → 完全にスキップ

5. 探索と抽出:
   └─ simgr.explore(find=, avoid=) → solver.eval()

---

6. デシジョンツリー

リバースチャレンジを解く必要がありますか?
│
├─ チャレンジは純粋な数学/方程式ですか?
│  └─ はい → Z3
│     ├─ 線形方程式 → BitVec + Solver
│     ├─ モジュラー演算 → BitVec (自然とmod 2^n)
│     ├─ ブール論理 → Bool + Solver
│     └─ 最適化 → Optimize + minimize/maximize
│
├─ 明確な成功/失敗を持つコンパイルされたバイナリですか?
│  └─ はい → angr
│     ├─ stdin経由の入力 → シンボリックstdin
│     ├─ argv経由の入力 → シンボリックargs付きfull_init_state
│     ├─ ファイル経由の入力 → SimFile
│     ├─ パス爆発 → 制約を追加、パスを回避、ループをフック
│     └─ 複雑なライブラリ呼び出し → SimProcedureでフック
│
├─ 特定の関数/領域をエミュレートする必要がありますか?
│  └─ はい → Unicorn Engine
│     ├─ 復号化ルーチン → コード+データをマップ、エミュレート、結果を読取
│     ├─ シェルコード解析 → シェルコードをマップ、syscallをフック
│     └─ キースケジュール → 異なる入力でエミュレート
│
├─ ファームウェア/エキゾチックアーキを解析する必要がありますか?
│  └─ はい → Qiling (OSサポート付き完全システムエミュレーション)
│
├─ バイナリはVM保護を持っていますか?
│  └─ ハンドラ解析にはangr + バイトコード制約にはZ3
│
└─ 上記のいずれも機能しませんか?
   ├─ 結合: Unicorn (具体領域) + Z3 (制約)
   ├─ デバッガを使用した手動リバースエンジニアリング
   └─ サイドチャネルアプローチ (ハードウェア用タイミング、電力解析)

---

7. 一般的な落とし穴と修正

問題	原因	修正
angrが永遠にハング	ループ内のパス爆発	ループバックエッジにavoid=を追加するか、ループをフック
Z3がunknownを返す	非線形制約が複雑すぎる	簡略化、サブ問題に分割、set_param("timeout", 5000)を使用
Unicornがsyscallでクラッシュ	syscallが処理されていない	syscall割り込みをフック、処理またはスキップ
angrが間違った結果を返す	状態初期化が不正	初期メモリレイアウトが実際のバイナリと一致することを確認
シンボリックメモリが大きすぎる	無制限のシンボリック読取	可能な限り配列インデックスを具体化
SimProcedureが間違った型	引数型のミスマッチ	呼び出し規約を確認 (cdecl vs fastcall)
angrがバイナリをロードできない	ライブラリの欠落	auto_load_libs=Falseを使用 + 必要なシンボルをフック

---

8. ツールバージョンとインストール

# angr (Python 3.8+)
pip install angr

# Z3
pip install z3-solver

# Unicorn Engine
pip install unicorn

# Capstone (逆アセンブル、Unicornとペア)
pip install capstone

# Keystone (アセンブル)
pip install keystone-engine