CoBRA

Coeficiente-Baseado em Reconstrução Aritmética — um simplificador de expressões de Aritmética Booleana Mista.

O CoBRA desofusca expressões que intercalam operadores aritméticos (+, -, *) com operadores bit a bit (&, |, ^, ~) e de deslocamento (<<, >>) — uma técnica comumente usada em ofuscação de software.

$ 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

Como Funciona

O CoBRA usa um orquestrador baseado em lista de trabalho para simplificar expressões. Cada entrada entra na lista de trabalho como um item de trabalho etiquetado com um tipo de estado. Um agendador seleciona o próximo passo a ser executado com base no estado do item, nas dependências de pré-requisitos e em um cache de tentativas que evita trabalho redundante.

Os 36 passos discretos estão organizados em famílias: processamento de AST, técnicas baseadas em assinatura, técnicas semilineares, decomposição e elevação. Alguns passos bifurcam alternativas locais ou resoluções filhas que são resolvidas por grupos de competição; fora desses grupos, a lista de trabalho retorna o primeiro candidato de nível superior totalmente verificado. Todos os resultados são verificados por amostragem de entradas aleatórias (padrão) ou por prova de equivalência com 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

Técnicas baseadas em assinatura avaliam a expressão em todas as entradas booleanas para obter um vetor de assinatura. Uma transformada butterfly CoB recupera os coeficientes da base de produtos-AND. Correspondência de padrões, ANF e recuperação polinomial lidam com diferentes níveis de complexidade.

Técnicas semilineares lidam com expressões com máscaras constantes (ex.: x & 0xFF). A expressão é decomposta em átomos bit a bit ponderados; em seguida, a recuperação de estrutura e o refinamento de termos simplificam a representação intermediária, e a montagem OR particionada por bits reconstrói o resultado final.

Decomposição tem como alvo expressões mistas com produtos de subexpressões bit a bit. Um núcleo polinomial é extraído e, em seguida, os resíduos são classificados e resolvidos (polinomial, nulo-booleano/fantasma ou fallback por template).

Elevação substitui subexpressões complexas por variáveis virtuais, resolve o esqueleto externo simplificado e, em seguida, substitui de volta.

Recursos

• Simplificação linear de MBA — somas ponderadas de átomos bit a bit via vetor de assinatura e transformada CoB
• Correspondência de padrões escalada — k * f(vars) + c com decomposição de Shannon para expressões booleanas de 4 a 5 variáveis
• Suporte semilinear — átomos com máscara constante com redução de constantes XOR/OR/NOT-AND, recuperação de estrutura, refinamento de termos e reconstrução particionada por bits
• Recuperação polinomial — termos multilineares e potências singulares via divisão de coeficientes e diferenças finitas
• Tratamento de produtos mistos — mecanismo de decomposição com extração de núcleo, resolução de resíduos e classificação de resíduos fantasma
• Elevação de subexpressões — substitui subárvores complexas por variáveis virtuais para reduzir a dimensão do problema
• Orquestrador de lista de trabalho — agendamento de passos ciente de DAG com deduplicação e busca limitada
• Grupos de competição — ramos alternativos locais e resoluções filhas usam seleção de vencedor baseada em custo com continuações
• Deslocamentos constantes — << é convertido em multiplicação, >> é simplificado via técnicas semilineares
• Limpeza de ANF — absorção, fatoração de cubo comum e reconhecimento de OR
• Largura de bits configurável — aritmética modular de 1 a 64 bits
• Eliminação de variáveis auxiliares — reduz a contagem de variáveis quando os termos se cancelam
• Verificação com Z3 — verificação opcional de equivalência da saída simplificada
• Autoteste por amostragem — validação leve com entradas aleatórias quando o Z3 não está disponível
• Plugin de pass para LLVM — integração direta em pipelines de compiladores (requer LLVM 19-22)

Compilação

Consulte BUILD.md para obter todos os detalhes, incluindo dependências opcionais (LLVM, Z3).

# Build dependencies (Abseil, Highway; optionally GoogleTest, LLVM, Z3)
cmake -S dependencies -B build-deps -DCMAKE_BUILD_TYPE=Release
cmake --build build-deps

# Build CoBRA
cmake -S . -B build \
  -DCMAKE_PREFIX_PATH=$(pwd)/build-deps/install \
  -DCMAKE_BUILD_TYPE=Release
cmake --build build

# (Optional) Build and run tests
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

Com o Plugin de Pass para LLVM

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

Uso

# Basic simplification
cobra-cli --mba "(x&y)+(x|y)"

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

# Enable Z3 equivalence verification
cobra-cli --mba "(a^b)+(a&b)+(a&b)" --verify

# Verbose output (show intermediate pipeline steps)
cobra-cli --mba "(x&y)+(x|y)" --verbose

Opções

Estrutura do Projeto

lib/core/                Core simplification engine (~50 source files)
  Orchestrator             Worklist scheduler, state machine, main simplification loop
  OrchestratorPasses       39-pass registry with DAG-aware scheduling
  CompetitionGroup         Multi-technique racing and winner selection
  ContinuationTypes        Deferred recombination data for pass composition
  JoinState                Multi-operand join tracking for structural rewrites
  SignatureSimplifier      Signature-based techniques (CoB, pattern matching, ANF)
  SignatureVector          Evaluate expression on {0,1}^n inputs
  AuxVarEliminator         Reduce variable count by detecting cancellations
  PatternMatcher           Recognize bitwise patterns (2-var/3-var tables, scaled)
  CoeffInterpolator        Butterfly interpolation for coefficient recovery
  CoBExprBuilder           Reconstruct expressions from CoB coefficients
  AnfTransform             Algebraic Normal Form conversion
  AnfCleanup               Absorption, factoring, OR recognition
  CoefficientSplitter      Separate bitwise vs. arithmetic contributions
  ArithmeticLowering       Lower arithmetic fragment to polynomial IR
  PolyNormalizer           Canonical form for polynomial expressions
  SingletonPowerRecovery   Detect x^k terms via finite differences
  DecompositionEngine      Extract-solve loop: polynomial core + residual solving
  GhostBasis               Ghost primitive library (mul_sub_and, mul3_sub_and3)
  GhostResidualSolver      Boolean-null classification and ghost residual solving
  WeightedPolyFit          2-adic weighted linear solve for polynomial quotients
  MixedProductRewriter     Expand bitwise products into linear sums
  TemplateDecomposer       Bounded template matching for mixed expressions
  ProductIdentityRecoverer Recover product-of-sums identities
  SemilinearNormalizer     Decompose into weighted bitwise atoms
  SemilinearSignature      Per-bit signature evaluation and linear shortcut
  StructureRecovery        XOR recovery, mask elimination, term coalescing
  TermRefiner              Dead-bit mask reduction, same-coefficient merge
  BitPartitioner           Group bit positions by semantic profile
  MaskedAtomReconstructor  Reassemble with OR-rewrite for disjoint masks
  Evaluator                Compiled expression evaluator

lib/llvm/                LLVM pass plugin (CobraPass, MBADetector, IRReconstructor)
lib/verify/              Z3-based equivalence verification
include/cobra/           Public headers
tools/cobra-cli/         CLI frontend and expression parser
test/                    1195 tests across ~63 test files

Testes

O CoBRA tem 1195 testes cobrindo benchmarks de unidade, integração e conjuntos de dados:

# Run all tests
ctest --test-dir build --output-on-failure

# Run a specific test suite
ctest --test-dir build -R test_simplifier --output-on-failure

# Run with verbose output
ctest --test-dir build -V

Os benchmarks de conjuntos de dados validam contra expressões ofuscadas do mundo real de múltiplas fontes independentes. Consulte DATASETS.md para o relatório completo de benchmarks — 75,126 expressões em 35 arquivos de conjuntos de dados de 7 fontes independentes.

Limitações Conhecidas

• MBAs polinomiais mistos profundamente intercalados — as expressões não suportadas restantes são predominantemente ASTs grandes e bastante duplicados, com operadores aritméticos e bit a bit intercalados. A elevação de subexpressões classificada por impacto recupera muitas delas, mas expressões que esgotam o orçamento da lista de trabalho após a elevação permanecem sem suporte
• Divergência de reconstrução no domínio booleano — um pequeno número de expressões produz candidatos CoB que são corretos em entradas {0,1} mas incorretos em largura total (base de produtos-AND vs. multiplicação aritmética). Esses casos são detectados e corretamente relatados como falha de verificação
• Sem minimização lógica geral — o CoBRA usa reescritas algébricas gulosas, não Quine-McCluskey/Espresso/BDD

Agradecimentos

Agradecimentos a Bas Zweers e à equipe da Back Engineering pela inspiração e orientação que ajudaram a moldar este projeto. Visualização recomendada: a palestra deles na re//verse 2026, Desofuscação de um Ofuscador Binário do Mundo Real.

Agradecimentos adicionais a Jack Royer, Matteo Favaro, Arnau Gàmez e outros colaboradores anônimos pela revisão e testes contínuos

Licença

Apache-2.0. Os conjuntos de dados de teste em test/datasets/ são redistribuídos de projetos de pesquisa de terceiros sob suas licenças originais (principalmente GPL-3.0). Consulte THIRD_PARTY_LICENSES para obter detalhes.