目录

DIVALARM - 实验要求
DIVALARM - 环境配置
DIVALARM - 基础运行
DIVALARM - LLVM基本指令结构
DIVALARM - 可达定义与污点分析
DIVALARM - 代码实现
DIVALARM - 问题

实验要求

基于LLVM和Z3，在基本的代码框架下，实现一个基于数据流分析的简单C程序和除0错漏洞分析器。

环境配置

1. 安装llvm
2. 下载z3 配置系统环境

版本号

软件	版本
llvm	8.0.1
z3	4.7.1

开发软件

Clion

基础运行

1. 导入动态库搜索路径
2. 如果在build下添加libz3.dylib文件(mac下，linux下为.so，windows下为.dll)
3. 添加动态库搜索路径

export DYLD_LIBRARY_PATH=../build

4. 运行

cd test
clang -emit-llvm -S -fno-discard-value-names -c xxx.c 
../build/constraint xxx.ll

LLVM基本指令结构

1. Alloca

%x = alloca i32, align 4

为变量分配空间
2. Store

// store Ins : store [volatile] <ty> <value>, <ty>* <pointer>
store i32 0, i32* %retval, align 4
store i32 %1, i32* %y, align 4

向变量中存储值, 第一个变量是value,第二个是pointer
3. Call

%call = call i32 (…) @tainted_input()

函数调用
4. Load

// loadIns: load [volatile] <ty>, <ty>* <pointer>
%1 = load i32, i32* %x, align 4

将pointer中的值复制到变量中，例子是将%x的值赋值到%1.

5. BinaryOperator

%5 = add i32 %4, 2

在我们的例子中，它指向一个代表数字2的Constant对象和另一个对应于寄存器%4的Instruction，（由于LLVM IR采用静态单一赋值形式，所以寄存器和Instruction其实是一个整体。寄存器号码是文本表示的产物。

6. ret

ret i32 %4

返回变量 %4的值

7. branch

• 有条件

br i1 %cmp, label %if.then, label %if.else

根据%cmp判断跳转，如果是真则跳转到标签%if.then

• 无条件

br label %if.end

直接跳转到%if.end
8. Cmp

%cmp = icmp sgt i32 %0, 2

比较指令
9. SExt

%idxprom = sext i32 %3 to i64

符号拓展
10. Getelementptr - inbounds

%arrayinit.begin = getelementptr inbounds [1 x [6 x i32]], [1 x [6 x i32]]* %a, i64 0, i64 0

• 为了得到复合数据结构子元素的地址。
• 仅仅执行地址计算，不访问内存。
• 还可用于计算地址的向量。
• 第一个参数始终是用作计算基础的类型。
• 第二个参数始终是指针或指针向量，并且是从中开始的基址。

可达定义与污点分析

关系定义

可达定义

• Def(X,Y): 变量X在指令Y处定义
• Use(X,Y): 变量X在指令Y处被使用
• Next(X,Y): 指令Y是指令X的后继
• Gen(Y,X): 定义X通过指令Y生成

污点分析

• Def(X,Y): 变量X在指令Y处定义
• Use(X,Y): 变量X在指令Y处被使用
• In(X,Y): 数据流X可以到达Y
• Taint(X): 指令X处存在一个污染函数
• Sanitizer(X): 指令X处存在一个保护函数(不被污染)
• Div(X,Y): 指令Y处存在一个除法指令，除数是X

规则定义

可达定义

• KILL(X,Z) :- Def(X,Y) && Def(X,Z)
• Out(X,Y) :- Gen(Y,X)
• Out(X,Y) :- In(X,Y) && !KILL(X,Y)
• In(X,Y) :- Out(X,Z) && Next(Z,Y)

污点分析

• Edge(Y,Z) :- Def(X,Y) && Use(X,Z) && In(X,Z)
• Path(X,Y) :- Edge(X,Y) && Taint(X)
• Path(X,Z) :- Path(X,Y) && Edge(Y,Z) && !Sanitizer(Y)
• Alarm(Z) :- Path(Y,Z) && Div(X,Z)

代码框架分析

文件分析

1. include文件夹

• Utils.h
  工具函数的头文件
• Extractor.h
  定义了Extractor class。 内含Z3不动点，规则关系提取方法，不动点求解方法。

2. src文件夹

• Constraint.cpp
  主函数所在文件。代码主要流程如下：
  定义规则关系提取器
  初始化规则和关系
  z3不动点求解器初始化
  添加fact
  运用Z3求解器进行求解
  (我们主要实现初始化规则和关系 以及 添加fact)
• Uitils.cpp
  一些方法的实现：
  将llvm指令类转化为字符串
  获取llvm指令的前继指令
  判断指令是否有污点函数
  判断指令是否有保护函数
• Extractor.cpp
  该文件是初始化规则和关系以及fact的实现处

执行流程分析

通过 clang llvm工具将.c文件生成为 .ll的llvm中间代码。
constraint 首先读取 .ll文件提取规则和关系。
其次开始根据llvm代码添加事实
利用Z3不动点进行求解。
如果Alarm存在满足的条件则会报除0错。

代码实现

规则添加

根据可达定义和污点分析的规则添加如下规则：

z3::expr X = C.bv_const(“X”, 32);
z3::expr Y = C.bv_const(“Y”, 32);
z3::expr Z = C.bv_const(“Z”, 32);z3::expr r1 = z3::forall(X, Y, Z,z3::implies(Def(X, Y) && Def(X, Z), Kill(X, Z)));
z3::expr r2 = z3::forall(X, Y,z3::implies(Gen(Y, X), Out(X, Y)));
z3::expr r3 = z3::forall(X, Y,z3::implies(In(X, Y) && !Kill(X, Y), Out(X, Y)));
z3::expr r4 = z3::forall(X, Y, Z,z3::implies(Out(X, Z) && Next(Z, Y), In(X, Y)));z3::expr t1 = z3::forall(X, Y, Z,z3::implies(Def(X, Y) && Use(X, Z) && In(X, Z), Edge(Y, Z)));
z3::expr t2 = z3::forall(X, Y,z3::implies(Edge(X, Y) && Taint(X), Path(X, Y)));
z3::expr t3 = z3::forall(X, Y, Z,z3::implies(Path(X, Y) && Edge(Y, Z) && !Sanitizer(Y), Path(X, Z)));
z3::expr t4 = z3::forall(X, Y, Z,z3::implies(Path(Y, Z) && Div(X, Z), Alarm(Z)));Solver->add_rule(r1, C.str_symbol(“KILL”));
Solver->add_rule(r2, C.str_symbol(“OUT_1”));
Solver->add_rule(r3, C.str_symbol("OUT_2"));
Solver->add_rule(r4, C.str_symbol(“IN”));
Solver->add_rule(t1, C.str_symbol("EDGE”));
Solver->add_rule(t2, C.str_symbol("PATH_1"));
Solver->add_rule(t3, C.str_symbol("PATH_2"));
Solver->add_rule(t4, C.str_symbol(“ALARM”));

事实添加

针对不同指令添加相应的事实。在这里只大概列出几条指令事实添加的范例：

// loadIns: load [volatile] <ty>, <ty>* <pointer>
if (LoadInst *LI = dyn_cast<LoadInst>(I)) {//std::cout << toString(LI->getPointerOperand()) <<“\n”;//std::cout << toString((Value *)&*I) << “\n”;addDef(InstMap, LI, LI);addUse(InstMap, LI->getPointerOperand(), LI);addGen(InstMap, LI, LI);
}// call Ins
if (CallInst *CI = dyn_cast<CallInst>(I)) {if (isTaintedInput(CI)) {addTaint(InstMap, CI);}if (isSanitizer(CI)) {addSanitizer(InstMap, CI);}if (CI->getCalledFunction()->getName().equals(“not_sanitizer”)) {addTaint(InstMap, CI);}if (CI->getCalledFunction()->getName().equals("untainted_input")) {addSanitizer(InstMap, CI);}addGen(InstMap, CI, CI);addDef(InstMap, CI, CI);
}

数组除0错

代码同时对数组中的元素支持除0错判断：
比如如下代码：

int x = tainted_input();
int z = 5;
int a[6] ={{1,1,4,1,x,1}};
//int k = sanitizer(x);
int y;
for(int i=1;i<3;i++){y = z/a[i];
}

数组中存在污点元素，虽然循环中不会到达污点元素，但是只要使用到了数组都会报除0错。

实现思路：
数组元素赋值时：

%arrayinit.element2 = getelementptr inbounds i32, i32* %arrayinit.element, i64 1
store i32 4, i32* %arrayinit.element2, align 4

追溯到数组的源头（整个数组的基地址）：

while (GetElementPtrInst *PreIns = dyn_cast<GetElementPtrInst>(To)) {To = PreIns->getPointerOperand();
}

找到数组定义：

%a = alloca [1 x [6 x i32]], align 16

对数组添加规则:

addGen(InstMap, SI, To);
addDef(InstMap, To, SI);

如果在除数处使用到数组:

%arrayidx6 = getelementptr inbounds [6 x i32], [6 x i32]* %arrayidx, i64 0, i64 %idxprom
%4 = load i32, i32* %arrayidx6, align 4
%div = sdiv i32 %2, %4

会将整个污点的数据流传递至除数从而报除0错。
这种思路不能精确到数组具体元素报除0错，只能检测当数组元素中存在0元素时，存在某处用了数组元素当除数是，才会报错。

结果分析

在给定的代码框架中，其中test有部分测试，Alarm显示全部正常。同时加入自己写的数组和指针的测试。测试结果如下：

simple0/1

//simple0.c
int main() {int x = tainted_input();int y = x;int z = 4 / y; // alarmreturn 0;
}

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-O5Oxj2DS-1596422466103)(%E6%88%AA%E5%B1%8F2020-06-18%20%E4%B8%8B%E5%8D%887.14.07.png)]

//simple1.c
int main(int argc, char **argv) {int x = tainted_input();int y = sanitizer(x);int z = 4 / y; // safey = not_sanitizer(x);z = 4 / y; // alarmreturn 0;
}

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-BMjbuFBS-1596422466105)(%E6%88%AA%E5%B1%8F2020-06-18%20%E4%B8%8B%E5%8D%887.15.12.png)]

loop0/1

//loop0.c
int main(int argc, char **argv) {int x;int y;x = 0;while (argc > 1) {x = tainted_input();y = x;argc--;}int z = 4 / y; // alarm
}

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-EOKxeQlD-1596422466106)(%E6%88%AA%E5%B1%8F2020-06-18%20%E4%B8%8B%E5%8D%887.33.07.png)]

//loop1.c
int main(int argc, char **argv) {int x;int y = tainted_input();x = 0;while (x > 0) {y = sanitizer(y);}int z = 4 / y; // alarm
}

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-fu1P4mYV-1596422466107)(%E6%88%AA%E5%B1%8F2020-06-18%20%E4%B8%8B%E5%8D%887.34.45.png)]

branch0/1

//branch0.c
int main(int argc, char **argv) {int x;int y;if (argc > 2) {x = 0;y = x;} else {x = tainted_input();y = x;}int z = 4 / y; // alarm
}

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-TqUgVQWa-1596422466109)(%E6%88%AA%E5%B1%8F2020-06-18%20%E4%B8%8B%E5%8D%887.35.48.png)]

//branch1.c
int main(int argc, char **argv) {int x = tainted_input();int y;if (argc > 2) {x = 0;y = sanitizer(x);} else {y = not_sanitizer(x);}int z = 4 / y; // alarm
}

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-vRgjgmJl-1596422466110)(%E6%88%AA%E5%B1%8F2020-06-18%20%E4%B8%8B%E5%8D%887.36.32.png)]

//branch2.c
int main(int argc, char **argv) {int x = tainted_input();int y;if (1) {y = 0;} else {y = 100;}int z = 4 / y; // alarm
}

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-XG9b21yH-1596422466111)(%E6%88%AA%E5%B1%8F2020-06-18%20%E4%B8%8B%E5%8D%887.37.55.png)]

array

//array.c
int main(int argc, char **argv) {int x = tainted_input();int z = 5;int a[1][6] ={{1,1,4,1,x,1}};//int k = sanitizer(x);int y;for(int i=1;i<3;i++){y = z/a[0][i];}
}

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-DVVQY8IV-1596422466112)(%E6%88%AA%E5%B1%8F2020-06-18%20%E4%B8%8B%E5%8D%887.39.12.png)]

//array1.c
int main(int argc, char **argv) {int x = tainted_input();int z = 5;int a[3] ={1,x,10000};//int k = sanitizer(x);int y;for(int i=0;i<3;i++){y = z/a[i];}
}

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-s5822VXP-1596422466113)(%E6%88%AA%E5%B1%8F2020-06-18%20%E4%B8%8B%E5%8D%888.11.06.png)]

//array2.c
int main(int argc, char **argv) {int x = tainted_input();int z = 5;int a[3];a[0] =1;a[1]=2;a[2]=0;//int k = sanitizer(x);int y;for(int i=0;i<3;i++){y = z/a[i];}
}

[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-qUn7GHOz-1596422466114)(%E6%88%AA%E5%B1%8F2020-06-18%20%E4%B8%8B%E5%8D%888.32.32.png)]

问题

在进行数组测试时候,如果数组已经复制好初值类似于以下代码

int a[3]={1,1,0};

此时在llvm-ir中，其代码如下：

%a = alloca [3 x i32], align 4
……
%0 = bitcast [3 x i32]* %a to i8*
call void @llvm.memcpy.p0i8.p0i8.i64(i8* align 4 %0, i8* align 4 bitcast ([3 x i32]* @__const.main.a to i8*), i64 12, i1 false)

因此无法检测a中的初值0。

而如果代码类似于以下:

int a[3];
a[0] = 1;
a[2] = 1;
a[3] = 0;

在llvm-IR中代码如下：

%a = alloca [3 x i32], align 4
……
%arrayidx = getelementptr inbounds [3 x i32], [3 x i32]* %a, i64 0, i64 0
store i32 1, i32* %arrayidx, align 4
%arrayidx1 = getelementptr inbounds [3 x i32], [3 x i32]* %a, i64 0, i64 1
store i32 2, i32* %arrayidx1, align 4
%arrayidx2 = getelementptr inbounds [3 x i32], [3 x i32]* %a, i64 0, i64 2
store i32 0, i32* %arrayidx2, align 4

因此可以通过store指令来检测初值。