mrphrazer/msynthEstrutura de desofuscação de código para simplificar expressões de Aritmética Booleana Mista (MBA)
Autor: Tim Blazytko e Moritz Schloegel
msynth é um framework de desofuscação de código para simplificar expressões de Aritmética Booleana Mista (MBA). Dado um oráculo de simplificação pré-computado, ele percorre uma expressão complexa representada como uma árvore de sintaxe abstrata (AST) e tenta simplificar subárvores usando várias técnicas de simplificação algébrica e semântica. Alternativamente, ele tenta simplificar expressões por meio de síntese estocástica de programas.
msynth é construído sobre o Miasm e inspirado nos artigos
"QSynth: A Program Synthesis based Approach for Binary Code Deobfuscation" de Robin David, Luigi Coniglio e Mariano Ceccato (NDSS, BAR 2020),
"Syntia: Synthesizing the Semantics of Obfuscated Code" de Tim Blazytko, Moritz Contag, Cornelius Aschermann e Thorsten Holz (USENIX Security 2017) e
"Search-Based Local Blackbox Deobfuscation: Understand, Improve and Mitigate" de 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" de Vidal Attias, Nicolas Bellec, Grégoire Menguy, Sébastien Bardin e Jean-Yves Marion (CCS 2025).
"Efficient Deobfuscation of Linear Mixed Boolean-Arithmetic Expressions" de Benjamin Reichenwallner e Peter Meerwald-Stadler (CheckMATE 2022) e
"Simplification of General Mixed Boolean-Arithmetic Expressions: GAMBA" de Benjamin Reichenwallner e Peter Meerwald-Stadler (WORMA 2023).
Ele pode ser usado em combinação com o motor de execução simbólica do Miasm para simplificar expressões complexas em código ofuscado ou como uma ferramenta autônoma para brincar com a simplificação 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 o msynth, siga estes passos:
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
Ao atualizar um ambiente existente, reinstale as dependências para obter o commit fixado do Miasm. Commits diferentes do Miasm podem reportar a mesma versão do pacote, então uma instalação regular pode deixar o commit mais antigo instalado:
python -m pip install --force-reinstall -r requirements.txt
Para gerar um oráculo, precisamos de uma tabela de consulta de simplificação (ou banco de dados) contendo um grande número de expressões. Usamos uma busca enumerativa para pré-computar expressões com tamanho de bit de 8, 16, 32 e 64 de acordo com as seguintes especificações:
até cinco variáveis p0, p1, p2, p3 e p4
operadores de truncamento para reduzir variáveis (se necessário) para 32, 16 e 8 bits,
as operações de vetor de bits adição, subtração, multiplicação, negação (menos unário), and/or/xor/not bit a bit e o deslocamento lógico para a esquerda,
e, para algumas tabelas, as constantes 0x0, 0x1, 0x2, 0x80, 0xff, 0x800, 0xffff, 0x8000_0000, 0xffff_ffff, 0x8000_0000_0000_0000 e 0xffff_ffff_ffff_ffff.
O banco de dados de exemplo incluído em database contém todas as 1.293.020 combinações criadas usando três variáveis e as constantes 0x0, 0x1 e 0x2 para até 7 nós (por exemplo, ((p0 + p1) * (p2 ^ 0x2)) ou ((p0 - p2) << (p1 + p2))). Bancos de dados pré-computados maiores podem ser encontrados aqui (~31GB descompactado). Observe que o código para pré-computar expressões não faz parte deste repositório. Planejamos lançá-lo em algum momento no futuro.
Como alternativa às tabelas de consulta pré-computadas, o msynth suporta simplificação de expressões por meio de síntese estocástica de programas. Para uma dada expressão aritmética complexa, o msynth pode aprender uma expressão mais curta que compartilha o mesmo comportamento de entrada-saída. Por enquanto, está implementado como um componente autônomo. No entanto, planejamos combinar ambas as abordagens de simplificação no futuro.
O caminho de síntese também usa Search Modulo Inference Rules (Smir) por padrão, seguindo o artigo CCS 2025 vinculado acima. Smir aumenta a busca local derivando candidatos próximos para padrões difíceis de sintetizar, como constantes arbitrárias, máscaras, deslocamentos e rotações constantes, expressões afins e expressões polinomiais limitadas.
Primeiro, vamos gerar um oráculo de simplificação que usa um banco de dados de simplificação pré-computado como entrada e agrupa as expressões contidas em classes de equivalência.
$ 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
Dependendo do tamanho do banco de dados de simplificação pré-computado, isso pode levar alguns minutos ou horas, dependendo do seu computador. Alternativamente, você pode usar o oracle.pickle pré-computado.
Opcionalmente, a flag --sqlite pode ser usada para gerar o oráculo em formato SQLite, o que permite carregamento preguiçoso e tempos de inicialização significativamente mais rápidos:
$ python scripts/gen_oracle.py database/3_variables_constants_7_nodes.txt oracle.db --sqlite
Depois disso, o oráculo serializado pode ser usado para simplificar expressões complexas:
from msynth import Simplifier
# initialize simplifier
simplifier = Simplifier(oracle_path)
# simplify expression
simplified = simplifier.simplify(expression)
Alternativamente, podemos simplificar expressões complexas por meio de síntese de programas e aprender expressões com o mesmo comportamento de entrada-saída:
from msynth import Synthesizer