🌟 Strilight

Высокопроизводительный $O(1)$ SMT-лифтинг циклов и страйдовый интервальный домен для анализа бинарных файлов x86_64

📖 1. Обзор и основная проблема

Традиционные движки символьного исполнения и динамической бинарной инструментации (DBI) (такие как angr, Triton или KLEE) страдают от печально известной проблемы взрыва путей и циклов. При обнаружении l[...]

Strilight решает эту проблему фундаментально, рассматривая циклы как алгебраические рекурренции в замкнутой форме в пределах страйдового интервального домена:

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

Вместо симуляции $N$ итераций, Strilight сжимает повторяющиеся трассы исполнения в иерархические структуры LoopBlock, вычисляет их абстрактные аффинные и полициклические шаги и выполняет лифтинг e[...]

⚡ 2. Ключевые архитектурные инновации

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): Определяет обратные рёбра и сжимает миллионы линейных трасс инструкций в компактные иерархические графы LoopBlock за $<1\text{ ms}$.
2. Страйдовый интервальный домен и VSA с двойной маской: Отслеживает преобразования регистров и памяти с помощью страйдов и модулярных конгруэнций: $$s[l, u] = { x \mid l \le x \le u \land (x - l) \equiv 0 \pmod s }$$
3. Извлечение полициклических и периодических паттернов: Обнаруживает сложные циклические преобразования памяти и субрегистров ($P > 1$).
4. Железный инвариантный контракт: Формулирует точное граничное условие первого выхода, чтобы предотвратить «телепортацию» SMT-решателей через границы завершения цикла: $$\text{ExitCondition}(\text{State}(N)) \land \forall k < N, \neg \text{ExitCondition}(\text{State}(k))$$
5. Развязанная модульная архитектура: Нативная дизассембляция Capstone с подключаемыми пользовательскими мостами трассировки.

🚀 3. Модульные профили распространения

Strilight поставляется в виде независимых модульных профилей, чтобы вы могли нести только те компоненты, которые нужны вашему конвейеру:

# 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. Таксономия тестового набора и верификация

Тестовый набор проверяет каждый модуль со 100% прохождением тестов на всех развязанных уровнях:

Уровень 1: Тесты ядра компрессора и абстрактной интерпретации (требуется strilight)

Ноль тяжёлых зависимостей от решателей. Выполняется за $<1\text{ second}$ на любой платформе:

Уровень 2: Тесты динамического слайсинга и трекера зависимостей (требуется strilight[tracker])

Проверяет полное отслеживание динамического потока данных и управляющих зависимостей:

Уровень 3: Тесты символьного SMT-лифтера и решателя (требуется strilight[solver])

Проверяет генерацию BitVector-уравнений, теневые подстановки и решение ограничений Z3:

💡 5. Быстрый старт: 3 способа использования Strilight

Вариант A: Анализ цикла в одну строку (sl.analyze)

Проанализируйте любой цикл в сыром машинном коде x86-64 и извлеките его преобразование в замкнутой форме одной строкой:

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

Вариант B: Дизассемблирование, сжатие и оценка по шагам

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

Вариант C: Мгновенное $O(1)$ SMT-решение с помощью Z3

Найдите количество итераций ($N$) или входной ключ, необходимый для выполнения целевого условия, за $<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. Результаты бенчмарков на реальных бинарных файлах

Протестировано на сложных 64-битных исполняемых файлах Windows (CrackMe Suite), содержащих вложенные циклы, субрегистровый слайсинг и обфусцированные страйдовые паттерны:

Проверка по эталону (Ground-Truth): Все восстановленные ключи проверяются запуском нативного скомпилированного бинарного файла (.exe) через subprocess и проверкой ответа ACCESS GRANTED.

📚 7. Справочник по API

Функции высокоуровневого фасада:

• sl.analyze(code_bytes, iterations=1000, ...): дизассемблирование и оценка одной строкой.
• sl.disassemble(code_bytes, base_address=0x1000, bit_mode=64): дизассемблер сырых байтов через Capstone.
• sl.compress(trace, min_iterations=3): иерархический компрессор трасс.
• sl.evaluate(block_or_trace, k_passes=100): вычислитель абстрактного состояния и инвариантов.

Основные классы:

• sl.Instruction: унифицированное представление инструкций ассемблера.
• sl.LoopBlock: иерархический узел цикла с границами итераций.
• sl.LoopSummary: сводка преобразования в замкнутой форме, содержащая дельты, циклические паттерны и множества констант.
• sl.LoopInvariantContract: формальный дескриптор структурного инварианта выхода и генератор правил границ SMT.
• sl.StridedInterval: математическое представление интервала с выравниванием страйдов и модулярной конгруэнцией.
• sl.Z3Translator: символьный SMT-лифтер, преобразующий сводки циклов в BitVector-ограничения Z3.

📄 Лицензия

Двойная лицензия: MIT / проприетарная. Разработано с ❤️ для высокопроизводительного реверс-инжиниринга и анализа бинарного кода.