CoBRA

Reconstrucción Aritmética Basada en Coeficientes — un simplificador de expresiones booleanas-aritméticas mixtas.

CoBRA desofusca expresiones que intercalan operaciones aritméticas (+, -, *) con operaciones bit a bit (&, |, ^, ~) y desplazamiento (<<, >>) — una técnica comúnmente usada en ofuscación 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

Cómo Funciona

CoBRA utiliza un orquestador basado en listas de trabajo para simplificar expresiones. Cada entrada ingresa a la lista de trabajo como un elemento etiquetado con un tipo de estado. Un planificador selecciona el siguiente pase a ejecutar según el estado del elemento, las dependencias previas y una caché de intentos que evita trabajo redundante.

36 pases discretos se organizan en familias: procesamiento de AST, técnicas basadas en firmas, técnicas semilineales, descomposición y elevación. Algunos pases generan alternativas locales o soluciones hijas que se resuelven mediante grupos de competencia; fuera de esos grupos, la lista de trabajo devuelve el primer candidato de nivel superior completamente verificado. Todos los resultados se verifican mediante comprobaciones aleatorias (por defecto) o prueba de equivalencia Z3 (--verify).

Expresión de entrada
       |
  [Planificador de lista de trabajo]
       |
  Los elementos fluyen a través de tipos de estado:
       |
  kFoldedAst ──> Pases de procesamiento de AST
       |         (clasificar, reducir, reescribir)
       |
       +──> kSignatureState ──> Técnicas de firma
       |    (coincidencia de patrones, CoB, ANF, recuperación polinómica)
       |
       +──> kSemilinearNormalizedIr ──> Técnicas semilineales
       |    (normalizar, recuperar estructura, refinar, reconstruir)
       |
       +──> kCoreCandidate / kRemainderState ──> Descomposición
       |    (extraer núcleo, clasificar residual, resolver)
       |
       +──> kLiftedSkeleton ──> Elevación
       |    (sustitución de variable virtual, resolución externa)
       |
       +──> kCandidateExpr ──> Verificación
            (comprobación aleatoria o prueba Z3)
       |
  Expresión simplificada

Técnicas basadas en firmas: evalúan la expresión en todas las entradas booleanas para obtener un vector de firma. Una transformación mariposa CoB recupera los coeficientes de la base de productos Y. La coincidencia de patrones, ANF y la recuperación polinómica manejan diferentes niveles de complejidad.

Técnicas semilineales: manejan expresiones con máscaras constantes (ej., x & 0xFF). La expresión se descompone en átomos bit a bit ponderados; luego, la recuperación de estructura y el refinamiento de términos simplifican la representación intermedia, y el ensamblado OR particionado por bits reconstruye el resultado final.

Descomposición: apunta a expresiones mixtas con productos de subexpresiones bit a bit. Se extrae un núcleo polinómico, luego se clasifican y resuelven los residuales (polinómico, booleano-nulo/fantasma o respaldo por plantilla).

Elevación: reemplaza subexpresiones complejas con variables virtuales, resuelve el esqueleto externo simplificado y luego sustituye hacia atrás.

Características

• Simplificación MBA lineal — sumas ponderadas de átomos bit a bit mediante vector de firma y transformación CoB
• Coincidencia de patrones escalada — k * f(vars) + c con descomposición de Shannon para expresiones booleanas de 4-5 variables
• Soporte semilineal — átomos con máscara constante y reducción de constantes XOR/OR/NOT-AND, recuperación de estructura, refinamiento de términos, reconstrucción particionada por bits
• Recuperación polinómica — términos multilineales y potencias singleton mediante división de coeficientes y diferencias finitas
• Manejo de productos mixtos — motor de descomposición con extracción de núcleo, resolución de residuales y clasificación de residuales fantasma
• Elevación de subexpresiones — reemplazo de subárboles complejos con variables virtuales para reducir la dimensión del problema
• Orquestador de lista de trabajo — planificación de pases consciente del DAG con desduplicación y búsqueda acotada
• Grupos de competencia — ramas alternativas locales y soluciones hijas usan selección de ganador basada en coste con continuaciones
• Desplazamientos constantes — << se desazucara a multiplicación, >> se simplifica mediante técnicas semilineales
• Limpiado ANF — absorción, factorización de cubos comunes y reconocimiento de OR
• Anchura de bits configurable — aritmética modular de 1 a 64 bits
• Eliminación de variables auxiliares — reduce el número de variables cuando se cancelan términos
• Verificación Z3 — comprobación opcional de equivalencia de la salida simplificada
• Autoverificación por comprobación aleatoria — validación ligera con entradas aleatorias cuando Z3 no está disponible
• Plugin de pase LLVM — integración directa en tuberías de compilador (requiere LLVM 19-22)

Compilación

Consulte BUILD.md para obtener detalles completos, incluyendo dependencias opcionales (LLVM, Z3).

# Dependencias de compilación (Abseil, Highway; opcionalmente GoogleTest, LLVM, Z3)
cmake -S dependencies -B build-deps -DCMAKE_BUILD_TYPE=Release
cmake --build build-deps

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

# (Opcional) Compilar y ejecutar pruebas
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

Con Plugin de Pase 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

# Simplificación básica
cobra-cli --mba "(x&y)+(x|y)"

# Especificar anchura de bits
cobra-cli --mba "(x&0xFF)+(x&0xFF00)" --bitwidth 16

# Habilitar verificación de equivalencia Z3
cobra-cli --mba "(a^b)+(a&b)+(a&b)" --verify

# Salida verbose (mostrar pasos intermedios de la tubería)
cobra-cli --mba "(x&y)+(x|y)" --verbose

Opciones

Estructura del Proyecto

lib/core/                Motor de simplificación principal (~50 archivos fuente)
  Orchestrator             Planificador de lista de trabajo, máquina de estados, bucle principal de simplificación
  OrchestratorPasses       Registro de 39 pases con planificación consciente del DAG
  CompetitionGroup         Carrera de múltiples técnicas y selección de ganador
  ContinuationTypes        Datos de recombinación diferida para composición de pases
  JoinState                Seguimiento de unión de múltiples operandos para reescrituras estructurales
  SignatureSimplifier      Técnicas basadas en firmas (CoB, coincidencia de patrones, ANF)
  SignatureVector          Evaluar expresión en entradas {0,1}^n
  AuxVarEliminator         Reducir número de variables detectando cancelaciones
  PatternMatcher           Reconocer patrones bit a bit (tablas 2-var/3-var, escaladas)
  CoeffInterpolator        Interpolación mariposa para recuperación de coeficientes
  CoBExprBuilder           Reconstruir expresiones a partir de coeficientes CoB
  AnfTransform             Conversión a Forma Normal Algebraica
  AnfCleanup               Absorción, factorización, reconocimiento de OR
  CoefficientSplitter      Separar contribuciones bit a bit vs. aritméticas
  ArithmeticLowering       Reducir fragmento aritmético a IR polinómico
  PolyNormalizer           Forma canónica para expresiones polinómicas
  SingletonPowerRecovery   Detectar términos x^k mediante diferencias finitas
  DecompositionEngine      Bucle extrae-resuelve: núcleo polinómico + resolución de residuales
  GhostBasis               Biblioteca de primitivas fantasma (mul_sub_and, mul3_sub_and3)
  GhostResidualSolver      Clasificación booleana-nula y resolución de residuales fantasma
  WeightedPolyFit          Ajuste lineal ponderado 2-ádico para cocientes polinómicos
  MixedProductRewriter     Expandir productos bit a bit en sumas lineales
  TemplateDecomposer       Coincidencia de plantillas acotada para expresiones mixtas
  ProductIdentityRecoverer Recuperar identidades de suma de productos
  SemilinearNormalizer     Descomponer en átomos bit a bit ponderados
  SemilinearSignature      Evaluación de firma por bit y atajo lineal
  StructureRecovery        Recuperación de XOR, eliminación de máscaras, coalescencia de términos
  TermRefiner              Reducción de máscaras de bits muertos, fusión de mismo coeficiente
  BitPartitioner           Agrupar posiciones de bits por perfil semántico
  MaskedAtomReconstructor  Reensamblaje con reescritura OR para máscaras disjuntas
  Evaluator                Evaluador de expresiones compilado

lib/llvm/                Plugin de pase LLVM (CobraPass, MBADetector, IRReconstructor)
lib/verify/              Verificación de equivalencia basada en Z3
include/cobra/           Cabeceras públicas
tools/cobra-cli/         Interfaz de línea de comandos y analizador de expresiones
test/                    1195 pruebas en ~63 archivos de prueba

Pruebas

CoBRA tiene 1195 pruebas que cubren benchmarks unitarios, de integración y de conjuntos de datos:

# Ejecutar todas las pruebas
ctest --test-dir build --output-on-failure

# Ejecutar un conjunto de pruebas específico
ctest --test-dir build -R test_simplifier --output-on-failure

# Ejecutar con salida detallada
ctest --test-dir build -V

Los benchmarks de conjuntos de datos validan contra expresiones ofuscadas del mundo real de múltiples fuentes independientes. Consulte DATASETS.md para el informe completo de benchmarks: 75,126 expresiones en 35 archivos de conjunto de datos de 7 fuentes independientes.

Limitaciones Conocidas

• MBA polinómicos mixtos profundamente intercalados — las expresiones restantes no soportadas son predominantemente AST grandes y fuertemente duplicados con operadores aritméticos y bit a bit intercalados. La elevación de subexpresiones clasificada por impacto recupera muchas de estas, pero las expresiones que agotan el presupuesto de la lista de trabajo después de la elevación siguen sin soporte
• Divergencia en la reconstrucción del dominio booleano — un pequeño número de expresiones produce candidatos CoB que son correctos en entradas {0,1} pero incorrectos a ancho completo (base de productos Y vs. multiplicación aritmética). Estos se detectan y se informan correctamente como fallos de verificación
• Sin minimización lógica general — CoBRA usa reescrituras algebraicas codiciosas, no Quine-McCluskey/Espresso/BDD

Agradecimientos

Gracias a Bas Zweers y al equipo de Back Engineering por la inspiración y guía que ayudaron a dar forma a este proyecto. Visualización recomendada: su charla re//verse 2026 Deobfuscation of a Real World Binary Obfuscator.

Agradecimientos adicionales a Jack Royer, Matteo Favaro, Arnau Gàmez y otros contribuyentes anónimos por la continua revisión y pruebas.

Licencia

Apache-2.0. Los conjuntos de datos de prueba en test/datasets/ se redistribuyen de proyectos de investigación de terceros bajo sus licencias originales (principalmente GPL-3.0). Consulte THIRD_PARTY_LICENSES para más detalles.