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 条
  • [11] Veanes M., Halleux P.D., Tillmann N., Rex: symbolic regular expression explorer, Third International Conference on Software Testing, Verification and Validation, pp. 498-507, (2010)
  • [12] Ramos D.A., Engler D., Under-constrained symbolic execution: correctness checking for real code, Usenix Conference on Security Symposium, pp. 49-64, (2015)
  • [13] Avgerinos T., Rebert A., Sang K.C., Et al., Enhancing symbolic execution with veritesting, International Conference on Software Engineering, pp. 1083-1094, (2014)
  • [14] Marinescu P.D., Cadar C., Make test-zesti: a symbolic execution solution for improving regression testing, International Conference on Software Engineering, pp. 716-726, (2012)
  • [15] 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)
  • [16] Marinescu P.D., Cadar C., KATCH: high-coverage testing of software patches, Joint Meeting on Foundations of Software Engineering, pp. 235-245, (2013)
12