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

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

Abstract

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

CLC Number:

TP311

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.

Figures/Tables 13

References 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.

Metrics

Recommended 0

No Suggested Reading articles found!

命令行输入	对应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

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 13

References 16

Related Articles 1

Metrics

Recommended 0