首页
社区
课程
招聘
[原创]符号执行--论文《Symbolic Execution for Software Testing: Three Decades Later》的阅读笔记
2021-11-21 19:13 13418

[原创]符号执行--论文《Symbolic Execution for Software Testing: Three Decades Later》的阅读笔记

2021-11-21 19:13
13418

符号执行可以被用于生成测试输入,以下为论文《Symbolic Execution for Software Testing: Three Decades Later》的阅读笔记

符号执行的key idea

把符号输入进程序里(而不是输入实际的数据),把程序中的函数变成符号表达式。程序的输出值也是输入符号表达式。

程序的表示方法

一个程序的执行路径可以表示为ture和false的序列,在序列的第i个位置为true则表示第i个条件判断语句执行then分支,若为false则执行else分支。
一个程序的所有的执行路径可以被表示成一颗执行树。

符号执行的过程

符号执行的过程中,一直存有一个符号状态集合

1
\delta

它是映射的集合,这里的映射是指把一个符号变量通过符号表达式变成另外一个符号变量。

 

符号执行的过程中,还有一个符号路径约束PC,这是符号表达式上的一个无量词的一阶式。

 

在每条路径开始执行前,都初始化这两个变量为,

1
2
3
\delta = 空集
 
PC = ture

符号执行阶段,这两个值会变化。
在一条执行路径结束的时候,会调用约束求解器去求解PC,从而生成真正的input values.如果程序用这个input values去执行,它的执行路径会跟符号执行的路径一致。
这就是符号执行的基本概念。

符号执行的例子

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
# Figure 1. 要用来进行符号执行的程序
 
1 int twice (int v) {
2 return 2∗v;
3 }
4
5 void testme (int x, int y) {
6 z = twice (y);
7 if (z == x) {
8 if (x > y+10)
9 ERROR;
10 }
11 }
12 }
13
14 /∗ simple driver exercising testme () with sym inputs ∗/
15 int main() {
16 x = sym input();
17 y = sym input();
18 testme (x, y );
19 return 0;
20 }

符号状态集合的变化

如上图,当程序执行到16,17行时,

1
\delta = \{x \rightarrow x_0,y \rightarrow y_0\}

其中x_0,y_0是两个初始的无约束符号值。

 

当执行到v=e这种赋值语句时,例如第6行代码时。符号状态会变为:

1
\delta = \{x \rightarrow x_0,y \rightarrow y_0\,z \rightarrow 2y_0\}

路径约束PC的变化

当执行到条件语句如:

1
if(e) S1 else S2
1
2
3
4
5
6
7
PC会被更新(then语句),
 
PC = PC \cap \delta(e)
 
然后还会生成一个新的路径约束 (else语句),
 
PC^{’} = PC \cap \lnot\delta(e)

如果PC可以满足对符号值的某些分配,那么符号执行继续沿着then这条分支执行下去,且符号状态为σ和符号路径约束为PC。

 

同样,如果PC'可满足,PC‘则使用符号状态σ和符号路径约束PC’创建另一个符号执行的实例,并沿着“else”分支继续执行;

 

如在第7行,会有两个路径约束被创建,分别对应于

1
2
3
x0 = 2y_0
 
x0 \neq 2y_0

在第8行,会有两个路径约束被创建,分别对应于

1
2
3
(x0 = 2y_0)\cap(x_0>y_0+10) ,
 
(x0 = 2y_0)\cap(x_0 \leq y_0+10)

约束求解

如果符号执行实例遇到了退出语句或错误(例如,程序崩溃或违反了断言),则终止符号执行的当前实例,并使用现成的约束求解器生成对当前符号路径约束得到真正的input datas.

当有无限循环时

1
2
3
4
5
6
7
8
9
10
1 void testme inf () {
2 int sum = 0;
3 int N = sym input();
4 while (N > 0) {
5 sum = sum + N;
6 N = sym input();
7 }
8 }
Figure 3. Simple example to illustrate infinite number of
execution paths.

1
2
3
PC = (\cap N_i > 0)\cap(N_{i+1} \leq 0)
 
\delta = \{N \rightarrow N_{n+1} , sum \rightarrow \sum Ni\}

PC的前面是若干个ture,最后一个是false.

 

在实践中,需要对路径搜索进行限制,例如,限制时间,限制路径的数量、限制路径的深度

当约束不能被求解的情况

情况一:函数是非线性函数时

若把上面的twice替换如下

1
2
3
4
5
1 int twice (int v) {
2 return (v∗v) % 50;
3 }
Figure 4. Simple modification of the example in Figure 1.
The function twice now performs some non-linear computation.

则执行到twice时,会产生两个路径约束:

1
2
3
x_0 \neq (y_0y_0)mod50
 
以及x_0 = (y_0y_0)mod50

此时常规的约束求解器是不能求解这个非线性表达式的。

情况二:没有函数源码时

如果我们连twice的源码都得不到呢,
则会有以下两个路径约束

1
2
3
x_0 \neq twice(y_0)
 
以及x_0 = twice(y_0)

此时常规的约束求解器还是无法求解。

 

符号执行的概念早在1975年就提出了,但是真正得到实用,却是在一种方式提出之后,即结合实际执行和符号化执行的一种方法:concolic execution,是真正意义上的动态符号执行。

Concolic Execution

Concolic Execution是把实际执行和符号执行结合的一种方法,以下称为混合执行。

 

混合执行的输入是随机生成的或者给定的一个具体的值,在执行过程中收集条件语句中的符号约束,然后对此约束取反,使用约束求解器来求解当前输入的变体,以便引导程序的下一次执行转向另一个执行路径

混合执行的步骤

我们依旧以上面那个程序的例子来说明

  1. 先产生一些随机输入,例如{x=22, y=7}

  2. 同时实际地和符号化地执行程序。这个实际执行会走到第7行的else分支,符号化执行会在实际执行路径生成路径约束

    1
    x_0 \neq 2y_0
  3. 然后混合执行会将路径约束的连接词取反,求解

    1
    x_0 = 2y_0

    得到一个测试输入{x=2, y=1},

  4. 这个新输入就会让执行一条不同的路径。之后,混合执行会在这个新的测试输入上再同时进行实际的和符号化的执行,执行会取与此前路径不同的分支,即第7行的then分支和第8行的else分支,这时产生的约束就是,
1
(x_0=2y_0) \cap (x_0 \leq y_0+10)
  1. 将上述的约束最后一个条件取反,也就是
    1
    (x_0=2y_0) \cap (x_0 > y_0+10)
    通过求解约束得到新的测试输入{x=30, y=15},程序会在这个输入上遇到ERROR语句。如此一来,我们就完成了所有3条路径的探索。

注意到,这里使用“以深度优先”的搜索策略来探索所有的执行路径;但是,我们可以使用其他策略来探索不同顺序的路径。

Execution-Generated Testing(EGT)

这一部分没读太懂,所以下面的内容读懂了再做补充吧。
EGT方法由EXE和KLEE工具扩展组合成,它工作通过区分程序的具体状态和符号状态来完成。

 

EGT在每次操作之前动态检查操作所涉及的值是否都是具体的。如果操作的值是具体的,则该操作将与原始程序中一样执行。否则,如果至少有一个值是符号值,则通过更新当前路径的路径条件,然后符号地执行该操作。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
# Figure 1. 要用来进行符号执行的程序
 
1 int twice (int v) {
2 return 2∗v;
3 }
4
5 void testme (int x, int y) {
6 z = twice (y);
7 if (z == x) {
8 if (x > y+10)
9 ERROR;
10 }
11 }
12 }
13
14 /∗ simple driver exercising testme () with sym inputs ∗/
15 int main() {
16 x = sym input();
17 y = sym input();
18 testme (x, y );
19 return 0;
20 }

例如,如果图1中的第17行更改为y=10,那么第6行将用具体参数20调用函数twice(),调用将像原始程序一样执行。然后,第7行上的分支将成为如果(20==x),符号执行会往两个方向执行,在“then”方向(会添加x=20的路径约束),以及“else”方向(会添加了x=20的约束)。注意,在“then”路径上,第8行变成了if(x>20),因此在“then”边是不可行的,因为x被约束等于20了。

 

参考文献:
https://zhuanlan.zhihu.com/p/26927127


[CTF入门培训]顶尖高校博士及硕士团队亲授《30小时教你玩转CTF》,视频+靶场+题目!助力进入CTF世界

收藏
点赞2
打赏
分享
最新回复 (0)
游客
登录 | 注册 方可回帖
返回