DenuvoSoftwareSolutions/GAMBA

# GAMBA GAMBA 是一个用于简化混合布尔算术表达式 (MBA) 的工具。 GAMBA 是 General Advanced Mixed Boolean Arithmetic simplifier 的缩写。 它使用线性代数简化器 [SiMBA](https://github.com/DenuvoSoftwareSolutions/SiMBA) 来迭代 简化潜在非线性输入 MBA 的线性子表达式。总体而言，其核心组成部分如下： - 使用抽象语法树 (AST) - 通过应用（简单和更复杂的）变换来隔离线性子表达式 - 重构以增加构建可简化的线性子表达式的机会 - 使用 SiMBA 简化线性子表达式 - 替换逻辑，用于在按位运算中暂时消除非平凡常数和算术运算 GAMBA 基于以下[论文](paper/paper.pdf)，亦请参阅用于演示的[幻灯片](slides/slides.pdf)：

@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 用于简化通用 MBA
- simplify.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 的检查。

表达式根据简化或验证的成功与否进行分类：

- *ok*: 简化为与相应基本事实完全相同结果的表达式
- *okz*: 可以使用算法验证其与基本事实等价的表达式（通过将表达式减去基本事实表达式简化为 0）
- *z3*: 可以使用 Z3 验证其与基本事实等价的表达式
- *to*: 算法超时的表达式
- *ng*: 简化和验证未成功的表达式
- *nc*: 如果使用 SiMBA，则未运行算法的表达式，因为基本事实不是线性的
- *err*: 发生错误的表达式

### 数据集

用于 experiments/tests.py 的数据集可以在目录 experiments/datasets/ 中找到。

- neureduce.txt: 使用选项 -d 0；来自 https://github.com/fvrmatteo/NeuReduce/tree/master/dataset/linear/test/test_data.csv（经过一些修复）
- mba_obf_linear.txt: 使用选项 -d 1；来自 https://github.com/nhpcc502/MBA-Obfuscator/tree/main/samples/ground.linear.poly.txt（1000 个线性表达式）
- mba_obf_nonlinear.txt: 使用选项 -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 个表达式；对非多项式表达式进行了一些修复）
- syntia.txt: 使用选项 -d 3；来自 MBA-Flatten，dataset/dataset_syntia.txt
- mba_flatten.txt: 使用选项 -d 4；来自 MBA-Flatten，dataset/pldi_dataset_linear_MBA.txt，dataset/pldi_dataset_poly_MBA.txt，dataset/pldi_dataset_nonpoly_MBA.txt 的前 1000 个表达式
- qsynth_ea.txt: 使用选项 -d 5；来自 https://github.com/werew/qsynth-artifacts/tree/master/datasets/syntia/ground_truth.json

此外，目录 experiments/datasets/bonus/ 中提供了以下额外数据集（出版物中未涵盖）：

- loki_tiny.txt: 使用选项 -d 6；来自 https://github.com/RUB-SysSec/loki/tree/main/experiments/experiment_10_mba_formula/data，由 [LOKI](https://github.com/RUB-SysSec/loki) 论文生成的 25000 个 MBA，用于简单的基本事实表达式（$x+y$, $x-y$, $x\\&y$, $x|y$, $x^y$），深度最大为 5

## MBA 格式

理论上变量数量是无限制的，但运行时间当然会随着变量数量增加而增加。对变量的符号没有严格的限制。它们必须以字母开头，并且可以包含字母、数字和下划线。例如，以下变量名都是可以的：

- $a$, $b$, $c$, ..., $x$, $y$, $z$, ...
- $v0$, $v1$, $v2$, ...
- $v\_0$, $v\_1$, $v\_2$, ...
- $X0$, $X1$, $X2$, ...
- $var0$, $var1$, $var2$, ...
- $var1a$, $var1b$, $var1c$, ...
- ...

支持以下运算符，按其在 Python 中的优先级排序：

- $**$: 幂运算
- $\mathord{\sim}$, $-$: 按位取反和一元减号
- $*$: 乘积
- $+$, $-$: 加法和减法
- <<: 左移
- &: 与运算
- $\mathbin{^\wedge}$: 异或
- $|$: 或运算

输入表达式中可以使用空格。例如，表达式 "x+y" 也可以写成 "x + y"。

## 依赖项

### Z3

如果使用简化表达式的可选验证功能，simplify_general.py 和 simplify.py 需要 SMT Solver **Z3**。如果不使用此选项，即使未安装 Z3 也不会抛出错误。

安装 Z3：

- 来自 Github 仓库：https://github.com/Z3Prover/z3
- 在 Debian 上：sudo apt-get install python3-z3

### NumPy

由于惰性原因需要科学计算包 **NumPy**，但对于运行来说并不是真正必不可少的。

注意：numpy.quantile 至少需要 1.15.0 版本

安装 NumPy：

- 来自 Github 仓库：https://github.com/numpy/numpy.git
- 在 Debian 上：sudo apt-get install python3-numpy

## 许可证

版权所有 (c) 2023 Denuvo GmbH，根据 [GPLv3](LICENSE) 发布。

## 联系方式

- Benjamin Reichenwallner: benjamin(dot)reichenwallner(at)denuvo(dot)com
- Peter Meerwald-Stadler: peter(dot)meerwald(at)denuvo(dot)com

标签：MBA表达式化简, odt, Python, SiMBA, TLS抓取, WORMA, 云安全监控, 云资产清单, 代码保护, 代码混淆, 反混淆, 可配置连接, 布尔算术混合, 恶意代码分析, 抽象语法树, 无后门, 程序分析, 符号执行, 线性代数, 网络安全, 表达式简化, 软件安全, 逆向工具, 逆向工程, 配置文件, 隐私保护, 静态分析