🌟 Strilight

Hochleistungsfähiges $O(1)$ SMT-Loop-Lifting & Strided Interval Domain für die x86_64-Binäranalyse

📖 1. Überblick & das Kernproblem

Traditionelle Engines für Symbolic Execution und Dynamic Binary Instrumentation (DBI) (wie angr, Triton oder KLEE) leiden unter dem berüchtigten Pfad- & Schleifenexplosionsproblem. Beim Auftreten einer S[...]

Strilight löst dieses Problem grundlegend, indem es Schleifen als geschlossene algebraische Rekurrenzen innerhalb der Strided Interval Domain behandelt:

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

Anstatt $N$ Iterationen zu simulieren, komprimiert Strilight repetitive Traces in hierarchische LoopBlock-Strukturen, bewertet ihre abstrakten affinen & polyzyklischen Schritte und überführt die [...]

⚡ 2. Zentrale architektonische Innovationen

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. Zero-Unroll-Trace-Kompression: Erkennt Rückkanten und komprimiert Millionen linearer Instruction-Traces in kompakte hierarchische LoopBlock-Graphen in $<1\text{ ms}$.
2. Strided Interval Domain & Dual-Mask-VSA: Verfolgt Register- und Speichertransformationen mithilfe von Strides und modularen Kongruenzen: $$s[l, u] = { x \mid l \le x \le u \land (x - l) \equiv 0 \pmod s }$$
3. Polycyclische & periodische Mustererkennung: Erkennt komplexe zyklische Speicher- und Sub-Register-Transformationen ($P > 1$).
4. Der Iron-Invariant-Contract: Formuliert die exakte First-Exit-Randbedingung, um SMT-Löser daran zu hindern, durch Schleifen-Terminierungsgrenzen zu „teleportieren": $$\text{ExitCondition}(\text{State}(N)) \land \forall k < N, \neg \text{ExitCondition}(\text{State}(k))$$
5. Entkoppelte modulare Architektur: Native Capstone-Disassemblierung mit pluggbaren benutzerdefinierten Tracer-Brücken.

🚀 3. Modulare Distributionsprofile

Strilight ist in unabhängigen modularen Profilen verpackt, sodass Sie nur die Komponenten mitnehmen, die Ihre Pipeline benötigt:

# 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. Test-Suite-Taxonomie & Verifikation

Die Test-Suite validiert jedes Modul mit einer 100%igen Bestehensquote über alle entkoppelten Ebenen hinweg:

Tier 1: Kernkompressor- & Abstract-Interpretation-Tests (erfordert strilight)

Keine schweren Solver-Abhängigkeiten. Läuft in $<1\text{ second}$ auf jeder Plattform:

Tier 2: Dynamic-Slicing- & Dependency-Tracker-Tests (erfordert strilight[tracker])

Validiert vollständiges dynamisches Data-Flow- und Control-Dependency-Tracking:

Tier 3: Symbolic-SMT-Lifter- & Solver-Tests (erfordert strilight[solver])

Validiert BitVector-Gleichungserzeugung, Shadow-Substitutionen und das Lösen von Z3-Constraints:

💡 5. Schnellstart: 3 Möglichkeiten, Strilight zu verwenden

Option A: Einzeilige Schleifenanalyse (sl.analyze)

Analysieren Sie jede rohe x86-64-Maschinencode-Schleife und extrahieren Sie ihre geschlossene Transformation in einer einzigen Zeile:

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())

Option B: Disassemblieren, Komprimieren & Bewerten Schritt für Schritt

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}")

Option C: Sofortiges $O(1)$-SMT-Lösen mit Z3

Lösen Sie nach der Anzahl der Iterationen ($N$) oder dem Eingabeschlüssel auf, der erforderlich ist, um eine Zielbedingung in $<100\text{ ms}$ zu erfüllen:

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. Benchmark-Ergebnisse an realen Binärdateien

Getestet gegen komplexe 64-Bit-Windows-Executables (CrackMe Suite) mit verschachtelten Schleifen, Sub-Register-Slicing und obfuskierten Stride-Mustern:

Ground-Truth-Verifikation: Alle wiederhergestellten Schlüssel werden verifiziert, indem die nativ kompilierte Binärdatei (.exe) über einen Subprozess ausgeführt und die ACCESS GRANTED-Antwort überprüft wird.

📚 7. API-Referenz

High-Level-Fassadenfunktionen:

• sl.analyze(code_bytes, iterations=1000, ...): Einzeilige Disassemblierung + Bewertung.
• sl.disassemble(code_bytes, base_address=0x1000, bit_mode=64): Raw-Byte-Disassembler über Capstone.
• sl.compress(trace, min_iterations=3): Hierarchischer Trace-Kompressor.
• sl.evaluate(block_or_trace, k_passes=100): Evaluator für abstrakten Zustand & Invarianten.

Kernklassen:

• sl.Instruction: Einheitliche Repräsentation von Assembly-Instructions.
• sl.LoopBlock: Hierarchischer Schleifenknoten mit Iterationsgrenzen.
• sl.LoopSummary: Zusammenfassung der geschlossenen Transformation mit Deltas, zyklischen Mustern und konstanten Mengen.
• sl.LoopInvariantContract: Formaler Deskriptor der strukturellen Exit-Invariante und Generator für SMT-Randregeln.
• sl.StridedInterval: Mathematische Intervallrepräsentation mit Stride-Ausrichtung und modularer Kongruenz.
• sl.Z3Translator: Symbolischer SMT-Lifter, der Schleifenzusammenfassungen in Z3-BitVector-Constraints umwandelt.

📄 Lizenz

Doppellizenz: MIT / Proprietär. Entwickelt mit ❤️ für leistungsstarkes Reverse-Engineering und Binäranalyse.