基于符号执行的二进制代码漏洞发现

计算机科学 ›› 2013, Vol. 40 ›› Issue (10): 119-121.

基于符号执行的二进制代码漏洞发现

牛伟纳,丁雪峰,刘智,张小松

电子科技大学计算机科学与工程学院成都 611731;四川大学信息管理中心成都 610065;电子科技大学计算机科学与工程学院成都 611731;电子科技大学计算机科学与工程学院成都 611731

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本文受四川省科技计划支撑项目(2012GZ0001),上海市科研计划项目(11511505300)资助

Vulnerability Finding Using Symbolic Execution on Binary Programs

NIU Wei-na,DING Xue-feng,LIU Zhi and ZHANG Xiao-song

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

摘要： 软件漏洞是安全问题的根源之一,fuzzing(模糊测试)是目前漏洞发现的关键技术,但是它通过随机改变输入无法有效地构造出测试用例,也无法消除测试用例的冗余性。为了克服传统fuzzing测试的缺点、有效生成测试输入且无需分析输入格式,针对二进制程序设计并实现了基于符号执行的漏洞发现系统SEVE。将程序的输入符号化,利用动态插桩工具建立符号变量的传播关系；在分支语句处收集路径约束条件,最后用解析器求解之并将其作为新的测试用例。用mp3和pdf 软件进行了实验,结果表明,该系统有效地提高了漏洞发现的效率与自动化程度。

关键词: 漏洞,二进制程序,符号执行,插桩,路径约束

Abstract: Software vulnerability is one main source of computer safety issues,and the key technology of vulnerabilities finding is fuzzing(fuzzy test)which is based on randomly changing the input,however,it cannot construct test cases effectively and eliminate the redundancy of test cases．In order to overcome the shortcomings of traditional fuzzing test,effectively generate test inputs and do not need to analyze the input format,we designed and implemented vulnerability found system(called SEVE) based on symbolic execution for binary program．SEVE makes the inputs symbolic and uses dynamic instrumentation tools to establish the propagation relationship of the symbolic variable,collect path constraints in branch statement,uses interpreter to solve these path constraints to obtain test cases．Experimental results which are based on mp3and pdf software show that the system can improve the efficiency and the degree of automation of vulnerability discovery.

Key words: Vulnerability,Binary program,Symbolic execution,Instrumentation,Path constraint

牛伟纳,丁雪峰,刘智,张小松. 基于符号执行的二进制代码漏洞发现[J]. 计算机科学, 2013, 40(10): 119-121. https://doi.org/

NIU Wei-na,DING Xue-feng,LIU Zhi and ZHANG Xiao-song. Vulnerability Finding Using Symbolic Execution on Binary Programs[J]. Computer Science, 2013, 40(10): 119-121. https://doi.org/

参考文献

[1] 王彤彤,韩文报,王航.基于安全需求的软件漏洞分析模型[J].计算机科学,2007,34(9):287-289
[2] 毛澄映,卢炎生,胡小华．数据挖掘技术在软件工程中的应用综述[J].计算机科学,2009,6(5):1-6
[3] Brumley D,Poosankam P,et al．Automatic patch-based exploit generation is possible:techniques and implications[C]∥ SP’08:Proceedings of the IEEE Security and Privacy Symposium．NJ:IEEE,2008:143-157
[4] 宋超臣,黄俊强,等．计算机安全漏洞检测技术综述[J]．技术研究,2012,1:77-79
[5] 吴志勇,王红川,等．Fuzzing技术综述[J].计算机应用研究,2010,7(3):829-832
[6] Miller B P,Fredriksenl．An empirical Study of the reliability of UNIX utilities [J]．Communications of the ACM,1990,33(12):32-44
[7] Miller Barton P,Gergogy C,Fresrick M．An empirical study of the robustness of MacOS applications using random testing[C]∥Proceedings of the 1st International Workshop on Random Testing．New York:ACM,2006:46-54
[8] 陈衍铃,赵静.基于虚拟化技术的动态污点分析[J].计算机应用,2011,1(9):2367-2372
[9] Cowbc,Pu C,et al．StackGuard:Automatic adaptive detectionand prevention of buffer-overflow attacks[C]∥Proceedings of the 7th conference on USENIX Security Symposium．Berkeley,1998:5-13
[10] King J C．Symbolic execution and program testing[C]∥Communications of the ACM.1976:385-394
[11] 过辰楷,姬秀娟,许静.基于分支混淆算法的符号执行技术 [J].计算机科学,2012,9(9):115-119
[12] Cadar C,Ganesh V,et al．EXE:Automatically generating inputs of death[C]∥CCS’06:Proceedings of the 13th ACM Confe-rence on Computer and Communications Security．New York:ACM,2006:322-335
[13] Luk C-K,Robert C,et al．Pin:building customized program an-alysis tools with dynamic instrumentation[C]∥PLDI05:Procee-dings of the ACM SIGPLAN Conference on Programming Language Design and Implementation．New York:ACM,2005:190-200
[14] De Moura,Leonardo,Bjrner,et al.Z3:an efficient SMT Solver[C]∥TACAS:Proceedings 14th International Conference．Berlin:Springer,2008:337-340
[15] 魏瑜豪,张玉清．基于fuzzing的MP3播放软件漏洞发掘技术[J].计算机工程,2007,33(24):158-167

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed