mrphrazer/msynthFramework di deoffuscamento del codice per semplificare le espressioni Mixed Boolean-Arithmetic (MBA)
Autore: Tim Blazytko e Moritz Schloegel
msynth è un framework di deoffuscamento del codice per semplificare espressioni Mixed Boolean-Arithmetic (MBA). Dato un oracolo di semplificazione precalcolato, attraversa un'espressione complessa rappresentata come albero sintattico astratto (AST) e tenta di semplificare i sottoalberi utilizzando varie tecniche di semplificazione algebrica e semantica. In alternativa, tenta di semplificare le espressioni tramite sintesi stocastica di programmi.
msynth è costruito sopra Miasm e ispirato ai paper
"QSynth: A Program Synthesis based Approach for Binary Code Deobfuscation" di Robin David, Luigi Coniglio e Mariano Ceccato (NDSS, BAR 2020),
"Syntia: Synthesizing the Semantics of Obfuscated Code" di Tim Blazytko, Moritz Contag, Cornelius Aschermann e Thorsten Holz (USENIX Security 2017) e
"Search-Based Local Blackbox Deobfuscation: Understand, Improve and Mitigate" di Grégoire Menguy, Sébastien Bardin, Richard Bonichon e Cauim de Souza de Lima (CCS 2021).
"Augmenting Search-based Program Synthesis with Local Inference Rules to Improve Black-box Deobfuscation" di Vidal Attias, Nicolas Bellec, Grégoire Menguy, Sébastien Bardin e Jean-Yves Marion (CCS 2025).
"Efficient Deobfuscation of Linear Mixed Boolean-Arithmetic Expressions" di Benjamin Reichenwallner e Peter Meerwald-Stadler (CheckMATE 2022) e
"Simplification of General Mixed Boolean-Arithmetic Expressions: GAMBA" di Benjamin Reichenwallner e Peter Meerwald-Stadler (WORMA 2023).
Può essere utilizzato in combinazione con il motore di esecuzione simbolica di Miasm per semplificare espressioni complesse in codice offuscato oppure come strumento autonomo per sperimentare con la semplificazione 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}
Per installare msynth segui questi passaggi:
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
Quando si aggiorna un ambiente esistente, reinstallare le dipendenze per acquisire il commit Miasm fissato. Commit Miasm diversi possono riportare la stessa versione del pacchetto, quindi una normale installazione può lasciare installato il commit precedente:
python -m pip install --force-reinstall -r requirements.txt
Per generare un oracolo, abbiamo bisogno di una tabella di lookup di semplificazione (o database) contenente un gran numero di espressioni. Abbiamo usato una ricerca enumerativa per precalcolare espressioni con una dimensione in bit di 8, 16, 32 e 64 secondo le seguenti specifiche:
fino a cinque variabili p0, p1, p2, p3 e p4
operatori di troncamento per ridurre le variabili (se necessario) a 32, 16 e 8 bit,
le operazioni su vettori di bit addizione, sottrazione, moltiplicazione, negazione (meno unario), and/or/xor/not bit a bit e lo shift logico a sinistra,
e, per alcune tabelle, le costanti 0x0, 0x1, 0x2, 0x80, 0xff, 0x800, 0xffff, 0x8000_0000, 0xffff_ffff, 0x8000_0000_0000_0000 e 0xffff_ffff_ffff_ffff.
Il database di esempio incluso in database contiene tutte le 1.293.020 combinazioni create utilizzando tre variabili e le costanti 0x0, 0x1 e 0x2 per un massimo di 7 nodi (ad esempio, ((p0 + p1) * (p2 ^ 0x2)) o ((p0 - p2) << (p1 + p2))). Database precalcolati più grandi possono essere trovati qui (~31GB decompresso). Nota che il codice per il precalcolo delle espressioni non fa parte di questo repository. Prevediamo di rilasciarlo in futuro.
Come alternativa alle tabelle di lookup precalcolate, msynth supporta la semplificazione di espressioni tramite sintesi stocastica di programmi. Per una data espressione aritmetica complessa, msynth può apprendere un'espressione più breve che condivide lo stesso comportamento input-output. Per ora, è implementata come componente autonomo. Tuttavia, prevediamo di combinare entrambi gli approcci di semplificazione in futuro.
Il percorso di sintesi utilizza anche Search Modulo Inference Rules (Smir) per impostazione predefinita, seguendo il paper CCS 2025 linkato sopra. Smir potenzia la ricerca locale derivando candidati vicini per pattern difficili da sintetizzare come costanti arbitrarie, maschere, shift e rotazioni costanti, espressioni affini ed espressioni polinomiali limitate.
Per prima cosa, generiamo un oracolo di semplificazione che utilizza un database di semplificazione precalcolato come input e raggruppa le espressioni contenute in classi di equivalenza.
$ 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
A seconda della dimensione del database di semplificazione precalcolato, questo può richiedere alcuni minuti o ore, a seconda del tuo computer. In alternativa, puoi usare l'oracle.pickle precalcolato.
Opzionalmente, il flag --sqlite può essere usato per generare l'oracolo in formato SQLite, il che abilita il caricamento lazy e tempi di avvio significativamente più rapidi:
$ python scripts/gen_oracle.py database/3_variables_constants_7_nodes.txt oracle.db --sqlite
Successivamente, l'oracolo serializzato può essere usato per semplificare espressioni complesse:
from msynth import Simplifier
# initialize simplifier
simplifier = Simplifier(oracle_path)
# simplify expression
simplified = simplifier.simplify(expression)