# SiMBA 线性 MBA 表达式化简工具 > Denuvo 发布的研究工具，用于化简线性混合布尔-算术（MBA）表达式；这类表达式混合使用位运算和整数运算，常见于代码混淆。它与 MBA-Blast、MBA-Solver 一样采用纯代数方法，依据线性 MBA 完全由其在 0/1 输入上的取值决定这一性质：对所有 0/1 输入组合求值，再把表达式改写为基本位运算表达式的线性组合，而无需先转换到 1 位空间。所附 Python 脚本可化简单个表达式或整个数据集，可检查输入是否为线性 MBA，并可用 Z3 证明结果与原式等价。 - 类型：工具 - 目标：二进制 - 类别：原生分析工具 - 关联：基础工具 - 来源复核于：2026-10-20 - 收录于：2026-11-02 - 原始资源： - 一手来源： - 目录页面： - 记录 JSON： - 英文版：[English](https://awesomerea.org/resources/simba-mba-simplifier/index.md) ## 使用条件与局限 - 配套 Benjamin Reichenwallner 与 Peter Meerwald-Stadler 在 CheckMATE 2022 研讨会（与 ACM CCS 2022 同期举办）发表的论文（DOI 10.1145/3560831.3564256，arXiv 2209.06335）；仓库还收录论文 PDF、幻灯片和演讲录像。所审阅的 main 提交日期为 2022-12-12，没有发布版或软件包，脚本直接在 src/ 下运行。 - 需要 Python 3；simplify_dataset.py 以及 simplify.py 的 -z 验证选项需要 Z3 的 Python 绑定。输入为表达式文本，或每行包含一个复杂表达式及其较简等价式的文件，可使用变量、常量以及 ~、一元负号、*、+、-、&、^ 和 | 运算符；工具不集成反汇编器或反编译器。输出常量取决于位宽，默认 64 位，可用 -b 设置。 - 只处理线性 MBA：可选的 -l 检查会拒绝变量相乘等非线性输入；README 提醒运算符优先级遵循 Python 规则，必要时须加括号。借助位运算表达式查找表细化结果的步骤只适用于至多三个变量；变量更多时保留通用的线性组合形式。 - 为复现论文的部分实验，data/ 提供生成的数据集：每个目标函数各有 1,000 个含 2 至 4 个变量的等价线性 MBA，x+y 另有 5 个和 6 个变量的数据集；README 还提到 7 个变量的数据集，但仓库中没有。这些数据集以 64 位为前提；simplify_dataset.py 会报告经 Z3 验证或完全一致的结果数量及平均耗时。仓库没有测试套件或 CI。 - 采用 GPL-3.0 许可，版权归 Denuvo GmbH（2022）。 ## 一手来源 1. 2. 3. 4. 5. 6. 7. 8. ## 同分区更多条目：原生二进制 - [GTIRB 二进制中间表示](https://awesomerea.org/zh/resources/gtirb/index.md) · 工具 - [Quokka 二进制导出工具](https://awesomerea.org/zh/resources/quokka-binary-exporter/index.md) · 工具 - [knife 静态逆向工程工具包](https://awesomerea.org/zh/resources/knife/index.md) · 工具 - [BARF 二进制分析与逆向工程框架](https://awesomerea.org/zh/resources/barf/index.md) · 工具 - [rabbitizer MIPS 指令解码器](https://awesomerea.org/zh/resources/rabbitizer/index.md) · 工具 - [ghidrecomp 命令行 Ghidra 批量反编译工具](https://awesomerea.org/zh/resources/ghidrecomp/index.md) · 工具 ## 关于此条目 说明已依据一手来源复核。 原创说明采用 MIT 许可；外部项目、论文与素材保留各自的权利和许可。