计算机科学 ›› 2026, Vol. 53 ›› Issue (6A): 250600035-7.doi: 10.11896/jsjkx.250600035

• 信息安全 • 上一篇    下一篇

基于符号执行的二进制漏洞自动验证方法

张媛媛1, 刘铁铭2, 刘国安2, 葛学帅2   

  1. 1 中国人民解放军第32738部队 郑州 450001
    2 信息工程大学 郑州 450001
  • 出版日期:2026-06-16 发布日期:2026-06-12
  • 通讯作者: 葛学帅(2091948556@qq.com)
  • 作者简介:(ZhengzhouZhangyy@163.com)
  • 基金资助:
    国家自然科学基金(62276091);河南省重大公益项目(201300311200)

Symbolic Execution-based Automated Verification Method for Binary Vulnerabilities

ZHANG Yuanyuan1, LIU Tieming2, LIU Guoan2, GE Xueshuai2   

  1. 1 Unit 32738 of the Chinese People's Liberation Army,Zhengzhou 450001,China
    2 Information Engineering University,Zhengzhou 450001,China
  • Published:2026-06-16 Online:2026-06-12
  • About author:ZHANG Yuanyuan,born in 1979,senior engineer.Her main research interests include computer science and technology and information systems.
    GE Xueshuai,born in 1997,postgraduate.His main research interests include binary vulnerability mining and automated exploitation of vulnerabilities.
  • Supported by:
    National Natural Science Foundation of China(62276091) and Major Public Welfare Projects in Henan Province(201300311200).

摘要: 随着软件系统应用的逐渐广泛,二进制漏洞数量持续增长,严重威胁着信息安全。现有研究缺乏能够有机整合漏洞检测、根源分析与自动化利用的综合解决方案,导致漏洞验证效率低下且覆盖范围有限。该研究旨在提出一种自动化、跨架构的二进制漏洞验证方法,实现从漏洞检测、根源定位到利用生成的全流程集成,并生成结构化验证报告。设计了一个基于符号执行的自动化验证框架,其包含预处理、漏洞检测、根源分析、利用生成与验证5个组件,采用脆弱点导向与路径引导相结合的符号执行策略,结合污点分析与约束求解,支持多架构分析。在14个测试样本上的验证表明,该方法成功检测出栈溢出、堆溢出、UAF、格式化字符串等漏洞类型,准确定位漏洞根源至基本块粒度,并实现了多数样本的自动化利用生成。该研究不仅提升了二进制漏洞验证的自动化程度与准确性,还为漏洞修复与防御提供了可靠依据,未来将进一步优化堆漏洞利用生成与大型应用程序的验证能力,并探索自动化修复技术。

关键词: 漏洞自动验证, 漏洞检测, 漏洞根源分析, 漏洞利用, 符号执行

Abstract: With the widespread application of software systems,the number of binary vulnerabilities continues to grow,posing serious threats to information security.Existing research lacks comprehensive solutions that organically integrate vulnerability detection,root cause analysis,and automated exploitation,resulting in inefficient and limited-coverage vulnerability verification.This study aims to propose an automated,cross-architecture binary vulnerability verification method that integrates the entire process from vulnerability detection and root cause localization to exploit generation,while producing structured verification reports.It designs an automated verification framework based on symbolic execution,which consists of five components:preprocessing,vulnerability detection,root cause analysis,exploit generation,and verification.By combining vulnerability-oriented and path-guided symbolic execution strategies with taint analysis and constraint solving,the framework supports multi-architecture analysis.Validation on 14 test samples demonstrate that the proposed method successfully detects various types of vulnerabilities including stack overflow,heap overflow,use-after-free(UAF),and format string vulnerabilities,accurately locates root causes at the basic-block level,and achieves automated exploit generation for most samples.This research not only enhances the automation and accuracy of binary vulnerability verification but also provides a reliable basis for vulnerability remediation and defense.Future work will focus on improving heap vulnerability exploit generation,expanding verification capabilities for large-scale applications,and exploring automated repair techniques.

Key words: Automated vulnerability verification, Vulnerability detection, Vulnerability root cause analysis, Exploitation of vulnera-bilities, Symbolic execution

中图分类号: 

  • TP309
[1] National information security vulnerability sharing platform.Data statistics[EB/OL].https://www.cnvd.org.cn/flaw/statistic.
[2] IBM Security.X-Force Threat Intelligence Index 2025[EB/OL].https://www.ibm.com/reports/threat-intelligence.
[3] BEAMAN C,REDBOURNE M,MUMMERY J D,et al.Fuzzing vulnerability discovery techniques:Survey,challenges and future directions[J].Computers & Security,2022,120:102813.
[4] RUARO N,ZENG K,DRESEL L,et al.SyML:Guiding symbolicexecution toward vulnerable states through pattern learning[C]//Proceedings of the 24th International Symposium on Research in Attacks,Intrusions and Defenses.2021:456-468.
[5] ZHANG Y,WANG J,BERZIN D,et al.Fixing Security Vulnerabilities with AI in OSS-Fuzz[J].arXiv:2411.03346,2024.
[6] JIANMING F,JING C,GUOJUN P.PVDF:An automaticpatch-based vulnerability description and fuzzing method[C]//Communication Security Conference(CSC 2014).2014:1-8.
[7] STEPHENS N,GROSEN J,SALLS C,et al.Driller:Augmenting fuzzing through selective symbolic execution[C]//NDSS.2016:1-16.
[8] YAO S,SHE D.Empc:Effective Path Prioritization for Symbolic Execution with Path Cover[C]//Proceedings of the 2025 IEEE Symposium on Security and Privacy(SP).IEEE,2025.
[9] NASHID N,DING D,GALLABA K,et al.Characterizing Multi-Hunk Patches:Divergence,Proximity,and LLM Repair Challenges[C]//Proceedings of the 40th IEEE/ACM International Conference on Automated Software Engineering(ASE).IEEE,2025:1629-1641.
[10] BLAZYTKO T,SCHLÖGEL M,ASCHERMANN C,et al.AURORA:Statistical crash analysis for automated root cause explanation[C]//Proceedings of the 29th USENIX Conference on Security Symposium.2020:235-252.
[11] XU J,MU D,XING X,et al.Postmortem Program Analysis with Hardware-Enhanced Post-Crash Artifacts[C]//USENIX Security Symposium.2017:17-32.
[12] BRUMLEY D,POOSANKAM P,SONG D,et al.Automaticpatch-based exploit generation is possible:Techniques and implications[C]//2008 IEEE Symposium on Security and Privacy(sp 2008).IEEE,2008:143-157.
[13] AVGERINOS T,CHA S K,REBERT A,et al.Automatic exploit generation[J].Communications of the ACM,2014,57(2):74-84.
[14] YILMAZ F,SRIDHAR M,CHOI W.Guide me to exploit:Assisted ROP exploit generation for ActionScript virtual machine[C]//Annual Computer Security Applications Conference.2020:386-400.
[15] LIU D,WANG P,ZHOU X,et al.ERACE:Toward Facilitating Exploit Generation for Kernel Race Vulnerabilities[J].Applied Sciences,2022,12(23):1-12.
[16] JIANG Z,ZHANG Y,XU J,et al.AEM:Facilitating Cross-Version Exploitability Assessment of Linux Kernel Vulnerabilities[C]//2023 IEEE Symposium on Security and Privacy(SP).IEEE Computer Society,2022:588-603.
[17] BUI Q C,IANNONE E,CAMPORESE M,et al.A Systematic Literature Review on Automated Exploit and Security Test Generation[J].arXiv:2502.04953,2025.
[18] CHA S K,AVGERINOS T,REBERT A,et al.Unleashing mayhem on binary code[C]//2012 IEEE Symposium on Security and Privacy.IEEE,2012:380-394.
[19] 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.IEEE,2012:78-87.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!