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

Symbolic execution optimization method based on input constraint

作　　者：汪孙律[1] 林渝淇[1] 杨秋松[1] 李明树[1] WANG Sunlyu;LIN Yuqi;YANG Qiusong;LI Mingshu(National Engineering Research Center of Fundamental Software,Institute of Software Chinese Academy of Sciences,Beijing 100190,China)

机构地区：[1]中国科学院软件研究所基础软件国家工程研究中心,北京100190

出　　处：《通信学报》2019年第3期19-27,共9页Journal on Communications

基　　金：中国科学院战略性先导科技专项基金资助项目(No.XDA-Y01-01)~~

摘　　要：为了解决符号执行中路径爆炸、新路径发现率低等问题,提出了基于输入约束的符号执行(ICBSE)优化框架。该方法通过分析程序代码自动提取3类输入约束,随后使用这些约束引导符号执行更关注于核心功能代码。在KLEE中实现了上述优化框架,并对coreutils、binutils、grep、patch、diff这5个程序套件中的7个常用程序做了检测。ICBSE发现了7个之前未知的缺陷(KLEE只检测其中3个)。同时,ICBSE将指令行覆盖率、分支覆盖率分别提升了约20%,时间开销降低了约15%。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%.

关 键 词：符号执行 输入约束 路径爆炸 缺陷查找 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]