基于输入约束的符号执行优化

doi:10.11959/j.issn.1000-436x.2019062

通信学报 ›› 2019, Vol. 40 ›› Issue (3): 19-27.doi: 10.11959/j.issn.1000-436x.2019062

基于输入约束的符号执行优化

汪孙律^1,2，林渝淇¹，杨秋松¹，李明树¹

1. 中国科学院软件研究所基础软件国家工程研究中心，北京 100190；2. 中国科学院大学计算机科学与技术学院，北京 101408

修回日期:2018-08-31 出版日期:2019-03-25 发布日期:2019-04-04
作者简介:汪孙律（1986- ），男，安徽安庆人，中国科学院软件研究所博士生，主要研究方向为软件安全。|林渝淇（1988- ），男，山东潍坊人，博士，中国科学院软件研究所助理研究员，主要研究方向为系统安全与可信计算。|杨秋松（1977- ），男，河北泊头人，博士，中国科学院软件研究所研究员、博士生导师，主要研究方向为软件工程、形式化方法、模型检测、安全操作系统。|李明树（1966- ），男，吉林德惠人，博士，中国科学院软件研究所研究员、博士生导师，主要研究方向为操作系统与基础软件、软硬件协同设计以及软件工程方法和软件过程技术等。
基金资助:
中国科学院战略性先导科技专项基金资助项目(XDA-Y01-01)

Symbolic execution optimization method based on input constraint

WANG Sunlyu^1,2, LIN Yuqi¹, YANG Qiusong¹, LI Mingshu¹

1. National Engineering Research Center of Fundamental Software, Institute of Software Chinese Academy of Sciences, Beijing 100190, China 2. School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing 101408, China

Revised:2018-08-31 Online:2019-03-25 Published:2019-04-04
Supported by:
Strategic Priority Research Program of Chinese Academy of Sciences(XDA-Y01-01)

摘要/Abstract

摘要：

为了解决符号执行中路径爆炸、新路径发现率低等问题，提出了基于输入约束的符号执行（ICBSE）优化框架。该方法通过分析程序代码自动提取3类输入约束，随后使用这些约束引导符号执行更关注于核心功能代码。在KLEE中实现了上述优化框架，并对coreutils、binutils、grep、patch、diff这5个程序套件中的7个常用程序做了检测。ICBSE发现了7个之前未知的缺陷（KLEE只检测其中3个）。同时，ICBSE将指令行覆盖率、分支覆盖率分别提升了约20%，时间开销降低了约15%。

关键词: 符号执行, 输入约束, 路径爆炸, 缺陷查找

Abstract:

To solve path explosion,low rate of new path’s finding in the software testing,a new vulnerability discovering architecture based on input constraint symbolic execution (ICBSE) was proposed.ICBSE analyzed program source code to extract three types of constraints automatically.ICBSE then used these input constraints to guide symbolic execution to focus on core functions.Through implemented this architecture in KLEE,and evaluated it on seven programs from five GNU software suites,such as coreutils,binutils,grep,patch and diff.ICBSE detected seven previously unknown bugs (KLEE found three of the seven).In addition,ICBSE increases instruction line coverage/branch coverage by about 20%,and decreases time for finding bugs by about 15%.

Key words: symbolic execution, input constraint, path explosion, bug finding

中图分类号:

TP311

汪孙律, 林渝淇, 杨秋松, 李明树. 基于输入约束的符号执行优化[J]. 通信学报, 2019, 40(3): 19-27.

Sunlyu WANG, Yuqi LIN, Qiusong YANG, Mingshu LI. Symbolic execution optimization method based on input constraint[J]. Journal on Communications, 2019, 40(3): 19-27.

图/表 13

图1

图2

图3

图4

图5

图6

表1

图7

表2

表3

表4

图8

图9

参考文献 16

[1]	张健 . 精确的程序静态分析[J]. 计算机学报, 2008,31(9): 1549-1553.
	ZHANG J . Sharp static analysis of programs[J]. Chinese Journal of Computers, 2008,31(9): 1549-1553.
[2]	KING J C . Symbolic execution and program testing[J]. Communications of the ACM, 1976,19(7): 385-394.
[3]	CADAR C , GODEFROID P , KHURSHID S ,et al. Symbolic execution for software testing in practice:preliminary assessment[C]// International Conference on Software Engineering. 2011： 1066-1071.
[4]	ANAND S , GODEFROID P , TILLMANN N . Demand-driven compositional symbolic execution[C]// Theory and Practice of Software,International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems. 2008: 367-381.
[5]	GODEFROID P , . Compositional dynamic test generation[C]// ACM Sigplan-Sigact Symposium on Principles of Programming Languages. 2007: 47-54.
[6]	WONG E , ZHANG L , WANG S ,et al. DASE:document-assisted symbolic execution for improving automated software testing[C]// IEEE International Conference on Software Engineering. 2015: 620-631.
[7]	CADAR C , DUNBAR D , ENGLER D . KLEE:unassisted and automatic generation of high-coverage tests for complex systems programs[C]// USENIX Conference on Operating Systems Design and Implementation. 2009: 209-224.
[8]	LATTNER C , ADVE V . LLVM:a compilation framework for lifelong program analysis ＆ transformation[C]// International Symposium on Code Generation and Optimization. 2004: 75-86.
[9]	DAVID T , ANDREA M , NOAM R ,et al. Chopped symbolic execution[C]// The 40th International Conference on Software Engineering. 2018: 350-360.
[10]	BJ?RNER N , TILLMANN N , VORONKOV A . Path feasibility analysis for string-manipulating programs[C]// TOOLS and Algorithms for the Construction and Analysis of Systems,International Conference. 2009: 307-321.
[11]	VEANES M , HALLEUX P D , TILLMANN N . Rex:symbolic regular expression explorer[C]// Third International Conference on Software Testing,Verification and Validation. 2010: 498-507.
[12]	RAMOS D A , ENGLER D . Under-constrained symbolic execution:correctness checking for real code[C]// Usenix Conference on Security Symposium. 2015: 49-64.
[13]	AVGERINOS T , REBERT A , SANG K C ,et al. Enhancing symbolic execution with veritesting[C]// International Conference on Software Engineering. 2014: 1083-1094.
[14]	MARINESCU P D , CADAR C . Make test-zesti:a symbolic execution solution for improving regression testing[C]// International Conference on Software Engineering. 2012: 716-726.
[15]	CADAR C , GODEFROID P , KHURSHID S ,et al. Symbolic execution for software testing in practice:preliminary assessment[C]// International Conference on Software Engineering. 2011: 1066-1071.
[16]	MARINESCU P D , CADAR C . KATCH:high-coverage testing of software patches[C]// Joint Meeting on Foundations of Software Engineering. 2013: 235-245.

命令行输入	对应KLEE参数	说明
-h -S	--sym-args 0 2 2	readelf带有0～2个长度为2的短选项
--debug-dump	--sym-args 0 1 13	readelf带有0～1个长度为13的长选项
info	--sym-args 0 1 10	--debug-dump 命令行选项后带的命令行参数
a.out	--sym-files 1 20	符号文件数量为1，长度为20

短选项	长选项	是否需要参数
-a	--all	no_argument
-h	--file-header	no_argument
-D	--use-dynamic	no_argument
-x	--hex-dump	required_argument
无	--debug-dump	optional_argument
-v	--version	no_argument

名称	版本	简介
coreutils	6.11	Linux常用工具集合，本文选用ls和sort这2个常用程序作为测试对象	ls:3 241 sort:2 317
binutils	2.14	Linux 二进制工具集合，本文选用readelf作为测试对象	12 076
diffutils	2.8	Linux文本比较工具，本文选用diff作为测试对象	1 114
grep	3.0	Linux grep命令	6 144
sed	4.2	Linux Sed命令	4 125
patch	2.7	Linux补丁工具	5 996

程序	位置	错误类型	KLEE	ICBSE
objdump	elf-attrs.c:463	整型溢出		√
readelf	readelf.c:532	指针越界	√	√
readelf	readelf.c:712	指针越界	√	√
readelf	readelf.c:2662	空指针	√	√
patch	gl_list.c:215	空指针		√
bool	text.c:231	空指针		√
head	head.c:297	内存耗尽		√

基于输入约束的符号执行优化

Symbolic execution optimization method based on input constraint

在线阅读

PDF下载

可视化

摘要/Abstract

引用本文

使用本文

图/表 13

参考文献 16

相关文章 1

Metrics

推荐阅读 0