🌟 Strilight

Lifting de Loops SMT de Alto Desempenho em $O(1)$ e Strided Interval Domain para Análise de Binários x86_64

📖 1. Visão Geral e o Problema Central

Mecanismos tradicionais de Execução Simbólica e Instrumentação Dinâmica de Binários (DBI) (como angr, Triton ou KLEE) sofrem do notório Problema de Explosão de Caminhos e Loops. Ao encontrar um l[...]

O Strilight resolve esse problema de forma fundamental ao tratar loops como recorrências algébricas de forma fechada dentro do Strided Interval Domain:

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

Em vez de simular $N$ iterações, o Strilight comprime traces de execução repetitivos em estruturas hierárquicas LoopBlock, avalia seus passos afins e policíclicos abstratos e eleva o e[...]

⚡ 2. Principais Inovações Arquiteturais

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. Compressão de Trace com Zero-Unroll: Identifica arestas de retorno (back-edges) e comprime milhões de traces lineares de instruções em grafos hierárquicos compactos LoopBlock em $<1\text{ ms}$.
2. Strided Interval Domain e VSA de Máscara Dupla: Rastreia transformações de registradores e memória usando strides e congruências modulares: $$s[l, u] = { x \mid l \le x \le u \land (x - l) \equiv 0 \pmod s }$$
3. Extração de Padrões Policíclicos e Periódicos: Detecta transformações cíclicas complexas de memória e sub-registradores ($P > 1$).
4. O Contrato de Invariante de Ferro: Formula a condição exata de contorno de primeira saída para impedir que solvers SMT se "teletransportem" através dos limites de terminação do loop: $$\text{ExitCondition}(\text{State}(N)) \land \forall k < N, \neg \text{ExitCondition}(\text{State}(k))$$
5. Arquitetura Modular Desacoplada: Desmontagem nativa com Capstone e pontes customizadas de tracer conectáveis.

🚀 3. Perfis de Distribuição Modular

O Strilight é empacotado como perfis modulares independentes para que você carregue apenas os componentes que seu pipeline precisa:

# 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. Taxonomia da Suíte de Testes e Verificação

A suíte de testes valida todos os módulos com 100% de taxa de aprovação nos testes em todas as camadas desacopladas:

Nível 1: Testes do Compressor Principal e de Interpretação Abstrata (Requer strilight)

Nenhuma dependência pesada de solver. Executa em $<1\text{ segundo}$ em qualquer plataforma:

Nível 2: Testes de Fatiamento Dinâmico e do Rastreador de Dependências (Requer strilight[tracker])

Valida o rastreamento completo de fluxo de dados dinâmico e de dependências de controle:

Nível 3: Testes do Elevador SMT Simbólico e do Solver (Requer strilight[solver])

Valida a geração de equações BitVector, substituições de sombra e a resolução de restrições com Z3:

💡 5. Início Rápido: 3 Formas de Usar o Strilight

Opção A: Análise de Loop em Uma Linha (sl.analyze)

Analise qualquer loop de código de máquina x86-64 bruto e extraia sua transformação de forma fechada em uma única linha:

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

Opção B: Desmontar, Comprimir e Avaliar Passo a 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}")

Opção C: Resolução SMT Instantânea em $O(1)$ com Z3

Resolva o número de iterações ($N$) ou a chave de entrada necessária para satisfazer uma condição de objetivo em $<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 Benchmark com Binários Reais

Testado com executáveis Windows de 64 bits complexos (CrackMe Suite) contendo loops aninhados, fatiamento de sub-registradores e padrões de stride ofuscados:

Verificação Ground-Truth: Todas as chaves recuperadas são verificadas executando o binário nativo compilado (.exe) via subprocess e confirmando a resposta ACCESS GRANTED.

📚 7. Referência da API

Funções de Fachada de Alto Nível:

• sl.analyze(code_bytes, iterations=1000, ...): Desmontagem + avaliação em uma linha.
• sl.disassemble(code_bytes, base_address=0x1000, bit_mode=64): Desmontador de bytes brutos via Capstone.
• sl.compress(trace, min_iterations=3): Compressor hierárquico de traces.
• sl.evaluate(block_or_trace, k_passes=100): Avaliador de estado abstrato e invariantes.

Classes Principais:

• sl.Instruction: Representação unificada de instruções de assembly.
• sl.LoopBlock: Nó de loop hierárquico com limites de iteração.
• sl.LoopSummary: Resumo da transformação de forma fechada contendo deltas, padrões cíclicos e conjuntos constantes.
• sl.LoopInvariantContract: Descritor formal do invariante estrutural de saída e gerador de regras de contorno SMT.
• sl.StridedInterval: Representação matemática de intervalos com alinhamento de stride e congruência modular.
• sl.Z3Translator: Elevador SMT simbólico que converte resumos de loops em restrições BitVector do Z3.

📄 Licença

Licença Dupla: MIT / Proprietária. Desenvolvido com ❤️ para engenharia reversa e análise de binários de alto desempenho.