Page 374 - 《软件学报》2025年第12期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2025,36(12):5755−5779 [doi: 10.13328/j.cnki.jos.007396] [CSTR: 32375.14.jos.007396] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
基于目标制导符号执行的智能合约安全漏洞检测

杨慧文 1 , 崔展齐 1 , 陈 翔 2 , 郑丽伟 1 , 刘建宾 1

1
(北京信息科技大学 计算机学院, 北京 100101)
2
(南通大学 信息科学技术学院, 江苏 南通 226019)
通信作者: 崔展齐, E-mail: czq@bistu.edu.cn

摘 要: 智能合约是运行在区块链上的计算机程序, 在扩展区块链功能、实现复杂应用的同时, 其潜在的安全漏洞
也带来巨大风险. 基于符号执行的安全漏洞检测方法具有精确度高、可生成能复现漏洞的测试用例等优势. 然而,
随着代码规模的增大, 符号执行技术容易受到路径爆炸、约束求解开销过大等问题的影响. 为此, 提出一种基于目
标制导符号执行的智能合约安全漏洞检测方法, 首先将静态分析工具或人工标注的漏洞语句作为目标, 分析目标
依赖语句, 补充事务序列以添加相关变量的符号约束. 然后, 基于智能合约字节码构建控制流图, 定位目标语句以
及目标依赖语句所在的基本块, 剪枝控制流图以生成制导信息. 最后, 根据制导信息优化符号执行的路径探索策略,
减少需要分析的基本块数量以及求解路径条件的时间, 最终高效地检测目标语句是否存在安全漏洞, 并输出可复
现漏洞的测试用例. 基于上述思路实现 Smart-Target 原型工具, 在 SB Curated 数据集上与符号执行工具 Mythril 进
行对比. 实验结果表明 Smart-Target 在安全漏洞检测和漏洞复现场景分别减少 60.76% 和 92.16% 的时间开销, 大
幅提高符号执行效率. 此外, Smart-Target 通过分析目标依赖语句使其多检测到 22.02% 的安全漏洞, 有效提升了漏
洞检测能力.
关键词: 智能合约; 符号执行; 目标制导测试; 安全漏洞检测; 安全漏洞复现
中图法分类号: TP309

中文引用格式: 杨慧文, 崔展齐, 陈翔, 郑丽伟, 刘建宾. 基于目标制导符号执行的智能合约安全漏洞检测. 软件学报, 2025, 36(12):
5755–5779. http://www.jos.org.cn/1000-9825/7396.htm
英文引用格式: Yang HW, Cui ZQ, Chen X, Zheng LW, Liu JB. Smart Contract Security Vulnerability Detection Based on Target-
guided Symbolic Execution. Ruan Jian Xue Bao/Journal of Software, 2025, 36(12): 5755–5779 (in Chinese). http://www.jos.org.cn/
1000-9825/7396.htm

Smart Contract Security Vulnerability Detection Based on Target-guided Symbolic Execution
1
1
1
2
YANG Hui-Wen , CUI Zhan-Qi , CHEN Xiang , ZHENG Li-Wei , LIU Jian-Bin 1
1
(Computer School, Beijing Information Science and Technology University, Beijing 100101, China)
2
(School of Information Science and Technology, Nantong University, Nantong 226019, China)
Abstract: Smart contracts are computer programs running on blockchain platforms, which extend the functionality of the blockchain and
enable complex applications. However, the potential security vulnerabilities of smart contracts can lead to significant financial losses.
Symbolic execution-based security vulnerability detection methods offer advantages such as high accuracy and the ability to generate test
cases that can reproduce vulnerabilities. Nevertheless, as the code size increases, symbolic execution faces challenges such as path
explosion and excessive constraint-solving overhead. To address those issues, a novel approach for detecting smart contract security
vulnerabilities through target-guided symbolic execution is proposed. First, vulnerable statements identified by static analysis tools or
manually are treated as targets. The statements that depend on these target statements are analyzed, and the transaction sequence is

* 基金项目: 江苏省前沿引领技术基础研究专项 (BK202002001); 北京信息科技大学“勤信人才”培育计划 (QXTCP B202406); 北京控制
工程研究所高可信嵌入式软件工程技术实验室开放基金 (LHCESET202307)
收稿时间: 2023-01-05; 修改时间: 2024-05-29; 采用时间: 2025-01-13; jos 在线出版时间: 2025-06-11
CNKI 网络首发时间: 2025-06-11