Symbolic execution optimization method based on input constraint

被引：0
|
作者：
Wang S. [1 ]
Lin Y. [1 ]
Yang Q. [1 ]
Li M. [1 ]
机构：
[1] National Engineering Research Center of Fundamental Software, Institute of Software Chinese Academy of Sciences, Beijing
来源：
Tongxin Xuebao/Journal on Communications | 2019年 / 40卷 / 03期
关键词：
Bug finding; Input constraint; Path explosion; Symbolic execution;
D O I：
10.11959/j.issn.1000-436x.2019062
中图分类号：
学科分类号：
摘要：
To solve path explosion, low rate of new path's finding in the software testing, a new vul-nerability 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 fo-cus 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%. © 2019, Editorial Board of Journal on Communications. All right reserved.
引用
收藏
页码：19 / 27
页数：8
相关论文
共 16 条
  • [1] Zhang J., Sharp static analysis of programs, Chinese Journal of Computers, 31, 9, pp. 1549-1553, (2008)
  • [2] King J.C., Symbolic execution and program testing, Communications of the ACM, 19, 7, pp. 385-394, (1976)
  • [3] Cadar C., Godefroid P., Khurshid S., Et al., Symbolic execution for software testing in practice: preliminary assessment, International Conference on Software Engineering, pp. 1066-1071, (2011)
  • [4] Anand S., Godefroid P., Tillmann N., Demand-driven compositional symbolic execu-tion, Theory and Practice of Software, International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems, pp. 367-381, (2008)
  • [5] Godefroid P., Compositional dynamic test generation, ACM Sigplan-Sigact Symposium on Principles of Programming Languages, pp. 47-54, (2007)
  • [6] Wong E., Zhang L., Wang S., Et al., DASE: document-assisted symbolic execution for im-proving automated software testing, IEEE International Conference on Software Engineering, pp. 620-631, (2015)
  • [7] Cadar C., Dunbar D., Engler D., KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs, USENIX Conference on Operating Systems Design and Implementation, pp. 209-224, (2009)
  • [8] Lattner C., Adve V., LLVM: a compilation framework for lifelong program analysis & transformation, International Symposium on Code Generation and Optimization, pp. 75-86, (2004)
  • [9] David T., Andrea M., Noam R., Et al., Chopped symbolic execution, The 40th International Conference on Software Engineering, pp. 350-360, (2018)
  • [10] Bjorner N., Tillmann N., Voronkov A., Path feasibility analysis for string-manipulating programs, TOOLS and Algorithms for the Construction and Analysis of Systems, International Conference, pp. 307-321, (2009)
12