工具
SiMBA 线性 MBA 表达式化简工具
Denuvo 发布的研究工具，用于化简线性混合布尔-算术（MBA）表达式；这类表达式混合使用位运算和整数运算，常见于代码混淆。它与 MBA-Blast、MBA-Solver 一样采用纯代数方法，依据线性 MBA 完全由其在 0/1 输入上的取值决定这一性质：对所有 0/1 输入组合求值，再把表达式改写为基本位运算表达式的线性组合，而无需先转换到 1 位空间。所附 Python 脚本可化简单个表达式或整个数据集，可检查输入是否为线性 MBA，并可用 Z3 证明结果与原式等价。
- 目标
- 二进制
- 类别
- 原生分析工具
- 关联
- 基础工具
- 来源复核于
使用条件与局限
- 配套 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）。所审来源未确立与 REA 的关联。
关于此条目
说明已依据一手来源复核；这不代表已运行验证、经过安全审计或确认兼容。
一手来源
- README.md GitHub · DenuvoSoftwareSolutions/SiMBA · 修订 2281799
- src/simplify.py GitHub · DenuvoSoftwareSolutions/SiMBA · 修订 2281799
- src/simplify_dataset.py GitHub · DenuvoSoftwareSolutions/SiMBA · 修订 2281799
- src/check_linear_mba.py GitHub · DenuvoSoftwareSolutions/SiMBA · 修订 2281799
- data GitHub · DenuvoSoftwareSolutions/SiMBA · 修订 2281799
- paper/paper.pdf GitHub · DenuvoSoftwareSolutions/SiMBA · 修订 2281799
- LICENSE GitHub · DenuvoSoftwareSolutions/SiMBA · 修订 2281799
- https://arxiv.org/abs/2209.06335