Symbolic execution optimization method based on input constraint

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

• symbolic execution
• input constraint
• path explosion
• bug finding