基于目标制导符号执行的智能合约安全漏洞检测
CSTR:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

TP309

基金项目:

江苏省前沿引领技术基础研究专项(BK202002001); 北京信息科技大学“勤信人才”培育计划 (QXTCP B202406); 北京控制工程研究所高可信嵌入式软件工程技术实验室开放基金 (LHCESET202307)


Smart Contract Security Vulnerability Detection Based on Target-guided Symbolic Execution
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    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 augmented with symbolic constraints for the relevant variables. Second, the control flow graph (CFG) is constructed based on the bytecode of smart contracts, with the basic blocks containing the target statements and the dependentstatements located. The CFG is then pruned to generate guidance information. Third, path exploration in symbolic execution is optimized by reducing the number of basic blocks to be analyzed and reducing the time required for solving path constraints. With the guidance information, vulnerabilities are efficiently detected, and test cases capable of reproducing the vulnerabilities are generated. Based on this approach, a prototype tool named Smart-Target is developed. Experiments conducted on the SB Curated dataset in comparison with the symbolic execution tool, Mythril, demonstrate that Smart-Target reduces time overheads by 60.76% and 92.16% in vulnerability detection and replication scenarios, respectively. In addition, the analysis of target statementdependencies enhances vulnerability detection capability by identifying 22.02% more security vulnerabilities.

    参考文献
    相似文献
    引证文献
引用本文

杨慧文,崔展齐,陈翔,郑丽伟,刘建宾.基于目标制导符号执行的智能合约安全漏洞检测.软件学报,,():1-25

复制
相关视频

分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2023-01-05
  • 最后修改日期:2024-05-29
  • 录用日期:
  • 在线发布日期: 2025-06-11
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号