mrphrazer/msynth

# msynth 作者：**Tim Blazytko** 和 **Moritz Schloegel** msynth 是一个用于简化混合布尔算术（MBA）表达式的代码去混淆框架。在给定预计算简化 Oracle 的情况下，它会遍历以抽象语法树（AST）形式表示的复杂表达式，并尝试基于 Oracle 查询来简化子树。或者，它尝试通过随机程序综合来简化表达式。 msynth 构建在 [Miasm](https://github.com/cea-sec/miasm) 之上，并受到以下论文的启发： * ["QSynth: A Program Synthesis based Approach for Binary Code Deobfuscation"](https://archive.bar/pdfs/bar2020-preprint9.pdf) 作者 Robin David, Luigi Coniglio 和 Mariano Ceccato (NDSS, BAR 2020), * ["Syntia: Synthesizing the Semantics of Obfuscated Code"](https://synthesis.to/papers/usenix17-syntia.pdf) 作者 Tim Blazytko, Moritz Contag, Cornelius Aschermann 和 Thorsten Holz (USENIX Security 2017) 以及 * ["Search-Based Local Blackbox Deobfuscation: Understand, Improve and Mitigate"](https://binsec.github.io/assets/publications/papers/2021-ccs.pdf) 作者 Grégoire Menguy, Sébastien Bardin, Richard Bonichon 和 Cauim de Souza de Lima (CCS 2021). 它可以与 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} ``` ## 核心功能 * 简化现实中遇到的大多数 MBA * 可以将整个表达式简化为常量 * 利用大型预计算查找表（以提高效率） * 可以使用 SMT solver 验证简化的正确性 * 可以从输入输出行为中学习表达式 * 支持并行化 * 完全集成到 Miasm 的符号执行引擎中 ## 安装 要安装 msynth，请按照以下步骤操作： ``` git clone https://github.com/mrphrazer/msynth.git cd msynth # 可选：使用 virtual environment python -m venv msynth-env source msynth-env/bin/activate # 安装依赖 pip install -r requirements.txt # 安装 msynth pip install . # 解压 database unzip -d database -q database/3_variables_constants_7_nodes.txt.zip ``` ## 预计算简化查找表 要生成 Oracle，我们需要一个包含大量表达式的简化查找表（或数据库）。我们根据以下规范，使用枚举搜索预计算了 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](/database/) 中包含的示例数据库包含使用三个变量以及常量 0x0、0x1 和 0x2 创建的、最多 7 个节点的所有 1,293,020 种组合（例如，`((p0 + p1) * (p2 ^ 0x2))` 或 `((p0 - p2) << (p1 + p2))`）。更大的预计算数据库可以在[这里](https://share.synthesis.to/msynth/simplification_databases.7z)(~31GB 解压后)找到。请注意，用于预计算表达式的代码 __不__ 包含在此存储库中。我们计划在将来的某个时间发布它。 ## 随机程序综合 作为预计算查找表的替代方案，msynth 支持通过随机程序综合进行表达式简化。对于给定的复杂算术表达式，msynth 可以学习一个具有相同输入输出行为的更短表达式。目前，它是作为一个独立组件实现的。但是，我们计划在未来结合这两种简化方法。 ## 使用示例 首先，让我们生成一个简化 Oracle，它使用预计算的简化数据库作为输入，并将包含的表达式聚类为等价类。 ``` $ 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](/oracle.pickle)。 或者，可以使用 `--sqlite` 标志生成 SQLite 格式的 Oracle，这可以实现延迟加载并显著缩短启动时间： ``` $ python scripts/gen_oracle.py database/3_variables_constants_7_nodes.txt oracle.db --sqlite ``` 之后，序列化的 Oracle 可用于简化复杂表达式： ``` from msynth import Simplifier # 初始化 simplifier simplifier = Simplifier(oracle_path) # 简化 expression simplified = simplifier.simplify(expression) ``` 或者，我们可以通过程序综合来简化复杂表达式，并学习具有相同输入输出行为的表达式： ``` from msynth import Synthesizer # 初始化 synthesizer synthesizer = Synthesizer() # 通过 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](/scripts) 目录中找到。 ## 限制与未来工作 * 不支持部分常量的综合 * 对截断和零/符号扩展的支持有限 * 预计算表可能不完整 ## 联系方式 欲了解更多信息，请联系 Tim Blazytko ([@mr_phrazer](https://twitter.com/mr_phrazer)) 或 Moritz Schloegel ([@m_u00d8](https://twitter.com/m_u00d8))。

标签：AST抽象语法树, CTF安全工具, DNS 反向解析, MBA表达式化简, Miasm, Oracle简化, QSynth, Syntia, 二进制安全, 云安全监控, 云资产清单, 代码反混淆, 恶意代码分析, 无线安全, 混淆还原, 程序合成, 符号执行, 自动化去混淆, 逆向工具, 逆向工程, 配置文件, 随机搜索, 静态分析