SiMBA 是一个用于简化线性混合布尔算术表达式（MBA）的工具。与 MBA-Blast 和 MBA-Solver 类似，它采用完全代数方法，基于线性 MBA 由其在全零和全一集合上的值完全确定的思路，但利用新的见解，即不需要转换到 1 位空间。
它基于以下论文：
@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}}
}
提供了两个主要程序（Python 3）：
simplify.py 用于简化单个线性 MBAsimplify_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 指定文件。文件的每一行必须包含一个复杂表达式以及一个等价的更简单表达式，用逗号分隔，例如：
(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$，额外提供了 $5$ 到 $7$ 个变量的数据集。这些 MBA 是使用基于 Zhou 等人 2007 年描述的方法的算法生成的，并在论文中有所描述。
请注意，这些数据集是针对 $b=64$ 位生成的。对于不同的位数，不能保证它们与 $e_i$ 的等价性。
为了重现其他实验，我们分别参考 MBA-Solver 仓库 和 NeuReduce 仓库 提供的数据集。
文件 check_linear_mba.py 被简化器使用，但它也提供自己的接口，例如：
python3 src/check_linear_mba.py "x+x" "x*x"
它检查所有通过命令行参数传递的表达式。在这种情况下，会产生以下输出：
*** Expression x+x
*** +++ valid
*** Expression x*x
*** --- not valid
变量数量理论上无限制，但运行时间随变量数量增加而增加。变量命名没有严格的限制。它们必须以字母开头，可以包含字母、数字和下划线。例如，以下变量名都是有效的：
支持以下运算符，按 Python 中的优先级顺序排列：
输入表达式中可以使用空白。例如，表达式 "x+y" 也可以写为 "x + y"。
请尊重运算符的优先级，必要时使用括号！例如，表达式 $1 + (x|y)$ 和 $1 + x|y$ 不等价，因为 $+$ 的优先级高于 $|$。注意，后者甚至不是线性 MBA。
SMT 求解器 Z3 是必需的：
安装 Z3：
sudo apt-get install python3-z3版权所有 (c) 2022 Denuvo GmbH，基于 GPLv3 发布。