数据流分析是软件分析中静态分析中比较重要的一部分，结合符号执行、污点分析、fuzzing技术可以发挥巨大的效用。本文从原理到实现讲解数据流分析的具体实现。

本文的例子来自https://github.com/petablox/cis573vm,其中还有许多关于软件分析的demo，大家有兴趣的可以去玩一下，对于理解相关技术机理有很大的帮助。

我实验过程中采用的LLVM版本是10.0.0，z3版本是4.8.11-64bit。

实验过程的原理是基本的可达定义(reaching defenition)，b站上的南京大学软件分析原理教学视频有相关内容。

我浅显的理解（纯小白，大佬勿喷）是数据流分析就是先将二进制文件处理成3AC code,然后我们根据自定义规则处理3ac code，生成约束表达式，循环迭代达到不动点，然后用z3求解器求解最终得到结果。

首先要知道我们需要处理的基本的3ac code有哪几种

实验框架中定义了Def、Use关系，针对Reaching Definition Analysis定义了Kill、Gen、Next、In、Out关系，针对Taint Analysis定义了Taint、Edge、Path、Sanitizer、Div、Alarm关系，其中每个关系的具体含义如下,接下来，需要对这些关系定义相应的规则，并将其添加进Z3求解器中求解。

规则定义主要分为两部分，第一部分为Reaching Definition Analysis，第二部分为Taint Analysis。

为Kill定义如下rule，如果变量X在指令Y处被定义，而后又在指令Z处被定义，那么认为定义Y被指令Z Kill，形式化表示如下：

Kill(Y, Z) :- Def(X, Y) & Def(X, Z)

为Out定义如下两条rules，第一条为如果定义Y被指令X生成，那么认为定义Y可以到达指令X后；第二条为如果定义Y可以到达X之前，并且定义Y没有被指令X Kill，那么认为定义Y可以到达指令X之后，形式化表示如下：

Out(X, Y) :- Gen(X, Y)

Out(X, Y) :- In(X, Y) & !Kill(Y,X)

为In定义如下rule，如果定义Y可以到达指令Z之后，并且指令Z的下一条指令为X，那么认为定义Y可以到达指令X之前，形式化表示如下：

In(X, Y) :- Out(Z,Y) & Next(Z, X)

为Edge定义如下rule，如果变量X在指令Y处被定义，并且变量X在指令Z处被使用，并且定义Y可以到达指令Z之前，那么认为存在一个从指令Y到Z的直接的数据流，形式化表示如下：

Edge(Y, Z) :- Def(X, Y) & Use(X, Z) & In(Z,Y)

为Path定义如下两条rules，第一条为如果指令I和指令J之间存在直接的数据流，并且在指令I位置处读取了受污染的输入，那么认为指令I和指令J之间传递受污染的数据流；第二条为如果指令I和指令J之间传递受污染的数据流，并且指令J和指令K之间存在直接的数据流，并且在指令J处没有对数据流进行清洗，那么认为指令I和指令K之间传递受污染的数据流，形式化表示如下：

Path(I, J) :- Edge(I,J) & Taint(I)

Path(I, K) :- Path(I,J) & Edge(J,K) & !Sanitizer(J)

为Alarm定义如下rule，如果在指令I和指令Y之间传递受污染的数据流，并且在指令Y处使用变量K作为除数，那么认为指令Y处存在潜在的可利用的除零错误，形式化表示如下：

Alarm( Y ) :- Path(I, Y) & Div(K,Y)

定义rule以及将rule添加进Z3求解器代码实现如下：

首先将simple0.c转换为llvm 3AC code如下：

可以看到几个主要的指令为store、load、call、div指令，那么先对这几个指令提取fact。

store指令格式为store [volatile] <ty> <value>, <ty>* <pointer>，包含Value Operand、Point Operand，利用StoreInst类，根据定义添加Def、Use、Gen关系，具体如下：

Load指令格式为loadIns: load [volatile] <ty>, <ty>* <pointer>，利用LoadInst类，同样根据定义添加Def、Use、Gen关系，具体如下：

对于call指令，根据函数名称，对于是否行taint函数、Sanitizer函数进行判断，利用CallInst类，根据定义添加Gen、Def关系，实现如下：

对于sdiv指令，由于没有专门的类处理sdiv指令，所以利用Instruction类中的getOpcodeName()函数根据指令名称进行判断，根据定义添加div、use关系，具体实现如下：

并且我们需要记录下每次处理指令，这样方便添加Next关系，具体实现如下：

至此我们初步完成了fact的提取，对测试用例进行测试，效果如下：

上述实现对于loop1.ll、branch2.ll的测试并未通过，branch2.ll代码如下：

经过分析，明确问题所在，具体为如果变量值赋值为常数0时，之前并没有对此添加taint关系，所以更改store指令提取fact如下：

查看Loop1.ll，找出loop1.ll代码未通过测试原因，loop1.ll代码如下：

经过分析，是因为没有对br跳转指令进行处理，进而导致程序分析默认在loop1.ll文件内顺序进行，从而导致错误发生，因此对于br指令进行处理，首先根据当前br指令的后继基本块数目进行遍历操作，将当前br指令每一个后继基本块的第一条指令与当前br指令添加Next关系，利用BranchInst类进行实现，具体如下：

并且需要对最开始的添加Next关系操作进行改动，如果当前指令的上一个指令为br跳转指令，由于我们已经在br指令处为其添加Next关系，所以不需要再次添加关系，具体如下：

然后再次对测试集进行测试，可以看到成功通过了全部测试集，效果如下：

数组测试用例如下

可以看到对数组进行处理时指令为getelementptr，利用对应的GetElementPtrInst类进行处理，我的实现思路是当数组中存在任何一个变量有tainted风险，并且div操作时用到了数组中的任何一个变量时，就发出警报，但我们并不能确定是否是数组中tianted元素作为除数，确保了soundness，允许错报，不允许漏报。

首先是对于store指令进行修改，要分两种情况处理，当处理指令不涉及数组元素时，与之前操作相同；但如果store指令用到数组元素时，那么就利用getPointerOperand()回溯到数组的初始化指令，比如%a = alloca [3 x i32], align 4,然后针对数组初始化指令进行相应的Gen、Def、Use关系添加。并且由于是对数组的初始化指令进行操作，所以为了确保soundness（允许误报、不允许漏报），一旦数组的初始化指令在store中被标记为tainted之后，后续store操作中不再对数组初始化指令添加Use、Gen、Def指令，防止将数组中的tianted关系kill掉。具体实现如下:

对load指令进行同样修改，区分load指令是否涉及数组元素，不涉及数组元素时，操作不变；涉及数组元素时，由于store操作时添加关系均是对于数组的初始化指令，所以load操作添加对应关系时，要将使用到的数组元素变为数组元素的初始化指令，具体如下：

对于其余指令的fact提取操作不变，效果如下：

本实验实现了一个基于数据流分析的简单（基本数据类型、只有一个main函数）C程序的除0错漏洞分析器，并支持数组处理，首先利用clang将c文件处理为LLVM 3AC code，然后分别针对数据流分析以及污点分析阶段定义了一系列关系以及规则，再利用LLVM相关函数处理IR，提取fact生成constraint，将constraint交到z3求解器中求解，根据rule判断是否蕴含除零错误的可能。

如果没有太明白的话，可能首先需要掌握清楚reaching definition，然后下载实验代码，观察代码框架，然后在结合本文来看可能会有新的体会。建议大家自己完成，遇到不懂的再来参考借鉴。

https://blog.csdn.net/qq_33265800/article/details/107758542

[招生]科锐逆向工程师培训(2024年11月15日实地，远程教学同时开班, 第51期)