mrphrazer/msynthCode-Deobfuskierungs-Framework zur Vereinfachung von Mixed Boolean-Arithmetic (MBA)-Ausdrücken
Autor: Tim Blazytko und Moritz Schloegel
msynth ist ein Code-Deobfuskierungs-Framework zur Vereinfachung von Mixed Boolean-Arithmetic (MBA)-Ausdrücken. Ausgehend von einem vorberechneten Vereinfachungs-Orakel durchläuft es einen komplexen Ausdruck, der als abstrakter Syntaxbaum (AST) dargestellt wird, und versucht, Teilbäume mithilfe verschiedener algebraischer und semantischer Vereinfachungstechniken zu vereinfachen. Alternativ versucht es, Ausdrücke durch stochastische Programmsynthese zu vereinfachen.
msynth baut auf Miasm auf und ist inspiriert von den folgenden Arbeiten:
"QSynth: A Program Synthesis based Approach for Binary Code Deobfuscation" von Robin David, Luigi Coniglio und Mariano Ceccato (NDSS, BAR 2020),
"Syntia: Synthesizing the Semantics of Obfuscated Code" von Tim Blazytko, Moritz Contag, Cornelius Aschermann und Thorsten Holz (USENIX Security 2017) und
"Search-Based Local Blackbox Deobfuscation: Understand, Improve and Mitigate" von Grégoire Menguy, Sébastien Bardin, Richard Bonichon und Cauim de Souza de Lima (CCS 2021).
"Augmenting Search-based Program Synthesis with Local Inference Rules to Improve Black-box Deobfuscation" von Vidal Attias, Nicolas Bellec, Grégoire Menguy, Sébastien Bardin und Jean-Yves Marion (CCS 2025).
"Efficient Deobfuscation of Linear Mixed Boolean-Arithmetic Expressions" von Benjamin Reichenwallner und Peter Meerwald-Stadler (CheckMATE 2022) und
"Simplification of General Mixed Boolean-Arithmetic Expressions: GAMBA" von Benjamin Reichenwallner und Peter Meerwald-Stadler (WORMA 2023).
Es kann in Kombination mit Miasms symbolischer Ausführungs-Engine verwendet werden, um komplexe Ausdrücke in obfuskiertem Code zu vereinfachen, oder als eigenständiges Werkzeug, um mit der MBA-Vereinfachung zu experimentieren.
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}
Um msynth zu installieren, folgen Sie diesen Schritten:
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
Beim Aktualisieren einer bestehenden Umgebung installieren Sie die Abhängigkeiten neu, um den gepinnten Miasm-Commit zu übernehmen. Verschiedene Miasm-Commits können dieselbe Paketversion melden, sodass eine reguläre Installation den älteren Commit installiert lassen kann:
python -m pip install --force-reinstall -r requirements.txt
Um ein Orakel zu generieren, benötigen wir eine Vereinfachungs-Lookup-Tabelle (oder Datenbank), die eine große Anzahl von Ausdrücken enthält. Wir haben eine enumerative Suche verwendet, um Ausdrücke mit einer Bitgröße von 8, 16, 32 und 64 gemäß den folgenden Spezifikationen vorzuberechnen:
bis zu fünf Variablen p0, p1, p2, p3 und p4
Trunkierungsoperatoren, um Variablen (falls nötig) auf 32, 16 und 8 Bit herunterzukonvertieren,
die Bitvektor-Operationen Addition, Subtraktion, Multiplikation, Negation (unäres Minus), bitweises Und/Oder/Xor/Nicht und die logische Linksverschiebung,
und, für einige Tabellen, die Konstanten 0x0, 0x1, 0x2, 0x80, 0xff, 0x800, 0xffff, 0x8000_0000, 0xffff_ffff, 0x8000_0000_0000_0000 und 0xffff_ffff_ffff_ffff.
Die in database enthaltene Beispieldatenbank enthält alle 1.293.020 Kombinationen, die durch die Verwendung von drei Variablen und den Konstanten 0x0, 0x1 und 0x2 für bis zu 7 Knoten entstehen (z. B. ((p0 + p1) * (p2 ^ 0x2)) oder ((p0 - p2) << (p1 + p2))). Größere vorberechnete Datenbanken finden Sie hier (~31 GB entpackt). Beachten Sie, dass der Code zur Vorberechnung von Ausdrücken nicht Teil dieses Repositorys ist. Wir planen, ihn zu einem späteren Zeitpunkt zu veröffentlichen.
Als Alternative zu vorberechneten Lookup-Tabellen unterstützt msynth die Ausdrucksvereinfachung durch stochastische Programmsynthese. Für einen gegebenen komplexen arithmetischen Ausdruck kann msynth einen kürzeren Ausdruck lernen, der dasselbe Eingabe-Ausgabe-Verhalten aufweist. Derzeit ist es als eigenständige Komponente implementiert. Wir planen jedoch, beide Vereinfachungsansätze in Zukunft zu kombinieren.
Der Synthesepfad verwendet standardmäßig auch Search Modulo Inference Rules (Smir), entsprechend dem oben verlinkten CCS-2025-Paper. Smir erweitert die lokale Suche, indem es nahegelegene Kandidaten für schwer zu synthetisierende Muster wie beliebige Konstanten, Masken, konstante Verschiebungen und Rotationen, affine Ausdrücke und beschränkte Polynomausdrücke ableitet.
Zunächst generieren wir ein Vereinfachungs-Orakel, das eine vorberechnete Vereinfachungsdatenbank als Eingabe verwendet und die enthaltenen Ausdrücke in Äquivalenzklassen clustert.
$ 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
Je nach Größe der vorberechneten Vereinfachungsdatenbank kann dies einige Minuten oder Stunden dauern, abhängig von Ihrem Computer. Alternativ können Sie das vorberechnete oracle.pickle verwenden.
Optional kann das Flag --sqlite verwendet werden, um das Orakel im SQLite-Format zu generieren, was Lazy Loading und deutlich schnellere Startzeiten ermöglicht:
$ python scripts/gen_oracle.py database/3_variables_constants_7_nodes.txt oracle.db --sqlite
Anschließend kann das serialisierte Orakel zur Vereinfachung komplexer Ausdrücke verwendet werden:
from msynth import Simplifier
# initialize simplifier
simplifier = Simplifier(oracle_path)
# simplify expression
simplified = simplifier.simplify(expression)