CoBRA

Coefficient-Based Reconstruction of Arithmetic — упроститель смешанных булево-арифметических выражений.

CoBRA деобфусцирует выражения, которые чередуют арифметические (+, -, *) с побитовыми (&, |, ^, ~) операторами и сдвигами (<<, >>) — техника, часто используемая в обфускации программного обеспечения.

$ cobra-cli --mba "(x&y)+(x|y)"
x + y

$ cobra-cli --mba "((a^b)|(a^c)) + 65469 * ~((a&(b&c))) + 65470 * (a&(b&c))" --bitwidth 16
67 + (a | b | c)

$ cobra-cli --mba "((a^b)&c) | ((a&b)^c)"
c ^ a & b

$ cobra-cli --mba "(x&0xFF)+(x&0xFF00)" --bitwidth 16
x

$ cobra-cli --mba "(x ^ 0x10) + 2 * (x & 0x10)"
16 + x

$ cobra-cli --mba "x << 3"
8 * x

$ cobra-cli --mba "~x"
~x

$ cobra-cli --mba "(x^y)*(x&y) + 3*(x|y)"
(x ^ y) * (x & y) + 3 * (x | y)

$ cobra-cli --mba '-357*(x&~y)*(x&y)+102*(x&~y)*(x&~y)+374*(x&~y)*~(x^y)
  -306*(x&~y)*~(x|y)-17*(x&~y)*~(x|~y)-105*~(x|~y)*(x&y)+30*~(x|~y)*(x&~y)
  +110*~(x|~y)*~(x^y)-90*~(x|~y)*~(x|y)-5*~(x|~y)*~(x|~y)+34*(x&~y)*~x
  -85*(x&~y)*~y+10*~(x|~y)*~x-25*~(x|~y)*~y'
22 * (x & y) + -17 * x + -5 * y

Как это работает

CoBRA использует оркестратор на основе списка задач (worklist) для упрощения выражений. Каждое входное выражение поступает в список задач как элемент, помеченный типом состояния. Планировщик выбирает следующий проход для выполнения на основе состояния элемента, зависимостей от предварительных условий и кэша попыток, предотвращающего избыточную работу.

36 дискретных проходов организованы в группы: обработка AST, методы на основе сигнатур, полулинейные методы, декомпозиция и подъём (lifting). Некоторые проходы создают локальные альтернативы или дочерние решения, которые разрешаются конкурентными группами; вне этих групп список задач возвращает первый полностью проверенный кандидат верхнего уровня. Все результаты проверяются выборочным тестированием на случайных входных данных (по умолчанию) или доказательством эквивалентности с помощью Z3 (--verify).

Input Expression
       |
  [Worklist Scheduler]
       |
  Work items flow through state kinds:
       |
  kFoldedAst ──> AST processing passes
       |         (classify, lower, rewrite)
       |
       +──> kSignatureState ──> Signature techniques
       |    (pattern match, CoB, ANF, polynomial recovery)
       |
       +──> kSemilinearNormalizedIr ──> Semilinear techniques
       |    (normalize, recover structure, refine, reconstruct)
       |
       +──> kCoreCandidate / kRemainderState ──> Decomposition
       |    (extract core, classify residual, solve)
       |
       +──> kLiftedSkeleton ──> Lifting
       |    (virtual variable substitution, outer solve)
       |
       +──> kCandidateExpr ──> Verification
            (spot-check or Z3 proof)
       |
  Simplified Expression

Методы на основе сигнатур вычисляют выражение на всех булевых входах, получая вектор сигнатуры. Преобразование CoB (бабочка) восстанавливает коэффициенты базиса AND-произведений. Сопоставление с образцом, ANF и полиномиальное восстановление охватывают разные уровни сложности.

Полулинейные методы обрабатывают выражения с константными масками (например, x & 0xFF). Выражение раскладывается на взвешенные побитовые атомы, затем восстановление структуры и уточнение членов упрощают промежуточное представление, а битово-раздельная OR-сборка восстанавливает конечный результат.

Декомпозиция нацелена на смешанные выражения с произведениями побитовых подвыражений. Извлекается полиномиальное ядро, затем остатки классифицируются и решаются (полиномиальный, булево-нулевой/призрачный или шаблонный запасной вариант).

Подъём (lifting) заменяет сложные подвыражения виртуальными переменными, решает упрощённый внешний каркас, а затем подставляет обратно.

Возможности

• Упрощение линейных MBA — взвешенные суммы побитовых атомов через сигнатурный вектор и преобразование CoB
• Масштабируемое сопоставление с образцом — k * f(vars) + c с декомпозицией Шеннона для булевых выражений с 4–5 переменными
• Поддержка полулинейных выражений — константно-маскированные атомы с понижением констант XOR/OR/NOT-AND, восстановлением структуры, уточнением членов, битово-раздельной реконструкцией
• Полиномиальное восстановление — мультилинейные члены и степени-одиночки через расщепление коэффициентов и конечные разности
• Обработка смешанных произведений — механизм декомпозиции с извлечением ядра, решением остатков и классификацией призрачных остатков
• Подъём подвыражений — замена сложных поддеревьев виртуальными переменными для уменьшения размерности задачи
• Оркестратор списка задач — планирование проходов с учётом DAG, дедупликацией и ограниченным поиском
• Конкурентные группы — локальные альтернативные ветви и дочерние решения используют выбор победителя на основе стоимости с продолжениями
• Константные сдвиги — << преобразуется в умножение, >> упрощается полулинейными методами
• Очистка ANF — поглощение, факторизация общих кубов и распознавание OR
• Настраиваемая разрядность — модульная арифметика от 1 до 64 бит
• Удаление вспомогательных переменных — уменьшение количества переменных при сокращении членов
• Верификация Z3 — опциональная проверка эквивалентности упрощённого результата
• Самотестирование выборочными проверками — лёгкая валидация случайными входами, если Z3 недоступен
• Плагин LLVM pass — интеграция напрямую в конвейеры компилятора (требуется LLVM 19–22)

Сборка

Полные сведения, включая опциональные зависимости (LLVM, Z3), см. в BUILD.md.

# Зависимости сборки (Abseil, Highway; опционально GoogleTest, LLVM, Z3)
cmake -S dependencies -B build-deps -DCMAKE_BUILD_TYPE=Release
cmake --build build-deps

# Сборка CoBRA
cmake -S . -B build \
  -DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
  -DCMAKE_BUILD_TYPE=Release
cmake --build build

# (Опционально) Сборка и запуск тестов
cmake -S dependencies -B build-deps -DCMAKE_BUILD_TYPE=Release -DCOBRA_BUILD_TESTS=ON
cmake --build build-deps
cmake -S . -B build \
  -DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
  -DCMAKE_BUILD_TYPE=Release \
  -DCOBRA_BUILD_TESTS=ON
cmake --build build
ctest --test-dir build --output-on-failure

С плагином LLVM Pass

cmake -S . -B build \
  -DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
  -DCOBRA_BUILD_LLVM_PASS=ON \
  -DCMAKE_BUILD_TYPE=Release
cmake --build build

Использование

# Базовое упрощение
cobra-cli --mba "(x&y)+(x|y)"

# Указание разрядности
cobra-cli --mba "(x&0xFF)+(x&0xFF00)" --bitwidth 16

# Включение верификации эквивалентности через Z3
cobra-cli --mba "(a^b)+(a&b)+(a&b)" --verify

# Подробный вывод (показ промежуточных шагов конвейера)
cobra-cli --mba "(x&y)+(x|y)" --verbose

Опции

Структура проекта

lib/core/                Основной механизм упрощения (~50 исходных файлов)
  Orchestrator             Планировщик списка задач, конечный автомат, основной цикл упрощения
  OrchestratorPasses       Реестр из 39 проходов с планированием с учётом DAG
  CompetitionGroup         Гонка многометодных техник и выбор победителя
  ContinuationTypes        Данные отложенной рекомбинации для композиции проходов
  JoinState                Отслеживание соединений многих операндов для структурных переписываний
  SignatureSimplifier      Методы на основе сигнатур (CoB, сопоставление с образцом, ANF)
  SignatureVector          Вычисление выражения на входах {0,1}^n
  AuxVarEliminator         Уменьшение числа переменных путём обнаружения сокращений
  PatternMatcher           Распознавание побитовых шаблонов (таблицы 2-перем/3-перем, масштабированные)
  CoeffInterpolator        Интерполяция бабочкой для восстановления коэффициентов
  CoBExprBuilder           Восстановление выражений из коэффициентов CoB
  AnfTransform             Преобразование в алгебраическую нормальную форму
  AnfCleanup               Поглощение, факторизация, распознавание OR
  CoefficientSplitter      Разделение вкладов побитовой и арифметической частей
  ArithmeticLowering       Понижение арифметического фрагмента до полиномиального IR
  PolyNormalizer           Каноническая форма полиномиальных выражений
  SingletonPowerRecovery   Обнаружение членов x^k через конечные разности
  DecompositionEngine      Цикл извлечения-решения: полиномиальное ядро + решение остатков
  GhostBasis               Библиотека призрачных примитивов (mul_sub_and, mul3_sub_and3)
  GhostResidualSolver      Булево-нулевая классификация и решение призрачных остатков
  WeightedPolyFit          2-адическое взвешенное линейное решение для полиномиальных частных
  MixedProductRewriter     Развёртывание побитовых произведений в линейные суммы
  TemplateDecomposer       Шаблонное сопоставление с ограничениями для смешанных выражений
  ProductIdentityRecoverer Восстановление тождеств вида произведение сумм
  SemilinearNormalizer     Разложение на взвешенные побитовые атомы
  SemilinearSignature      Вычисление сигнатуры на бит и линейное сокращение
  StructureRecovery        Восстановление XOR, устранение масок, слияние членов
  TermRefiner              Сокращение мёртвых битовых масок, слияние одинаковых коэффициентов
  BitPartitioner           Группировка битовых позиций по семантическому профилю
  MaskedAtomReconstructor  Сборка с переписыванием OR для непересекающихся масок
  Evaluator                Компилированный вычислитель выражений

lib/llvm/                Плагин LLVM pass (CobraPass, MBADetector, IRReconstructor)
lib/verify/              Верификация эквивалентности на основе Z3
include/cobra/           Публичные заголовки
tools/cobra-cli/         CLI-интерфейс и парсер выражений
test/                    1195 тестов в ~63 тестовых файлах

Тестирование

CoBRA содержит 1195 тестов, охватывающих модульное, интеграционное и бенчмарки на наборах данных:

# Запуск всех тестов
ctest --test-dir build --output-on-failure

# Запуск определённого набора тестов
ctest --test-dir build -R test_simplifier --output-on-failure

# Запуск с подробным выводом
ctest --test-dir build -V

Бенчмарки на наборах данных проверяют работу на реальных обфусцированных выражениях из нескольких независимых источников. Полный отчёт см. в DATASETS.md — 75 126 выражений из 35 файлов наборов данных от 7 независимых источников.

Известные ограничения

• Глубоко перемешанные смешанно-полиномиальные MBA — оставшиеся неподдерживаемые выражения в основном представляют собой большие, сильно дублированные AST с чередованием арифметических и побитовых операторов. Подъём подвыражений, ранжированный по влиянию, восстанавливает многие из них, но выражения, исчерпавшие бюджет списка задач после подъёма, остаются неподдерживаемыми
• Расхождение реконструкции в булевой области — небольшое число выражений даёт кандидаты CoB, правильные на входах {0,1}, но неправильные при полной разрядности (AND-произведение против арифметического умножения). Такие случаи обнаруживаются и правильно сообщаются как не прошедшие верификацию
• Нет общей логической минимизации — CoBRA использует жадные алгебраические переписывания, а не Quine-McCluskey/Espresso/BDD

Благодарности

Спасибо Bas Zweers и команде Back Engineering за вдохновение и руководство, которые помогли сформировать этот проект. Рекомендуем к просмотру: их доклад re//verse 2026 Deobfuscation of a Real World Binary Obfuscator.

Дополнительная благодарность Jack Royer, Matteo Favaro, Arnau Gàmez и другим анонимным участникам за постоянное рецензирование и тестирование.

Лицензия

Apache-2.0. Тестовые наборы данных в test/datasets/ распространяются из сторонних исследовательских проектов под их оригинальными лицензиями (в основном GPL-3.0). Подробности см. в THIRD_PARTY_LICENSES.