mrphrazer/msynthFramework de désobfuscation de code pour simplifier les expressions Mixed Boolean-Arithmetic (MBA)
Auteur : Tim Blazytko et Moritz Schloegel
msynth est un framework de désobfuscation de code permettant de simplifier les expressions d'arithmétique booléenne mixte (MBA). Étant donné un oracle de simplification pré-calculé, il parcourt une expression complexe représentée sous forme d'arbre syntaxique abstrait (AST) et tente de simplifier les sous-arbres à l'aide de diverses techniques de simplification algébrique et sémantique. Alternativement, il tente de simplifier les expressions via la synthèse de programmes stochastique.
msynth est construit sur Miasm et inspiré par les articles
"QSynth: A Program Synthesis based Approach for Binary Code Deobfuscation" de Robin David, Luigi Coniglio et Mariano Ceccato (NDSS, BAR 2020),
"Syntia: Synthesizing the Semantics of Obfuscated Code" de Tim Blazytko, Moritz Contag, Cornelius Aschermann et Thorsten Holz (USENIX Security 2017) et
"Search-Based Local Blackbox Deobfuscation: Understand, Improve and Mitigate" de Grégoire Menguy, Sébastien Bardin, Richard Bonichon et 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 et Jean-Yves Marion (CCS 2025).
"Efficient Deobfuscation of Linear Mixed Boolean-Arithmetic Expressions" de Benjamin Reichenwallner et Peter Meerwald-Stadler (CheckMATE 2022) et
"Simplification of General Mixed Boolean-Arithmetic Expressions: GAMBA" de Benjamin Reichenwallner et Peter Meerwald-Stadler (WORMA 2023).
Il peut être utilisé en combinaison avec le moteur d'exécution symbolique de Miasm pour simplifier des expressions complexes dans du code obfusqué ou comme outil autonome pour expérimenter la simplification 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}
Pour installer msynth, suivez ces étapes :
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
Lors de la mise à jour d'un environnement existant, réinstallez les dépendances pour récupérer le commit Miasm épinglé. Différents commits Miasm peuvent signaler la même version de paquet, donc une installation normale peut laisser l'ancien commit installé :
python -m pip install --force-reinstall -r requirements.txt
Pour générer un oracle, nous avons besoin d'une table de correspondance de simplification (ou base de données) contenant un grand nombre d'expressions. Nous avons utilisé une recherche énumérative pour pré-calculer des expressions avec une taille de bit de 8, 16, 32 et 64 selon les spécifications suivantes :
jusqu'à cinq variables p0, p1, p2, p3 et p4
des opérateurs de troncature pour réduire les variables (si nécessaire) à 32, 16 et 8 bits,
les opérations sur vecteurs de bits addition, soustraction, multiplication, négation (moins unaire), et/ou/xor/non bit à bit et le décalage logique à gauche,
et, pour certaines tables, les constantes 0x0, 0x1, 0x2, 0x80, 0xff, 0x800, 0xffff, 0x8000_0000, 0xffff_ffff, 0x8000_0000_0000_0000 et 0xffff_ffff_ffff_ffff.
La base de données d'exemple incluse dans database contient les 1 293 020 combinaisons créées en utilisant trois variables et les constantes 0x0, 0x1 et 0x2 pour jusqu'à 7 nœuds (par exemple, ((p0 + p1) * (p2 ^ 0x2)) ou ((p0 - p2) << (p1 + p2))). Des bases de données pré-calculées plus grandes sont disponibles ici (~31 Go décompressé). Notez que le code de pré-calcul des expressions ne fait pas partie de ce dépôt. Nous prévoyons de le publier à un moment donné dans le futur.
Comme alternative aux tables de correspondance pré-calculées, msynth prend en charge la simplification d'expressions via la synthèse de programmes stochastique. Pour une expression arithmétique complexe donnée, msynth peut apprendre une expression plus courte qui partage le même comportement entrée-sortie. Pour l'instant, elle est implémentée comme un composant autonome. Cependant, nous prévoyons de combiner les deux approches de simplification à l'avenir.
Le chemin de synthèse utilise également Search Modulo Inference Rules (Smir) par défaut, conformément à l'article CCS 2025 lié ci-dessus. Smir augmente la recherche locale en dérivant des candidats proches pour des motifs difficiles à synthétiser tels que les constantes arbitraires, les masques, les décalages et rotations constants, les expressions affines et les expressions polynomiales bornées.
D'abord, générons un oracle de simplification qui utilise une base de données de simplification pré-calculée en entrée et regroupe les expressions contenues dans des classes d'équivalence.
$ 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
Selon la taille de la base de données de simplification pré-calculée, cela peut prendre quelques minutes ou heures, selon votre ordinateur. Alternativement, vous pouvez utiliser l'oracle.pickle pré-calculé.
Optionnellement, l'option --sqlite peut être utilisée pour générer l'oracle au format SQLite, ce qui permet un chargement paresseux et des temps de démarrage nettement plus rapides :
$ python scripts/gen_oracle.py database/3_variables_constants_7_nodes.txt oracle.db --sqlite
Ensuite, l'oracle sérialisé peut être utilisé pour simplifier des expressions complexes :
from msynth import Simplifier