首页
论坛
课程
招聘
[原创]线性MBA混淆的LLVM Pass实现
2022-2-21 21:53 11186

[原创]线性MBA混淆的LLVM Pass实现

2022-2-21 21:53
11186

混合布尔算术(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
基本思路:

  1. 随机选取termsNumber个布尔表达式构造真值表矩阵(参考上面的矩阵A)
  2. 令AY=0,将矩阵方程转换为线性方程组,用z3-solver求出解向量Y
  3. 解向量Y即为MBA恒等式的参数,将参数与对应的布尔表达式相乘,得到项,将每一项相加,合并同类项,得到等于0的线性MBA恒等式
  4. 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 != 0
for(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 - yx ^ 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恒等式,并保存在文件里,混淆的时候从文件取用即可。


[2022夏季班]《安卓高级研修班(网课)》月薪三万班招生中~

最后于 2022-3-2 10:56 被34r7hm4n编辑 ,原因:
收藏
点赞9
打赏
分享
最新回复 (3)
雪    币: 7704
活跃值: 活跃值 (4669)
能力值: ( LV2,RANK:10 )
在线值:
发帖
回帖
粉丝
zhczf 活跃值 2022-2-22 08:24
2
0
虽然看不懂,也来支持楼主分享这个前沿技术
雪    币: 5980
活跃值: 活跃值 (2011)
能力值: ( LV6,RANK:80 )
在线值:
发帖
回帖
粉丝
黑洛 活跃值 1 2022-3-8 19:26
3
0
插眼,已star
雪    币: 2071
活跃值: 活跃值 (3510)
能力值: ( LV2,RANK:10 )
在线值:
发帖
回帖
粉丝
lhxdiao 活跃值 2022-3-13 20:44
4
0
感谢分享
游客
登录 | 注册 方可回帖
返回