软件学报

作者：杨慧文，崔展齐，陈翔，郑丽伟，刘建宾

单位：杨慧文，北京信息科技大学 计算机学院, 北京 10010111,崔展齐，北京信息科技大学 计算机学院, 北京 10010102,陈翔，南通大学 信息科学技术学院, 江苏 南通 22601903,郑丽伟，北京信息科技大学 计算机学院, 北京 10010104,刘建宾，北京信息科技大学 计算机学院, 北京 10010105

关键词：智能合约;符号执行;目标制导测试;安全漏洞检测;安全漏洞复现

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

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

来源：2025年第12期

《软件学报》期刊编辑部

查看软件学报杂志2025年第12期