Advanced Search
Volume 41 Issue 12
Dec.  2015
Turn off MathJax
Article Contents
Journal of Beijing University of Aeronautics and Astronautics  > 2015  >  41(12): 2348-2355.
CAI Jun, ZOU Peng, MA Jinxin, et al. Dynamic symbolic execution approach based on tabu search[J]. Journal of Beijing University of Aeronautics and Astronautics, 2015, 41(12): 2348-2355. doi: 10.13700/j.bh.1001-5965.2015.0164(in Chinese)
Citation: CAI Jun, ZOU Peng, MA Jinxin, et al. Dynamic symbolic execution approach based on tabu search[J]. Journal of Beijing University of Aeronautics and Astronautics, 2015, 41(12): 2348-2355. doi: 10.13700/j.bh.1001-5965.2015.0164(in Chinese)
shu

Dynamic symbolic execution approach based on tabu search

doi: 10.13700/j.bh.1001-5965.2015.0164
  • 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

  • Received Date: 23 Mar 2015
  • Rev Recd Date: 19 Jun 2015
  • Publish Date: 20 Dec 2015
    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.

     

    • FullText(HTML)
  • loading
    • References(22)
  • [1]
    Armour-Brown C,Borntraeger C,Fitzhardinge J,et al.Valgrind[EB/OL].[S.l.,s.n.][2015-05-15].
    [2]
    Ganesh V,Hansen T.STP constraint solver[EB/OL].[S.l.,s.n.](2015-04-02)[2015-05-15].
    [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].
    [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].
    [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.
    • Relative Articles
    • Supplements(0)
    • Cited By
  • 加载中

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索
    Get Citation
    PDF
    XML

    Article Metrics

    Article views(1013) PDF downloads(500) Cited by()
    Proportional views
    Related

    Copyright © Journal of Beijing University of Aeronautics and Astronautics

    Address: Editorial Department of Journal of Beijing University of Aeronautics and Astronautics, 37 Xueyuan Road, Haidian District, Beijing Post Code: 100191 Email: jbuaa@cqjj8.com

    Supported by: Beijing Renhe Information Technology Co., Ltd.    

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return