mrphrazer/msynthФреймворк для деобфускации кода, упрощающий смешанные булево-арифметические (MBA) выражения
Автор: Tim Blazytko и Moritz Schloegel
msynth — это фреймворк для деобфускации кода, предназначенный для упрощения смешанных булево-арифметических (Mixed Boolean-Arithmetic, MBA) выражений. Имея предварительно вычисленный оракул упрощения, он обходит сложное выражение, представленное в виде абстрактного синтаксического дерева (AST), и пытается упростить поддеревья с помощью различных алгебраических и семантических методов упрощения. В качестве альтернативы он пытается упростить выражения посредством стохастического синтеза программ.
msynth построен на основе Miasm и вдохновлён следующими работами:
"QSynth: A Program Synthesis based Approach for Binary Code Deobfuscation" — Robin David, Luigi Coniglio и Mariano Ceccato (NDSS, BAR 2020),
"Syntia: Synthesizing the Semantics of Obfuscated Code" — Tim Blazytko, Moritz Contag, Cornelius Aschermann и Thorsten Holz (USENIX Security 2017) и
"Search-Based Local Blackbox Deobfuscation: Understand, Improve and Mitigate" — Grégoire Menguy, Sébastien Bardin, Richard Bonichon и Cauim de Souza de Lima (CCS 2021).
"Augmenting Search-based Program Synthesis with Local Inference Rules to Improve Black-box Deobfuscation" — Vidal Attias, Nicolas Bellec, Grégoire Menguy, Sébastien Bardin и Jean-Yves Marion (CCS 2025).
"Efficient Deobfuscation of Linear Mixed Boolean-Arithmetic Expressions" — Benjamin Reichenwallner и Peter Meerwald-Stadler (CheckMATE 2022) и
"Simplification of General Mixed Boolean-Arithmetic Expressions: GAMBA" — Benjamin Reichenwallner и Peter Meerwald-Stadler (WORMA 2023).
Его можно использовать в сочетании с движком символьного исполнения Miasm для упрощения сложных выражений в обфусцированном коде или как отдельный инструмент для экспериментов с упрощением 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}
Чтобы установить msynth, выполните следующие шаги:
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
При обновлении существующего окружения переустановите зависимости, чтобы подхватить зафиксированный коммит Miasm. Разные коммиты Miasm могут сообщать одну и ту же версию пакета, поэтому обычная установка может оставить установленным более старый коммит:
python -m pip install --force-reinstall -r requirements.txt
Чтобы сгенерировать оракул, нам нужна таблица поиска (или база данных) для упрощения, содержащая большое количество выражений. Мы использовали перечислительный поиск для предварительного вычисления выражений с разрядностью 8, 16, 32 и 64 бита в соответствии со следующими спецификациями:
до пяти переменных p0, p1, p2, p3 и p4
операторы усечения для приведения переменных (при необходимости) к 32, 16 и 8 битам,
битовые векторные операции сложения, вычитания, умножения, отрицания (унарный минус), побитовые and/or/xor/not и логический сдвиг влево,
и, для некоторых таблиц, константы 0x0, 0x1, 0x2, 0x80, 0xff, 0x800, 0xffff, 0x8000_0000, 0xffff_ffff, 0x8000_0000_0000_0000 и 0xffff_ffff_ffff_ffff.
Пример базы данных, включённой в database, содержит все 1 293 020 комбинаций, созданных с использованием трёх переменных и констант 0x0, 0x1 и 0x2 для вплоть до 7 узлов (например, ((p0 + p1) * (p2 ^ 0x2)) или ((p0 - p2) << (p1 + p2))). Более крупные предварительно вычисленные базы данных можно найти здесь (~31 ГБ в распакованном виде). Обратите внимание, что код для предварительного вычисления выражений не является частью этого репозитория. Мы планируем выпустить его в будущем.
В качестве альтернативы предварительно вычисленным таблицам поиска msynth поддерживает упрощение выражений посредством стохастического синтеза программ. Для заданного сложного арифметического выражения msynth может обучить более короткое выражение, обладающее тем же поведением «вход-выход». На данный момент это реализовано как отдельный компонент. Однако в будущем мы планируем объединить оба подхода к упрощению.
Путь синтеза также по умолчанию использует Search Modulo Inference Rules (Smir), следуя статье CCS 2025, указанной выше. Smir дополняет локальный поиск, выводя близлежащих кандидатов для трудно синтезируемых шаблонов, таких как произвольные константы, маски, константные сдвиги и вращения, аффинные выражения и ограниченные полиномиальные выражения.
Сначала сгенерируем оракул упрощения, который использует предварительно вычисленную базу данных упрощения в качестве входных данных и кластеризует содержащиеся в ней выражения в классы эквивалентности.
$ 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
В зависимости от размера предварительно вычисленной базы данных упрощения это может занять несколько минут или часов, в зависимости от вашего компьютера. В качестве альтернативы можно использовать предварительно вычисленный oracle.pickle.
Опционально можно использовать флаг --sqlite для генерации оракула в формате SQLite, что обеспечивает ленивую загрузку и значительно более быстрое время запуска:
$ python scripts/gen_oracle.py database/3_variables_constants_7_nodes.txt oracle.db --sqlite
После этого сериализованный оракул можно использовать для упрощения сложных выражений:
from msynth import Simplifier
# initialize simplifier
simplifier = Simplifier(oracle_path)
# simplify expression
simplified = simplifier.simplify(expression)