(二)数据流分析&污点分析&符号执行

2022/09/23

数据流分析污点分析符号执行三种常见概念进行区分

数据流分析

数据流分析是一种用来获取相关数据沿着程序执行路径流动的信息分析技术。分析对象是程序执行路径上的数据流动或可能的取值。

分类

根据对程序路径的分析精度分类:

根据分析程序路径的深度分类:

漏洞检测

基于数据流的源代码漏洞分析的原理如下图所示:

image-20221222145301058

污点分析

基本原理

污点分析是一种跟踪并分析污点信息在程序中流动的技术。在漏洞分析中,使用污点分析技术将所感兴趣的数据(通常来自程序的外部输入)标记为污点数据,然后通过跟踪和污点数据相关的信息的流向,可以知道它们是否会影响某些关键的程序操作,进而挖掘程序漏洞。即将程序是否存在某种漏洞的问题转化为污点信息是否会被 Sink 点上的操作所使用的问题。

污点分析常常包括以下几个部分:

[...]
scanf("%d", &x);    // Source 点,输入数据被标记为污点信息,并且认为变量 x 是污染的
[...]
y = x + k;          // 如果二元操作的操作数是污染的,那么操作结果也是污染的,所以变量 y 也是污染的
[...]
x = 0;              // 如果一个被污染的变量被赋值为一个常数,那么认为它是未污染的,所以 x 转变成未污染的
[...]
while (i < y)       // Sink 点,如果规定循环的次数不能受程序输入的影响,那么需要检查 y 是否被污染

然而污点信息不仅可以通过数据依赖传播,还可以通过控制依赖传播。我们将通过数据依赖传播的信息流称为显式信息流,将通过控制依赖传播的信息流称为隐式信息流。

例子:

 if (x > 0)    
 	y = 1;
 else   
 	y = 0;

变量 y 的取值依赖于变量 x 的取值,如果变量 x 是污染的,那么变量 y 也应该是污染的。

通常我们将使用污点分析可以检测的程序漏洞称为污点类型的漏洞,例如 SQL 注入漏洞

String user = getUser();
String pass = getPass();
String sqlQuery = "select * from login where user='" + user + "' and pass='" + pass + "'";
Statement stam = con.createStatement();
ResultSetrs = stam.executeQuery(sqlQuery);
if (rs.next())
    success = true;

在进行污点分析时,将变量 user 和 pass 标记为污染的,由于变量 sqlQuery 的值受到 user 和 pass 的影响,所以将 sqlQuery 也标记为污染的。程序将变量 sqlQuery 作为参数构造 SQL 操作语句,于是可以判定程序存在 SQL 注入漏洞

使用污点分析检测程序漏洞的工作原理如下图所示:

image-20221222150738760

符号执行

通俗解释

在计算机科学中,符号执行技术指的是通过程序分析的方法,确定哪些输入向量会对应导致程序的执行结果为某个向量的方法 —-维基百科

通俗的说,如果把一个程序比作王者荣耀中的英雄,英雄的最终属性值为程序的输出(包括攻击力、防御力、血槽、蓝槽),英雄的武器出装为程序的输入(出无尽还是破军)。那么符号执行技术的任务就是,给定了一个英雄的最终属性值,分析出该英雄可以通过哪些出装方式达到这种最终属性值

也就是一种程序分析技术,且是白盒静态

以下面的源代码为例子:

int m=M, n=N, q=Q; 
int x1=0,x2=0,x3=0;
if(m!=0)
{
    x1=-2;
}
if(n<12)
{
    if(!m && q)
    {
        x2=1;
    }
    x3=2;
}
assert(x1+x2+x3!=3) // if =3 then program crash

上述代码是一个简单的c语言分支结构代码,它的输入是M,N,Q三个变量;输出是x1,x2,x3的三个变量的和。我们这里设置的条件是想看看什么样的输入向量<M,N,Q>的情况下,得到的三个输出变量的和等于3

那么我们通过下面的树形结构来看看所有的情况:

image-20221221225618882

上树形图已经将所有可能的情况列举出,其中,叶子节点显示的数值表示当前输入情况下,可以得到的数值,(比如,如果英雄出装是M^(N<12),那么最终的属性值R=0),可以发现,当条件为~M^(N<5)^Q时,得到了最终结果等于3.即,我们通过这种方式逆向发现了输入向量。如果把结果条件更改为漏洞条件,理论上也是能够进行漏洞挖掘了

对于如何根据最终得到的结果求解输入向量,已经有很多现成的数学工具可以使用。上述问题其实可以规约成约束规划的求解问题(更详细的介绍看这里:Constraint_programming )。比较著名的工具比如SMT(Satisfiability Modulo Theory,可满足性模理论)和SAT.

使用符号执行检测程序漏洞的原理如下图所示:

image-20221221230504182

但是在实际的漏洞分析过程中,目标程序可能更加复杂,没有我们上面的例子这么简单。实际的程序中,可能包含了与外设交互的系统函数,而这些系统函数的输入输出并不会直接赋值到符号中,从而阻断了此类问题的求解

比如下面的这个包含了文件读写的例子

int main(int argc, char* argv[])
{
    FILE *fop = fopen("test.txt");
    ...
    if(argc > 3)
    {
        fputs("Too many parameters, exit.", fop);
    }
    else
    {
        fputs("Ok, we will run normally.", fop);
    }
    ...
    output = fgets(..., fop);
    assert(!strcmp(output, "Ok, we will run normally.")); // if str is "OK,..." then program crash
    return 0;
}

上述示例代码中,我们想要发现什么情况下会得到输出”Ok, we will run normally.”这个字符串。通过一系列的执行到if语句,此时,根据程序输入的参数个数将会产生两个分支。分支语句中将执行系统的文件写操作。**在传统的符号执行过程中,此类函数如果继续沿着系统函数的调用传递下去的话,符号数值的传递将会丢失。**而在之后的output = fgets(…, fop);这行代码中,符号从外部获得的数值也将无法正常的赋值到output中。因此,符号执行无法求解上述问题,因为在调用系统函数与外设交互的时候,符号数值的赋值过程被截断了

为了解决这个问题,最经典的项目就是基于LLVM的KLEE(klee)它把一系列的与外设有关的系统函数给重新写了一下,使得符号数值的传递能够继续下去。从比较简化的角度来说,就是把上面的fputs函数修改成,字符串赋值到某个变量中,比如可以是上面的fop里面。再把fgets函数修改成从某个变量获取内容,比如可以是把fop的地址给output。这样,就能够把符号数值的传递给续上。当然,这里举的例子是比较简单的例子,实际在重写函数的时候,会要处理更复杂的情况。在KLEE中,它重新对40个系统调用进行了建模,比如open, read, write, stat, lseek, ftruncate, ioctl。感兴趣的读者可以进一步阅读他们发表在OSDI2008年的论文(KLEE-OSDI08)他们的文章深入浅出,非常适合学习。

面临挑战&解决方案

上面我们只是举了一个问题,符号执行曾经遇到过很多问题,使其难以应用在真实的程序分析中。经过研究者的不懈努力,这些问题多多少少得到了解决,由此也产生了一大批优秀的学术论文。这一部分将简单介绍其中的一些关键挑战以及对应的解决方案。

路径爆炸(Path Explosion)

由于在每一个条件分支都会产生两个不同约束,符号执行要探索的执行路径依分支数指数增长。在时间和资源有限的情况下,应该对最相关的路径进行探索,这就涉及到了路径选择的问题。通过路径选择的方法缓解指数爆炸问题,主要有两种方法:

1)使用启发式函数对路径进行搜索,目的是先探索最值得探索的路径;

2)使用一些可靠的程序分析技术减少路径探索的复杂性。

约束求解(Constraint Solving.)

符号执行在2005年之后的突然重新流行,一大部分原因是因为求解器能力的提升,能够求解复杂的路径约束。但是约束求解在某种程度上依然是符号执行的关键瓶颈之一,也就是说符号执行所需求的约束求解能力超出了当前约束求解器的能力。所以,实现约束求解优化就变得十分重要。

内存建模(Memory Modeling)

程序语句转换为符号约束的精度对符号执行能实现的覆盖率以及约束求解的可伸缩性有很大影响。例如,使用数学整数(actual mathematical integers)去近似去代替固定宽度的整数变量,这样的内存模型可能会更有效率,但另一方面,根据诸如算术溢出之类的极端情况,可能导致代码分析不精确-这可能会导致符号执行遗漏路径或探索不可行的路径。

处理并发(Handling Concurrency)

大型程序通常是并发的。因为这种程序的内在特性,动态符号执行系统可以被用来高效地测试并发程序,包括复杂数据输入的应用、分布式系统以及GPGPU程序