🌟 Strilight

Elevación de bucles SMT de alto rendimiento $O(1)$ y dominio de intervalos con stride para análisis de binarios x86_64

📖 1. Descripción general y el problema central

Los motores tradicionales de Ejecución Simbólica e Instrumentación Binaria Dinámica (DBI) (como angr, Triton o KLEE) sufren el notorio Problema de Explosión de Caminos y Bucles. Cuando se encuentran con un l[...]

Strilight resuelve esto de forma fundamental al tratar los bucles como recurrencias algebraicas de forma cerrada dentro del Dominio de Intervalos con Stride:

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

En lugar de simular $N$ iteraciones, Strilight comprime las trazas de ejecución repetitivas en estructuras jerárquicas LoopBlock, evalúa sus pasos afines y policíclicos abstractos, y eleva la e[...]

⚡ 2. Innovaciones arquitectónicas clave

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. Compresión de trazas sin desenrollado: Identifica los bordes de retroceso y comprime millones de trazas de instrucciones lineales en grafos jerárquicos compactos LoopBlock en $<1\text{ ms}$.
2. Dominio de Intervalos con Stride y VSA de doble máscara: Realiza el seguimiento de las transformaciones de registros y memoria mediante strides y congruencias modulares: $$s[l, u] = { x \mid l \le x \le u \land (x - l) \equiv 0 \pmod s }$$
3. Extracción de patrones policíclicos y periódicos: Detecta transformaciones cíclicas complejas de memoria y de sub-registros ($P > 1$).
4. El Contrato de Invariante de Hierro: Formula la condición de frontera exacta de primera salida para evitar que los solucionadores SMT se "teletransporten" a través de los límites de terminación del bucle: $$\text{ExitCondition}(\text{State}(N)) \land \forall k < N, \neg \text{ExitCondition}(\text{State}(k))$$
5. Arquitectura modular desacoplada: Desensamblado nativo con Capstone y puentes de trazado personalizados conectables.

🚀 3. Perfiles de distribución modular

Strilight se distribuye como perfiles modulares independientes para que solo cargues los componentes que tu pipeline necesita:

# 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. Taxonomía de la suite de pruebas y verificación

La suite de pruebas valida cada módulo con una tasa de aprobación del 100% en todas las capas desacopladas:

Nivel 1: Pruebas del compresor principal y de interpretación abstracta (Requiere strilight)

Sin dependencias pesadas de solucionadores. Se ejecuta en $<1\text{ segundo}$ en cualquier plataforma:

Nivel 2: Pruebas de segmentación dinámica y rastreador de dependencias (Requiere strilight[tracker])

Valida el seguimiento completo del flujo de datos dinámico y las dependencias de control:

Nivel 3: Pruebas del elevador SMT simbólico y del solucionador (Requiere strilight[solver])

Valida la generación de ecuaciones de BitVector, sustituciones sombra y resolución de restricciones con Z3:

💡 5. Inicio rápido: 3 formas de usar Strilight

Opción A: Análisis de bucles en una sola línea (sl.analyze)

Analiza cualquier bucle de código máquina x86-64 crudo y extrae su transformación de forma cerrada en una sola línea:

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

Opción B: Desensamblar, comprimir y evaluar paso a paso

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

Opción C: Resolución SMT instantánea $O(1)$ con Z3

Resuelve el número de iteraciones ($N$) o la clave de entrada necesaria para satisfacer una condición objetivo en $<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. Resultados de evaluación comparativa con binarios reales

Probado con ejecutables complejos de Windows de 64 bits (CrackMe Suite) que contienen bucles anidados, segmentación de sub-registros y patrones de stride ofuscados:

Verificación de referencia (ground-truth): Todas las claves recuperadas se verifican ejecutando el binario nativo compilado (.exe) mediante subprocess y comprobando la respuesta ACCESS GRANTED.

📚 7. Referencia de la API

Funciones de fachada de alto nivel:

• sl.analyze(code_bytes, iterations=1000, ...): Desensamblado y evaluación en una sola línea.
• sl.disassemble(code_bytes, base_address=0x1000, bit_mode=64): Desensamblador de bytes crudos mediante Capstone.
• sl.compress(trace, min_iterations=3): Compresor jerárquico de trazas.
• sl.evaluate(block_or_trace, k_passes=100): Evaluador de estados abstractos e invariantes.

Clases principales:

• sl.Instruction: Representación unificada de instrucciones de ensamblador.
• sl.LoopBlock: Nodo jerárquico de bucle con límites de iteración.
• sl.LoopSummary: Resumen de transformación de forma cerrada que contiene deltas, patrones cíclicos y conjuntos constantes.
• sl.LoopInvariantContract: Descriptor formal de invariante estructural de salida y generador de reglas de frontera SMT.
• sl.StridedInterval: Representación matemática de intervalos con alineación de stride y congruencia modular.
• sl.Z3Translator: Elevador SMT simbólico que convierte resúmenes de bucles en restricciones BitVector de Z3.

📄 Licencia

Licencia dual: MIT / Propietaria. Desarrollado con ❤️ para la ingeniería inversa de alto rendimiento y el análisis de binarios.