Symbolic Execution Optimization Methods for Specific File Structures and Key Instructions

doi:10.3969/j.issn.1671-1122.2018.09.014

Abstract

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

CLC Number:

TP309

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.

Figures/Tables 7

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