🌟 Strilight

Lifting SMT $O(1)$ di Loop ad Alte Prestazioni e Dominio a Intervalli Strided per l'Analisi Binaria x86_64

📖 1. Panoramica e il Problema Centrale

L'esecuzione simbolica tradizionale e i motori di Dynamic Binary Instrumentation (DBI) (come angr, Triton o KLEE) soffrono del noto Problema dell'Esplosione dei Percorsi e dei Loop. Quando si incontra un l[...]

Strilight risolve questo problema alla radice, trattando i loop come ricorrenze algebriche in forma chiusa all'interno del Dominio a Intervalli Strided:

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

Invece di simulare $N$ iterazioni, Strilight comprime le tracce di esecuzione ripetitive in strutture gerarchiche LoopBlock, valuta i loro passi astratti affini e policiclici e solleva l'e[...]

⚡ 2. Innovazioni Architetturali Chiave

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. Compressione della Traccia Zero-Unroll: identifica i back-edge e comprime milioni di tracce di istruzioni lineari in grafi gerarchici e compatti di LoopBlock in $<1\text{ ms}$.
2. Dominio a Intervalli Strided e VSA a Doppia Maschera: tiene traccia delle trasformazioni di registri e memoria usando stride e congruenze modulari: $$s[l, u] = { x \mid l \le x \le u \land (x - l) \equiv 0 \pmod s }$$
3. Estrazione di Pattern Policiclici e Periodici: rileva complesse trasformazioni cicliche della memoria e dei sotto-registri ($P > 1$).
4. Il Contratto dell'Invariante di Ferro: formula l'esatta condizione al contorno di prima uscita per impedire ai solver SMT di "teletrasportarsi" attraverso i limiti di terminazione dei loop: $$\text{ExitCondition}(\text{State}(N)) \land \forall k < N, \neg \text{ExitCondition}(\text{State}(k))$$
5. Architettura Modulare Disaccoppiata: disassemblaggio nativo Capstone con bridge personalizzati pluggable per i tracer.

🚀 3. Profili di Distribuzione Modulari

Strilight è distribuito come profili modulari indipendenti, così da portare con te solo i componenti di cui la tua pipeline ha bisogno:

# 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. Tassonomia e Verifica della Suite di Test

La suite di test valida ogni modulo con un tasso di superamento dei test del 100% su tutti i livelli disaccoppiati:

Livello 1: Test del Compressore Core e dell'Interpretazione Astratta (Richiede strilight)

Zero dipendenze pesanti dal solver. Viene eseguita in $<1\text{ second}$ su qualsiasi piattaforma:

Livello 2: Test dello Slicing Dinamico e del Tracker delle Dipendenze (Richiede strilight[tracker])

Valida il tracciamento completo del data-flow dinamico e delle dipendenze di controllo:

Livello 3: Test del Lifter SMT Simbolico e del Solver (Richiede strilight[solver])

Valida la generazione di equazioni BitVector, le sostituzioni shadow e la risoluzione dei vincoli Z3:

💡 5. Avvio Rapido: 3 Modi per Usare Strilight

Opzione A: Analisi del Loop in Una Riga (sl.analyze)

Analizza qualsiasi loop di codice macchina x86-64 grezzo ed estrai la sua trasformazione in forma chiusa in una sola riga:

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

Opzione B: Disassembla, Comprimi e Valuta Passo per Passo

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

Opzione C: Risoluzione SMT $O(1)$ Istantanea con Z3

Risolve il numero di iterazioni ($N$) o la chiave di input necessaria per soddisfare una condizione obiettivo in $<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. Risultati dei Benchmark su Binari Reali

Testato su eseguibili Windows a 64 bit complessi (CrackMe Suite) contenenti loop annidati, slicing di sotto-registri e pattern di stride offuscati:

Verifica Ground-Truth: tutte le chiavi recuperate vengono verificate eseguendo il binario nativo compilato (.exe) tramite subprocess e verificando la risposta ACCESS GRANTED.

📚 7. Riferimento API

Funzioni Facade di Alto Livello:

• sl.analyze(code_bytes, iterations=1000, ...): disassemblaggio + valutazione in una sola riga.
• sl.disassemble(code_bytes, base_address=0x1000, bit_mode=64): disassembler di byte grezzi tramite Capstone.
• sl.compress(trace, min_iterations=3): compressore gerarchico di tracce.
• sl.evaluate(block_or_trace, k_passes=100): valutatore dello stato astratto e degli invarianti.

Classi Principali:

• sl.Instruction: rappresentazione unificata delle istruzioni assembly.
• sl.LoopBlock: nodo di loop gerarchico con limiti di iterazione.
• sl.LoopSummary: riepilogo della trasformazione in forma chiusa contenente delta, pattern ciclici e insiemi di costanti.
• sl.LoopInvariantContract: descrittore formale dell'invariante strutturale di uscita e generatore di regole di confine SMT.
• sl.StridedInterval: rappresentazione matematica di intervallo con allineamento dello stride e congruenza modulare.
• sl.Z3Translator: lifter SMT simbolico che converte i riepiloghi dei loop in vincoli BitVector Z3.

📄 Licenza

Doppia Licenza: MIT / Proprietaria. Sviluppato con ❤️ per il reverse engineering ad alte prestazioni e l'analisi binaria.