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

汪孙律; 林渝淇; 杨秋松; 李明树

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

您当前的位置：

首页 >

文章列表页 >

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

学术论文 | 更新时间：2024-06-05

- 基于输入约束的符号执行优化
- Symbolic execution optimization method based on input constraint
- 通信学报 2019年40卷第3期页码：19-27
- 作者机构：
  
  中国科学院软件研究所基础软件国家工程研究中心，北京 100190
- 作者简介：
  
  [ "汪孙律（1986- ），男，安徽安庆人，中国科学院软件研究所博士生，主要研究方向为软件安全。" ]
  [ "林渝淇（1988- ），男，山东潍坊人，博士，中国科学院软件研究所助理研究员，主要研究方向为系统安全与可信计算。" ]
  [ "杨秋松（1977- ），男，河北泊头人，博士，中国科学院软件研究所研究员、博士生导师，主要研究方向为软件工程、形式化方法、模型检测、安全操作系统。" ]
  [ "李明树（1966- ），男，吉林德惠人，博士，中国科学院软件研究所研究员、博士生导师，主要研究方向为操作系统与基础软件、软硬件协同设计以及软件工程方法和软件过程技术等。" ]
- 基金信息：
  
  中国科学院战略性先导科技专项基金资助项目(XDA-Y01-01)
- DOI：10.11959/j.issn.1000-436x.2019062
  中图分类号： TP311
- 网络首发：2019-03，
  
  纸质出版：2019-03-25
- 稿件说明：
移动端阅览
汪孙律, 林渝淇, 杨秋松, 等. 基于输入约束的符号执行优化[J]. 通信学报, 2019,40(3):19-27.

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.
汪孙律, 林渝淇, 杨秋松, 等. 基于输入约束的符号执行优化[J]. 通信学报, 2019,40(3):19-27. DOI： 10.11959/j.issn.1000-436x.2019062.

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 .

浏览量

2030

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于变量符号关联分析的程序状态优化方法

β-NaGd_0.794 Yb_0.200 Ho_0.001 Tm_0.005 F₄ 纳米颗粒的白色上转换发光

一维纳米SiC-CNTs复合结构的生长机制和阴极射线发光

Si基CeO₂薄膜的发光特性

In_0.2Ga_0.8As/GaAs单量子阱PL谱温度特性及其机制