Symbolic execution optimization method based on input constraint

Sunlyu WANG; Yuqi LIN; Qiusong YANG; Mingshu LI

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

您当前的位置：

首页 >

文章列表页 >

Symbolic execution optimization method based on input constraint

Papers | 更新时间：2024-06-05

- Symbolic execution optimization method based on input constraint
- Journal on Communications Vol. 40, Issue 3, Pages: 19-27(2019)
- 作者机构：
  
  中国科学院软件研究所基础软件国家工程研究中心，北京 100190
- 作者简介：
- 基金信息：
  
  Strategic Priority Research Program of Chinese Academy of Sciences(XDA-Y01-01)
- DOI：10.11959/j.issn.1000-436x.2019062
  CLC： TP311
- Online First：2019-03，
  
  Published：25 March 2019
- 稿件说明：
移动端阅览
Sunlyu WANG, Yuqi LIN, Qiusong YANG, et al. Symbolic execution optimization method based on input constraint[J]. Journal on Communications, 2019, 40(3): 19-27.
DOI：

Sunlyu WANG, Yuqi LIN, Qiusong YANG, et al. Symbolic execution optimization method based on input constraint[J]. Journal on Communications, 2019, 40(3): 19-27. DOI： 10.11959/j.issn.1000-436x.2019062.

摘要

为了解决符号执行中路径爆炸、新路径发现率低等问题，提出了基于输入约束的符号执行（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%.

关键词

Keywords

references

张健 . 精确的程序静态分析 [J ] . 计算机学报 , 2008 , 31 ( 9 ): 1549 - 1553 .

ZHANG J . Sharp static analysis of programs [J ] . Chinese Journal of Computers , 2008 , 31 ( 9 ): 1549 - 1553 .

KING J C . Symbolic execution and program testing [J ] . Communications of the ACM , 1976 , 19 ( 7 ): 385 - 394 .

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 .

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 .

GODEFROID P , . Compositional dynamic test generation [C ] // ACM Sigplan-Sigact Symposium on Principles of Programming Languages . 2007 : 47 - 54 .

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 .

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 .

LATTNER C , ADVE V . LLVM:a compilation framework for lifelong program analysis ＆ transformation [C ] // International Symposium on Code Generation and Optimization . 2004 : 75 - 86 .

DAVID T , ANDREA M , NOAM R , et al . Chopped symbolic execution [C ] // The 40th International Conference on Software Engineering . 2018 : 350 - 360 .

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 .

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 .

RAMOS D A , ENGLER D . Under-constrained symbolic execution:correctness checking for real code [C ] // Usenix Conference on Security Symposium . 2015 : 49 - 64 .

AVGERINOS T , REBERT A , SANG K C , et al . Enhancing symbolic execution with veritesting [C ] // International Conference on Software Engineering . 2014 : 1083 - 1094 .

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 .

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 .

MARINESCU P D , CADAR C . KATCH:high-coverage testing of software patches [C ] // Joint Meeting on Foundations of Software Engineering . 2013 : 235 - 245 .

Views

2475

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Program state optimal method based on variable symbolic relation analysis

Related Author

Xi GUO

Pan WANG

Related Institution

College of Informatics,Huazhong Agriculture University

Department of Power Engineering,Wuhan Electric Power Technical College

AI问答

⁰