针对特定文件结构和关键指令的符号执行优化方法

doi:10.3969/j.issn.1671-1122.2018.09.014

信息网络安全 ›› 2018, Vol. 18 ›› Issue (9): 86-94.doi: 10.3969/j.issn.1671-1122.2018.09.014

针对特定文件结构和关键指令的符号执行优化方法

陈虎¹, 周瑶¹, 赵军锁²

1.华南理工大学软件学院, 广东广州 510006
2.中国科学院软件研究所, 北京 100190

收稿日期:2018-07-17 出版日期:2018-09-30 发布日期:2020-05-11
作者简介:
作者简介：陈虎（1974—）,男,江苏,副教授,博士,主要研究方向为高性能计算、信息安全;周瑶（1995—）,男,湖北,硕士研究生,主要研究方向为自动化漏洞挖掘;赵军锁（1973—）,男,河北,研究员,硕士,主要研究方向为先进计算、智能信息处理、软件定义卫星。

Symbolic Execution Optimization Methods for Specific File Structures and Key Instructions

Hu CHEN¹, Yao ZHOU¹, Junsuo ZHAO²

1.School of Software Engineering, South China University of Technology, Guangzhou Guangdong 510006, China
2.Institute of Software, Chinese Academy of Science, Beijing 100190, China

Received:2018-07-17 Online:2018-09-30 Published:2020-05-11

摘要/Abstract

摘要：

针对符号执行面临的文件结构信息缺失和路径爆炸问题,文章分别提出了优化方法。参数固定方法维持文件结构信息字段在新生成的测试案例中为固定值,以保证文件格式的合法性。针对关键指令的剪枝方法融合了静态分析技术,确保符号执行仅产生可以覆盖关键指令的测试案例。此外,文章还提出了基于路径深度和覆盖率的测试案例选择策略和约束求解并行化两种优化方法,以提高符号执行效率。实验表明,采用文章方法可以发现原有符号执行工具不能发现的漏洞,符号执行效率提高43倍,证实了优化方法的有效性。

关键词: 符号执行, 静态分析, 约束求解

Abstract:

In view of the lack of file structure information and path explosion in symbol execution, this paper puts forward the optimization method respectively. The parameter immobilization method maintains the file structure information field as a fixed value in the newly generated test case to ensure the legality of the file format. The pruning method for key instruction that combines static analysis technology ensures symbol execution to only produce test cases that can cover key instructions. This paper also proposes two optimization methods which are test case selection strategy based on path depth and the coverage rate and constraint solving parallelization to improve the efficiency of symbol execution. Experiments show that the proposed optimization method can find vulnerabilities that the original symbolic execution tool can't detect. The efficiency of symbolic execution is increased by nearly 43 times, which confirms the effectiveness of the optimization methods.

Key words: symbolic execution, static analysis, constraint solving

中图分类号:

TP309

陈虎, 周瑶, 赵军锁. 针对特定文件结构和关键指令的符号执行优化方法[J]. 信息网络安全, 2018, 18(9): 86-94.

Hu CHEN, Yao ZHOU, Junsuo ZHAO. Symbolic Execution Optimization Methods for Specific File Structures and Key Instructions[J]. Netinfo Security, 2018, 18(9): 86-94.

图/表 7

参考文献 14

[1]	KING J C.Symbolic Execution and Program Testing[J].Communications of the ACM,1976, 19(7): 385-394.
[2]	CADAR C, Sen K.Symbolic Execution for Software Testing: Three Decades Later[J]. Communications of the ACM, 2013,56(2):82-90.
[3]	WANG Xiajing, HU Changzhen, MA Rui, et al.A Survey of the Key Technology of Binary Program Vulnerability Discovery[J].Netinfo Security,2017,17(8):1-13.
	王夏菁,胡昌振,马锐,等.二进制程序漏洞挖掘关键技术研究综述[J].信息网络安全, 2017,17(8):1-13.
[4]	SCHWARTZ E J, AVGERINOS T, BRUMLEY D.All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution(But Might Have Been Afraid to Ask)[C]//IEEE. 2010 IEEE Symposium on Security and Privacy, May 16-19, 2010, Berkeley/Oakland, CA, USA.NJ:IEEE, 2010:317-331.
[5]	SONG Zheng, WANG Yongjian, JIN Bo, et al.Review on Dynamic Taint Analysis of Binary Programs[J].Netinfo Security,2016,16(3):77-83.
	宋铮,王永剑,金波,等.二进制程序动态污点分析技术研究综述[J].信息网络安全,2016,16(3):77-83.
[6]	BRUMLEY D, JAGER I, AVERRINOS T, et al.BAP: A Binary Analysis Platform[C]//ACM. The 23rd International Conference on Computer Aided Verification, July 14 - 20, 2011, Snowbird, UT,USA. New York: ACM,2011: 463-469.
[7]	AVGERINOS T, REBERT A, BRUMLEY D, et al.Unleashing Maythem on Binary Code[C]//IEEE. 2012 IEEE Symposium on Security and Privacy, May 20-23,2012, San Francisco,CA,USA.NJ:IEEE,2012:380-394.
[8]	AVGERINOS T, REBERT A,CHA S K, et al.Enhancing Symbolic Execution with Veritesting[C]//ACM. The 36th International Conference on Software Engineering, May 31 - June 7, 2014, Hyderabad, India. New York:ACM, 2014:1083-1094.
[9]	ISAEV K, SIDOROV D V.The Use of Dynamic Analysis for Generation of Input Data that Demonstrates Critical Bugs and Vulnerabilities in Programs[J]. Programming and Computer Software, 2010,36(4):225-236.
[10]	NETHERCOTE N, SEWARD J.Valgrind: A Framework for Heavyweight Dynamic Binary Instrumentation[C]//ACM. The 28th ACM Sigplan Conference on Programming Language Design and Implementation, June 10 - 13, 2007, San Diego, California, USA. New York:ACM,2007:89-100.
[11]	PENG Jianshan, XI Qi, WANG Qingxian.Automatic Exploitation of Integer Overflow Vulnerabilities in Binary Programs[J].Netinfo Security,2017,17(5):14-21.
	彭建山,奚琪,王清贤.二进制程序整型溢出漏洞的自动验证方法[J].信息网络安全,2017,17(5):14-21.
[12]	Microsoft CabinetFormat.Microsoft[EB/OL].,2018-5-17.
[13]	Adobe Developers Association. TIFF Revision 6.0[EB/OL].,1992-6-3.
[14]	XU Weiyang, LI Yao, TANG Yong, et al.Research on Cross-architecture Vulnerabilities Searching in Binary Executables[J].Netinfo Security,2017,17(9):21-25.
	徐威扬,李尧,唐勇,等.一种跨指令架构二进制漏洞搜索技术研究[J].信息网络安全,2017,17(9):21-25.

针对特定文件结构和关键指令的符号执行优化方法

Symbolic Execution Optimization Methods for Specific File Structures and Key Instructions

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 7

参考文献 14

相关文章 11

编辑推荐

Metrics

本文评价

[1]	胡建伟, 赵伟, 闫峥, 章芮. 基于机器学习的SQL注入漏洞挖掘技术的分析与实现[J]. 信息网络安全, 2019, 19(11): 36-42.
[2]	王夏菁, 胡昌振, 马锐, 高欣竺. 二进制程序漏洞挖掘关键技术研究综述[J]. 信息网络安全, 2017, 17(8): 1-13.
[3]	彭建山, 奚琪, 王清贤. 二进制程序整型溢出漏洞的自动验证方法[J]. 信息网络安全, 2017, 17(5): 14-21.
[4]	李汶洋. Android操作系统恶意软件检测技术研究[J]. 信息网络安全, 2015, 15(9): 62-65.
[5]	张帆, 钟章队. 基于权限分析的手机恶意软件检测与防范[J]. 信息网络安全, 2015, 15(10): 66-73.
[6]	陈震;许建林;余奕凡;刘洪健. 移动网络软件架构中的安全技术研究[J]. , 2013, 13(12): 0-0.
[7]	舒心;王永伦;张鑫. 手机病毒分析与防范[J]. , 2012, 12(8): 0-0.
[8]	李向东;刘晓;夏冰;郑秋生. 恶意代码检测技术及其在等级保护工作中的应用[J]. , 2012, 12(8): 0-0.
[9]	王一岚;郭嵩. 基于静态分析的Java源代码后门检测技术研究[J]. , 2012, 12(7): 0-0.
[10]	贾菲;刘威. 基于Android平台恶意代码逆向分析技术的研究[J]. , 2012, 12(4): 0-0.
[11]	时志伟;李小军. 基于信息流分析的源代码漏洞挖掘技术研究[J]. , 2011, 11(11): 0-0.