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

doi:10.3969/j.issn.0372-2112.2020.12.018

电子学报 ›› 2020, Vol. 48 ›› Issue (12): 2417-2424.DOI: 10.3969/j.issn.0372-2112.2020.12.018

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

汪孙律^1,2, 杨秋松¹, 李明树¹

1. 中国科学院软件研究所基础软件国家工程研究中心, 北京 100190;
2. 中国科学院大学计算机科学与技术学院, 北京 101408

收稿日期:2019-09-04 修回日期:2020-11-04 出版日期:2020-12-25
- 通讯作者:
- 汪孙律
- 作者简介:
- 李明树 男,1966年5月出生,吉林德惠人,博士,中国科学院软件研究所研究员、博士生导师,主要究方向是:操作系统与基础软件,软硬件协同设计,以及软件工程方法和软件过程技术等;杨秋松 男,1977年8月出生,河北泊头人,博士,中国科学院软件研究所研究员、博士生导师,主要研究方向是:软件工程、形式化方法、模型检测、安全操作系统.
- 基金资助:
- 中国科学院战略性先导科技专项 (No.XDA-Y01-01）

A Symbolic Execution Optimization Method Based on File Format Constraint

WANG Sun-lü^1,2, YANG Qiu-song¹, LI Ming-shu¹

1. NFS, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China;
2. School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing 101408, China

Received:2019-09-04 Revised:2020-11-04 Online:2020-12-25 Published:2020-12-25
- Corresponding author:
- WANG Sun-lü
- Supported by:
- Chinese Academy of Sciences Strategic Pilot Project (No.XDA-Y01-01)

摘要/Abstract

摘要： 为了解决符号执行中路径爆炸、新路径发现率低等问题，提出了针对文件格式数据块约束的符号执行分析方法（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%.

Key words: symbolic execution, file format constraint, path explosion, bug finding

中图分类号:

TP311

. 一种针对格式文件的符号执行优化方法[J]. 电子学报, 2020, 48(12): 2417-2424.

. A Symbolic Execution Optimization Method Based on File Format Constraint[J]. Acta Electronica Sinica, 2020, 48(12): 2417-2424.

参考文献

[1] Wang M,Liang J,Chen Y,et al.SAFL:Increasing and accelerating testing coverage with symbolic execution and guided fuzzing[A].Proceedings of the 40th International Conference on Software Engineering:Companion Proceeedings[C].Gothenburg Sweden:IEEE Computer Society,2018.61-64.
[2] Corteggiani N,Camurati G,Francillon A.Inception:system-wide security testing of real-world embedded systems software[A].27th USENIX Conference on Security Symposium[C].Baltimore,MD:USENIX Association,2018.309-326.
[3] Mechtaev S,Nguyen M D,Noller Y,et al.Semantic program repair using a reference implementation[A].Proceedings of the 40th International Conference on Software Engineering[C].Gothenburg Sweden:IEEE Computer Society,2018.129-139.
[4] Wong E,Zhang L,Wang S,et al.DASE:Document-assisted symbolic execution for improving automated software testing[A].2015 IEEE/ACM 37th IEEE International Conference on Software Engineering[C].Florence Italy:IEEE Computer Society,2015.620-631.
[5] Cadar C,Dunbar D,Engler D R.KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs[A]. 8th USENIX Symposium on Operating Systems Design and Implementation,OSDI 2008[C].San Diego,California:USENIX Association,2008.209-224.
[6] 杨超,郭云飞,扈红超,等.基于符号执行的软件缓存侧信道脆弱性检测技术[J].电子学报,2019,47(6):1194-1200. YANG Chao,GUO Yun-fei,et al.Cache-based side-channel vulnerability detection based on symbolic execution[J].Acta Electronica Sinica,2019,47(6):1194-1200.(in Chinese)
[7] 赵祖威,冯世宁,汤恩义,等.一种符号执行制导的循环内界分析方法[J].电子学报,2017(11):16-26. ZHAO Zu-wei,FENG Shi-ning,et al.A symbolic execution guided inner loop bound analysis[J].Acta Electronica Sinica,2017(11):16-26.(in Chinese)
[8] 徐超,陈勇,葛红美,等.基于符号执行的能耗错误检测方法[J].电子学报,2016,44(5):1040-1050. XU Chao,CHEN Yong,GE Hong-mei,et al.Symbolic execution based energy bug detecting method[J].Acta Electronica Sinica,2016,44(5):1040-1050.(in Chinese)
[9] Trabish,David,Mattavelli,Andrea,Rinetzky,Noam,et al.Chopped symbolic execution[A].Proceedings of the 40th International Conference on Software Engineering:Companion Proceeedings[C].Gothenburg Sweden:IEEE Computer Society,2018.350-360.
[10] Palikareva H,Kuchta T,Cadar C.Shadow of a doubt:testing for divergences between software versions[A].IEEE/ACM International Conference on Software Engineering[C].Austin,TX:IEEE,2016.1181-1192.
[11] Marinescu P D,Cadar C.KATCH:high-coverage testing of software patches[A].Proceedings of the 20139th Joint Meeting on Foundations of Software Engineering[C].Saint Petersburg Russia:ACM,2013.235-245.
[12] 甘水滔,王林章,谢向辉,等.一种基于程序功能标签切片的制导符号执行分析方法[J].软件学报,2019,30(11):3259-3280.

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

A Symbolic Execution Optimization Method Based on File Format Constraint

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 6

编辑推荐

Metrics

[1]	杨超, 郭云飞, 扈红超, 刘文彦, 霍树民, 王亚文. 基于符号执行的软件缓存侧信道脆弱性检测技术[J]. 电子学报, 2019, 47(6): 1194-1200.
[2]	郭曦, 王盼. 基于依赖条件重构的程序符号值分析方法[J]. 电子学报, 2019, 47(3): 630-635.
[3]	赵祖威, 冯世宁, 汤恩义, 陈鑫, 李宣东, 潘敏学, 赵晨. 一种符号执行制导的循环内界分析方法[J]. 电子学报, 2017, 45(11): 2582-2592.
[4]	徐超, 陈勇, 葛红美, 何炎祥. 基于符号执行的能耗错误检测方法[J]. 电子学报, 2016, 44(5): 1040-1050.
[5]	王志, 贾春福, 刘伟杰, 王晓初, 张海宁, 于晓旭, 陈喆. 一种抵抗符号执行的路径分支混淆技术[J]. 电子学报, 2015, 43(5): 870-878.
[6]	万勇兵, 徐中伟, 梅萌. 一种符号化执行的实时系统一致性测试生成方法[J]. 电子学报, 2013, 41(11): 2276-2284.