Review of Symbolic Execution Technology and Applications

doi:10.3778/j.issn.1002-8331.2209-0359

Abstract

Abstract: Symbolic execution is a program analysis technique that has the advantage of finding deep program errors by collecting constraints on program paths and generating high-coverage test cases using constraint solvers. First, the concept and development history of symbolic execution are sorted out, and the intermediate language, path search and constraint solving of symbolic execution techniques are categorized and explained from the core design of symbolic execution system. Then, it investigates the progress of existing research work, selects the most prominent security vulnerabilities, and systematically analyzes the details of the application of symbolic execution technology in terms of vulnerability exploitation and vulnerability detection. Finally, some research results are selected and analyzed according to the characteristics of symbolic execution technology, and the limitations and solutions faced by symbolic execution technology are discussed, and the future trends are foreseen.

Key words: symbolic execution, symbolic execution system, constraint solving, exploit generation, vulnerability detection

摘要： 符号执行是一种程序分析技术，通过收集程序路径上约束条件并利用约束求解器生成高覆盖率的测试用例，能发现深层次程序错误的优势。梳理了符号执行概念和发展历程，从符号执行系统核心设计切入，对符号执行技术的中间语言、路径搜索和约束求解进行分类阐述。调研现有研究工作进展，选取应用最突出的安全漏洞方面，从漏洞利用与漏洞检测上系统地分析符号执行技术应用细节。依据符号执行技术特点选取一些研究成果整理分析，探讨符号执行技术面临的局限与解决方案，并展望了未来趋势。

关键词: 符号执行, 符号执行系统, 约束求解, 漏洞利用, 漏洞检测

WU Hao, ZHOU Shilong, SHI Donghui, LI Qiang. Review of Symbolic Execution Technology and Applications[J]. Computer Engineering and Applications, 2023, 59(8): 56-72.

吴皓, 周世龙, 史东辉, 李强. 符号执行技术及应用研究综述[J]. 计算机工程与应用, 2023, 59(8): 56-72.

References

[1] ZHANG T，WANG P，GUO X.A survey of symbolic execution and its tool KLEE[J].Procedia Computer Science，2020，166：330-334.
[2] P?S?REANU C S，KERSTEN R，LUCKOW K，et al.Symbolic execution and recent applications to worst-case execution，load testing，and security analysis[J].Advances in Computers，2019，113：289-314.
[3] P?S?REANU C S，RUNGTA N.Symbolic PathFinder：symbolic execution of Java bytecode[C]//Proceedings of the IEEE/ACM International Conference on Automated Software Engineering，2010：179-180.
[4] BOUNIMOVA E，GODEFROID P，MOLNAR D.Billions and billions of constraints：whitebox fuzz testing in production[C]//2013 35th International Conference on Software Engineering（ICSE），2013：122-131.
[5] CADAR C，SEN K.Symbolic execution for software testing：three decades later[J].Communications of the ACM，2013，56（2）：82-90.
[6] 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，2011：1066-1071.
[7] KING J C.Symbolic execution and program testing[J].Communications of the ACM，1976，19（7）：385-394.
[8] SEN K.Concolic testing[C]//Proceedings of the Twenty-second IEEE/ACM International Conference on Automated Software Engineering，2007：571-572.
[9] SEN K.Concolic testing：a decade later （keynote）[C]//Proceedings of the 13th International Workshop on Dynamic Analysis，2015.
[10] CADAR C，GANESH V，PAWLOWSKI P M，et al.EXE：automatically generating inputs of death[J].ACM Transactions on Information and System Security（TISSEC），2008，12（2）：1-38.
[11] CHIPOUNOV V，GEORGESCU V，ZAMFIR C，et al.Selective symbolic execution[C]//Proceedings of the 5th Workshop on Hot Topics in System Dependability（HotDep），2009.
[12] WEN S，FENG C，MENG Q，et al.Testing network protocol binary software with selective symbolic execution[C]//2016 12th International Conference on Computational Intelligence and Security（CIS），2016：318-322.
[13] CHANDRA S，FINK S J，SRIDHARAN M.Snugglebug：a powerful approach to weakest preconditions[C]//Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation，2009：363-374.
[14] DINGES P，AGHA G.Targeted test input generation using symbolic-concrete backward execution[C]//Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering，2014：31-36.
[15] STEPHENS N，GROSEN J，SALLS C，et al.Driller：augmenting fuzzing through selective symbolic execution[C]//Proceedings of NDSS，2016：1-16.
[16] POEPLAU S，FRANCILLON A.Symbolic execution with {SymCC}：don’t interpret，compile![C]//29th USENIX Security Symposium（USENIX Security 20），2020：181-198.
[17] CADAR C，NOWACK M.KLEE symbolic execution engine in 2019[J].International Journal on Software Tools for Technology Transfer，2020：1-4.
[18] BUCUR S，URECHE V，ZAMFIR C，et al.Parallel symbolic execution for automated real-world software testing[C]//Proceedings of the Sixth Conference on Computer Systems，2011：183-198.
[19] SHOSHITAISHVILI Y，WANG R，SALLS C，et al.Sok：（state of） the art of war：offensive techniques in binary analysis[C]//2016 IEEE Symposium on Security and Privacy（SP），2016：138-157.
[20] SONG D，BRUMLEY D，YIN H，et al.BitBlaze：a new approach to computer security via binary analysis[C]//International Conference on Information Systems Security.Berlin，Heidelberg：Springer，2008：1-25.
[21] BURNIM J，SEN K.Heuristics for scalable dynamic test generation[C]//2008 23rd IEEE/ACM International Conference on Automated Software Engineering，2008：443-446.
[22] CHIPOUNOV V，KUZNETSOV V，CANDEA G.S2E：a platform for in-vivo multi-path analysis of software systems[J].ACM Sigplan Notices，2011，46（3）：265-278.
[23] CHIPOUNOV V，KUZNETSOV V，CANDEA G.The S2E platform：design，implementation，and applications[J].ACM Transactions on Computer Systems（TOCS），2012，30（1）：1-49.
[24] POEPLAU S，FRANCILLON A.Systematic comparison of symbolic execution systems：intermediate representation and its generation[C]//Proceedings of the 35th Annual Computer Security Applications Conference，2019：163-176.
[25] YUN I，LEE S，XU M，et al.{QSYM}：a practical concolic execution engine tailored for hybrid fuzzing[C]//27th USENIX Security Symposium（USENIX Security 18），2018：745-761.
[26] POEPLAUS，FRANCILLON A.SymQEMU：compilation-based symbolic execution for binaries[C]//Proceedings of NDSS，2021.
[27] 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，2005：213-223.
[28] WANG H，LIU T，GUAN X，et al.Dependence guided symbolic execution[J].IEEE Transactions on Software Engineering，2017，43（3）：252-271.
[29] BARDIN S，BAUFRETON P，CORNUET N，et al.Binary-level testing of embedded programs[C]//2013 13th International Conference on Quality Software，2013：11-20.
[30] DAVID R，BARDIN S，TAT D，et al.BINSEC/SE：a dynamic symbolic execution toolkit for binary-level analysis[C]//2016 IEEE 23rd International Conference on Software Analysis，Evolution，and Reengineering（SANER），2016：653-656.
[31] CHEN Z，CHEN Z，SHUAI Z，et al.Synthesize solving strategy for symbolic execution[C]//Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis，2021：348-360.
[32] GIANTSIOS A，PAPASPYROU N，SAGONAS K.Concolic testing for functional languages[C]//Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming，2015：137-148.
[33] GUPTA A，MAJUMDAR R，RYBALCHENKO A.From tests to proofs[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin，Heidelberg：Springer，2009：262-276.
[34] VISHNYAKOV A，FEDOTOV A，KUTS D，et al.Sydr：cutting edge dynamic symbolic execution[C]//2020 Ivannikov ISPRAS Open Conference（ISPRAS），2020：46-54.
[35] MAJUMDAR R，SEN K.Hybrid concolic testing[C]//29th International Conference on Software Engineering（ICSE’07），2007：416-426.
[36] CLAESSEN K，HUGHES J.QuickCheck：a lightweight tool for random testing of Haskell programs[C]//Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming，2000：268-279.
[37] MA K K，YIT PHANG K，FOSTER J S，et al.Directed symbolic execution[C]//International Static Analysis Symposium.Berlin，Heidelberg：Springer，2011：95-111.
[38] GERASIMOV A Y.Directed dynamic symbolic execution for static analysis warnings confirmation[J].Programming and Computer Software，2018，44（5）：316-323.
[39] PAPADAKIS M，MALEVRIS N.A symbolic execution tool based on the elimination of infeasible paths[C]//2010 Fifth International Conference on Software Engineering Advances，2010：435-440.
[40] SU T，PU G，FANG B，et al.Automated coverage-driven test data generation using dynamic symbolic execution[C]//2014 Eighth International Conference on Software Security and Reliability（SERE），2014：98-107.
[41] DONG Q，YAN J，ZHANG J，et al.A search strategy guided by uncovered branches for concolic testing[C]//2013 13th International Conference on Quality Software，2013：21-24.
[42] PARK S，HOSSAIN B M M，HUSSAIN I，et al.Carfast：achieving higher statement coverage faster[C]//Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering，2012：1-11.
[43] CREST：automatic test generation tool for C[EB/OL].（2009-03-06）[2022-05-31].https：//code.google.com/p/crest/.
[44] NOLLER Y，KERSTEN R，P?S?REANU C S.Badger：complexity analysis with fuzzing and symbolic execution[C]//Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis，2018：322-332.
[45] B?TTINGER K，ECKERT C.Deepfuzz：triggering vulnerabilities deeply hidden in binaries[C]//International Conference on Detection of Intrusions and Malware，and Vulnerability Assessment.Cham：Springer，2016：25-34.
[46] KUCHTA T，PALIKAREVA H，CADAR C.Shadow symbolic execution for testing software patches[J].ACM Transactions on Software Engineering and Methodology（TOSEM），2018，27（3）：1-32.
[47] MARINESCU P D，CADAR C.KATCH：high-coverage testing of software patches[C]//Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering，2013：235-245.
[48] LI M，CHEN Y，WANG L，et al.Dynamically validating static memory leak warnings[C]//Proceedings of the 2013 International Symposium on Software Testing and Analysis，2013：112-122.
[49] KRISHNAMOORTHY S，HSIAO M S，LINGAPPAN L.Strategies for scalable symbolic execution-driven test generation for programs[J].Science China Information Sciences，2011，54（9）：1797-1812.
[50] MOURA L，BJ?RNER N.Z3：an efficient SMT solver[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin，Heidelberg：Springer，2008：337-340.
[51] STUMP A，BARRETT C W，DILL D L.CVC：a cooperating validity checker[C]//International Conference on Computer Aided Verification.Berlin，Heidelberg：Springer，2002：500-504.
[52] Anon STP（simple theorem prover）[EB/OL].（2006-01-01）[2022-06-15].http：//sourceforge.net/projects/stp-fast-prover.
[53] ZHANG Y，CHEN Z，SHUAI Z，et al.Multiplex symbolic execution：exploring multiple paths by solving once[C]//2020 35th IEEE/ACM International Conference on Automated Software Engineering（ASE），2020：846-857.
[54] 胡浩，叶润国，张红旗，等.面向漏洞生命周期的安全风险度量方法[J].软件学报，2018，29（5）：1213-1229.
HU H，YE R G，ZHANG H Q，et al.Vulnerability life cycle oriented security risk metric method[J].Journal of Software，2018，29（5）：1213-1229.
[55] 国家信息安全漏洞库[EB/OL].（2022-05-01）[2022-10-31].http：//www.cnnvd.org.cn/web/vulreport/queryListByType.tag?qnewtype=2.
China national vulnerability database of information security[EB/OL].（2022-05-01）[2022-10-31].http：//www.cnnvd.org.cn/web/vulreport/queryListByType.tag?qnewtype=2.
[56] HUANG N，HUANG S，CHANG C.Analysis to heap overflow exploit in linux with symbolic execution[C]//IOP Conference Series：Earth and Environmental Science，2019.
[57] AVGERINOS T，CHA S K，REBERT A，et al.Automatic exploit generation[J].Communications of the ACM，2014，57（2）：74-84.
[58] CHA S K，AVGERINOS T，REBERT A，et al.Unleashing mayhem on binary code[C]//2012 IEEE Symposium on Security and Privacy，2012：380-394.
[59] HUANG S K，HUANG M H，HUANG P Y，et al.Crax：software crash analysis for automatic exploit generation by modeling attacks as symbolic continuations[C]//2012 IEEE Sixth International Conference on Software Security and Reliability，2012：78-87.
[60] ECKERT M，BIANCHI A，WANG R，et al.{HeapHopper}：bringing bounded model checking to heap implementation security[C]//27th USENIX Security Symposium（USENIX Security 18），2018：99-116.
[61] 方皓，吴礼发，吴志勇.基于符号执行的Return-to-dl-resolve利用代码自动生成方法[J].计算机科学，2019，46（2）：127-132.
FANG H，WU L F，WU Z Y.Automatic return-to-dl-resolve exploit generation method based on symbolic execution[J].Computer Science，2019，46（2）：127-132.
[62] 黄桦烽，苏璞睿，杨轶，等.可控内存写漏洞自动利用生成方法[J].通信学报，2022，43（1）：83-95.
HUANG H F，SU P R，YANG Y，et al.Automatic exploitation generation method of write-what-where vulnerability[J].Journal on Communication，2022，43（1）：83-95.
[63] PADARYAN V A，KAUSHAN V V，FEDOTOV A N.Automated exploit generation method for stack buffer overflow vulnerabilities[J].Proceedings of the Institute for System Programming of RAS（Proceedings of ISP RAS），2014，26（3）：127-144.
[64] WANG Y，ZHANG C，XIANG X，et al.Revery：from proof-of-concept to exploitable[C]//Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security，2018：1914-1927.
[65] WU W，CHEN Y，XU J，et al.{FUZE}：towards facilitating exploit generation for kernel {Use-After-Free} vulnerabilities[C]//27th USENIX Security Symposium（USENIX Security 18），2018：781-797.
[66] LIU D，WANG J，RONG Z，et al.Pangr：a behavior-based automatic vulnerability detection and exploitation framework[C]//2018 17th IEEE International Conference on Trust，Security and Privacy in Computing and Communications/12th IEEE International Conference on Big Data Science and Engineering（TrustCom/BigDataSE），2018：705-712.
[67] 王瑞鹏，张旻，黄晖，等.基于符号执行的格式化字符串漏洞自动验证方法研究[J].空军工程大学学报（自然科学版），2021，22（3）：82-88.
WANG R P，ZHANG M，HUANG H，et al.Research on automatic exploit generation method of format string vulnerability based on symbolic execution[J].Journal of Air Force Engineering University（Natural Science Edition），2021，22（3）：82-88.
[68] DIXIT S，GEETHNA T K，JAYARAMAN S，et al.AngErza：automated exploit generation[C]//2021 12th International Conference on Computing Communication and Networking Technologies，2021：1-6.
[69] GARCIA J，HAMMAD M，GHORBANI N，et al.Automatic generation of inter-component communication exploits for Android applications[C]//Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering，2017：661-671.
[70] LUO L，ZENG Q，CAO C，et al.System service call-oriented symbolic execution of Android framework with applications to vulnerability discovery and exploit generation[C]//Proceedings of the 15th Annual International Conference on Mobile Systems，Applications，and Services，2017：225-238.
[71] YANG G，HUANG J，GU G.Automated generation of event-oriented exploits in Android hybrid apps[C]//Network and Distributed System Security Symposium，2018.
[72] ZHOU M，ZENG F，ZHANG Y，et al.Automatic generation of capability leaks’ exploits for Android applications[C]//IEEE International Conference on Software Testing，Verification and Validation Workshops（ICSTW），2019：291-295.
[73] SEN K.Automated test generation using concolic testing[C]//Proceedings of the 8th India Software Engineering Conference，2015.
[74] SEN K，MARINOV D，AGHA G.CUTE：a concolic unit testing engine for C[J].ACM SIGSOFT Software Engineering Notes，2005，30（5）：263-272.
[75] DURAIBI S，ALASHJAEE A M，SONG J.A survey of symbolic execution tools[J].International Journal of Computer Science and Security（IJCSS），2019，13（6）：244-255.
[76] CADAR C，DUNBAR D，ENGLER D R.Klee：unassisted and automatic generation of high-coverage tests for complex systems programs[C]//Proceedings of OSDI，2008：209-224.
[77] P?S?REANU C S，VISSER W，BUSHNELL D，et al.Symbolic PathFinder：integrating symbolic execution with model checking for Java bytecode analysis[J].Automated Software Engineering，2013，20（3）：391-425.
[78] BRAIONE P，DENARO G，PEZZè M.JBSE：a symbolic executor for java programs with complex heap inputs[C]//Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering，2016：1018-1022.
[79] SEN K，AGHA G.CUTE and jCUTE：concolic unit testing and explicit path model-checking tools[C]//International Conference on Computer Aided Verification.Berlin，Heidelberg：Springer，2006：419-423.
[80] LUCKOW K，DIMJA?EVI? M，GIANNAKOPOULOU D，et al.JDART：a dynamic symbolic analysis framework[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin，Heidelberg：Springer，2016：442-459.
[81] CHEN T，ZHANG X，CHEN R，et al.Conpy：concolic execution engine for python applications[C]//International Conference on Algorithms and Architectures for Parallel Processing.Cham：Springer，2014：150-163.
[82] SAXENA P，AKHAWE D，HANNA S，et al.A symbolic execution framework for javascript[C]//2010 IEEE Symposium on Security and Privacy，2010：513-528.
[83] CHAUDHURI A，FOSTER J S.Symbolic security analysis of ruby-on-rails web applications[C]//Proceedings of the 17th ACM Conference on Computer and Communications Security，2010：585-594.
[84] TILLMANN N，HALLEUX J.Pex-white box test generation for .net[C]//International Conference on Tests and Proofs.Berlin，Heidelberg：Springer，2008：134-153.
[85] GODEFROID P，LEVIN M Y，MOLNAR D.SAGE：whitebox fuzzing for security testing[J].Communications of the ACM，2012，55（3）：40-44.
[86] 牛伟纳，丁雪峰，刘智，等.基于符号执行的二进制代码漏洞发现[J].计算机科学，2013，40（10）：119-121.
NIU W N，DING X F，LIU Z，et al.Vulnerability finding using symbolic execution on binary programs[J].Computer Science，2013，40（10）：119-121.
[87] LETYCHEVSKYI O.Two-level algebraic method for detection of vulnerabilities in binary code[C]//2019 10th IEEE International Conference on Intelligent Data Acquisition and Advanced Computing Systems：Technology and Applications（IDAACS），2019：1074-1077.
[88] WEN S，FENG C，MENG Q，et al.Analyzing network protocol binary software with joint symbolic execution[C]//2016 3rd International Conference on Systems and Informatics（ICSAI），2016：738-742.
[89] Online Computer Library Center.CVE details[EB/OL].（2022-05-01）[2022-10-31].https：//www.cvedetails.com/vulnerabilities-by-types.php.
[90] 肖奇学，陈渝，戚兰兰，等.堆分配大小可控的检测与分析[J].清华大学学报（自然科学版），2015，55（5）：572-578.
XIAO Q X，CHEN Y，QI L L，et al.Detection and analysis of size controlled heap allocation[J].Journal of Tsinghua University，2015，55（5）：572-578.
[91] 张超，潘祖烈，樊靖.基于符号执行的堆溢出fastbin攻击检测方法[J].计算机工程，2020，46（10）：151-158.
ZHANG C，PAN Z L，FAN J.Detection method for heap overflow fastbin attack based on symbolic execution[J].Computer Engineering，2020，46（10）：151-158.
[92] 黄宁，黄曙光，梁智超.基于符号执行的Unlink攻击检测方法[J].华南理工大学学报（自然科学版），2018，46（8）：81-87.
HUANG N，HUANG S G，LIANG Z C.Detection of unlink attack based on symbolic execution[J].Journal of South China University of Technology（Natural Science Edition），2018，46（8）：81-87.
[93] KAREEM F Q，AMEEN S Y，SALIH A A，et al.SQL injection attacks prevention system technology[J].Asian Journal of Research in Computer Science，2021，6（15）：13-32.
[94] FU X，LU X，PELTSVERGER B，et al.A static analysis framework for detecting SQL injection vulnerabilities[C]//31st Annual International Computer Software and Applications Conference（COMP SAC 2007），2007：87-96.
[95] FU X，QIAN K.SAFELI：SQL injection scanner using symbolic execution[C]//Proceedings of the 2008 Workshop on Testing，Analysis，and Verification of Web Services and Applications，2008：34-39.
[96] BISHT P，HINRICHS T，SKRUPSKY N，et al.Notamper：automatic blackbox detection of parameter tampering opportunities in web applications[C]//Proceedings of the 17th ACM Conference on Computer and Communications Security，2010：607-618.
[97] WANG D，ZHAO W B，DING Z M.Review of detection for injection vulnerability of Web application[J]Journal of Beijing University of Technology，2016，42（12）：1822-1832.
[98] HALFOND W G J，CHOUDHARY S R，ORSO A.Penetration testing with improved input vector identification[C]//2009 International Conference on Software Testing Verification and Validation，2009：346-355.
[99] LIU M，ZHANG B，CHEN W，et al.A survey of exploitation and detection methods of XSS vulnerabilities[J].IEEE Access，2019，7：182004-182016.
[100] 孙基男，潘克峰，陈雪峰，等.基于符号执行的注入类安全漏洞的分析技术[J].北京大学学报（自然科学版），2018，54（1）：1-13.
SUN J N，PAN K F，CHEN X F，et al.Static analysis of injection security vulnerabilities based on symbolic execution[J].Acta Scientiarum Naturalium Universitatis Pekinensis，2018，54（1）：1-13.
[101] 刘双印，雷墨鹥兮，王璐，等.区块链关键技术及存在问题研究综述[J].计算机工程与应用，2022，58（3）：66-82.
LIU S Y，LEI M Y X，WANG L，et al.Survey of blockchain key technologies and existing problems[J].Computer Engineering and Applications，2022，58（3）：66-82.
[102] 张弛，司徒凌云，王林章.物联网固件安全缺陷检测研究进展[J].信息安全学报，2021，6（3）：141-158.
ZHANG C，SITU L Y，WANG L Z.Research progress on security defect detection of IoT firmware[J].Journal of Cyber Security，2021，6（3）：141-158.
[103] SHAO J，VU M，ZHANG M，et al.Symbolic ns-3 for efficient exhaustive testing：design，implementation，and simulations[C]//Proceedings of the Workshop on ns-3，2022：49-56.
[104] QIANG W，LIAO Y，SUN G，et al.Patch-related vulnerability detection based on symbolic execution[J].IEEE Access，2017，5：20777-20784.
[105] FEIST J，MOUNIER L，BARDIN S，et al.Finding the needle in the heap：combining static analysis and dynamic symbolic execution to trigger use-after-free[C]//Proceedings of the 6th Workshop on Software Security，Protection，and Reverse Engineering，2016：1-12.
[106] CHEN N，KIM S.Star：stack trace based automatic crash reproduction via symbolic execution[J].IEEE Transactions on Software Engineering，2014，41（2）：198-220.
[107] SEREBRYANY K.Continuous fuzzing with libFuzzer and addressSanitizer[C]//2016 IEEE Cybersecurity Development（SecDev），2016.
[108] 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]//2010 IEEE Symposium on Security and Privacy，2010：317-331.
[109] 梅瑞，严寒冰，沈元，等.二进制代码切片技术在恶意代码检测中的应用研究[J].信息安全学报，2021，6（3）：125-140.
MEI R，YAN H B，SHEN Y，et al.Application research of slicing technology of binary executables in malware detection[J].Journal of Cyber Security，2021，6（3）：125-140.
[110] LI Y，HUANG C，WANG Z，et al.Survey of software vulnerability mining methods based on machine learning[J].Journal of Software，2020，31（7）：2040-2061.
[111] 黄桦烽，王嘉捷，杨轶，等.有限资源条件下的软件漏洞自动挖掘与利用[J].计算机研究与发展，2019，56（11）：2299-2314.
HUANG H F，WANG J J，YANG Y，et al.Automatic software vulnerability discovery and exploit under the limited resource conditions[J].Journal of Computer Research and Development，2019，56（11）：2299-2314.
[112] BALDONI R，COPPA E，D’ELIA D C，et al.A survey of symbolic execution techniques[J].ACM Computing Surveys（CSUR），2018，51（3）：1-39.
[113] BOER F S，BONSANGUE M.Symbolic execution formally explained[J].Formal Aspects of Computing，2021，33（4）：617-636.
[114] MUSTAFA A，WAN-KADIR W M N，IBRAHIM N，et al.Automated test case generation from requirements：a systematic literature review[J].Computers，Materials and Continua，2021，67（2）：1819-1833.
[115] BUSSE F，NOWACK M，CADAR C.Running symbolic execution forever[C]//Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis，2020：63-74.
[116] KAPUS T，CADAR C.A segmented memory model for symbolic execution[C]//Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering，2019：774-784.
[117] LUO S，XU H，BI Y，et al.Boosting symbolic execution via constraint solving time prediction （experience paper）[C]//Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis，2021：336-347.
[118] ZHENG P，ZHENG Z，LUO X.Park：accelerating smart contract vulnerability detection via parallel-fork symbolic execution[C]//Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis，2022：740-751.
[119] ZHENG L，LIAO X，JIN H.Efficient and scalable graph parallel processing with symbolic execution[J].ACM Transactions on Architecture and Code Optimization（TACO），2018，15（1）：1-25.
[120] SABBAGHI A，KEYVANPOUR M R.A systematic review of search strategies in dynamic symbolic execution[J].Computer Standards & Interfaces，2020，72：103444.
[121] HE J，SIVANRUPAN G，TSANKOV P，et al.Learning to explore paths for symbolic execution[C]//Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security，2021：2526-2540.
[122] TALJAARD J，GELDENHUYS J，VISSER W.Constraint caching revisited[C]//NASA Formal Methods Symposium.Cham：Springer，2020：251-266.
[123] PANDEY A，KOTCHARLAKOTA P R G，ROY S.Deferred concretization in symbolic execution via fuzzing[C]//Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis，2019：228-238.
[124] KAPUS T，BUSSE F，CADAR C.Pending constraints in symbolic execution for better exploration and seeding[C]//2020 35th IEEE/ACM International Conference on Automated Software Engineering（ASE），2020：115-126.