denuvosoftwaresolutions/gambaSimplification of General Mixed Boolean-Arithmetic Expressions: GAMBA
GAMBA 是一款用于简化混合布尔算术表达式 (MBA) 的工具。GAMBA 是 General Advanced Mixed Boolean Arithmetic simplifier（通用高级混合布尔算术简化器）的缩写。它利用线性代数简化器 SiMBA 来迭代简化潜在非线性输入 MBA 中的线性子表达式。总体而言，其核心组成部分如下：
@inproceedings{gamba2023,
author = {Reichenwallner, Benjamin and Meerwald-Stadler, Peter},
title = {Simplification of General Mixed Boolean-Arithmetic Expressions: {GAMBA}},
address = {Delft, The Netherlands},
year = {2023},
month = jul,
publisher = {IEEE},
pages = {427--438},
doi = {10.1109/EuroSPW59978.2023.00053},
howpublished = {https://arxiv.org/abs/2305.06763},
booktitle = {Proceedings of the 2nd Workshop on Robust Malware Analysis, WORMA'23,
co-located with the 8th IEEE European Symposium on Security and Privacy}
}
提供了两个主要程序：
simplify_general.py 用于简化一般 MBAsimplify.py 用于简化线性 MBA另外，还提供了一个测试脚本，用于重现论文中所述的结果。
要简化单个表达式 expr，请使用：
python3 src/simplify_general.py "expr"
或者，可以一次简化多个表达式，例如：
python3 src/simplify_general.py "x+x" "y*y" "a&a"
实际上，每个不是选项的命令行参数都被视为要简化的表达式。请注意，省略引号可能导致意外行为。简化结果会打印到命令行，如下所示：
*** Expression x+x
*** ... simplified to 2*x
*** Expression y*y
*** ... simplified to y**2
*** Expression a
*** ... simplified to a
如果使用选项 -z，则会通过 Z3 验证简化结果在语义上是否与原始表达式等价。只要算法正常工作，这不会影响命令行输出：
python3 src/simplify_general.py "x+x" -z
如果算法输出了错误结果，则会触发以下错误：
*** Expression x+x
Error in simplification! Simplified expression is not equivalent to original one!
此外，还可以对特定比特数以内的所有可能输入进行数值验证。使用选项 -v 并指定输入的最大比特数即可启用：
python3 src/simplify_general.py "x+x" -v 3
若出现错误结果，输出可能如下所示：
*** Expression x+x
*** ... verify via evaluation ... [ ] 0%
*** ... verification failed for input [1, 0]: orig 1, output 2
GAMBA 输出表达式中出现的常数显然取决于常数和变量所使用的比特数。该数字默认为 $64$，可通过选项 -b 设置：
python3 src/simplify_general.py "-x" -b 32
默认情况下，输出中的常数会以尽可能接近零的表示形式报告。也就是说，在上面的例子中，数字 -1 将保持不变：
*** Expression -x
*** ... simplified to -x
此行为可以更改：使用选项 -m 可启用常数的模归约：
python3 src/simplify_general.py "-x" -b 32 -m
那么，对于 $b$ 位比特数，常数始终位于 $0$ 到 $2^b-1$ 之间。因此，上面的调用将产生以下输出：
*** Expression -x
*** ... simplified to 4294967295*x
文件 src/simplify.py 旨在供 src/simplify_general.py 使用，但也能够独立运行。使用命令行选项 -h 查看可用设置。
文件 experiments/tests.py 可用于重现论文中所述的实验。默认情况下，它会在 6 个数据集上运行 GAMBA：
python3 experiments/tests.py
或者，也可以使用选项 --linear 或 -l 指示其仅运行 SiMBA。在这种情况下，SiMBA 只在线性真值 MBA 上运行：
python3 experiments/tests.py --linear
可通过选项 --check (-c) 或 --z3 (-z) 分别启用数值检查或 Z3 检查。
表达式根据简化或验证成功情况进行分类：
用于 experiments/tests.py 的数据集可在目录 experiments/datasets/ 中找到。
-d 0；来自 https://github.com/fvrmatteo/NeuReduce/tree/master/dataset/linear/test/test_data.csv（已应用一些修复）-d 1；来自 https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt（1000 个线性表达式）-d 2；来自 https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt 和 https://github.com/nhpcc502/MBA-Obfuscator/tree/master/samples/ground.linear.nonpoly.txt（各 500 个表达式；非多项式表达式已修复）-d 3；来自 MBA-Flatten, dataset/dataset_syntia.txt-d 4；来自 MBA-Flatten, dataset/pldi_dataset_linear_MBA.txt、dataset/pldi_dataset_poly_MBA.txt、dataset/pldi_dataset_nonpoly_MBA.txt 的前 1000 个表达式-d 5；来自 https://github.com/werew/qsynth-artifacts/tree/master/datasets/syntia/ground_truth.json此外，目录 experiments/datasets/bonus/ 中还提供了以下额外数据集（未在出版物中涉及）：
-d 6；来自 https://github.com/RUB-SysSec/loki/tree/main/experiments/experiment_10_mba_formula/data，由 LOKI 论文生成的 25000 个 MBA，用于简单真值表达式（$x+y$、$x-y$、$x\&y$、$x|y$、$x^y$），深度最高为 5变量数量理论上是无限制的，但运行时间会随变量数量增加而增加。变量表示法没有严格限制。它们必须以字母开头，可以包含字母、数字和下划线。例如，以下变量名称都是可以的：
支持以下运算符，其优先级与 Python 中相同：
输入表达式中可以使用空格。例如，表达式 "x+y" 也可以写为 "x + y"。
请尊重运算符优先级，必要时使用括号！例如，表达式 $1 + (x|y)$ 和 $1 + x|y$ 是不等价的，因为 $+$ 的优先级高于 $|$。注意，后者甚至不是线性 MBA。
如果使用可选的简化表达式验证功能，则 simplify_general.py 和 simplify.py 需要 SMT 求解器 Z3。如果不使用此选项，即使未安装 Z3 也不会引发错误。
安装 Z3：
sudo apt-get install python3-z3由于惰性原因需要科学计算包 NumPy，但实际上对于运行并非必需。 注意：numpy.quantile 至少需要 1.15.0 版本。
安装 NumPy：
sudo apt-get install python3-numpy版权所有 (c) 2023 Denuvo GmbH，以 GPLv3 许可发布。