DenuvoSoftwareSolutions/SiMBA

GitHub: DenuvoSoftwareSolutions/SiMBA

SiMBA 是一个高效的线性混合布尔算术（MBA）表达式简化工具，用于代码去混淆和逆向分析。

Stars: 184 | Forks: 19

# SiMBA SiMBA 是一个用于简化线性混合布尔算术表达式（MBA）的工具。像 [MBA-Blast](https://github.com/softsec-unh/MBA-Blast) 和 [MBA-Solver](https://github.com/softsec-unh/MBA-Solver/) 一样，它使用基于线性 MBA 完全由其在零和一集合上的值确定这一思想的完全代数方法，但利用了新的见解，即为此不需要转换到 1 位空间。它基于以下 [论文](paper/paper.pdf)：

@inproceedings{simba2022,

    author = {Reichenwallner, Benjamin and Meerwald-Stadler, Peter},

    title = {Efficient deobfuscation of linear mixed Boolean-arithmetic expressions},

    year = {2022},

    month = nov,

    address = {Los Angeles, CA, USA},

    date = {November 7 - 11, 2022},

    booktitle = {Proceedings of the CheckMATE 2022 workshop, co-located with the ACM Conference on Computer and Communication Security, CCS'22},

    pages = {19--28},

    doi = {10.1145/3560831.3564256},

    publisher = {ACM},

    howpublished = {\url{https://arxiv.org/abs/2209.06335}}

}

查找演示的 [幻灯片](slides/slides.pdf) 和 [视频录像](slides/video.mp4)。也可通过 ACM 获取。

## 内容

提供了两个主要程序（Python 3）：

- simplify.py 用于简化单个线性 MBA
- simplify_dataset.py 用于简化文件中包含的一组线性 MBA，并通过与同样包含在该文件中的相应更简单表达式进行比较来验证它们

此外，程序 check_linear_mba.py 可用于检查表达式是否表示线性 MBA。

## 用法

### 简化单个表达式

为了简化单个表达式 expr，请使用


```
python3 src/simplify.py "expr"
```


或者，可以一次简化多个表达式，例如：


```
python3 src/simplify.py "x+x" "a&a"
```


实际上，每个不是选项的命令行参数都被视为要简化的表达式。请注意，省略引号可能会导致不良行为。简化结果将打印到命令行，如下所示：


```
*** Expression x+x

*** ... simplified to 2*x

*** Expression a

*** ... simplified to a
```


默认情况下，不会执行输入表达式是否为线性 MBA 的检查。可以通过选项 **-l** 选择启用此检查：


```
python3 src/simplify.py "x*x" -l
```


由于 $x*x$ 不是线性 MBA，在这种情况下将显示以下输出：


```
*** Expression x*x

Error: Input expression may be no linear MBA: x*x
```


如果使用选项 **-z**，简化结果最终将使用 *Z3* 验证是否等于原始表达式。只要算法正常工作且输入表达式是线性 MBA，这不会影响命令行输出：


```
python3 src/simplify.py "x*x" -z
```


这将触发以下错误：


```
*** Expression x*x

Error in simplification! Simplified expression is not equivalent to original one!
```


由于 SiMBA 输出表达式中出现的常数始终是非负的，因此它们可能取决于用于常数以及变量的位数。该数字默认为 $64$，可以使用选项 **-b** 进行设置：


```
python3 src/simplify.py "-x" -b 32
```


对于位数 $b$，输出中出现的常数始终介于 $0$ 和 $2^b-1$ 之间。因此，上面的调用将意味着以下输出：


```
*** Expression -x

*** ... simplified to 4294967295*x
```


### 从文件简化和验证表达式

为了简化存储在路径为 path_to_file 的文件中的表达式，请使用


```
python3 src/simplify_dataset.py -f path_to_file
```


也就是说，必须使用选项 **-f** 指定文件。文件的每一行必须包含一个复杂表达式以及一个等效的简单表达式，用逗号分隔，例如：

[example-expressions.txt](example-expressions.txt)：


(x&y)+(x|y), x+y

(x|y)-(~x&y)-(x&~y), x&y

-(a|~b)+(~b)+(a&~b)+b, a^b

2*(s&~t)+2*(s^t)-(s|t)+2*~(s^t)-~t-~(s&t), s

对于每一行，复杂表达式和简单表达式都会被简化并最终进行比较。简化后者的原因是使验证结果独立于空格、因子或加数的顺序等。

与 simplify.py 一样，可以分别使用选项 **-l** 和 **-z** 启用线性检查以及正确简化检查，并且可以使用选项 **-b** 指定位数。如果只想在指定文件中包含的特定最大数量的表达式上运行 SiMBA，则可以通过选项 **-r** 指定该最大数量：


```
python3 src/simplify_dataset.py -f some_file.txt -r 2
```


如果 some_file.txt 包含上面列出的表达式，则只会简化其中的前两个：


```
Simplify expressions from data/some_file.txt ...

  * total count: 2

  * verified: 2

  * equal: 2

  * average duration: 0.00014788552653044462
```


在任何情况下，输出都会提供有关以下内容的信息：

- 输入中的表达式总数，
- 在简化后使用 Z3 验证为等效于相应更简单表达式的表达式数量（除非简化结果已经具有完全相同的字符串表示），
- 简化为与相应简单表达式完全相同的表达式的数量，以及
- 平均运行时间（以秒为单位）。

默认情况下，简化结果不会打印，仅显示这些统计信息。如果需要有关前者的信息，可以使用选项 **-v**：


```
python3 src/simplify_dataset.py -f some_file.txt -v
```


然后将显示以下输出：


```
Simplify expressions from data/some_file.txt ...



    *** 1 groundtruth x+y, simplified x+y => equal: True, verified: True

    *** 2 groundtruth x&y, simplified x&y => equal: True, verified: True

    *** 3 groundtruth a^b, simplified a^b => equal: True, verified: True

    *** 4 groundtruth s, simplified s => equal: True, verified: True



  * total count: 4

  * verified: 4

  * equal: 4

  * average duration: 0.00016793253598734736
```


另一个选项 **-e** 提供了使用仿射函数 $f(x) = ax+b$ 编码所有表达式输出的可能性，其中 $a,b$ 为 $1$ 和 $2^b-1$ 之间的随机整数，如果 $b$ 是位数：


```
python3 src/simplify_dataset.py -f some_file.txt -v -e
```


当然，同一函数将应用于同一行中的一对表达式。这将给出类似于以下的输出：


```
Simplify expressions from data/some_file.txt ...



    *** 1 groundtruth 10623056950310032687+5038261596809828791*x+5038261596809828791*y, simplified 10623056950310032687+5038261596809828791*x+5038261596809828791*y => equal: True, verified: True

    *** 2 groundtruth 15181401701264988765+3962868592131193124*(x&y), simplified 15181401701264988765+3962868592131193124*(x&y) => equal: True, verified: True

    *** 3 groundtruth 6812440940417974076+11894131080657788315*(a^b), simplified 6812440940417974076+11894131080657788315*(a^b) => equal: True, verified: True

    *** 4 groundtruth 4558303267887122851+10271005790757592209*s, simplified 4558303267887122851+10271005790757592209*s => equal: True, verified: True



  * total count: 4

  * verified: 4

  * equal: 4

  * average duration: 0.00019435951253399253
```


## 可复现性

为了复现论文中所述的部分实验，可以使用目录 data/ 中包含的任何数据集文件。对于以下每个函数 $e_1,\ldots, e_5$，提供了使用 $2$、$3$ 或 $4$ 个变量的 $1\,000$ 个等效线性 MBA 的数据集：

- $e_1(x,y) = x+y$
- $e_2 = 49\,374$
- $e_3(x) = 3\,735\,936\,685\, x + 49\,374$
- $e_4(x,y) = 3\,735\,936\,685\, (x\mathbin{^\wedge}y) + 49\,374$
- $e_5(x) = 3\,735\,936\,685\cdot \mathord{\sim} x$

对于 $e_1$，提供了 $5$ 到 $7$ 个变量的额外数据集。这些 MBA 是使用基于 Zhou 等人于 2007 年描述并在论文中描述的方法的算法生成的。

为了复现进一步的实验，我们分别参考 [MBA-Solver repository](https://github.com/softsec-unh/MBA-Solver/blob/main/full-dataset/pldi_dataset_linear_MBA.txt) 和 [NeuReduce repository](https://github.com/fvrmatteo/NeuReduce/tree/master/dataset/linear/test) 提供的数据集。

### 检查线性

文件 check_linear_mba.py 被简化器使用，但它也提供了自己的接口，例如：


```
python3 src/check_linear_mba.py "x+x" "x*x"
```


它检查通过命令行参数传递的所有表达式。在这种情况下，它将意味着以下输出：


```
*** Expression x+x

*** +++ valid

*** Expression x*x

*** --- not valid
```


## 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"。

## 依赖项

SMT 求解器 **Z3** 是必需的

- 在 simplify_dataset.py 中，用于验证简化表达式等效于相应的简单表达式，以及
- 在 simplify.py 中，如果使用了简化表达式的可选验证。如果未使用此选项，即使未安装 Z3 也不会引发错误。

安装 Z3：

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

## 许可证

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

## 联系方式

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

标签：CTF安全, DNS 反向解析, MBA表达式, Python, TLS抓取, 二进制分析, 云安全监控, 云安全运维, 云资产清单, 代数简化, 代码优化, 代码混淆, 去混淆, 反混淆, 可配置连接, 学术论文实现, 布尔算术混合表达式, 恶意代码分析, 无后门, 程序分析, 符号执行, 编译器优化, 表达式简化, 软件安全, 逆向工具, 逆向工程, 配置文件, 静态分析