作者：Tim Blazytko 和 Moritz Schloegel
msynth 是一个代码反混淆框架，用于简化混合布尔算术（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 位，
位向量运算：加法、减法、乘法、取负（一元负号）、按位与/或/异或/非以及逻辑左移，
并且，对于某些表，还包括常量 0x0、0x1、0x2、0x80、0xff、0x800、0xffff、0x8000_0000、0xffff_ffff、0x8000_0000_0000_0000 和 0xffff_ffff_ffff_ffff。
database 中包含的示例数据库包含使用三个变量和常量 0x0、0x1 和 0x2 为最多 7 个节点创建的全部 1,293,020 种组合（例如 ((p0 + p1) * (p2 ^ 0x2)) 或 ((p0 - p2) << (p1 + p2))）。更大的预计算数据库可在此处找到（解压后约 31GB）。请注意，用于预计算表达式的代码__不__属于本仓库的一部分。我们计划在未来某个时候发布它。
作为预计算查找表的替代方案，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)
或者，我们可以通过程序合成来简化复杂表达式，并学习具有相同输入-输出行为的表达式：
from msynth import Synthesizer
# initialize synthesizer
synthesizer = Synthesizer()
# simplify via program synthesis
simplified = synthesizer.simplify(expression)
还可以将表达式简化与 Miasm 的符号执行引擎结合起来：
$ python scripts/symbolic_simplification.py samples/mba_challenge 0x1290 oracle.pickle
[snip]
before: {({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}
simplified: {RDI[0:32] + RSI[0:32] 0 32, 0x0 32 64}
[snip]
更多使用示例可在 scripts 目录中找到。
如需更多信息，请联系 Tim Blazytko（@mr_phrazer）或 Moritz Schloegel（@m_u00d8）。