微信服务号

微信订阅号

2025-4-13- 2
Home > Archive>Volume 30, Issue 11, 2019 >3259-3280. DOI:10.13328/j.cnki.jos.005562
PDF HTML XML Export Cite reminder
Guiding Symbolic Execution Analysis by Leveraging Program Function Label Slice
Author:
Affiliation:

Clc Number:

TP311

Fund Project:

National Natural Science Foundation of China (91318301, 61170066, 6147179)

  • Article
    • | |
  • Metrics
    • |
  • Reference [70]
    • |
  • Related
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    This paper introduces a novel approach called OPT-SSE to speed up and scale symbolic execution-guided symbolic execution method based on program function label slice. The OPT-SSE is constituted by two parts. One part is static analysis, which decomposes the whole program execution paths by different program function label slices through establishing the mapping between function tags and program CFG. The other part is specified function tags guided rule symbolic execution, which cuts unrelated branch path timely according to specified function tags flow when taking symbolic execution analysis. Through analyzing specified function label slice or different function label slices concurrently, OPT-SSE could avoid stuck in complex cycle, which is beneficial for speeding up goal-guided process and scaling the symbolic execution. OPT-SSE is evaluated on twenty applications from ten famous open softwares, like binutils, gzip, coreutils, and so on. Through comparison with KLEE, OPT-SSE speeded up goal-guided by 4.238 times, increased the goal-guided success rate about 31%, and increased instruction coverage about 8.95%, branch coverage about 8.28%.

    Reference
    [1] Nielson F, Nielson HR, Hankin C. Principles of Program Analysis. Berlin, Heidelberg:Spriner-Verlag, 1999.
    [2] Chen TY. Adaptive random testing. In:Proc. of the Advances in Computer Science (ASIAN 2004). Berlin, Heidelberg:Spriner-Verlag, 2005.320-329.
    [3] King JC. Symbolic execution and program testing. Communications of the ACM, 1976,19(7):385-394.
    [4] Gan ST, Qin XJ, Chen ZN, Wang LZ. Software vulnerability code clone detection method based on characteristic metrics. Ruan Jian Xue Bao/Journal of Software, 2015,26(2):348-363(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4786.htm[doi:10.13328/j.cnki.jos.004786]
    [5] Qin XJ, Gan ST, Chen ZN. A static detecting technology of software code secure vulnerability based on first-order logic. SCIENTIA SINICA Informationis, 2014,44(1):108-129(in Chinese with English abstract).
    [6] Bessey A, Block K, Chelf B, et al. A few billion lines of code later:Using static analysis to find bugs in the real world. Communications of the ACM, 2010,53(2):66-75.
    [7] Cadar C, Godefroid P, Khurshid S, et al. Symbolic execution for software testing in practice:preliminary assessment. In:Proc. of the 33rd Int'l Conf. on Software Engineering. ACM Press, 2011.1066-1071.
    [8] Cadar C, Ganesh V, Pawlowski PM, et al. EXE:Automatically generating inputs of death. ACM Trans. on Information and System Security, 2006,12(2):322-335.
    [9] Cadar C, Dunbar D, Engler D. KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs. In:Proc. of the 8th USENIX Conf. on Operating Systems Design and Implementation. USENIX Association, 2008.209-224.
    [10] Reanu CS, Mehlitz PC, Bushnell DH, et al. Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In:Proc. of the 2008 Int'l Symp. on Software Testing and Analysis. 2008.15-26.
    [11] Păsăreanu CS, Rungta N. Symbolic PathFinder:Symbolic execution of Java bytecode. In:Proc. of the IEEE/ACM Int'l Conf. on Automated Software Engineering. 2010.179-180.
    [12] Saxena P, Akhawe D, Hanna S, Mao F, McCamant S, Song D. A symbolic execution framework for JavaScript. In:Proc. of the 2010 IEEE Symp. on Security and Privacy (SP). IEEE, 2010.513-528.
    [13] Bucur S, Kinder J, Candea G. Prototyping symbolic execution engines for interpreted languages. ACM SIGPLAN Notices, 2014, 49(4):239-254.
    [14] Godefroid P, Klarlund N, Sen K. Dart:Directed automated random testing. In:Proc. of the 2005 ACM SIGPLAN Conf. on Programming Language Design and Implementation. 2005.213-223.
    [15] Godefroid P, Levin MY, Molnar D. SAGE:Whitebox fuzzing for security testing. Queue, 2012,10(3):40-44.
    [16] Chipounov V, Kuznetsov V, Candea G. S2E:A platform for in-vivo multi-path analysis of software systems. ACM SIGPLAN Notices, 2011,39(1):265-278.
    [17] Chipounov V, Kuznetsov V, Candea G. The S2E platform:Design, implementation, and applications. ACM Trans. on Computer Systems, 2012,30(1):1-49.
    [18] Chipounov V, Candea G. Dynamically translating x86 to LLVM using QEMU. In:Proc. of the Dynamic Binary Translator. 2010.
    [19] Cha SK, Avgerinos T, Rebert A, et al. Unleashing mayhem on binary code. In:Proc. of the IEEE Symp. on Security & Privacy. IEEE Computer Society, 2012.380-394.
    [20] Nethercote N, Seward J. Valgrind:A framework for heavy-weight dynamic binary instrumentation. In:Proc. of the Proerence on Computer Aided Verification. 2011.
    [21] Godefroid P, Levin M, Molnar D. Automated whitebox fuzz testing. In:Proc. of the 15th Annual Network and Distributed System Security Symp. 2008.
    [22] Sen K, Marinov D, Agha G. Cute:A concolic unit testing engine for c. In:Proc. of the 10th European Software Engineering Conf., Held Jointly with 13th ACMSIGSOFT Int'l Symp. on Foundations of Software Engineering. 2005.263-272.
    [23] Nikolai T, de Halleux J. Pex-white box test generation for.NET. In:Proc. of the Tests and Proofs, Second International Conference (TAP 2008). 2008.134-153.
    [24] Kuznetsov V, Chipounov V, Candea G. Testing closed-source binary device drivers with DDT. In:Proc. of the USENIX Annual Technical Conf. 2010.4-5.
    [25] Renzelmann MJ, Kadav A, Swift MM. SymDrive:Testing drivers without devices. In:Proc. of the 10th USENIX Conf. on Operating Systems Design and Implementation. USENIX Association, 2012.279-292.
    [26] Davidson D, Moench B, Jha S, Ristenpart T. FIE on firmware:Finding vulnerabilities in embedded systems using symbolic execution. In:Proc. of the SEC 201322nd USENIX Conf. on Security. 2013.463-478.
    [27] Zaddach J, Bruno L, Francillon A, Balzarotti D. Avatar:A framework to support dynamic security analysis of embedded systems' firmwares. In:Proc. of the Network and Distributed System Security Symp. 2014.23-26.
    [28] Cadar C, Sen K. Symbolic execution for software testing:Three decades later. Communications of the ACM, 2013,56(2):82-90.
    [29] Necula GC, McPeak S, Rahul SP, Weimer W. CIL:Intermediate language and tools for analysis and transformation of C programs. In:Proc. of the 2007 ACM SIGPLAN Conf. on Programming Language Design and Implementation. New York:ACM Press, 2007.89-100.
    [30] Brumley D, Jager I, Avgerinos T, et al. BAP:A binary analysis platform. In:Proc. of the Computer Aided Verification. Berlin, Heidelberg:Spriner-Verlag, 2011.463-469.
    [31] Zhao J, Nagarakatte S, Martin MMK, Zdancewic S. Formalizing the LLVM intermediate representation for verified program transformations. In:Proc. of the 39th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL 2012). New York:ACM Press, 2012.427-440.
    [32] Vanegue J. Static binary analysis with adomain specific language. In:Proc. of the EKOPARTY 2008.2008.
    [33] Balakrishnan G, Gruian R, Reps T, Teitelbaum T. Codesurfer/X86-A platform for analyzing x86 executables. In:Proc. of the Int'l Conf. on Compiler Construction (CC 2005). 2005.250-254.
    [34] Dullien T, Porst S. REIL:A platform-independent intermediate representation of disassembled code for static code analysis. In:Proc. of the CanSecWest 2009.2009.
    [35] Xie T, Tillmann N, de Halleux P, Schulte W. Fitness-guided path exploration in dynamic symbolic execution. In:Proc. of the Annual IEEE/IFIP Int'l Conf. on Dependable Systems and Networks (DSN 2009). 2009.359-368.
    [36] Li Y, Su Z, Wang L, et al. Steering symbolic execution to less traveled paths. In:Proc. of the 2013 ACM SIGPLAN Int'l Conf. on Object Oriented Programming Systems Languages & Applications (OOPSLA 2013). 2013.19-32.
    [37] Romano A, Engler D. Expression reduction from programs in a symbolic binary executor. In:Proc. of the Model Checking Software. Berlin, Heidelberg:Spriner-Verlag, 2013.301-319.
    [38] Zhang YF, Chen ZB, Wang J. S2PF:Speculative symbolic PathFinder. ACM Sigsoft Software Engineering Notes, 2012,37(6):1-5.
    [39] Qin XJ, Zhou L, Chen ZN, Gan ST. Software vulnerable trace's solving algorithm based on lazy symbolic execution. Chinese Journal of Computers, 2015,38(11):2290-2230(in Chinese with English abstract).
    [40] Li Y, Cheung SC, Zhang X, et al. Scaling up symbolic analysis by removing z-equivalent states. ACM Trans. on Software Engineering & Methodology, 2014,23(4):1-32.
    [41] Bugrara S, Engler D. Redundant state detection for dynamic symbolic execution. In:Proc. of the USENIX Annual Technical Conf. 2013.199-211.
    [42] Agrawal H, Horgan JR. Dynamic program slicing. ACM Sigplan Notices, 1990,25(6):246-256.
    [43] Hansen T, Schachte P, Søndergaard H. State joining and splitting for the symbolic execution of binaries. In:Proc. of the Runtime Verification. Berlin, Heidelberg:Spriner-Verlag, 2009.76-92.
    [44] Boonstoppel P, Cadar C, Engler D. RWset:Attacking path explosion in constraint-based test generation. In:Proc. of the Theory and Practice of Software, 14th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg:Springer-Verlag, 2008.351-366.
    [45] Kuznetsov V, Kinder J, Bucur S, et al. Efficient state merging in symbolic execution. In:Proc. of the ACM SIGPLAN 2012 Conf. on Programming Language Design and Implementation (PLDI 2012). 2012.193-204.
    [46] Le W. Segmented symbolic analysis. In:Proc. of the 201335th Int'l Conf. on IEEE Software Engineering. 2013.212-221.
    [47] Ramos DA, Engler D. Under-constrained symbolic execution:Correctness checking for real code. In:Proc. of the 201524th USENIX Conf. on Security Symp. 2015.49-64.
    [48] Ramos DA, Engler DR. Practical, low-effort equivalence verification of real code. In:Proc. of the Computer Aided Verification. Berlin, Heidelberg:Spriner-Verlag, 2011.669-685.
    [49] Sinha N, Wang C. Staged concurrent program analysis. In:Proc. of the 18th ACM Sigsoft Int'l Symp. on Foundations of Software Engineering. ACM Press, 2010.47-56.
    [50] Zamfir C, Candea G. Execution Synthesis:A technique for automated software debugging. In:Proc. of the Eurosys. 2009.321-334.
    [51] Majumdar R, Sen K. Hybrid concolic testing. In:Proc. of the 29th Int'l Conf. on Software Engineering. Washington:IEEE Computer Society, 2007.416-426.
    [52] Wong E, Zhang L, Wang S, et al. DASE:Document-assisted symbolic execution for improving automated software testing. In:Proc. of the 2015 IEEE/ACM 37th IEEE Int'l Conf. on Software Engineering (ICSE). IEEE, 2015.620-631.
    [53] Bucur S, Ureche V, Zamfir C, et al. Parallel symbolic execution for automated real-world software testing. In:Proc. of the 6th Conf. on Computer Systems. ACM Press, 2011.183-198.
    [54] Avgerinos T, Rebert A, Sang KC, et al. Enhancing symbolic execution with veritesting. In:Proc. of the ICSE 2014.2014.1083-1094.
    [55] Siddiqui JH, Khurshid S. Scaling symbolic execution using ranged analysis. ACM Sigplan Notices, 2012,47(10):523-536.
    [56] Ma KK, Phang KY, Foster JS, Hicks M. Directed symbolic execution. In:Proc. of the 18th Int'l Static Analysis Symp. (SAS). Venice:Berlin, Heidelberg:Spriner-Verlag, 2011.
    [57] Marinescu PD, Cadar C. Make test-zesti:A symbolic execution solution for improving regression testing. In:Proc. of the 2012 Int'l Conf. on Software Engineering. 2012.716-726.
    [58] Zhang Y, Clien Z, Wang J, et al. Regular property guided dynamic symbolic execution. In:Proc. of the 2015 IEEE/ACM 37th IEEE Int'l Conf. on Software Engineering (ICSE). IEEE, 2015.643-653.
    [59] Yang G, Person S, Rungta N, et al. Directed incremental symbolic execution. ACM Sigplan Notices, 2011,46(1):504-515.
    [60] Taneja K, Xie T, Tillmann N, et al. eXpress:Guided path exploration for efficient regression test generation. In:Proc. of the Companion ICSE. 2011.311-314.
    [61] Marinescu PD, Cadar C. High-coverage symbolic patch testing. In:Proc. of the 19th Int'l Conf. on Model Checking Software. Springer-Verlag, 2012.7-21.
    [62] Marinescu PD, Cadar C. KATCH:High-coverage testing of software patches. In:Proc. of the 20139th Joint Meeting on Foundations of Software Engineering. ACM Press, 2013.235-245.
    [63] Dijkstra EW. A Discipline of Programming. Prentice Hall, Inc., 1976.
    [64] Babic D, Martignoni L, McCamant S, Song D. Statically-directed dynamic automated test generation. In:Proc. of the 2011 Int'l Symp. on Software Testing and Analysis. ACM Press, 2011.12-22.
    [65] Guo SJ, Kusano M, Wang C, Yang ZJ, Gupta A. Assertion guided symbolic execution of multithreaded programs. In:Proc. of the ACM SIGSOFT Symp. on the Foundations of Software Engineering (FSE). 2015.
    [66] Ge X, Taneja K, Xie T, et al. DyTa:Dynamic symbolic execution guided with static verification results. In:Proc. of the Int'l Conf. on Software Engineering. 2011.992-994.
    附中文参考文献:
    [4] 甘水滔,秦晓军,陈左宁,王林章.一种基于特征矩阵的软件脆弱性代码克隆检测方法.软件学报,2015,26(2):348-363. http://www.jos.org.cn/1000-9825/4786.htm[doi:10.13328/j.cnki.jos.004786]
    [5] 秦晓军,甘水滔,陈左宁.一种基于一阶逻辑的软件代码安全性缺陷静态检测技术.中国科学:信息科学,2014,44(1):108-129.
    [39] 秦晓军,周林,陈左宁,甘水滔.基于懒符号执行的软件脆弱性路径求解算法.计算机学报,2015,38(11):2290-2230.
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

甘水滔,王林章,谢向辉,秦晓军,周林,陈左宁.一种基于程序功能标签切片的制导符号执行分析方法.软件学报,2019,30(11):3259-3280

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:January 14,2016
  • Revised:February 19,2016
  • Online: May 02,2018
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2034776Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063