基于禁忌搜索的动态符号执行方法

蔡军; 邹鹏; 马金鑫; 何骏

doi:10.13700/j.bh.1001-5965.2015.0164

基于禁忌搜索的动态符号执行方法

doi: 10.13700/j.bh.1001-5965.2015.0164

蔡军¹,
邹鹏^1, ,,
马金鑫²,
何骏¹

1.
装备学院复杂电子系统仿真实验室, 北京 101416
2. 中国信息安全测评中心, 北京 100085

基金项目: 国家“863”计划(2012AA012902);“核高基”国家科技重大专项基金(2013ZX01045-004)

详细信息

作者简介:
蔡军(1982-),男,湖北天门人,博士研究生,cjgfkd@163.com

通讯作者:
邹鹏(1957-),男,山东高青人,教授,zpeng@nudt.edu.cn,主要研究方向为信息安全.

中图分类号: TP309
计量
- 文章访问数: 783
- HTML全文浏览量: 22
- PDF下载量: 497
- 被引次数: 0
出版历程
- 收稿日期: 2015-03-23
- 修回日期: 2015-06-19
- 网络出版日期: 2015-12-20

Dynamic symbolic execution approach based on tabu search

CAI Jun¹,
ZOU Peng^{1
, ,},
MA Jinxin²,
HE Jun¹

1.
Science and Technology on Complex Electronic System Simulation Laboratory, Academy of Equipment, Beijing 101416, China
2. China Informaiton Technology Security Evaluation Center, Beijing 100085, China

摘要

摘要: 软件漏洞是网络安全问题的根源之一,软件漏洞检测是当前网络安全领域的一个研究热点.动态符号执行是近年来研究较多的一种漏洞检测技术,针对现有动态符号执行方法在通过约束求解生成测试用例时,生成的测试用例存在大量重复或近似重复的问题,提出了一种基于禁忌搜索的动态符号执行方法,并实现了一个相应的工具原型SwordSE.该方法利用了禁忌搜索算法的全局逐步寻优能力,通过建立评价函数来优选种子文件,通过建立禁忌表来避免重复搜索.实验结果表明,SwordSE的路径搜索效率明显优于现有工具,且已发现0day漏洞4个.
- 网络安全 /
- 软件漏洞检测 /
- 禁忌搜索 /
- 动态符号执行 /
- 中间表示
Abstract: Software vulnerabilities are one of the root causes of network security problem, and software vulnerability detection is currently a hot topic in the field of network security. Dynamic symbolic execution is one of the most studied approaches for vulnerability detection recently. Aimed at the problem that existing dynamic symbolic approaches produced a large number of duplicate or near-duplicate test cases, we proposed a novel dynamic symbolic execution approach based on tabu search, and implemented a corresponding tool named SwordSE. The proposed approach took advantage of the tabu search algorithm's ability of global optimization, it can do optimized seed selection by establishing an evaluation function, and can avoid duplicate path search by establishing a tabu list. Experiment results show that SwordSE's path search efficiency is significantly better than those of existing tools, and has detected four zero-day vulnerabilities until now.
- network security /
- software vulnerability detection /
- tabu search /
- dynamic symbolic execution /
- intermediate representation

HTML全文

参考文献(22)

[1]	Armour-Brown C,Borntraeger C,Fitzhardinge J,et al.Valgrind[EB/OL].[S.l.,s.n.][2015-05-15].http://valgrind.org/.
[2]	Ganesh V,Hansen T.STP constraint solver[EB/OL].[S.l.,s.n.](2015-04-02)[2015-05-15].http://stp.github.io/.
[3]	Glover F.Tabu search—Part I[J].ORSA Journal on Computing,1989,1(3):190-206.
[4]	Glover F.Tabu search—Part II[J].ORSA Journal on Computing,1990,2(1):4-32.
[5]	百度百科.禁忌搜索算法[EB/OL].[S.l.,s.n.][2015-05-15].http://baike.baidu.com/link?url=JqehYmMCAMqByyT SESOHM4_qjLUmbDLbM7L3iX2ZSu5vQRFpQgWXDR2Q2CDAR-qdgQfD4OR-zYq5e3EvEUT_Ta. Baidu encyclopedia.Tabu search algorithm[EB/OL].[S.l.,s.n.][2015-05-15].http://baike.baidu.com/link?url=JqehYmMCAMqByyTSESOHM4_qjLUmbDLbM7L3iX2ZSu5vQRFp Qg- WXDR2Q2CDAR-qdgQfD4OR-zYq5e3EvEUT_Ta.
[6]	邢文训,谢金星.现代优化计算方法[M].第2版.北京:清华大学出版社,2005:51-58. Xing W X,Xie J X.Modern optimization methods[M].2nd ed.Beijing:Tsinghua University Press,2005:51-58.
[7]	Cadar C,Godefroid P,Khurshid S,et al.Symbolic execution for software testing in practice:Preliminary assessment[C]//Proceedings of the 33rd International Conference on Software Engineering.New York:ACM,2011:1066-1071.
[8]	Avgerinos T,Rebert A,Cha S K,et al.Enhancing symbolic execution with veritesting[C]//Proceedings of the 36th International Conference on Software Engineering.New York:ACM,2014:1083-1094.
[9]	王铁磊.面向二进制程序的漏洞挖掘关键技术研究[D].北京:北京大学,2011. Wang T L.Research on binary-executable-oriented software vulnerability detection[D].Beijing:Peking University,2011(in Chinese).
[10]	Godefroid P,Klarlund N,Sen K.Dart:Directed automated random testing[C]//Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation.New York:ACM,2005:213-223.
[11]	Sen K,Marinov D,Agha G.Cute:A concolic unit testing engine for C[C]//Proceedings of the Joint 10th European Software Engineering Conference and 13th ACM SIGSOFT Symposium on the Foundations of Software Engineering.New York:ACM,2005:263-272.
[12]	Cadar C,Ganesh V,Pawlowski P M,et al.EXE:Automatically generating inputs of death[J].ACM Transactions on Information and System Security,2008,12(2):10.
[13]	Cadar C,Dunbar D,Engler D R.KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs[C]//Proceedings of the 8th USENIX Symposium on Operating System Design and Implementation.Berkeley,CA:USENIX,2008,8:209-224.
[14]	Godefroid P,Levin M,Molnar D.Automated whitebox fuzz testing[C]//Proceedings of the 16th Annual Network and Distributed System Security Symposium.[s.l.]:The Internet Society,2008:151-166.
[15]	Sogeti ESEC Lab.Fuzzgrind[EB/OL].[S.l.,s.n.][2015-05-15].http://esec-lab.sogeti.com/pages/fuzzgrind.html.
[16]	Chipounov V,Kuznetsov V,Candea G.S2E:A platform for in-vivo multi-path analysis of software systems[J].ACM SIGARCH Computer Architecture News,2011,39(1):265-278.
[17]	Martignoni L,McCamant S,Poosankam P,et al.Path-exploration lifting:Hi-fi tests for lo-fi emulators[J].ACM SIGARCH Computer Architecture News,2012,40(1):337-348.
[18]	Moskewicz M W,Madigan C F,Zhao Y,et al.Chaff:Engineering an efficient SAT solver[C]//Proceedings of the 38th Annual Design Automation Conference.New York:ACM,2001:530-535.
[19]	Goldberg E,Novikov Y.BerkMin:A fast and robust SAT-solver[J].Discrete Applied Mathematics,2007,155(12):1549-1561.
[20]	Hamadi Y,Jabbour S,Sais L.ManySAT:A parallel SAT solver[J].Journal on Satisfiability Boolean Modeling & Computation,2009,6(4):245-262.
[21]	de Moura L,Bjørner N.Tools and algorithms for the construction and analysis of systems[M].Berlin Heidelberg:Springer,2008:337-340.
[22]	Bouton T,de Oliveira D C B,Déharbe D,et al.Automated deduction-CADE-22[M].Berlin Heidelberg:Springer,2009:151-156.