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