一种针对格式文件的符号执行优化方法

汪孙律; 杨秋松; 李明树

doi:10.3969/j.issn.0372-2112.2020.12.018

您当前的位置：

首页 >

文章列表页 >

一种针对格式文件的符号执行优化方法

学术论文 | 更新时间：2025-12-08

- 一种针对格式文件的符号执行优化方法
- A Symbolic Execution Optimization Method Based on File Format Constraint
- 电子学报 2020年48卷第12期页码：2417-2424
- 作者机构：
  
  1. 中国科学院软件研究所基础软件国家工程研究中心,北京,100190
  2. 中国科学院大学计算机科学与技术学院,北京,101408
  3. 中国科学院软件研究所基础软件国家工程研究中心,北京,100190
  4. 中国科学院大学计算机科学与技术学院,北京,101408
- 作者简介：
- 基金信息：
  
  中国科学院战略性先导科技专项 (No.XDA-Y01-01）
- DOI：10.3969/j.issn.0372-2112.2020.12.018
  中图分类号： TP311
- 网络出版：2020-12-25，
  
  纸质出版：2020
- 稿件说明：
移动端阅览
汪孙律, 杨秋松, 李明树. 一种针对格式文件的符号执行优化方法[J]. 电子学报, 2020,48(12):2417-2424.

WANG Sun-l, YANG Qiu-song, LI Ming-shu. A Symbolic Execution Optimization Method Based on File Format Constraint[J]. Acta Electronica Sinica, 2020, 48(12): 2417-2424.
汪孙律, 杨秋松, 李明树. 一种针对格式文件的符号执行优化方法[J]. 电子学报, 2020,48(12):2417-2424. DOI： 10.3969/j.issn.0372-2112.2020.12.018.

WANG Sun-l, YANG Qiu-song, LI Ming-shu. A Symbolic Execution Optimization Method Based on File Format Constraint[J]. Acta Electronica Sinica, 2020, 48(12): 2417-2424. DOI： 10.3969/j.issn.0372-2112.2020.12.018.

摘要

为了解决符号执行中路径爆炸、新路径发现率低等问题，提出了针对文件格式数据块约束的符号执行分析方法（FFCBSE，File Format Constraint Based Symbolic Execution）优化框架.文件格式信息的缺失会影响符号执行的效率以及测试用例生成，该方法通过分析程序代码自动分析程序读取的格式文件数据块之间的依赖关系并建立相关约束，随后使用这些约束引导符号执行更关注于核心功能代码区域.在KLEE中实现了上述优化框架，并对Tcpdump、Readelf、Elfdump、File、Zlib等7个常用文件处理程序做了检测.和KLEE以及DASE相比，FFCBSE发现了13个之前未知的缺陷，在指令覆盖率和分支覆盖率有10%~225%不同程度的提升.

Abstract

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%.

关键词

Keywords

references

浏览量

下载量

CSCD

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

提交

工具集

关联资源

一种抵抗符号执行的路径分支混淆技术

基于符号执行的能耗错误检测方法

一种符号执行制导的循环内界分析方法

基于依赖条件重构的程序符号值分析方法