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