A Symbolic Execution Optimization Method Based on File Format Constraint [一种针对格式文件的符号执行优化方法]

作者：Wang S.-L.^*; Yang Q.-S.; Li M.-S.

来源：Acta Electronica Sinica, 2020, 48(12): 2417-2424.

DOI：10.3969/j.issn.0372-2112.2020.12.018

• Bug finding
• File format constraint
• Path explosion
• Symbolic execution

To solve problems like path explosion, low rate of new path's finding in the software testing, a new vulnerability discovering architecture based on file format constraint (FFCBSE) was proposed. FFCBSE analyzed program source code to extract file structure constraints automatically. FFCBSE then used these structure constraints to guide symbolic execution to focus on core functions. This architecture was implemented in KLEE, and it was evaluated on seven file processing applications, such as Tcpdump, Readelf, File, Zlib. Compare with KLEE and DASE, FFCBSE detects thirteen previously unknown bugs. In addition, FFCBSE increases instruction line coverage/branch coverage by 10%~ 225%.

• 单位
  中国科学院大学