Chopped Symbolic Execution

1.引言
2.Overview
3.Chopped Symbolic Executio(CSE)
- 3.1.静态推理过程
- 3.2.多重recovery state
- 3.3.处理多重skip function
- 3.4.Memory Allocations
- 3.5.Chopping-aware搜索策略
- 3.6.局限性
4.实现
5.实验
- 5.1.Failure reproduction
- 5.2.Test Suite Augmentation
参考文献

1.引言

符号执行工具受到路径爆炸和约束求解限制的影响。下面的示例来自libtasn1的 extract_octet 函数，libtasn1根据ASN1规则解析输入字符串，libtasn1 4.5版本以前的release都会受到堆溢出漏洞的影响（CVE-2015-3622），示例中：

每一轮循环

extract_octet 会调用 get_length 求出当前ASN数据对应的长度。
要么调用 append_value 创建1个AST结点（对应ASN1规则，推测是终端结点）。
要么递归调用 extract_octet 建立语法树。

其中第21行更新 str_len 会导致第8行调用 get_length 会造成堆缓冲区溢出。

在对上面示例进行符号执行时，嵌套函数调用会造成路径爆炸。输入长度为 n 的符号字符串对 get_length 进行符号执行会产生 4 * n 条路径，append_value 更是会产生更多路径并且由于大量调用约束求解影响性能。

为了执行到漏洞触发点，输入会经过2945次函数调用覆盖98个不同的函数，包括386727个指令。其中大部分函数调用与需要出发的漏洞没有太大关系，比如上述bug涉及 DECR_LEN 和 get_length，与 append_value没有太多关系。

因此作者提出一种新颖的符号执行形式，称之为chopped symbolic execution（CSE），允许用户在分析过程中指定要排除的代码中不感兴趣的部分（本文是函数调用），从而只针对重要的路径进行探索。

2.Overview

这里通过一个示例来整体说明CSE的工作流程，下图b部分每个灰色椭圆为1个状态，下图 main 调用了 f，而 f 为用户指定的要跳过的部分。

当一个状态对应的下一条指令为调用 f，CSE会clone当前状态为snapshot(1)（快照状态），并跳过当前函数调用。从下条指令开始，CSE需要考虑 load 指令可能会对 f 中的某些指令产生数据依赖。（f 修改了 p->z, p->x, p->y，main 第9行读取了 p.y，数据依赖于 f 第22行。，这里作者将第9行 p.y 这种读取可能受到影响的操作定义为dependent loads）。
如果 main 函数中符号执行到11行else分支中的代码，那么不会触发dependent loads，因此不会调用 f 函数。
如果走的是第8行then分支，则会在第9行触发dependent loads p.y，此时CSE会在将当前状态暂停并符号执行 f，并且当前状态会成为dependent state(2)，CSE基于之前的snapshot创建一个新的recovery state(3)，并开始符号执行 f。在上面示例 p.y 对应状态为dependent state，f 入口处对应状态为recovery state。
执行recovery state发生fork时会将fork同步回dependent state(4, 5)。
对dependent load操作读取的内存行 store 的操作也会同步回dependent state(6)。
如果recovery state下成功返回了，那么恢复对应dependent state的执行。如果执行recovery state时发生了错误，那么对应的dependent state也会停止执行。

同时还需要注意的是

当执行recovery state时，对应dependent state上的约束条件也会同步过来，保证路径约束的一致性。
在recovery state的执行中，很多路径对dependent loads并没有影响，比如 k % 2，这里作者用到program slice技术，相对于写入dependent loads读取的内存位置的 store 指令对函数 f 进行切片（示例中从 p->y++ 对应的 store 指令开始切片）
- 如果 f 调用了其它函数，也对调用链上的其它函数进行slice）。
- 示例中，slice可以去掉16-17行和20行。
理论上dependent state和recovery state是一一对应的。

在示例中：

1.main 函数执行到第7行，创建snapshot并跳过函数调用。
2.执行到第9行，将当前状态变成dependent state并暂停。
3.克隆snapshot创建recovery state，将dependent state的约束条件 j > 0 同步到recovery state。
4-5.基于dependent load读取的内存地址对函数 f 进行slice，理论上能删除16-17行和20行，19行fork的时候，dependent state中也会发生fork。
6.其中一个forked recovery state会更新 p->y 的值，因此在dependent state对应位置上也会更新。
7.最终，recovery state成功返回，CSE恢复dependent state开始符号执行。

3.Chopped Symbolic Executio(CSE)

与普通的符号执行相比

CSE多引入了一个外部参数 skipFunctions。（为用户指定跳过的函数，上面示例中 skipFunctions = {f}）
同时对于 load, store, br, ret, call 指令添加了特殊处理。
对于符号状态，成员变量多了
- skipped（为 list 类型），每个元素为当前状态跳过的1个函数调用及对应snapshot。
- isRecovery（bool 类型），标识当前状态是否是 recoveryState。
- overwrittenSet（set 类型），记录当前状态写入过的地址。

上面红框标出的为CSE相比普通符号执行添加的部分：

Call 指令：如果当前状态 s 对应将要执行的指令是 call，并且调用的函数在 skipFunctions 中，那么基于当前状态clone一个 snapshot，将 (f, snapshot) 添加到 s.skipped 列表中。
Load 指令：需要考虑是不是dependent load，如果 s 对应将要执行的指令是 load，首先查看 load 读取的内存地址 addr，如果 s 跳过的函数中存在可能修改 addr 的指令，那么创建 recoveryState。这里用到了2个辅助函数 mayMod 和 createRecoveryState。
Br 指令：需要考虑是不是在recovery state中的分支，如果是就需要同时考虑dependent state中的具体情况，recovery state中发生的fork也要同步到dependent state中。
Store 指令：如果当前是在recovery state中进行 store，那么会将修改的值同步到dependent state中。否则，将写入的地址记入到 overwrittenSet 中。
Return 指令：如果当前状态是recovery state并且 ret 指令是在skipfunction函数体中，那么recovery state被终止，同时恢复dependent state执行。

需要注意的有：

3.1.静态推理过程

处理dependent load时用到了 MayMod 函数

上面的函数需要先进行指针分析，作者用到了context-insensitive, flow-insensitive, field-sensitive的指针分析算法。需要注意的是：

指针分析在1个测试程序的分析过程只执行1次。
每次创建recovery state的时候都会先进行slice，也就是slice会进行多次。

ModSet 用到了指针分析结果，指针分析中每个指针变量的内存位置会用 allocation site 进行抽象，比如 L: p=malloc(4) 属于1个allocation site，计作 ASLAS_LASL，如果程序中包含 p = q，那么 p 可能指向 ASLAS_LASL。指向图中的每个结点是一个指针变量名或者 allocation site，边表示潜在的指向关系。

指针分析算法是flow-insensitive的，因此在当前函数中可能存在其它 store 指令修改 addr，因此：

addr 必须可能被 skipFunction 修改。
在skip function call和dependent load指令中间不能有其它对 addr 进行修改的 store 指令，之前用到的 overWritten 成员变量正是用来判断当前 addr 是否已被其它 store 指令修改。

3.2.多重recovery state

7   f(&p,k); // skip
8   // next two branches depend on the side effects of f
9   if (p.x)
10    p.z++;
11  if (p.y)
12    p.z--;

上述示例中 f 的内容跟上一个示例一样，那么第9行读取 p.x 和第11行读取 p.y 处都会出现dependent load，并且都会产生dependent state和recovery state，但是，p.x 是在 k > 0 的情况下修改的，p.y 是在 k <= 0 的情况下产生的。因此在第一个dependent state恢复执行时，应该同步第一个recovery state中的约束，避免第二个dependent state中走向不可执行的path。

如下所示，第一个dependent state恢复后会fork成2个，一个添加约束条件 k > 0，另一个 k <= 0。而 p.y 只在第2个state中修改。

3.3.处理多重skip function

符号执行时可能会碰到多个skip function对一个 addr 进行写入的情况，作者用执行路径上最后一个可能修改 addr 的function进行搜索。

同样的还有1个问题，就是一个skip function可能会依赖于另一个skip function，如下面代码：

1  struct point { int x, y;};
2  void f1(struct point *p) {3    p->y = 1;
4  }
5  void f2(struct point *p) {6    if (p->y)
7      p->x = 1;
8  }
9  void g() {10   struct point p;
11   f1(&p); // skip
12   f2(&p); // skip
13   if (p.x) {14     // ...
15   }
16 }

执行到13行读取 p.x 触发dependent load，开始搜索 f2，执行到第6行读取 p->y 触发dependent load，此时探索 f1，因此 f1 执行完返回 f2 再执行完返回 g。同时注意的时 f2 对应的recovery state的 skipFunctions 一开始就包括了 f1。

为了提高CSE的效率，作者用到了recovery cache。

3.4.Memory Allocations

考虑以下代码，第8第9行都会触发dependent load，第8行dependent load会执行 f 第3行 malloc 语句，而第9行触发时又会执行第3、4行语句，这样 malloc 就执行了2次，会生成2个不同的地址，这其实是个错误。

为了预防这种错误，对于每个skip function，作者都会维护一个 list，其中每一个元素是 f 中的一个allocation site，与指针分析时不同，每个allocation site都会用其调用栈进行标识，这样当出现重复执行 alloca 指令的时候就能避免这种结果。

1  struct point { int x, y; } *p = NULL;
2  void f() {3    p = malloc(sizeof(struct point));
4    p->x = 0;
5  }
6  void g() {7    f(); // skip
8    if (p)
9    if (p->x) {10     // ...
11   }
12 }

3.5.Chopping-aware搜索策略

传统SE中的搜索策略并没有考虑到CSE中状态的特性，在CSE中状态可分为normal和recovery（不考虑dependent），作者提出了一个新的搜索策略

传统搜索策略只用到了一个state worklist，CSE中用到2个，一个normal state worklist，一个recovery state worklist。
在选择状态的时候，首先以指定概率选择一个worklist（作者设定normal 0.8, recovery 0.2），然后再以正常方式选择状态。

3.6.局限性

主要的局限性来自符号地址，一个符号地址可能对应多个 allocation site，由此可能引用到多个skip function。此外，当在recovery state对某个地址执行存储时，CSE需要一个具体的加载地址来更新。

CSE目前侧重于跳过函数。然而，这种方法可以更通用：理论上可以跳过任何保留程序控制流的任意代码部分。

4.实现

项目的github地址，Chopper基于klee(commit b2f93ff)实现，指针分析用到SVF，反向切片用到了DG，用到了LLVM版本3.4.2，约束求解器为STP 2.1.2。

5.实验

实验主要探究2方面：

Failure reproduction：能比标准符号执行更快或者找到更多的bug吗？
Test suite augmentation：Chopper能否补充标准符号执行？

5.1.Failure reproduction

benchmark为libtasn1，包含的漏洞包括（都属于缓冲区溢出访问）：

Vulnerability	Version	C SLOC
CVE-2012-1569	2.11	24448
CVE-2014-3467	3.5	22,091
CVE-2015-2806	4.3	28115
CVE-2015-3622	4.4	28109

CVE-2014-3467有3个触发位置因此在实验中被当成3个漏洞。

实现包括以下工作：

手动为libtasn1库创建一个执行驱动程序，以从其公共接口运行库，模拟外部程序的交互(GnuTLS)。
通过检查代码和漏洞报告来手动导出要跳过的函数集，漏洞报告通常包括堆栈跟踪，有时还来自动态分析工具。对于选定的case，作者设法在每次失败不到30分钟的时间内确定要排除的候选函数集，但熟悉代码的开发人员应该能够更快地做到这一点。
采用的搜索策略包括DFS，随机状态搜索，覆盖率引导（klee选项为 dfs, random-state, nurs:covnew），限时24小时。

实验结果如下所示：

下图展示了Chopper在检测过程中生成的recovery和snapshot数量，以及用slice和不用slice的运行时间

在检测CVE-2015-2806的时候，Chopper生成了0个recovery state，意味着skip function从没被执行过，因此跳过了许多不必要的执行。在检测CVE-2014-3467时，Chopper在slice的情况下提高了运行效率。但是在检测CVE-2012-1569时，不用slice反而运行更快，合理的解释是slice带来了额外的开销。

5.2.Test Suite Augmentation

这部分做的是覆盖率测试，用到的benchmark是BC, LibYAML和GNU oSIP，这部分对比的是纯Klee和Klee+Chopper组合，Klee+Chopper的运行流程为：

先运行Klee生成初始Testcase，统计line和branch覆盖率，用到的策略为 nurs:covnew，限时1小时。
收集没被覆盖的函数，比如 f 调用 g 和 h，f 和 h 已被覆盖，那么skip function就包含 h，包含 f 的话 g 就不可达了。
运行chopper，对于normal state使用 nurs:covnew 策略，对于recovery state使用 dfs 策略，限时1小时。

实验结果在下表。

参考文献

Chopped Symbolic Execution; David Trabish, Andrea Mattavelli, Noam Rinetzky, Cristian Cadar

会议论文分享-ICSE18-chopped符号执行相关推荐

【论文分享】Chopped Symbolic Execution
论文名:Chopped Symbolic Execution 来源会议:ICSE 2018 论文下载地址:https://dl.acm.org/doi/10.1145/3180155.3180251 ...
会议论文分享-FSE20-基于学习的状态修剪策略
基于学习的状态修剪策略 1.引言 2.Homi算法 2.1.概率修剪策略 2.2.Homi 2.2.1.Collecting Promising Data 2.2.2.Generating Featu ...
科研效率直线提升！如何一键下载会议论文？ACL 2020 论文代码批量下载打包分享
ACL 2020 论文代码批量下载打包分享 1. 提取代码 2. EndNote批量导入,看论文可以如此轻松! 3. 论文批量分享全文总结如何通过代码批量自动化爬取会议论文代码如下,其他会议同 ...
CVPR 2021论文分享会日程公布！
↑↑↑关注后"星标"Datawhale 每日干货 & 每月组队学习,不错过 Datawhale学术活动:CVPR 2021论文分享会随着人工智能的火热,AAAI.Neu ...
4个Keynote、12篇论文分享、40个Poster，CVPR 2021论文分享会全日程公布
随着人工智能的火热,AAAI.NeurIPS.CVPR 等顶级学术会议的影响力也愈来越大,每年接收论文.参会人数的数量连创新高.但受疫情影响,近两年国外举办的学术会议都转为了线上,无法满足学者们现场交 ...
会议论文_InVisor会议论文辅导发表
CPCI/EI会议论文辅导发表:商科专业同学看过来!学术背景快速提升!(此外还有理工科方向的科研,详情请咨询客服) 快速学术成果验收:3-6个月周期,快速实现背景提升定制化科研服务:1v1针对性科研 ...
新星云集！CVPR 论文分享会圆桌论坛：计算机视觉科研之“路”
微软亚洲研究院 2021 CVPR 论文分享会各个主题已分享完毕 CVPR 2021 目标检测.跟踪和姿态估计最新进展分享 CVPR 2021 机器学习及多模态最新进展分享 CVPR 2021 3D视 ...
预告｜CVPR 2021 论文分享会日程公布！与计算机视觉领域学者一起收获“立体”参会体验...
微软亚洲研究院 2021 CVPR 论文分享会将于 4 月 22 日 9:00 至 18:00 在线上举行,对计算机视觉领域感兴趣的你是否已经安排好时间等待各位"大佬"的分享了呢? ...
预告｜ 4月22日，CVPR 2021论文分享会详细介绍，学术新星云集！
国际计算机视觉与模式识别会议(CVPR)是人工智能领域最有学术影响力的顶级会议之一.根据 CVPR 2021 官方公布的论文收录结果,今年一共有 1663 篇论文被接收,接收率为 23.7%,相较于去 ...

会议论文分享-ICSE18-chopped符号执行