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

Опции

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