mrphrazer/msynthFramework de desofuscación de código para simplificar expresiones de Aritmética Booleana Mixta (MBA)
Autor: Tim Blazytko y Moritz Schloegel
msynth es un framework de desofuscación de código para simplificar expresiones de Aritmética Booleana Mixta (MBA). Dado un oráculo de simplificación precalculado, recorre una expresión compleja representada como un árbol de sintaxis abstracta (AST) e intenta simplificar subárboles utilizando diversas técnicas de simplificación algebraica y semántica. Alternativamente, intenta simplificar expresiones mediante síntesis estocástica de programas.
msynth está construido sobre Miasm y está inspirado en los artículos
"QSynth: A Program Synthesis based Approach for Binary Code Deobfuscation" de Robin David, Luigi Coniglio y Mariano Ceccato (NDSS, BAR 2020),
"Syntia: Synthesizing the Semantics of Obfuscated Code" de Tim Blazytko, Moritz Contag, Cornelius Aschermann y Thorsten Holz (USENIX Security 2017) y
"Search-Based Local Blackbox Deobfuscation: Understand, Improve and Mitigate" de Grégoire Menguy, Sébastien Bardin, Richard Bonichon y Cauim de Souza de Lima (CCS 2021).
"Augmenting Search-based Program Synthesis with Local Inference Rules to Improve Black-box Deobfuscation" de Vidal Attias, Nicolas Bellec, Grégoire Menguy, Sébastien Bardin y Jean-Yves Marion (CCS 2025).
"Efficient Deobfuscation of Linear Mixed Boolean-Arithmetic Expressions" de Benjamin Reichenwallner y Peter Meerwald-Stadler (CheckMATE 2022) y
"Simplification of General Mixed Boolean-Arithmetic Expressions: GAMBA" de Benjamin Reichenwallner y Peter Meerwald-Stadler (WORMA 2023).
Puede utilizarse en combinación con el motor de ejecución simbólica de Miasm para simplificar expresiones complejas en código ofuscado o como una herramienta independiente para experimentar con la simplificación de MBA.
original: {((((((((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) ^ 0xFFFFFFFF) & RDX[0:32]) + ((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) & (RDX[0:32] ^ 0xFFFFFFFF)) + -(((((((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) ^ 0xFFFFFFFF) & RDX[0:32]) + ((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) | (((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32])) + ({RDI[0:32] & ({RDI[0:32] & RSI[0:32] 0 32, 0x0 32 64} * 0x2 + {RDI[0:32] ^ RSI[0:32] 0 32, 0x0 32 64})[0:32] 0 32, 0x0 32 64} * 0x2 + {((((RSI[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + RSI[0:32]) & RSI[0:32]) + (((RDI + {(RDI[0:32] ^ 0xFFFFFFFF) | RDX[0:32] 0 32, 0x0 32 64} + 0x1)[0:32] ^ 0xFFFFFFFF) & RDX[0:32]) + (RDI[0:32] ^ ({RDI[0:32] & RSI[0:32] 0 32, 0x0 32 64} * 0x2 + {RDI[0:32] ^ RSI[0:32] 0 32, 0x0 32 64})[0:32]) + ((RDI[0:32] ^ 0xFFFFFFFF) | RDX[0:32]) + (RDI + RDX + 0x1)[0:32] 0 32, 0x0 32 64})[0:32]) * 0x2 0 32, 0x0 32 64}
simplified: {(-RDX[0:32] + ((RDI[0:32] + RDX[0:32] + RSI[0:32]) << 0x1)) * 0x2 0 32, 0x0 32 64}
Para instalar msynth siga estos pasos:
git clone https://github.com/mrphrazer/msynth.git
cd msynth
# optionally: use a virtual environment
python -m venv msynth-env
source msynth-env/bin/activate
# install dependencies
pip install -r requirements.txt
# install msynth
pip install .
# unzip database
unzip -d database -q database/3_variables_constants_7_nodes.txt.zip
Al actualizar un entorno existente, reinstale las dependencias para adoptar el commit de Miasm fijado. Distintos commits de Miasm pueden reportar la misma versión del paquete, por lo que una instalación normal puede dejar instalado el commit anterior:
python -m pip install --force-reinstall -r requirements.txt
Para generar un oráculo, necesitamos una tabla de búsqueda de simplificación (o base de datos) que contenga un gran número de expresiones. Utilizamos una búsqueda enumerativa para precalcular expresiones con un tamaño de bit de 8, 16, 32 y 64 según las siguientes especificaciones:
hasta cinco variables p0, p1, p2, p3 y p4
operadores de truncamiento para reducir variables (si es necesario) a 32, 16 y 8 bits,
las operaciones de vectores de bits suma, resta, multiplicación, negación (menos unario), and/or/xor/not a nivel de bits y el desplazamiento lógico a la izquierda,
y, para algunas tablas, las constantes 0x0, 0x1, 0x2, 0x80, 0xff, 0x800, 0xffff, 0x8000_0000, 0xffff_ffff, 0x8000_0000_0000_0000 y 0xffff_ffff_ffff_ffff.
La base de datos de ejemplo incluida en database contiene las 1.293.020 combinaciones creadas al usar tres variables y las constantes 0x0, 0x1 y 0x2 para hasta 7 nodos (por ejemplo, ((p0 + p1) * (p2 ^ 0x2)) o ((p0 - p2) << (p1 + p2))). Puede encontrar bases de datos precalculadas más grandes aquí (~31GB descomprimidas). Tenga en cuenta que el código para precalcular expresiones no forma parte de este repositorio. Planeamos publicarlo en algún momento en el futuro.
Como alternativa a las tablas de búsqueda precalculadas, msynth soporta la simplificación de expresiones mediante síntesis estocástica de programas. Para una expresión aritmética compleja dada, msynth puede aprender una expresión más corta que comparta el mismo comportamiento de entrada-salida. Por ahora, está implementado como un componente independiente. Sin embargo, planeamos combinar ambos enfoques de simplificación en el futuro.
La ruta de síntesis también utiliza Search Modulo Inference Rules (Smir) por defecto, siguiendo el artículo de CCS 2025 enlazado anteriormente. Smir aumenta la búsqueda local derivando candidatos cercanos para patrones difíciles de sintetizar, como constantes arbitrarias, máscaras, desplazamientos y rotaciones constantes, expresiones afines y expresiones polinómicas acotadas.
Primero, generemos un oráculo de simplificación que use una base de datos de simplificación precalculada como entrada y agrupe las expresiones contenidas en clases de equivalencia.
$ python scripts/gen_oracle.py database/3_variables_constants_7_nodes.txt oracle.pickle
msynth - INFO: Computing oracle for 30 variables and 50 samples.
Using library at 'database/3_variables_constants_7_nodes.txt'
msynth - INFO: Writing oracle to oracle.pickle
msynth - INFO: Done in 632.84 seconds
Dependiendo del tamaño de la base de datos de simplificación precalculada, esto puede tardar unos minutos u horas, según su computadora. Alternativamente, puede usar el oracle.pickle precalculado.
Opcionalmente, se puede usar la bandera --sqlite para generar el oráculo en formato SQLite, lo que permite la carga diferida y tiempos de inicio significativamente más rápidos:
$ python scripts/gen_oracle.py database/3_variables_constants_7_nodes.txt oracle.db --sqlite
Posteriormente, el oráculo serializado puede usarse para simplificar expresiones complejas:
from msynth import Simplifier
# initialize simplifier
simplifier = Simplifier(oracle_path)
# simplify expression
simplified = simplifier.simplify(expression)