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

5768 软件学报 2025 年第 36 卷第 12 期

基本块, 蓝色节点表示由入口 (即 0 号节点) 出发到达红色或绿色节点所经过的基本块. 根据剪枝后的控制流图生
成制导信息.

0 0
13 13
65 191 65 191
76 335 203 199 76 335 203 199
412 87 343 347 1213 412 87 343 347 1213
454 420 455 98 1371 1293 424 420 455 98 1371 1293
1605 463 467 109 564 1320 1605 463 467 109 564 1320
1611 120 607 576 572 1301 1334 1611 120 607 576 572 1301 1334
1685 654 131 615 619 2235 1354 1685 654 131 615 619 2235 1354
1814 662 666 741 142 2241 1363 1814 662 666 741 142 2241 1363
1821 2260 749 753 828 153 1821 2260 749 753 828 153
1826 2333 840 836 164 972 1826 2333 840 836 164 972
1837 1833 2371 1017 175 980 984 1837 1833 2371 1017 175 980 984
2451 1029 1025 1094 186 2529 2451 1029 1025 1094 186 2529
2478 2729 1102 1106 2541 2542 2478 2729 1102 1106 2541 2542
2492 2749 2748 3099 2630 2634 2492 2749 2748 3099 2630 2634
2459 2512 2823 2459 2512 2823
2521 2828 2521 2828
2835 2839 2835 2839
图 5 图 1 所示代码片段控制流图

表 4 图 1 代码片段的定位结果

类型 行号 源代码位置 指令序号 基本块序号
72 2645:23 1904–1914 1837
漏洞语句
90 3172:30 2701–2711 2634
71 2547:88 1827–1836 1826
79 2859:38 1497–1500 1371
目标依赖语句
88 3117:19 2535–2541 2529
89 3140:28 2642–2633 2542

最后进行目标制导符号执行, 在符号执行过程中根据制导信息判断跳转基本块是否被标记为可达, 跳过与目
标语句或目标依赖语句无关的基本块. 目标制导符号执行的结果显示, 仅用时 107.4 s 即完成了安全漏洞检测, 并
成功检测出第 72 行和第 90 行的整型溢出漏洞, 检测结果与 Mythril 相同.
对比图 5(a) 和 (b) 两张子图可以看出, 符号执行仅需对红色、绿色和蓝色共 35 个 (总基本块的 30%) 基本块进行
遍历和分析, 对 28 条 (总基本块跳转的 28.6%) 路径的约束条件进行求解, 即可对该智能合约代码进行安全漏洞检测.
若直接使用 Mythril 对全部代码进行测试, 用时 560.8 s 可检测出第 72 行和第 90 行的整型溢出漏洞. 总体上
看, 本文提出的方法减少了 80.85% 的符号执行时间开销, 提高了安全漏洞检测的效率, 并成功生成了能够复现漏
洞的测试用例.

5 实验设计及评估

基于所提出方法, 我们在智能合约符号执行工具 Mythril 的基础上实现了原型工具 Smart-Target. Mythril 结合