摘要
符号执行是一种程序分析技术,通过收集程序路径上约束条件并利用约束求解器生成高覆盖率的测试用例,能发现深层次程序错误的优势。梳理了符号执行概念和发展历程,从符号执行系统核心设计切入,对符号执行技术的中间语言、路径搜索和约束求解进行分类阐述。调研现有研究工作进展,选取应用最突出的安全漏洞方面,从漏洞利用与漏洞检测上系统地分析符号执行技术应用细节。依据符号执行技术特点选取一些研究成果整理分析,探讨符号执行技术面临的局限与解决方案,并展望了未来趋势。
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.
作者
吴皓
周世龙
史东辉
李强
WU Hao;ZHOU Shilong;SHI Donghui;LI Qiang(School of Electronic and Information Engineering,Anhui Jianzhu University,Hefei 230601,China;School of Electronic Countermeasures,National University of Defense Technology,Hefei 230037,China)
出处
《计算机工程与应用》
CSCD
北大核心
2023年第8期56-72,共17页
Computer Engineering and Applications
基金
“十四五”共用技术项目(0722-217FJ129YPF)。
关键词
符号执行
符号执行系统
约束求解
漏洞利用
漏洞检测
symbolic execution
symbolic execution system
constraint solving
exploit generation
vulnerability detection
