🌟 Strilight

Lifting de boucles SMT $O(1)$ haute performance et domaine d'intervalles à pas pour l'analyse binaire x86_64

📖 1. Vue d'ensemble et problème central

Les moteurs traditionnels d'exécution symbolique et d'instrumentation binaire dynamique (DBI) (tels que angr, Triton ou KLEE) souffrent du tristement célèbre problème d'explosion des chemins et des boucles. Lorsqu'ils rencontrent une l[...]

Strilight résout fondamentalement ce problème en traitant les boucles comme des récurrences algébriques de forme fermée au sein du domaine d'intervalles à pas :

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

Au lieu de simuler $N$ itérations, Strilight compresse les traces d'exécution répétitives en structures hiérarchiques LoopBlock, évalue leurs étapes abstraites affines et polycycliques, et effectue le lifting de l'e[...]

⚡ 2. Innovations architecturales clés

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. Compression de traces sans déroulage : identifie les arêtes de retour et compresse des millions de traces d'instructions linéaires en graphes hiérarchiques compacts LoopBlock en $<1\text{ ms}$.
2. Domaine d'intervalles à pas et VSA à double masque : suit les transformations des registres et de la mémoire à l'aide de pas et de congruences modulaires : $$s[l, u] = { x \mid l \le x \le u \land (x - l) \equiv 0 \pmod s }$$
3. Extraction de motifs polycycliques et périodiques : détecte les transformations cycliques complexes de la mémoire et des sous-registres ($P > 1$).
4. Le contrat d'invariant de fer : formule la condition de frontière exacte de première sortie pour empêcher les solveurs SMT de se "téléporter" à travers les bornes de terminaison des boucles : $$\text{ExitCondition}(\text{State}(N)) \land \forall k < N, \neg \text{ExitCondition}(\text{State}(k))$$
5. Architecture modulaire découplée : désassemblage natif Capstone avec ponts traceurs personnalisés enfichables.

🚀 3. Profils de distribution modulaires

Strilight est fourni sous forme de profils modulaires indépendants afin que vous n'embarquiez que les composants dont votre pipeline a besoin :

# 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. Taxonomie et vérification de la suite de tests

La suite de tests valide chaque module avec un taux de réussite de 100 % dans les couches découplées :

Niveau 1 : Tests du compresseur principal et d'interprétation abstraite (nécessite strilight)

Aucune dépendance lourde de solveur. S'exécute en $<1\text{ seconde}$ sur n'importe quelle plateforme :

Niveau 2 : Tests de découpage dynamique et de suivi des dépendances (nécessite strilight[tracker])

Valide le suivi complet du flux de données dynamique et des dépendances de contrôle :

Niveau 3 : Tests du lifter SMT symbolique et du solveur (nécessite strilight[solver])

Valide la génération d'équations BitVector, les substitutions fantômes et la résolution de contraintes Z3 :

💡 5. Démarrage rapide : 3 façons d'utiliser Strilight

Option A : Analyse de boucle en une ligne (sl.analyze)

Analysez n'importe quelle boucle de code machine x86-64 brut et extrayez sa transformation de forme fermée en une seule ligne :

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 : Désassemblage, compression et évaluation étape par étape

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 : Résolution SMT $O(1)$ instantanée avec Z3

Résolvez le nombre d'itérations ($N$) ou la clé d'entrée requise pour satisfaire une condition objectif 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. Résultats de benchmark sur des binaires réels

Testé sur des exécutables Windows 64 bits complexes (CrackMe Suite) contenant des boucles imbriquées, du découpage de sous-registres et des motifs de pas obscurcis :

Vérification de vérité terrain : Toutes les clés récupérées sont vérifiées en exécutant le binaire compilé natif (.exe) via subprocess et en confirmant la réponse ACCESS GRANTED.

📚 7. Référence de l'API

Fonctions de façade de haut niveau :

• sl.analyze(code_bytes, iterations=1000, ...) : désassemblage + évaluation en une ligne.
• sl.disassemble(code_bytes, base_address=0x1000, bit_mode=64) : désassembleur d'octets bruts via Capstone.
• sl.compress(trace, min_iterations=3) : compresseur de traces hiérarchique.
• sl.evaluate(block_or_trace, k_passes=100) : évaluateur d'état abstrait et d'invariants.

Classes principales :

• sl.Instruction : représentation unifiée d'instruction assembleur.
• sl.LoopBlock : nœud de boucle hiérarchique avec bornes d'itérations.
• sl.LoopSummary : résumé de transformation de forme fermée contenant les deltas, les motifs cycliques et les ensembles de constantes.
• sl.LoopInvariantContract : descripteur formel d'invariant de sortie structurel et générateur de règles de frontière SMT.
• sl.StridedInterval : représentation mathématique d'intervalle avec alignement de pas et congruence modulaire.
• sl.Z3Translator : lifter SMT symbolique convertissant les résumés de boucle en contraintes BitVector Z3.

📄 Licence

Double licence : MIT / propriétaire. Développé avec ❤️ pour la rétro-ingénierie haute performance et l'analyse binaire.