Simplificando la complejidad de los MBAs con CoBRA
CYBERSECURITY ANÁLISIS DESTACADO

Simplificando la complejidad de los MBAs con CoBRA

FUENTE

The Trail of Bits Blog

DATE

READ

6 min de lectura

CoBRA es una herramienta de código abierto diseñada para simplificar las expresiones de Álgebra Booleana Mixta (MBA) que se utilizan comúnmente en malware y protección de software. A diferencia de los métodos anteriores, …

La desobfuscación MBA combina operaciones simples como x + y con enredos de operadores aritméticos y de bits. Los autores de malware y los protectores de software se basan en ella, ya que ninguna técnica de simplificación estándar cubre ambos dominios simultáneamente; los simplificadores algebraicos no entienden la lógica de bits, y los minimizadores booleanos no pueden manejar la aritmética. Estamos lanzando CoBRA, una herramienta de código abierto que simplifica toda la gama de expresiones MBA utilizadas en la práctica. Aplícalo a una expresión desobfuscada y recupera una versión simplificada equivalente: $ 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 simplifica el 99.86% de las 73,000+ expresiones extraídas de siete conjuntos de datos independientes. Se entrega como una herramienta de línea de comandos, una biblioteca C++, y un plugin de pas en LLVM. Si has encontrado desobfuscación MBA durante el análisis de malware, la reversión de esquemas de protección de software, o al deshacer VM-based obfuscators, CoBRA te devuelve expresiones legibles. ¿Por qué los enfoques existentes no funcionan La dificultad principal es que la verificación de identidades MBA requiere razonar sobre cómo interactúan los bits y la aritmética bajo el envoltura modular, donde los valores sobrepasan y giran silenciosamente a una anchura de bits fija. Una identidad como (x ^ y) + 2 * (x & y) == x + y es verdadera precisamente debido a esta interacción, pero los simplificadores algebraicos solo ven la aritmética y los minimizadores booleanos solo ven la lógica; ninguno puede verificarlo por sí solo. Los desobfuscadores superponen estas sustituciones para construir expresiones arbitrariamente complejas a partir de operaciones más simples. Los simplificadores MBA anteriores han abordado partes de este problema. SiMBA maneja bien las expresiones lineales. GAMBA extiende el soporte a los casos polinómicos. Hasta CoBRA, ninguna herramienta única logró altas tasas de éxito en toda la gama de tipos de expresiones MBA que los ingenieros de seguridad encuentran en la práctica. ¿Cómo funciona CoBRA CoBRA utiliza un orquestador basado en una lista de tareas pendientes que clasifica cada expresión de entrada y selecciona la combinación correcta de técnicas de simplificación. El orquestador gestiona 36 pas discretos organizados en cuatro familias: lineales, semilineales, polinómicas y mixtas, y enruta los elementos de trabajo en función de la estructura de la expresión. La mayoría de las expresiones MBA en la práctica son lineales: sumas de términos de bits como (x & y), (x | y), y ~x, cada uno multiplicado por una constante. Para estas, el orquestador evalúa la expresión en todas las entradas booleanas para producir una firma, luego compite múltiples técnicas de recuperación entre sí y elige el resultado verificado más barato. Aquí está cómo se ve para (x ^ y) + 2 * (x & y): CoBRA flujo de simplificación lineal: (x ^ y) + 2 * (x & y) Paso 1: Clasificación La expresión de entrada se identifica como MBA lineal ↓ Paso 2: Generación de la tabla de verdad Evaluar en todas las entradas booleanas → [0, 1, 1, 2] tabla de verdad ↓ Paso 3a: Coincidencia de patrones Búsqueda en la base de datos de patrones Paso 3b: Conversión ANF Forma normal de bits Paso 3c: Interpolación Solución de los coeficientes base ↓ Paso 4: Competencia Comparar resultados candidatos → Ganador: x + y (Costo más bajo) ↓ Paso 5: Verificación Spot-check contra 64 entradas aleatorias o probar con Z3 → Pasa Cuando aparecen máscaras constantes (como x & 0xFF), la expresión entra en el flujo semi-lineal de CoBRA, que la descompone en sus bloques de bits más pequeños, recupera patrones estructurales, y reconstruye un resultado simplificado a través de ensamblaje particionado en bits. Para expresiones que involucran productos de subexpresiones de bits (como (x & y) * (x | y)), un motor de descomposición extrae núcleos polinómicos y resuelve residuos. Las expresiones mixtas que combinan productos con operaciones de bits a menudo contienen subexpresiones repetidas. Un paso de elevación reemplaza estas con variables temporales, simplificando las piezas internas primero, luego resuelve la expresión que las conecta. Aquí está cómo se ve para un producto de identidad (x & y) * (x | y) + (x & ~y) * (~x & y): CoBRA flujo de simplificación mixta: (x & y) * (x | y) + (x & ~y) * (~x & y) Paso 1: Clasificación La entrada se identifica como MBA mixta ↓ Paso 2: Descomposición Descomponer en subexpresiones ↓ (x & y) * (x | y) (x & ~y) * (~x & y) ↓ ↓ Paso 3: Lift & Solve Elevar productos, resolver piezas internas ↓ Paso 4: Collapse Identidad Colapsar identidad de producto → x * y ↓ Paso 5: Verificación Spot-check contra 64 entradas aleatorias o probar con Z3 → Pasa Independientemente de qué flujo pase una expresión, el paso final es el mismo: CoBRA verifica cada resultado contra entradas aleatorias o prueba la equivalencia con Z3. No se devuelve ninguna simplificación a menos que esté confirmada como correcta. ¿Qué puedes hacer con ello CoBRA funciona en tres modos: CLI tool: pasar una expresión directamente y obtener la versión simplificada. Usa –bitwidth para establecer el ancho de aritmética modular (de 1 a 64 bits) y –verify para pruebas de equivalencia con Z3. C++ library: enlazar a la biblioteca central de CoBRA para integrar la simplificación en tus propias herramientas. Si estás construyendo un pipeline de análisis automatizado, la API Simplify toma una expresión y devuelve un resultado simplificado o informa que es no soportada. LLVM pass plugin: carga libCobraPass.so en opt para desobfuscación de patrones MBA directamente en LLVM IR. Si estás construyendo pipelines de desobfuscación sobre herramientas como Remill, se integra directamente como un pas. Maneja patrones que abarcan múltiples bloques básicos y aplica una puerta de costo, reemplazando instrucciones solo cuando la forma simplificada es más pequeña, y soporta LLVM 19 a 22. Validados contra siete conjuntos de datos independientes Hemos probado CoBRA contra 73,066 expresiones de SiMBA, GAMBA, OSES, y cuatro fuentes independientes. Cubren todo el espectro de complejidad de MBA, desde expresiones lineales de dos variables hasta desobfuscaciones mixtas de productos profundamente anidadas. Categorías Expresiones Tasa de Simplificación Lineal ~55,000 ~55,000 ~100% Semilinear ~1,000 ~1,000 ~100% Polynomial ~5,000 ~4,950 ~99% Mixed ~9,000 ~8,900 ~99% Total 73,066 72,960 99.86% Las 106 expresiones no soportadas son casos mixtos de dominio sensibles a portencias donde las operaciones de bits y aritméticas interactúan de maneras que no pueden descomponerse por las técnicas actuales. CoBRA informa que son no soportadas en lugar de adivinar incorrectamente. El desglose completo del rendimiento está en DATASETS.md. ¿Qué sigue Los fallos restantes de CoBRA caen en dos categorías: expresiones con duplicación de subexpresiones que agotan el presupuesto de trabajo incluso con el paso de elevación, y residuos sensibles a portencias donde máscaras de bits sobre productos aritméticos crean dependencias a nivel de bits que ninguna técnica de descomposición actual puede recuperar. También estamos explorando opciones de integración más amplias más allá de solo un plugin de LLVM, como plugins nativos para IDA Pro y Binary Ninja. La fuente está disponible en GitHub bajo la licencia Apache 2.0. Si encuentras expresiones que CoBRA no puede simplificar, por favor abre un problema en el repositorio. Queremos los problemas difíciles.