混合布尔算术运算的混淆及反混淆

白云点缀的藍 · 发表于 2021-11-21 12:44

本帖最后由 A-new 于 2021-11-21 15:38 编辑

前言

最近看了几篇关于混合布尔算术MBA(Mixed Bitwise-Arithmetic)的论文，可以用于处理vmp万用门的混淆，所以写出来和大家分享一下。混合布尔算术运算结合了算术运算(加法、减法和乘法等)和布尔运算(与、或、非和异或)。混合布尔算术运算的混淆可以将一个简单的表达式等价地转换到难以理解和分析的复杂表达式。针对静态和动态的分析，该混淆技术可以用于隐藏某些常量或者一些运算。

MBA表达式的定义

先说明一下，本文所讨论的运算都是针对整数类型的变量。
MBA可以划分为线性MBA和多项式MBA。定义如下：
图片1.png

MBA混淆

线性MBA表达式

如果E=0成立，就可以得到一个恒等式，比如下面这个
图片2.png
那么就可以使用右边的表达式代替x+y，从而达到混淆的目的。我们可以使用z3化简一下，但是效果不尽人意。利用z3验证上面这个等式不恒等时，check输出为unsat，说明等式是成立的。
图片3.png
上述恒等式可以通过真值表来构造，在构造之前需要用到一个重要的结论。
同一个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
用z3验证如下
图片5.png
这个例子虽然简单，但通过上述方法可以构造出比较复杂的MBA表达式
图片6.png
b图中的z可以为任意的整数，只要在构造MBA时，z前面的系数为0即可

多项式MBA表达式

多项式MBA可以通过多项式来构造。
图片7.png
图片8.png
当P(Q(X)+E)中的X为常量时，可以达到隐藏变量的目的。不过需要注意的是表达式E里面最好包含一个常数项，因为展开之后可能会泄露出来。
图片9.png

MBA反混淆

通过前面构造MBA的过程中可以看出，真值表是构造MBA恒等式的基础，同样也可以用来化简MBA的混淆。继续以两个变量x和y为例，首先构造一个行列式不为0的真值表，如下图所示
图片10.png
因为行列式不为0，说明列向量是线性无关的，其它任意向量都可以由上面4个列向量线性表出。其它布尔表达式对应的真值看成一个列向量的话，那么它就可以由上面4个列向量线性表出。
图片11.png
上面那个表格的第一列为第二列布尔表达式的真值，第三列为第二列布尔表达式的MBA形式。可以看到第三列MBA表达式都可以由x,y,x∧y,-1的线性组合表示。针对一个MBA表达式，如果是隐藏的x和y的某种算术运算，可以通过上面那个表格把MBA每一项的布尔表达式替换成对应第三列的MBA表达式，最后合并同类项化简。
图片12.png
如果MBA表达式代表的是一个布尔运算，在合并同类项化简之后可以和一些常见的布尔表达式的真值进行匹配，如果真值相同，那么就是对应的布尔运算。
现在回过头来看看vmp的万用门混淆，vmp里面使用not_not_and 和not_not_or模拟了其它逻辑运算指令和一些算术运算指令。
MBA-Blast: Unveiling and Simplifying Mixed Boolean-Arithmetic Obfuscation这篇论文后面给出了一些vmp万用门混淆化简的例子
图片13.png
这里我再给出我上篇文章《利用机器学习分析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
可以看出E的真值和x异或y是相同的，那么根据前面那个重要结论得到E = x^y,从而得到

MEMORY[0x5036EDC] = (MEMORY[0xFFFFCFB4] - 0x34C612) ^ 0xFFFF969C

图片15.png

总结

根据前面提到的论文的描述和实验结果表明，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)

参考文献.part1.rar (4 MB, 下载次数: 26)

小远zi · 发表于 2021-11-22 12:51

本帖最后由小远zi 于 2021-11-22 12:53 编辑

根据作者白云点缀的藍文章中的思路写了一个简单的实现，https://github.com/llxiaoyuan/MBA-Gen

白云点缀的藍 · 发表于 2021-11-22 18:10

xtdong 发表于 2021-11-22 17:45
感谢楼主分享，问楼主一个问题哈，布尔电路和算术电路的规模可以理解为电路门的个数，但是他们的的深度应该 ...

我不是很懂电路，算术运算和布尔运算都是运算规则，这个和电路怎么设计关系不大，只要实现了这些规则就好

codol · 发表于 2021-11-21 17:23

学习了，谢谢楼主

wasm2023 · 发表于 2021-11-21 19:15

楼主强大，膜拜

七剑 · 发表于 2021-11-22 08:12

虽然看不懂，但还是非常佩服楼主。

jackss · 发表于 2021-11-22 09:47

完全看不懂，这些在那里学习的？

JPK · 发表于 2021-11-22 10:25

受教了，vmp真心让人很头痛

小远zi · 发表于 2021-11-22 11:12

本帖最后由小远zi 于 2021-11-22 13:31 编辑

https://www.youtube.com/watch?v=CzjgiVU5bII&t=148s

根据作者白云点缀的藍文章中的思路写了一个简单的实现，https://github.com/llxiaoyuan/MBA-Gen

tntliming · 发表于 2021-11-22 11:27

完全看不懂系列

怜渠客 · 发表于 2021-11-22 11:31

仔细的学习一下

weenie1128 · 发表于 2021-11-22 11:38