最近看了几篇关于混合布尔算术MBA(Mixed Bitwise-Arithmetic)的论文，可以用于处理vmp万用门的混淆，所以写出来和大家分享一下。混合布尔算术运算结合了算术运算(加法、减法和乘法等)和布尔运算(与、或、非和异或)。混合布尔算术运算的混淆可以将一个简单的表达式等价地转换到难以理解和分析的复杂表达式。针对静态和动态的分析，该混淆技术可以用于隐藏某些常量或者一些运算。
MBA表达式的定义
先说明一下，本文所讨论的运算都是针对整数类型的变量。
MBA可以划分为线性MBA和多项式MBA。定义如下：
图片1.png (59.93 KB, 下载次数: 0)
下载附件
2021-11-21 12:19 上传
MBA混淆
线性MBA表达式
如果E=0成立，就可以得到一个恒等式，比如下面这个
图片2.png (1.53 KB, 下载次数: 0)
下载附件
2021-11-21 12:23 上传
那么就可以使用右边的表达式代替x+y，从而达到混淆的目的。我们可以使用z3化简一下，但是效果不尽人意。利用z3验证上面这个等式不恒等时，check输出为unsat，说明等式是成立的。
图片3.png (8.12 KB, 下载次数: 0)
下载附件
2021-11-21 12:19 上传
上述恒等式可以通过真值表来构造，在构造之前需要用到一个重要的结论。
同一个MBA表达式，n位变量的情况和1位变量同样适用
这个结论是MBA混淆的基础。因为真值表是针对1位变量的情况，可以枚举出布尔表达式所有可能的值，这就可以很方便的构造出MBA恒等式。那么根据之前这个重要结论就可以把利用真值表构造出来的MBA恒等式应用于n位的情况。证明细节可以看以下两个论文
Information Hiding in Software with Mixed Boolean-Arithmetic Transforms
MBA-Blast: Unveiling and Simplifying Mixed Boolean-Arithmetic Obfuscation
这里我以两个变量作为例子构造MBA表达式。
图片4.png (54.52 KB, 下载次数: 0)
下载附件
2021-11-21 12:19 上传
用z3验证如下
图片5.png (7.78 KB, 下载次数: 0)
下载附件
2021-11-21 12:19 上传
这个例子虽然简单，但通过上述方法可以构造出比较复杂的MBA表达式
图片6.png (42.89 KB, 下载次数: 0)
下载附件
2021-11-21 12:20 上传
b图中的z可以为任意的整数，只要在构造MBA时，z前面的系数为0即可
多项式MBA表达式
多项式MBA可以通过多项式来构造。
图片7.png (51.41 KB, 下载次数: 1)
下载附件
2021-11-21 12:20 上传
图片8.png (7.96 KB, 下载次数: 0)
下载附件
2021-11-21 12:20 上传
当P(Q(X)+E)中的X为常量时，可以达到隐藏变量的目的。不过需要注意的是表达式E里面最好包含一个常数项，因为展开之后可能会泄露出来。
图片9.png (27.63 KB, 下载次数: 0)
下载附件
2021-11-21 12:20 上传
MBA反混淆
通过前面构造MBA的过程中可以看出，真值表是构造MBA恒等式的基础，同样也可以用来化简MBA的混淆。继续以两个变量x和y为例，首先构造一个行列式不为0的真值表，如下图所示
图片10.png (13.34 KB, 下载次数: 0)
下载附件
2021-11-21 12:20 上传
因为行列式不为0，说明列向量是线性无关的，其它任意向量都可以由上面4个列向量线性表出。其它布尔表达式对应的真值看成一个列向量的话，那么它就可以由上面4个列向量线性表出。
图片11.png (78 KB, 下载次数: 0)
下载附件
2021-11-21 12:20 上传
上面那个表格的第一列为第二列布尔表达式的真值，第三列为第二列布尔表达式的MBA形式。可以看到第三列MBA表达式都可以由x,y,x∧y,-1的线性组合表示。针对一个MBA表达式，如果是隐藏的x和y的某种算术运算，可以通过上面那个表格把MBA每一项的布尔表达式替换成对应第三列的MBA表达式，最后合并同类项化简。
图片12.png (22.47 KB, 下载次数: 0)
下载附件
2021-11-21 12:20 上传
如果MBA表达式代表的是一个布尔运算，在合并同类项化简之后可以和一些常见的布尔表达式的真值进行匹配，如果真值相同，那么就是对应的布尔运算。
现在回过头来看看vmp的万用门混淆，vmp里面使用not_not_and 和not_not_or模拟了其它逻辑运算指令和一些算术运算指令。
MBA-Blast: Unveiling and Simplifying Mixed Boolean-Arithmetic Obfuscation这篇论文后面给出了一些vmp万用门混淆化简的例子
图片13.png (58.5 KB, 下载次数: 0)
下载附件
2021-11-21 12:20 上传
这里我再给出我上篇文章《利用机器学习分析vmp的思路》中反编译后遇到的一个表达式
MEMORY[0x5036EDC] = ~(~(MEMORY[0xFFFFCFB4] - 0x34C612) & 0x6963) & ~((MEMORY[0xFFFFCFB4] - 0x34C612) & 0xFFFF969C)
令E = MEMORY[0x5036EDC]
x = MEMORY[0xFFFFCFB4] - 0x34C612
y = 0xFFFF969
那么E = ~(~x & ~y) & ~(x & y)就是一个纯粹的布尔表达式, E对应的真值表为
图片14.png (11.79 KB, 下载次数: 0)
下载附件
2021-11-21 12:20 上传
可以看出E的真值和x异或y是相同的，那么根据前面那个重要结论得到E = x^y,从而得到
MEMORY[0x5036EDC] = (MEMORY[0xFFFFCFB4] - 0x34C612) ^ 0xFFFF969C
图片15.png (8.09 KB, 下载次数: 0)
下载附件
2021-11-21 12:20 上传
总结
根据前面提到的论文的描述和实验结果表明，MBA混淆确实能够有效的抵抗一些约束求解器的分析。所以在利用约束求解器分析前，有必要进行一定的化简或者去混淆。同时，MBA混淆方式也同样可以运用到不透明谓词。其实，在没有给定特定的名称之前，混合算术和位运算符的表达式已经广泛使用了。处理器中能够支持的任意位运算符或算术运算符都可以用于构造MBA表达式。比如刚刚化简的那个vmp表达式
MEMORY[0x5036EDC] = (MEMORY[0xFFFFCFB4] - 0x34C612) ^ 0xFFFF969C
可能这种类型的混合运算表达式太常见了，还不足以达到混淆的程度，所以没有引起大家的特别注意。
参考文献
Boosting SMT Solver Performance on Mixed-Bitwise-Arithmetic Expressions
Obfuscation with Mixed Boolean-Arithmetic Expressions : reconstruction, analysis and simplification tools
Information Hiding in Software with Mixed Boolean-Arithmetic Transforms
MBA-Blast: Unveiling and Simplifying Mixed Boolean-Arithmetic Obfuscation
参考文献.part2.rar
(3.1 MB, 下载次数: 36)
2021-11-21 15:37 上传
点击文件名下载附件
下载积分: 吾爱币 -1 CB
参考文献.part1.rar
(4 MB, 下载次数: 26)
2021-11-21 15:37 上传
点击文件名下载附件
下载积分: 吾爱币 -1 CB
