-
-
[原创]线性MBA混淆的LLVM Pass实现
-
2022-2-21 21:53
-
混合布尔算术（Mixed Boolean-Arithmetic, MBA）是2007年提出的一种混淆算法，这种算法由算数运算（例如ADD、SUB、MUL）和布尔运算（例如AND、OR、NOT）的混合使用组成。针对MBA的去混淆研究在长时间内都处于起步阶段，直到去年的一篇顶会论文MBA-Blast: Unveiling and Simplifying Mixed Boolean-Arithmetic Obfuscation才提出了比较完美的去混淆方案。
本文讲解如何用LLVM Pass实现线性MBA表达式混淆。另外本文还涉及少量线性代数和数论的知识，并且本文使用的定理不会提供证明，证明请参考原论文。
原论文：Information Hiding in Software with Mixed Boolean-Arithmetic Transforms
后续文章：多项式MBA原理及其在代码混淆中的应用
0x00. 基本定义
Boolean-arithmetic algebra (BA-algebra), BA[n]是一个代数系统，其定义如下：
其中Bn表示所有n位二进制数的集合（其中n为正整数），后面的所有运算都是建立在集合Bn上的运算，上标有s运算表示有符号数的运算，否则为无符号数。
多项式MBA的形式如下，其中ai是常量，ei,j(x1,...,xt)表示由变量x1,...,xt组成的按位运算表达式：
线性MBA表达式是多项式MBA表达式的简化版，其形式如下：
举个例子，第一个式子是由四个变量组成的多项式MBA表达式，第二个式子是由两个变量组成的线性MBA表达式：
0x01. 线性MBA恒等式构造
看雪貌似不太支持数学公式，所以这部分我就直接贴图了：
实际上布尔表达式可以随意选取，最后都能得到一个为0的恒等式（前提是至少有一个系数aj不为0）。
如果要对x+y进行替换，那么就在MBA恒等式两边加上x+y，得到x+y=...的恒等式，所以可以用右边复杂的MBA表达式对左边的x+y进行替换，以达到混淆的目的。
0x02. LLVM Pass实现
源码：LinearMBAObfuscation.cpp 以及 MBAUtils.cpp
也欢迎大家关注我的项目：Pluto-Obfuscator
基本思路：
- 随机选取
termsNumber个布尔表达式构造真值表矩阵（参考上面的矩阵A） - 令AY=0，将矩阵方程转换为线性方程组，用z3-solver求出解向量Y
- 解向量Y即为MBA恒等式的参数，将参数与对应的布尔表达式相乘，得到项，将每一项相加，合并同类项，得到等于0的线性MBA恒等式
- 以
x + y的混淆为例，在恒等式左右两边同时加上x + y，得到x + y的MBA表达式替换。
1. 真值表
构造MBA恒等式的基础是真值表。以两个变量的MBA表达式为例，两个变量总共有四种可能的取值（x=0,y=0;x=0,y=1;x=1,y=0;x=1,y=1），可以转换为包含四个元素的列向量，例如x & y的真值表可以转换为{0, 0, 0, 1}。
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 | int8_t truthTable[15][4] = { {0, 0, 0, 1}, // x & y {0, 0, 1, 0}, // x & ~y {0, 0, 1, 1}, // x {0, 1, 0, 0}, // ~x & y {0, 1, 0, 1}, // y {0, 1, 1, 0}, // x ^ y {0, 1, 1, 1}, // x | y {1, 0, 0, 0}, // ~(x | y) {1, 0, 0, 1}, // ~(x ^ y) {1, 0, 1, 0}, // ~y {1, 0, 1, 1}, // x | ~y {1, 1, 0, 0}, // ~x {1, 1, 0, 1}, // ~x | y {1, 1, 1, 0}, // ~(x & y) {1, 1, 1, 1}, // -1}; |
2. 选取布尔表达式
在预先设定的15个布尔表达式里随机选取termsNumber个来构造真值表矩阵。
1 2 3 4 5 6 7 8 9 10 11 12 13 | int64_t* llvm::generateLinearMBA(int termsNumber){ int* exprSelector = new int[termsNumber]; while(true){ context c; vector<expr> params; solver s(c); for(int i = 0;i < termsNumber;i ++){ string paramName = formatv("a{0:d}", i); params.push_back(c.int_const(paramName.c_str())); } for(int i = 0;i < termsNumber;i ++){ exprSelector[i] = rand() % 15; } |
3. 方程求解
将矩阵方程转换为线性方程组，然后用z3求解。并且解不能为0向量：
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 | for(int i = 0;i < 4;i ++){ expr equ = c.int_val(0); for(int j = 0;j < termsNumber;j ++){ equ = equ + params[j] * truthTable[exprSelector[j]][i]; } s.add(equ == 0);}expr notZeroCond = c.bool_val(false);// a1 != 0 || a2 != 0 || ... || an != 0for(int i = 0;i < termsNumber;i ++){ notZeroCond = notZeroCond || (params[i] != 0);}s.add(notZeroCond);if(s.check() != sat){ continue;}model m = s.get_model(); |
4. 合并同类项
将布尔表达式相同的项合并（最多可能有15个项，对应15个布尔表达式）。并且合并之后不能所有的项都是0：
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 | int64_t *terms = new int64_t[15]; fill_n(terms, 15, 0); for(int i = 0;i < termsNumber;i ++){ terms[exprSelector[i]] += m.eval(params[i]).as_int64(); } // reject if all params are 0 bool all_zero = true; for(int i = 0;i < 15;i ++){ if(terms[i] != 0) all_zero = false; } if(all_zero){ delete[] terms; continue; } return terms; }} |
5. 替换
替换的原理非常简单，如果要替换的式子是x + y，那么在生成的MBA恒等式左右两边同时加上x + y即可。将存储了MBA表达式参数的terms[2]和terms[4]（对应x和y）加上1即可。其他的式子如x - y、x ^ y等也是同理：
1 2 3 4 5 6 7 | void LinearMBAObfuscation::substituteAdd(BinaryOperator *BI){ int64_t *terms = generateLinearMBA(TermsNumber); terms[2] += 1; terms[4] += 1; Value *mbaExpr = insertLinearMBA(terms, BI); BI->replaceAllUsesWith(mbaExpr);} |
0x03. 混淆效果
对AES进行混淆，以下是SubBytes函数的混淆效果：
0x04. 改进思路
z3求解线性方程组的速度比较慢，所以如果在混淆的时候临时去生成MBA恒等式，那么当项目比较大的时候会耗费很多时间（尤其是加密相关的程序，涉及大量运算）。所以可以事先生成一些MBA恒等式，并保存在文件里，混淆的时候从文件取用即可。
[培训]二进制漏洞攻防（第3期）；满10人开班；模糊测试与工具使用二次开发；网络协议漏洞挖掘；Linux内核漏洞挖掘与利用；AOSP漏洞挖掘与利用；代码审计。
|
|
|---|---|
|
|
|
|
|
|
|
|
|
