-
-
[原创]线性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原理及其在代码混淆中的应用
Boolean-arithmetic algebra (BA-algebra), BA[n]是一个代数系统，其定义如下：
其中Bn表示所有n位二进制数的集合（其中n为正整数），后面的所有运算都是建立在集合Bn上的运算，上标有s运算表示有符号数的运算，否则为无符号数。
多项式MBA的形式如下，其中ai是常量，ei,j(x1,...,xt)表示由变量x1,...,xt组成的按位运算表达式：
线性MBA表达式是多项式MBA表达式的简化版，其形式如下：
举个例子，第一个式子是由四个变量组成的多项式MBA表达式，第二个式子是由两个变量组成的线性MBA表达式：
看雪貌似不太支持数学公式，所以这部分我就直接贴图了：
实际上布尔表达式可以随意选取，最后都能得到一个为0的恒等式（前提是至少有一个系数aj不为0）。
如果要对x+y进行替换，那么就在MBA恒等式两边加上x+y，得到x+y=...的恒等式，所以可以用右边复杂的MBA表达式对左边的x+y进行替换，以达到混淆的目的。
源码：LinearMBAObfuscation.cpp 以及 MBAUtils.cpp
也欢迎大家关注我的项目：Pluto-Obfuscator
基本思路：
构造MBA恒等式的基础是真值表。以两个变量的MBA表达式为例，两个变量总共有四种可能的取值（x=0,y=0;x=0,y=1;x=1,y=0;x=1,y=1），可以转换为包含四个元素的列向量，例如x & y的真值表可以转换为{0, 0, 0, 1}。
在预先设定的15个布尔表达式里随机选取termsNumber个来构造真值表矩阵。
将矩阵方程转换为线性方程组，然后用z3求解。并且解不能为0向量：
将布尔表达式相同的项合并（最多可能有15个项，对应15个布尔表达式）。并且合并之后不能所有的项都是0：
替换的原理非常简单，如果要替换的式子是x + y，那么在生成的MBA恒等式左右两边同时加上x + y即可。将存储了MBA表达式参数的terms[2]和terms[4]（对应x和y）加上1即可。其他的式子如x - y、x ^ y等也是同理：
对AES进行混淆，以下是SubBytes函数的混淆效果：
z3求解线性方程组的速度比较慢，所以如果在混淆的时候临时去生成MBA恒等式，那么当项目比较大的时候会耗费很多时间（尤其是加密相关的程序，涉及大量运算）。所以可以事先生成一些MBA恒等式，并保存在文件里，混淆的时候从文件取用即可。
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
};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
};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;
}
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;
}
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();
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];
}
[培训]内核驱动高级班，冲击BAT一流互联网大厂工作，每周日13:00-18:00直播授课
|
|
|---|---|
|
|
|
|
|
|
|
|
|
