🌟 Strilight

x86_64 バイナリ解析のための高性能 $O(1)$ SMT ループリフティング＆ストライド区間ドメイン

📖 1. 概要と中核となる問題

従来のシンボリック実行および動的バイナリ計装（DBI）エンジン（angr、Triton、KLEE など）は、悪名高いパス＆ループ爆発問題に悩まされています。l[...] に遭遇すると

Strilight は、ストライド区間ドメイン内でループを閉形式代数漸化式として扱うことで、この問題を根本的に解決します：

$$\vec{\mathbf{R}}(N) = \vec{\mathbf{R}}_0 + \vec{\boldsymbol{\Delta}} \cdot N$$

$N$ 回の反復をシミュレートする代わりに、Strilight は反復的な実行トレースを階層的な LoopBlock 構造に圧縮し、それらの抽象アフィン＆多周期ステップを評価して、e[...]

⚡ 2. 主要なアーキテクチャ革新

graph LR
    A[Raw Machine Code / Trace] --> B[sl.disassemble & sl.compress]
    B --> C[sl.evaluate / LoopEvaluator]
    C -->|Strided Interval Domain| D[LoopSummary + Invariant Contract]
    D -->|O1 Closed-Form Lifting| E["Z3 SMT-LIB2 Solver"]
    E --> F[Instant Solution in less than 100 ms]

1. ゼロアンロールトレース圧縮： バックエッジを特定し、数百万の線形命令トレースを $<1\text{ ms}$ でコンパクトな階層 LoopBlock グラフに圧縮します。
2. ストライド区間ドメイン＆デュアルマスク VSA： ストライドと剰余合同を使用してレジスタおよびメモリ変換を追跡します： $$s[l, u] = { x \mid l \le x \le u \land (x - l) \equiv 0 \pmod s }$$
3. Polycyclic（多周期）＆周期的パターン抽出： 複雑な循環メモリおよびサブレジスタ変換（$P > 1$）を検出します。
4. Iron Invariant Contract（鉄壁不変契約）： SMT ソルバーがループ終了境界を「テレポート」するのを防ぐため、正確な最初の出口境界条件を定式化します： $$\text{ExitCondition}(\text{State}(N)) \land \forall k < N, \neg \text{ExitCondition}(\text{State}(k))$$
5. 分離モジュールアーキテクチャ： プラグ可能なカスタムトレーサーブリッジを備えたネイティブ Capstone 逆アセンブル。

🚀 3. モジュール別配布プロファイル

Strilight は独立したモジュラープロファイルとしてパッケージ化されているため、パイプラインに必要なコンポーネントだけを取り込めます：

# Profile 1: Core Engine (Pure Compressor + Embedded Def-Use Slicer + Capstone)
pip install strilight

# Profile 2: Symbolic Engine (Core Compressor + Z3 O(1) SMT Lifter)
pip install strilight[solver]

# Profile 3: Dynamic Slicing Suite (Core Compressor + Full PathTree Backward/Forward Tracker)
pip install strilight[tracker]

# Profile 4: Complete Bundle (All Engines + Full Tracker + Z3 Solver)
pip install strilight[all]

🧪 4. テストスイートの分類と検証

テストスイートは、分離された各レイヤーにわたって 100% のテスト合格率で全モジュールを検証します：

Tier 1: コア圧縮器＆抽象解釈テスト（strilight が必要）

ヘビーなソルバー依存関係なし。どのプラットフォームでも $<1\text{ 秒}$ で実行されます：

Tier 2: 動的スライシング＆依存関係トラッカーテスト（strilight[tracker] が必要）

完全な動的データフローおよび制御依存関係の追跡を検証します：

Tier 3: シンボリック SMT リフター＆ソルバーテスト（strilight[solver] が必要）

BitVector 方程式生成、シャドウ置換、および Z3 制約解決を検証します：

💡 5. クイックスタート：Strilight を使う 3 つの方法

オプション A: ワンライナーループ解析（sl.analyze）

任意の生の x86-64 マシンコードループを解析し、その閉形式変換を 1 行で抽出します：

import strilight as sl

# Loop bytecode: add eax, 8; sub ebx, 3; inc ecx; cmp ecx, 100000; jl 0x1000
loop_bytes = bytes.fromhex("83c008 83eb03 ffc1 81f9a0860100 7ced")

# ONE-LINE ANALYSIS:
summary = sl.analyze(loop_bytes, iterations=100000)

print(summary.deltas)
# Output: {'eax': 8, 'ebx': -3, 'ecx': 1}

# View the mathematical invariant contract:
print(summary.invariant_contract.to_dict())

オプション B: ステップバイステップで逆アセンブル・圧縮・評価

import strilight as sl

# 1. Disassemble machine code bytes
instructions = sl.disassemble(loop_bytes, base_address=0x1000)

# 2. Package into a symbolic loop block
block = sl.LoopBlock(body=instructions, iterations=100000)

# 3. Extract closed-form mathematical steps (Deltas & Exit Predicates)
summary = sl.evaluate(block)
print(f"Exit Condition: {summary.exit_condition}")

オプション C: Z3 によるインスタント $O(1)$ SMT 解決

目標条件を満たすために必要な反復回数（$N$）または入力キーを $<100\text{ ms}$ で解決します：

import strilight as sl
import z3

# Disassemble and evaluate
summary = sl.analyze(loop_bytes, iterations=100000)

# Initialize Z3 translator
translator = sl.Z3Translator()
translator.solver.add(translator.get_register('eax') == 0)
translator.solver.add(translator.get_register('ebx') == 500000)
translator.solver.add(translator.get_register('ecx') == 0)

# Lift loop summary in O(1) into Z3
translator.translate_loop_summary(summary, max_iterations=100000)

# Goal: When does EAX reach 800,000?
translator.solver.add(translator.get_register('eax') == 800000)

# Solve in milliseconds!
if translator.solver.check() == z3.sat:
    model = translator.solver.model()
    solved_N = model.eval(summary.loop_counter_var).as_long()
    print(f"[+] Solved N = {solved_N:,} iterations in O(1) time!")

📊 6. 実世界バイナリベンチマーク結果

入れ子ループ、サブレジスタスライシング、および難読化されたストライドパターンを含む複雑な 64 ビット Windows 実行ファイル（CrackMe Suite）に対してテスト済み：

グラウンドトゥルース検証： 回収されたすべてのキーは、サブプロセス経由でネイティブコンパイル済みバイナリ（.exe）を実行し、ACCESS GRANTED 応答をアサートすることで検証されます。

📚 7. API リファレンス

高レベルファサード関数：

• sl.analyze(code_bytes, iterations=1000, ...)：ワンライナー逆アセンブル＋評価。
• sl.disassemble(code_bytes, base_address=0x1000, bit_mode=64)：Capstone による生バイト逆アセンブラ。
• sl.compress(trace, min_iterations=3)：階層トレース圧縮器。
• sl.evaluate(block_or_trace, k_passes=100)：抽象状態＆不変式評価器。

コアクラス：

• sl.Instruction：統合アセンブリ命令表現。
• sl.LoopBlock：反復境界を持つ階層ループノード。
• sl.LoopSummary：デルタ、循環パターン、および定数セットを含む閉形式変換サマリー。
• sl.LoopInvariantContract：形式的な構造的出口不変条件記述子および SMT 境界ルールジェネレーター。
• sl.StridedInterval：ストライド整列と剰余合同を備えた数学的区間表現。
• sl.Z3Translator：ループサマリーを Z3 BitVector 制約に変換するシンボリック SMT リフター。

📄 ライセンス

デュアルライセンス：MIT / プロプライエタリ。 高性能リバースエンジニアリングとバイナリ解析のために ❤️ を込めて開発されました。