reverse-engineering-deep-analysis について
セキュリティ研究者向けに、隔離環境での動的解析とシンボリック実行を扱うリバースエンジニアリングスキルです。既存のライブラリやパターンを先に確認し、複数の手法で分析結果を検証します。
主な機能
- 01ライブラリカタログと既存パターンの事前確認
- 02隔離サンドボックスでの動的解析
- 03GDBによる実行状態とシステムコールの追跡
- 04AngrとZ3によるシンボリック実行
- 05メモリ、スタック、ネットワークの証拠収集
- 06分析結果の相互検証と記録
活用シーン
- 01許可を得た不審なバイナリの解析
- 02実行時の挙動や悪意ある指標の抽出
- 03脆弱性評価と未探索パスの調査
- 04シンボリック実行によるCTF課題の入力探索
MCP 対応
ガイドでは、安全なバイナリ実行にsandbox-validator、実行時の発見事項の保存にmemory-mcp、パス判断と可視化にsequential-thinkingとgraph-analystを挙げています。
インストール
コマンドをコピーしてターミナルで実行します。
npx skills add https:/ / github.com/ dnyoussef/ context-cascade --skill reverse-engineering-deep-analysisインストール後、Claude Code で/reverse-engineering-deep-analysisを入力して読み込まれたか確認します。
同梱ファイル
SKILL.md と一緒にインストールされる参考資料やスクリプト。
SKILL-meta.yamlresources/README.mdresources/scripts/angr-symbolic-exec.pygdb-automation.py詳細
ライブラリファーストプロトコル(必須)
いかなるコードを書く前にも、以下を確認しなければなりません:
ステップ 1:ライブラリカタログ
- 場所:
.claude/library/catalog.json - 一致率が 70% 超の場合:再利用または適応
ステップ 2:パターンガイド
- 場所:
.claude/docs/inventories/LIBRARY-PATTERNS-GUIDE.md - パターンが存在する場合:文書化されたアプローチに従う
ステップ 3:既存のプロジェクト
- 場所:
D:\Projects\* - 見つかった場合:抽出して適応
判断マトリクス
| 一致 | アクション |
|---|---|
| ライブラリ >90% | そのまま再利用 |
| ライブラリ 70-90% | 最小限の適応 |
| パターンが存在 | パターンに従う |
| プロジェクト内 | 抽出 |
| 一致なし | 構築(後でライブラリに追加) |
このスキルを使用する場合
このスキルは、マルウェアサンプルの分析、セキュリティ研究のためのバイナリのリバースエンジニアリング、脆弱性評価の実施、疑わしいファイルからの IOC の抽出、サプライチェーンセキュリティのためのソフトウェア検証、または CTF チャレンジやバイナリエクスプロイト研究の実施を行う場合に使用します。
このスキルを使用しない場合
商用ソフトウェアの不正なリバースエンジニアリング、本番システム上でのバイナリ分析、法的許可のないソフトウェアのリバース、利用規約や EULA への違反、または分離された環境外でのマルウェア分析には使用しないでください。単純な文字列抽出には避けてください(代わりに基本的なツールを使用してください)。
成功基準
- セキュリティに関連するすべての動作が特定されている(ネットワーク、ファイル、レジストリ、プロセスのアクティビティ)
- 悪意のある指標が信頼スコア付きで抽出されている(IOC、C2 ドメイン、暗号鍵)
- 脆弱性が該当する場合は CVE マッピング付きで文書化されている
- 分析がサンドボックス環境内で完了している(スナップショット付きの VM/コンテナ)
- 所見が複数の分析方法で検証されている(静的+動的+シンボリック)
- 完全な IOC レポートが生成されている(脅威インテリジェンス共有用の STIX/MISP 形式)
- 脆弱性評価における誤検知がゼロ
- エクスプロイトの概念実証が作成されている(脆弱性研究の場合)
エッジケースと課題
- 解析回避技術(デバッガ検出、VM 検出、タイミングチェック)
- アンパックが必要な難読化またはパックされたバイナリ
- 暗号化されたペイロードを持つ多段階マルウェア
- 専門的な分析を要するカーネルモードルートキット
- シンボリック実行の状態爆発(10,000 パス超)
- 複雑なプログラムでのバイナリ分析タイムアウト(24 時間超)
- 正規ソフトウェアの動作による誤検知
- SSL 傍受を要する暗号化されたネットワークトラフィック
ガードレール(重要なセキュリティルール)
- 未知のバイナリをホストシステム上で決して実行しない(分離された VM/サンドボックスでのみ)
- 適切な封じ込めなしでマルウェアを決して分析しない(エアギャップされたラボが望ましい)
- 法的許可なしでソフトウェアを決してリバースエンジニアリングしない
- 抽出した認証情報や暗号鍵を公開で決して共有しない
- 不正使用のためにライセンス機構を決して回避しない
- 常にネットワーク監視付きのサンドボックス環境を使用する
- 疑わしいバイナリを実行する前に常に VM スナップショットを取得する
- 常に複数の分析方法で所見を検証する
- 常にタイムスタンプ付きで分析方法論を文書化する
- 安全であると証明されるまで常にバイナリを悪意があると見なす
- マルウェアの通信を防ぐために常にネットワーク分離を使用する
- 共有前に常に IOC をサニタイズする(内部 IP アドレスを秘匿する)
証拠に基づく検証
すべてのリバースエンジニアリングの所見は、以下によって検証されなければなりません:
- 複数手法による分析 - 静的+動的+シンボリック実行が同じ動作を確認する
- サンドボックス検証 - 分離環境で実行し、すべてのアクティビティをキャプチャする
- ネットワーク監視 - パケットキャプチャがネットワークベースの所見を検証する
- メモリフォレンジック - メモリダンプを通じて実行時のシークレットを検証する
- 振る舞いの相関 - 既知のマルウェアシグネチャ(YARA、ClamAV)と相互参照する
- 再現性 - 2 人目のアナリストが分析成果物から所見を再現できる
リバースエンジニアリング:詳細分析
このスキルの機能
ランタイム実行とシンボリック探索を通じて、深いリバースエンジニアリングを実行します:
- レベル 3(1 時間以内):動的解析 - GDB を使用してサンドボックス内で実行し、メモリやシークレットをキャプチャし、システムコールをトレースします
- レベル 4(2〜6 時間):シンボリック実行 - Angr/Z3 を使用して、目標状態に到達する入力を合成します
判断ゲート:レベル 3 の後、未探索のパスに到達するためにシンボリック実行が必要かどうかを評価します。
タイムボックス:合計 3〜7 時間
前提条件
レベル 3 のツール
- GEF または Pwndbg 拡張機能を備えた GDB
- strace/ltrace - システムコール/ライブラリコールのトレース
- サンドボックス環境 - 分離された実行(firejail、Docker、またはカスタム)
レベル 4 のツール
- Angr - シンボリック実行フレームワーク(Python)
- Z3 - SMT ソルバー
- Python 3.9+ - Angr スクリプト用
MCP サーバー
sandbox-validator- 安全なバイナリ実行memory-mcp- ランタイムの調査結果を保存sequential-thinking- パス探索の判断graph-analyst- 実行パスを可視化
⚠️ 重大なセキュリティ警告
未知のバイナリをホストシステム上で絶対に実行しないでください!
すべての動的解析、デバッグ、シンボリック実行は、以下で実行する必要があります:
- 分離された VM(ロールバック用のスナップショットを備えた VMware/VirtualBox)
- セキュリティポリシーを設定した Docker コンテナ(
--security-opt、--cap-drop=ALL) - ネットワーク監視を備えた sandbox-configurator スキル経由の E2B サンドボックス
- 専用のマルウェア解析ラボ(APT を扱う場合はエアギャップ化)
安全でない実行の結果:
- カーネルレベルのルートキットを伴うマルウェア感染
- メモリ破損とシステムの不安定化
- 隠蔽チャネルを介したデータ流出
- トロイの木馬化されたビルドによるサプライチェーン攻撃
- システムの完全な侵害
安全なプラクティス:
- 常にスナップショット付きのサンドボックス環境を使用する
- 実行中のシステムコールとネットワークアクティビティを監視する
- GDB/Angr は分離されたコンテナ内でのみ使用する
- 本番システム上のバイナリにデバッガをアタッチしない
- シンボリック実行の前にすべての入力を検証する
- 静的解析によって安全であると証明されるまで、すべてのバイナリを悪意があるとみなす
クイックスタート
# 1. Full deep analysis (Levels 3+4)
/re:deep crackme.exe
# 2. Dynamic analysis only (Level 3)
/re:dynamic server.bin --args "--port 8080"
# 3. Symbolic execution only (Level 4)
/re:symbolic challenge.exe --target-addr 0x401337
レベル 3:動的解析(1 時間以内)
ステップ 1:サンドボックス内での安全な実行
/re:dynamic binary.exe --args "test input" --sandbox true
サンドボックス化:
- ファイルシステムの分離(/usr、/bin を読み取り専用に)
- ネットワークを無効化または監視
- プロセス制限(CPU、メモリ、時間)
- マルウェアの脱出を防止
ステップ 2:静的解析コンテキストの取得
実行の前に、スキルはレベル 2 の調査結果を自動的に取得します:
// Check memory-mcp for static analysis results
const staticFindings = await mcp__memory-mcp__vector_search({
query: binary_hash,
filter: {category: "reverse-engineering", re_level: 2}
})
// Extract critical functions and suggested breakpoints
const breakpoints = staticFindings.critical_functions.map(f => f.address)
// Example: ["0x401234", "0x401567", "0x4018ab"]
ステップ 3:ブレークポイントを自動ロードした GDB セッション
レベル 2 の静的解析からブレークポイントを自動的にロードします:
# Auto-generated from static analysis
break *0x401234 # check_password function
break *0x401567 # validate_license function
break *0x4018ab # decrypt_config function
# Run with test input
run --flag "test_input_from_user"
GDB セッションコマンド(自動的に実行されます):
# At each breakpoint:
# 1. Dump all registers
info registers
# 2. Dump stack (100 bytes)
x/100x $rsp
# 3. Dump heap allocations (if applicable)
info proc mappings
x/100x [heap_address]
# 4. Search for secrets in memory
find 0x600000, 0x700000, "password"
find 0x600000, 0x700000, "admin"
# 5. Dump interesting strings from registers
x/s $rdi # First argument (often string pointer)
x/s $rsi # Second argument
ステップ 4:ランタイム状態のキャプチャ
各ブレークポイントで、スキルは以下をキャプチャします:
レジスタ状態:
RAX: 0x0000000000401337
RBX: 0x0000000000000000
RCX: 0x00007fffffffe010 → "user_input_here"
RDX: 0x0000000000000010
RSI: 0x00007fffffffe020 → "expected_password"
RDI: 0x00007fffffffe030 → buffer
RBP: 0x00007fffffffe100
RSP: 0x00007fffffffe0e0
RIP: 0x0000000000401234 → check_password
スタックダンプ(re-project/dbg/0x401234-stack.bin に保存):
0x7fffffffe0e0: 0x0000000000401337 0x0000000000000000
0x7fffffffe0f0: 0x00007fffffffe200 0x0000000000000001
メモリ内のシークレット(自動的に抽出):
Found at 0x601000: "admin:SecretP@ss123"
Found at 0x601020: "license_key=ABC-DEF-GHI-JKL"
Found at 0x601040: "api_token=eyJhbGciOiJIUzI1NiIs..."
システムコールトレース(strace 経由):
# Automatically executed in parallel
strace -o re-project/dbg/syscalls.log ./binary.exe --flag test
出力:
open("/etc/config.ini", O_RDONLY) = 3
read(3, "password=admin123\n", 1024) = 18
socket(AF_INET, SOCK_STREAM, 0) = 4
connect(4, {sa_family=AF_INET, sin_port=htons(443), sin_addr=inet_addr("192.168.1.100")}, 16) = 0
send(4, "POST /api/login HTTP/1.1\r\n...", 256, 0) = 256
ステップ 5:出力構造
re-project/dbg/
├── gdb-session.log # Full GDB transcript
├── breakpoints.txt # List of breakpoints set
├── memory-dumps/
│ ├── 0x401234-registers.txt
│ ├── 0x401234-stack.bin
│ ├── 0x401567-registers.txt
│ ├── 0x401567-stack.bin
│ └── 0x4018ab-heap.bin
├── syscalls.log # strace output
├── libcalls.log # ltrace output
└── runtime-secrets.txt # Extracted passwords, keys, tokens
ステップ 6:判断ゲート - レベル 4 にエスカレートするか?
// Automatically evaluated via sequential-thinking MCP
const decision = await mcp__sequential-thinking__evaluate({
question: "Should we proceed to symbolic execution (Level 4)?",
factors: [
`Branches explored: ${explored_branches}/${total_branches}`,
`Unreachable code found: ${unreachable_functions.length > 0}`,
`User's question answered: ${findings_sufficient}`,
`Input-dependent paths: ${symbolic_paths_needed}`
]
})
// Example evaluation:
// - Explored 12/20 branches (60% coverage)
// - Found 3 unreachable functions (possible anti-debug)
// - User wants to reach "win" function at 0x401337 (NOT YET REACHED)
// - Input-dependent path detected (password check with strcmp)
// DECISION: ESCALATE TO LEVEL 4
レベル 4:シンボリック実行(2〜6 時間)
ステップ 1:動的解析から目標状態を定義する
# From Level 3: Couldn't reach "win" function at 0x401337 with manual inputs
target_addr = 0x401337 # Goal: Find input that reaches this
# From Level 3: These functions lead to failure/exit
avoid_addrs = [
0x401400, # fail_message function
0x401500, # bad_password function
0x401600 # exit_program function
]
ステップ 2:シンボリック探索の起動
/re:symbolic binary.exe \
--target-addr 0x401337 \
--avoid-addrs 0x401400,0x401500,0x401600 \
--max-states 1000 \
--timeout 7200
内部で行われていること:
import angr
import claripy
# Step 2.1: Load binary into Angr project
project = angr.Project('./binary.exe', auto_load_libs=False)
# Step 2.2: Create symbolic input
# Assume input is 32-byte flag
flag_length = 32
flag = claripy.BVS('flag', flag_length * 8)
# Step 2.3: Create entry state with symbolic stdin
state = project.factory.entry_state(
stdin=flag,
add_options={angr.options.LAZY_SOLVES}
)
# Step 2.4: Add constraints - printable ASCII only
for byte in flag.chop(8):
state.add_constraints(byte >= 0x20) # Printable ASCII start
state.add_constraints(byte <= 0x7e) # Printable ASCII end
# Step 2.5: Create simulation manager
simgr = project.factory.simulation_manager(state)
# Step 2.6: Explore paths (DFS strategy)
simgr.explore(
find=0x401337, # Target address
avoid=[0x401400, 0x401500, 0x401600], # Avoid addresses
num_find=1, # Stop after finding first solution
max_states=1000 # Prevent state explosion
)
# Step 2.7: Check if solution found
if simgr.found:
# Extract concrete input
solution_state = simgr.found[0]
solution = solution_state.solver.eval(flag, cast_to=bytes)
print(f"Solution: {solution.decode()}")
# Save solution
with open('re-project/sym/solutions/solution-1.txt', 'wb') as f:
f.write(solution)
else:
print("No solution found within constraints")
ステップ 3:高度なシンボリック技法
技法 1:ライブラリ関数のフック
# Replace complex library functions with symbolic summaries
import angr
# Hook strcmp to return symbolic value
class StrCmpHook(angr.SimProcedure):
def run(self, s1, s2):
# Return symbolic comparison result
s1_str = self.state.memory.load(s1, 32)
s2_str = self.state.memory.load(s2, 32)
return s1_str == s2_str
project.hook_symbol('strcmp', StrCmpHook())
技法 2:複雑なパスのための状態マージ
# Merge states at loop entry to prevent explosion
simgr.use_technique(angr.exploration_techniques.Veritesting())
# Alternative: Manual state merging
while simgr.active:
simgr.step()
if len(simgr.active) > 50:
# Merge similar states
simgr.merge()
技法 3:制約の単純化
# Add intermediate constraints to guide exploration
state.add_constraints(
flag[0:4] == b'FLAG' # Known prefix from hints
)
# This reduces search space dramatically
# Without: 256^32 possibilities
# With: 256^28 possibilities (4 bytes fixed)
ステップ 4:解の検証
# Test synthesized input
echo "FLAG_synthesized_solution_here" | ./binary.exe
# Expected output:
# "Success! You reached the target state."
# "Congratulations! Flag: CTF{...}"
検証手順:
- 合成した入力でバイナリを実行する
- 実行が目標アドレス(0x401337)に到達することを確認する
- 出力が期待される成功メッセージと一致することを確認する
- 検証済みの解を memory-mcp に保存する
ステップ 5:出力構造
re-project/sym/
├── angr-script.py # Reproducible Angr script
├── solutions/
│ ├── solution-1.txt # First valid solution
│ ├── solution-2.txt # Alternative solution (if --find-all)
│ └── solution-3.txt
├── constraints/
│ ├── path-1.smt2 # Z3 constraints for path 1
│ ├── path-2.smt2
│ └── simplified.smt2 # Simplified constraint set
├── validation.log # Validation test results
└── exploration-metrics.json # States explored, time taken, coverage
exploration-metrics.json:
{
"total_states": 847,
"found_states": 3,
"avoided_states": 124,
"deadended_states": 720,
"execution_time_sec": 3245,
"coverage_percent": 78.5,
"memory_usage_mb": 2847,
"solutions_found": 3
}
高度なオプション
カスタムブレークポイント(動的解析)
# Set breakpoints at crypto functions
/re:dynamic binary.exe --breakpoints AES_encrypt,RSA_sign,MD5_update
# Set breakpoints at specific addresses
/re:dynamic binary.exe --breakpoints 0x401000,0x402000,0x403000
# Conditional breakpoints (GDB syntax)
/re:dynamic binary.exe --breakpoints "0x401234 if $rdi == 0x601000"
高度な GDB スクリプティング:
# Custom GDB Python script (auto-loaded if found)
# re-project/gdb-script.py
import gdb
class PasswordBreakpoint(gdb.Breakpoint):
def __init__(self, location):
super().__init__(location)
def stop(self):
# Extract password from RDI register
rdi = gdb.parse_and_eval('$rdi')
password = gdb.execute(f'x/s {rdi}', to_string=True)
# Log to file
with open('passwords.log', 'a') as f:
f.write(f"{password}\n")
# Continue execution
return False
# Set custom breakpoint
PasswordBreakpoint("check_password")
シンボリック探索戦略
戦略 1: すべての解を見つける
# Exhaustive search (may take hours)
/re:symbolic binary.exe \
--target-addr 0x401337 \
--find-all true \
--max-solutions 10 \
--timeout 14400
# In Angr script
simgr.explore(
find=0x401337,
avoid=avoid_addrs,
num_find=10 # Find up to 10 solutions
)
# Process all found solutions
for idx, state in enumerate(simgr.found):
solution = state.solver.eval(flag, cast_to=bytes)
with open(f'solution-{idx+1}.txt', 'wb') as f:
f.write(solution)
戦略 2: 状態爆発を制限する
# Aggressive pruning
/re:symbolic binary.exe \
--max-states 100 \
--avoid-addrs 0x401400,0x401500,0x401600 \
--strategy dfs # Depth-first search (memory efficient)
# Use Veritesting to merge paths
simgr.use_technique(angr.exploration_techniques.Veritesting())
# Drop states if too many active
simgr.use_technique(angr.exploration_techniques.LengthLimiter(max_length=100))
# Prioritize states closer to target
simgr.use_technique(angr.exploration_techniques.Explorer(
find=0x401337,
avoid=avoid_addrs,
num_find=1
))
戦略 3: 制約が不十分なシンボリック実行
# Start from target address and work backwards
project = angr.Project('./binary.exe')
# Create state at target address (not entry point)
state = project.factory.blank_state(addr=0x401337)
# Make all memory symbolic
state.options.add(angr.options.SYMBION_SYNC_CLE)
# Explore backwards to find required input
simgr = project.factory.simulation_manager(state)
simgr.explore(find=project.entry)
# This finds inputs that MUST lead to target
メモリダンプ分析
# Dump specific memory regions
/re:dynamic binary.exe \
--dump-regions heap,stack,data \
--dump-at-breakpoints 0x401234,0x401567
カスタムメモリ分析:
# GDB Python script for heap analysis
import gdb
def analyze_heap():
# Get heap boundaries
mappings = gdb.execute('info proc mappings', to_string=True)
heap_start = extract_heap_start(mappings)
heap_end = extract_heap_end(mappings)
# Scan for interesting patterns
for addr in range(heap_start, heap_end, 8):
value = gdb.execute(f'x/g {addr}', to_string=True)
# Check if value looks like a pointer
if is_valid_pointer(value):
gdb.execute(f'x/s {value}') # Dereference as string
analyze_heap()
包括的なワークフロー例
ワークフロー 1: 実行時のシークレットを用いたマルウェア分析
シナリオ: マルウェアサンプルを分析し、C2 サーバーの URL と暗号化キーを抽出する
フェーズ 1: 動的分析(レベル 3)
# Step 1: Safe sandbox execution
/re:dynamic malware.exe --sandbox true --network-monitor true
# Step 2: GDB session auto-starts with breakpoints from static analysis
# Breakpoints at: decrypt_config, connect_to_c2, send_beacon
# Step 3: At decrypt_config breakpoint (0x401234)
(gdb) info registers
RAX: 0x0000000000601000 → encrypted_buffer
RDI: 0x0000000000601100 → decryption_key
(gdb) x/s 0x601100
0x601100: "hardcoded_AES_key_12345"
# Step 4: Continue to connect_to_c2 breakpoint (0x401567)
(gdb) continue
(gdb) x/s $rdi
0x601200: "http://malicious-c2.tk:8443/beacon"
# Step 5: Extract all findings
Runtime Secrets Found:
- AES Key: "hardcoded_AES_key_12345"
- C2 URL: "http://malicious-c2.tk:8443/beacon"
- User-Agent: "Mozilla/5.0 (Windows NT 10.0; Win64; x64)"
フェーズ 2: 判断ゲート
// Automatically evaluated
QUESTION: "Proceed to symbolic execution?"
FACTORS:
- All critical functions reached ✅
- Secrets extracted (AES key, C2 URL) ✅
- User's question answered (extract IOCs) ✅
- No unreachable paths requiring symbolic execution ❌
DECISION: STOP AT LEVEL 3 (sufficient findings)
出力: 完全な IOC 抽出を伴い、マルウェア分析が 45 分で完了します。
ワークフロー 2: CTF チャレンジ - ライセンスチェックのリバースエンジニアリング
シナリオ: バイナリ内の「プレミアム機能」を解除するための有効なライセンスキーを見つける
フェーズ 1: 動的分析(レベル 3)
# Step 1: Test with invalid key
/re:dynamic challenge.exe --args "--license AAAA-BBBB-CCCC-DDDD"
# Output: "Invalid license key"
# Step 2: GDB reveals license check at 0x401234
(gdb) break *0x401234
(gdb) run --license AAAA-BBBB-CCCC-DDDD
# Step 3: Examine comparison
(gdb) x/s $rdi
0x7fffffffe010: "AAAA-BBBB-CCCC-DDDD" # User input
(gdb) x/s $rsi
0x601000: [encrypted data, not readable]
# Observation: License key is compared against encrypted/hashed value
# Cannot extract valid key directly from memory
フェーズ 2: 判断ゲート
QUESTION: "Proceed to symbolic execution?"
FACTORS:
- License check function found ✅
- Valid key NOT extractable from memory ✅
- Comparison is complex (encryption/hashing) ✅
- User wants valid license key ✅
DECISION: ESCALATE TO LEVEL 4 (symbolic execution required)
フェーズ 3: シンボリック実行(レベル 4)
# Launch Angr symbolic execution
/re:symbolic challenge.exe \
--target-addr 0x401337 \ # "Premium features unlocked" message
--avoid-addrs 0x401400 \ # "Invalid license" path
--input-format "FLAG-XXXX-XXXX-XXXX" \
--max-states 500
Angr スクリプト(自動生成):
import angr
import claripy
project = angr.Project('./challenge.exe', auto_load_libs=False)
# License key format: FLAG-XXXX-XXXX-XXXX (19 chars)
license_key = claripy.BVS('license', 19 * 8)
# Create entry state with symbolic license as argv[2]
state = project.factory.entry_state(args=['./challenge.exe', '--license', license_key])
# Constrain to valid format: FLAG-XXXX-XXXX-XXXX
for i in range(19):
if i in [0, 1, 2, 3]: # "FLAG"
state.add_constraints(license_key.get_byte(i) == ord("FLAG"[i]))
elif i in [4, 9, 14]: # Dashes
state.add_constraints(license_key.get_byte(i) == ord('-'))
else: # X = uppercase letters or digits
byte = license_key.get_byte(i)
state.add_constraints(
claripy.Or(
claripy.And(byte >= ord('A'), byte <= ord('Z')),
claripy.And(byte >= ord('0'), byte <= ord('9'))
)
)
# Explore
simgr = project.factory.simulation_manager(state)
simgr.explore(find=0x401337, avoid=0x401400)
if simgr.found:
solution = simgr.found[0].solver.eval(license_key, cast_to=bytes)
print(f"Valid License: {solution.decode()}")
# Output: "FLAG-A7B2-C9D4-E1F6"
検証:
$ ./challenge.exe --license FLAG-A7B2-C9D4-E1F6
Premium features unlocked!
Congratulations! Here is your flag: CTF{symbolic_execution_wins}
出力: チャレンジを合計 3.5 時間で解決(45 分の動的分析 + 3 時間のシンボリック実行)。
ワークフロー 3: 脆弱性リサーチ - バッファオーバーフロー
シナリオ: サーバーバイナリ内で悪用可能なバッファオーバーフローを見つける
フェーズ 1: 動的分析(レベル 3)
# Step 1: Launch server in sandbox
/re:dynamic server.bin --args "--port 8080" --sandbox true
# Step 2: Fuzz with large inputs
echo "A"*1000 | nc localhost 8080
# GDB catches segfault
Program received signal SIGSEGV, Segmentation fault.
0x4141414141414141 in ?? ()
# Step 3: Analyze crash
(gdb) info registers
RIP: 0x4141414141414141 # Overwritten return address
RSP: 0x7fffffffe100
RBP: 0x4141414141414141
(gdb) x/100x $rsp
# Shows stack completely overwritten with 'A' (0x41)
# Step 4: Find offset to return address
# Use pattern_create and pattern_offset from GEF/Pwndbg
(gdb) pattern create 1000
(gdb) run
# Crash at offset 512
# Confirmed: Buffer overflow at offset 512, control of RIP
フェーズ 2: 判断ゲート
QUESTION: "Proceed to symbolic execution?"
FACTORS:
- Buffer overflow confirmed ✅
- Offset to RIP known (512 bytes) ✅
- Exploitation demonstrated ✅
- User's goal: find vulnerability ✅ (COMPLETE)
DECISION: STOP AT LEVEL 3 (vulnerability found)
出力: 脆弱性リサーチが 30 分で完了します。
トラブルシューティング
問題 1: サンドボックスが実行をブロックする
症状: バイナリが「Permission denied」またはシステムコールがブロックされたエラーで実行に失敗する
原因: サンドボックスが厳しすぎて、必要なシステムコールをブロックしている
解決策 1: 必要なシステムコールをホワイトリストに登録する
# Check which syscalls are blocked
strace ./binary.exe 2>&1 | grep "Operation not permitted"
# Create custom seccomp profile
cat > sandbox-profile.json <<EOF
{
"defaultAction": "SCMP_ACT_ERRNO",
"syscalls": [
{"names": ["read", "write", "open", "close"], "action": "SCMP_ACT_ALLOW"},
{"names": ["socket", "connect"], "action": "SCMP_ACT_ALLOW"}
]
}
EOF
# Use custom profile
/re:dynamic binary.exe --sandbox-profile sandbox-profile.json
解決策 2: より制限の緩いサンドボックスを使用する
# Disable network isolation only (allow file access)
/re:dynamic server.bin --sandbox true --allow-network true
# Or use Docker instead of seccomp
docker run --rm -v $(pwd):/work -it ubuntu:20.04 /work/binary.exe
問題 2: GDB のアタッチに失敗する
症状: 「ptrace: Operation not permitted」が表示される、または GDB が起動しない
原因: システムのセキュリティ設定が ptrace を妨げている
解決策 1: 一時的に ptrace を許可する(Linux)
# Check current setting
cat /proc/sys/kernel/yama/ptrace_scope
# 1 = restricted, 0 = unrestricted
# Temporarily allow (requires sudo)
echo 0 | sudo tee /proc/sys/kernel/yama/ptrace_scope
# Rerun analysis
/re:dynamic binary.exe
解決策 2: sudo で GDB を実行する
sudo /re:dynamic binary.exe
解決策 3: コンテナを使用する(ホストの制限を回避する)
docker run --cap-add=SYS_PTRACE --rm -it ubuntu:20.04 bash
# Inside container:
apt update && apt install gdb
gdb ./binary.exe
問題 3: Angr の状態爆発
症状: シンボリック実行がメモリ不足になる、または数千のアクティブ状態によりタイムアウトする
原因: バイナリの分岐が多すぎて、指数的な状態爆発が発生している
解決策 1: avoid 状態をさらに追加する
# Find all "failure" functions from static analysis
/re:static binary.exe --list-functions | grep -i "fail\|error\|exit"
# Add all failure addresses to avoid list
/re:symbolic binary.exe \
--target-addr 0x401337 \
--avoid-addrs 0x401400,0x401500,0x401600,0x401700,0x401800 \
--max-states 100
解決策 2: Veritesting を使用する(状態を自動的にマージする)
# In custom Angr script
simgr.use_technique(angr.exploration_techniques.Veritesting())
# This merges similar states, reducing explosion by 10-100x
解決策 3: 中間アドレスから開始する(重要でないコードをスキップする)
# Skip initialization code, start at license check function
state = project.factory.blank_state(addr=0x401234)
# Set up expected register/memory state (from Level 3 analysis)
state.regs.rdi = state.solver.BVS('input', 32*8)
# Explore from this point only
simgr = project.factory.simulation_manager(state)
simgr.explore(find=0x401337)
問題 4: メモリダンプが大きすぎる
症状: GDB が数ギガバイトのメモリをダンプし、ディスク容量を圧迫する
原因: 対象の領域ではなくアドレス空間全体をダンプしている
解決策 1: vmmap から特定のメモリ領域を対象にする
# Check memory mappings
(gdb) info proc mappings
# Example output:
# 0x400000-0x600000 r-xp /path/binary.exe (code)
# 0x600000-0x700000 rw-p /path/binary.exe (data)
# 0x7ffff7a0d000-0x7ffff7bcd000 r-xp /lib/libc.so (library)
# Dump ONLY data section (where secrets likely are)
(gdb) dump binary memory data-section.bin 0x600000 0x700000
# Dump ONLY stack (where local variables are)
(gdb) dump binary memory stack.bin $rsp-0x1000 $rsp+0x1000
解決策 2: 選択的なブレークポイントダンプを使用する
# Only dump memory at specific breakpoints, not every instruction
/re:dynamic binary.exe \
--breakpoints 0x401234,0x401567 \
--dump-at-breakpoints true \
--dump-regions stack,heap
問題 5: シンボリック実行のタイムアウト
症状: Angr が数時間実行しても解を見つけられない
原因: 制約ソルバー(Z3)が複雑な制約で行き詰まっている
解決策 1: タイムアウトを増やし、制約を単純化する
/re:symbolic binary.exe \
--timeout 14400 \ # 4 hours
--max-states 200 \
--simplify-constraints true
解決策 2: インクリメンタルソルビングを使用する
# Add constraints incrementally instead of all at once
state.solver.add(constraint1)
if state.satisfiable():
state.solver.add(constraint2)
if state.satisfiable():
state.solver.add(constraint3)
解決策 3: より高速なソルバー(CVC4 または Boolector)を使用する
import angr
import claripy
# Use faster solver backend
claripy.backends.backend_manager.backends._eager_backends = [
claripy.backends.BackendConcrete,
claripy.backends.BackendZ3 # Replace with BackendCVC4
]
パフォーマンス最適化
動的分析の高速化(レベル 3)
最適化 1: 並列システムコールトレース
# Run strace and ltrace in parallel
(strace -o syscalls.log ./binary.exe &)
(ltrace -o libcalls.log ./binary.exe &)
wait
最適化 2: 自動化のための GDB スクリプティング
# GDB Python script for automatic analysis
# re-project/auto-analyze.py
import gdb
breakpoints = [0x401234, 0x401567, 0x4018ab]
for bp_addr in breakpoints:
gdb.Breakpoint(f"*{bp_addr}")
# Run until first breakpoint
gdb.execute('run')
# At each breakpoint, dump and continue
for i in range(len(breakpoints)):
# Dump state
regs = gdb.execute('info registers', to_string=True)
stack = gdb.execute('x/100x $rsp', to_string=True)
with open(f'bp-{i}-state.txt', 'w') as f:
f.write(f"Registers:\n{regs}\nStack:\n{stack}\n")
# Continue
if i < len(breakpoints) - 1:
gdb.execute('continue')
使用方法:
gdb -x auto-analyze.py ./binary.exe
最適化 3: 選択的なメモリダンプ
# Only dump memory if interesting patterns found
/re:dynamic binary.exe \
--dump-on-pattern "password|secret|key|token" \
--dump-regions heap
シンボリック実行の高速化(レベル 4)
最適化 1: より高速な探索戦略を使用する
# DFS is memory-efficient but may explore wrong paths
simgr.use_technique(angr.exploration_techniques.DFS())
# BFS finds shortest path but uses more memory
simgr.use_technique(angr.exploration_techniques.BFS())
# Hybrid: BFS until 100 states, then switch to DFS
simgr.use_technique(angr.exploration_techniques.Explorer(
find=0x401337,
num_find=1
))
最適化 2: 入力空間を事前に制約する
# If you know input must start with "FLAG"
for i, char in enumerate("FLAG"):
state.add_constraints(flag.get_byte(i) == ord(char))
# This reduces search space from 256^32 to 256^28
最適化 3: 複雑な関数をフックする
# Replace slow library functions with fast symbolic summaries
project.hook_symbol('strlen', angr.SIM_PROCEDURES['libc']['strlen']())
project.hook_symbol('strcmp', angr.SIM_PROCEDURES['libc']['strcmp']())
project.hook_symbol('memcpy', angr.SIM_PROCEDURES['libc']['memcpy']())
# These are much faster than symbolically executing the actual implementations
最適化 4: 探索を並列化する
# Split state space across multiple cores
from multiprocessing import Pool
def explore_from_state(state):
simgr = project.factory.simulation_manager(state)
simgr.explore(find=0x401337, avoid=avoid_addrs)
return simgr.found
# Split initial state into 4 copies with different constraints
states = [state.copy() for _ in range(4)]
states[0].add_constraints(flag[0] < 0x40)
states[1].add_constraints(claripy.And(flag[0] >= 0x40, flag[0] < 0x60))
states[2].add_constraints(claripy.And(flag[0] >= 0x60, flag[0] < 0x80))
states[3].add_constraints(flag[0] >= 0x80)
# Explore in parallel
with Pool(4) as p:
results = p.map(explore_from_state, states)
# Collect solutions
for found_states in results:
if found_states:
print(found_states[0].solver.eval(flag, cast_to=bytes))
Memory-MCP 統合
レベル 3 の調査結果を保存する
// After dynamic analysis completes
mcp__memory-mcp__memory_store({
content: {
binary_hash: "sha256:abc123...",
re_level: 3,
execution_summary: {
breakpoints_hit: ["0x401234", "0x401567", "0x4018ab"],
runtime_secrets: [
{type: "password", value: "admin123", location: "0x601000"},
{type: "api_key", value: "sk_live_...", location: "0x601020"}
],
syscalls: ["open", "read", "socket", "connect", "send"],
network_activity: [
{proto: "HTTP", dest: "192.168.1.100:443", data: "POST /api/login"}
]
},
gdb_dumps: {
registers: "re-project/dbg/memory-dumps/",
stack: "re-project/dbg/memory-dumps/",
heap: "re-project/dbg/memory-dumps/"
}
},
metadata: {
agent: "RE-Runtime-Tracer",
category: "reverse-engineering",
intent: "dynamic-analysis",
layer: "long_term",
project: `binary-analysis-${date}`,
keywords: ["gdb", "dynamic", "runtime", "secrets"],
re_level: 3,
binary_hash: "sha256:abc123...",
timestamp: new Date().toISOString()
}
})
レベル 4 の調査結果を保存する
// After symbolic execution completes
mcp__memory-mcp__memory_store({
content: {
binary_hash: "sha256:abc123...",
re_level: 4,
symbolic_summary: {
target_address: "0x401337",
avoid_addresses: ["0x401400", "0x401500"],
solutions_found: 3,
solutions: [
{input: "FLAG-A7B2-C9D4-E1F6", validated: true},
{input: "FLAG-B8C3-D0E5-F2G7", validated: true},
{input: "FLAG-C9D4-E1F6-G3H8", validated: true}
],
exploration_metrics: {
total_states: 847,
execution_time_sec: 3245,
coverage_percent: 78.5
}
},
angr_script: "re-project/sym/angr-script.py",
constraints: "re-project/sym/constraints/"
},
metadata: {
agent: "RE-Symbolic-Solver",
category: "reverse-engineering",
intent: "symbolic-execution",
layer: "long_term",
project: `binary-analysis-${date}`,
keywords: ["angr", "symbolic", "z3", "solver"],
re_level: 4,
binary_hash: "sha256:abc123...",
timestamp: new Date().toISOString()
}
})
ハンドオフパターン: レベル 3 → レベル 4
// Level 3 stores handoff data
mcp__memory-mcp__memory_store({
key: `re-handoff/dynamic-to-symbolic/${binary_hash}`,
value: {
decision: "ESCALATE_TO_LEVEL_4",
reason: "Target function unreachable with manual inputs",
target_address: "0x401337",
avoid_addresses: ["0x401400", "0x401500", "0x401600"],
input_format: "FLAG-XXXX-XXXX-XXXX",
breakpoint_findings: {
"0x401234": {
description: "License check function",
comparison_type: "encrypted",
extractable: false
}
}
}
})
// Level 4 retrieves handoff data
const handoff = await mcp__memory-mcp__vector_search({
query: `re-handoff/dynamic-to-symbolic/${binary_hash}`
})
// Use handoff data to configure Angr
const target = handoff.target_address
const avoid = handoff.avoid_addresses
const input_format = handoff.input_format
エージェントとコマンド
起動されるエージェント
-
RE-Runtime-Tracer (レベル 3)
- 専門分野: GDB/strace/ltrace による動的解析
- ツール: GDB+GEF/Pwndbg、strace、ltrace、サンドボックス環境
- 出力: メモリダンプ、システムコールトレース、実行時のシークレット
-
RE-Symbolic-Solver (レベル 4)
- 専門分野: Angr/Z3 によるシンボリック実行
- ツール: Angr、Z3、Python シンボリック実行フレームワーク
- 出力: 合成された入力、制約ファイル、検証済みのソリューション
-
sandbox-validator (レベル 3、自動)
- 安全なバイナリ実行環境を提供します
- マルウェアの脱出とシステムへの損傷を防ぎます
-
graph-analyst (レベル 4、自動)
- 実行パスの可視化を生成します
- 制約依存関係グラフを作成します
スラッシュコマンド
/re:deep <binary>- 完全なレベル 3+4 分析 (このスキルの主要コマンド)/re:dynamic <binary>- レベル 3 のみ (動的解析)/re:symbolic <binary>- レベル 4 のみ (シンボリック実行)
MCP サーバー
- sandbox-validator: 分離による安全なバイナリ実行
- memory-mcp: セッションをまたぐ永続化、ハンドオフの調整
- sequential-thinking: エスカレーションのための意思決定ゲートロジック
- graph-analyst: 実行パスと制約の可視化
関連スキル
- リバースエンジニアリング: クイックトリアージ - レベル 1-2 (文字列 + 静的)
- リバースエンジニアリング: ファームウェア - レベル 5 (ファームウェア抽出)
- 機能性監査 - リバースエンジニアリングされたロジックを検証
- 本番環境バリデーター - 分析結果が本番環境対応であることを確認
リソース
外部ツール
- GDB - GNU デバッガー
- GEF - GDB 拡張機能
- Pwndbg - エクスプロイト開発用の GDB プラグイン
- Angr - バイナリ解析プラットフォーム
- Z3 - Microsoft SMT ソルバー
学習リソース
- Angr ドキュメント - Angr の完全ガイド
- Z3 チュートリアル - Z3 Python バインディング
- GDB から LLDB へのコマンドマップ - macOS ユーザー向け
- Practical Binary Analysis - 書籍
コミュニティ
- Angr Slack - 公式 Angr コミュニティ
- r/ReverseEngineering - Subreddit
- Binary Ninja Discord - リバースエンジニアリングコミュニティ
作成日: 2025-11-01 RE レベル: 3-4 (動的解析 + シンボリック実行) タイムボックス: 3-7 時間 エージェント: RE-Runtime-Tracer、RE-Symbolic-Solver カテゴリ: セキュリティ、マルウェア解析、CTF、バイナリエクスプロイト 難易度: 上級
中核となる原則
リバースエンジニアリング: ディープ分析は 3 つの基本原則に基づいて動作します:
原則 1: 分離を最優先した実行
実行時解析は、マルウェアの脱出とシステムの侵害を防ぐため、必ず分離された環境で行わなければなりません。
実際には:
- ネットワーク監視を備えたスナップショット VM/コンテナですべてのバイナリを実行する
- サンドボックス化されたデバッガー (Docker 内の GDB、スナップショットモードの QEMU) を使用する
- 実行中にシステムコール、ネットワークトラフィック、ファイル操作を監視する
- APT 分析用にエアギャップされたラボインフラを維持する
原則 2: 複数手法による検証
単一の解析手法で完全な真実が得られることはなく、相互検証によって誤検知を防ぎます。
実際には:
- 静的解析の知見は動的実行によって確認されなければならない
- 動的な挙動は複数回の実行を通じて再現可能でなければならない
- シンボリック実行の結果は実際の実行パスと照合して検証されなければならない
- メモリダンプはネットワークキャプチャとシステムコールトレースと関連付けられなければならない
原則 3: 段階的なエスカレーション
軽量な手法から始め、分析時間を最小限に抑えるために必要な場合にのみエスカレーションします。
実際には:
- レベル 3(動的)は、1 時間以内にマルウェアの挙動の 80% を明らかにします
- 手動でパスに到達できない場合にのみ、レベル 4(シンボリック)にエスカレーションします
- 意思決定ゲートを使用して、単純な分析タスクの過剰な設計を避けます
- 調査結果を memory-mcp にキャッシュして、重複した作業を防ぎます
よくあるアンチパターン
| アンチパターン | 問題 | 解決策 |
|---|---|---|
| ホストシステム上でマルウェアを実行する | システム全体の侵害、データ漏洩、ランサムウェアの展開 | 常にスナップショット、ネットワーク監視、ロールバック機能を備えた分離された VM を使用してください |
| 動的解析の前に静的解析を省略する | 理解せずに実行して時間を無駄にし、パックされたバイナリを見逃す | まずレベル 1〜2(strings + 静的)を実行して、エントリポイントとブレークポイントを特定してください |
| シンボリック実行に過度に依存する | 状態爆発、分析タイムアウト、リソース枯渇 | 手動ファジングでは到達できない入力依存のパスにのみ、シンボリック実行を使用してください |
| アンチ分析技術を無視する | デバッガ検出により分析が終了し、VM 検出により挙動が変化する | アンチデバッグチェックにパッチを適用し、ステルスなデバッグ環境を使用し、タイミング攻撃を監視してください |
| 方法論を文書化しない | 結果が再現できず、調査結果が異議を唱えられ、法的問題が生じる | すべての操作にタイムスタンプを付け、GDB のトランスクリプトを保存し、使用したツールのバージョンとコマンドを文書化してください |
結論
Reverse Engineering: Deep Analysis は、静的コード検査と完全なプログラム理解をつなぐ重要な架け橋です。ランタイム実行(レベル 3)とシンボリックなパス探索(レベル 4)を組み合わせることで、このスキルはセキュリティ研究者がシークレットを抽出し、脆弱性を検証し、特定のプログラム状態に到達する入力を合成することを可能にします。これはマルウェア分析、CTF チャレンジ、脆弱性研究に不可欠な機能です。
このスキルの力は、自動化された意思決定ゲートと段階的なエスカレーション戦略にあります。リソース集約的なシンボリック実行にすぐに飛びつくのではなく、このスキルは GDB とシステムコールトレースを使用した軽量な動的解析から始めます。手動実行でターゲット状態に到達できない場合にのみ、Angr ベースのシンボリック実行にエスカレーションし、分析時間を最小限に抑えながら調査結果を最大化します。
静的解析では明らかにできないランタイム挙動を理解する必要がある場合に、このスキルを使用してください。メモリ内のシークレット、ネットワーク通信パターン、複雑な認証スキームの有効な入力などです。このスキルは、マルウェアから侵害指標を抽出し、クラックメで有効なライセンスキーを見つけ、脆弱性の概念実証エクスプロイトを生成することに優れています。クロスセッションの永続化のための memory-mcp 統合と、ファームウェア分析(レベル 5)とのハンドオフ調整を組み合わせることで、学術研究と本番セキュリティ運用の両方に適した包括的なリバースエンジニアリングワークフローを形成します。