Page 357 - 《软件学报》2026年第1期
P. 357

354                                                        软件学报  2026  年第  37  卷第  1  期


                 用, 一旦该合约被恶意利用, 用户的代币可能会被完全提走.
                  2.2.4    治理漏洞
                    在去中心化治理中, 项目通常会发行治理代币, 持有这些代币的用户可以参与投票, 决定项目的参数更改、资
                 金分配以及重要协议升级. 一般而言, 治理提案会依据代币持有者的投票结果来决定是否通过. 治理攻击正是指利
                 用该机制的漏洞来影响投票过程来达成攻击目的. 例如                   2022  年  4  月  17  日, DeFi 项目  Beanstalk Farms 被盗取
                 1.82  亿美元, 原因是一名攻击者以闪电般的速度进行了恶意收购, 购买了代币的控股权, 并立即投票决定将所有资
                 金都发给自己     [99] .
                    治理攻击    [100] 的手段包括代币囤积、恶意提案和治理篡改等. 代币囤积是指攻击者在短时间内购买大量的治
                 理代币, 以增加自己的投票权, 确保在关键提案上占据主导地位. 恶意提案是指攻击者通过提交对自己有利的提
                 案, 例如将项目资金转移到自己的地址、修改协议中的关键参数, 并且可以利用囤积的治理代币确保提案通过. 治
                 理篡改是指攻击者试图改变治理规则本身.

                  3   智能合约与   DeFi 协议漏洞检测方法

                    本节针对智能合约层和         DeFi 协议层的漏洞分别进行检测方法的介绍. 在智能合约层, 由于该领域的漏洞类型
                 相对明确且检测技术较为成熟, 现有方法已能有效覆盖多种漏洞类型. 因此, 本文重点关注基于深度学习和大型语
                 言模型等新兴检测方法的研究进展. 在            DeFi 协议层, 由于漏洞类型之间差异较大, 大多数检测方法只能针对一种
                 漏洞类型. 值得注意的是, 部分重要         DeFi 协议漏洞类型    (如治理漏洞) 仍缺乏有效的检测手段, 亟待进一步研究突破.
                  3.1   智能合约层漏洞检测方法

                    本节在前期智能合约漏洞检测技术及相关综述的基础上                    [18,25] , 将智能合约层漏洞检测方法归纳为       4  类: 静态
                 分析方法、模糊测试方法、基于深度学习的方法和基于                   LLM  的方法. 随后, 分别对传统智能合约漏洞检测方法和
                 基于  LLM  的智能合约漏洞检测方法进行总结, 并深入分析              LLM  在智能合约漏洞检测领域的发展潜力.
                  3.1.1    静态分析方法
                    由于形式化验证、符号执行、污点分析以及基于中间表示的核心检测功能均在程序未执行的状态下进行, 本
                 文将其统一归类为静态分析方法. 本节将重点阐述这些技术的定义与原理, 并直观展示其在漏洞检测中的具体应
                 用. 智能合约漏洞检测的静态分析方法工作流程如图                 4  所示.

                                                                         分析方法
                                    代码建模                         形式化验证           符号执行
                              形式         F*                    系统模型    验证    符号化     搜集路
                                                                              变量
                                                                                     径约束
                              化语        KEVM
                               言      LLVM bitcode             形式规约           约束    探索可执
                                                    预定规则                      求解     行路径
                                            SSA
                                     SlithIR
                              中间    EthIR  LLVM-IR                                              处理分析结果
                              表示
                 智能合约                 XML 解析树                     污点分析           中间表示
                                     控制流图 (CFG)
                              依赖    状态依赖图 (SDG)                数据流     传播    合约中间表示
                               图    程序依赖图 (PDG)                跟踪      路径              ࢲ ݔ
                                                                       分析    漏洞检测逻辑
                                             图 4 智能合约静态分析方法工作流程

                  3.1.1.1    形式化验证
                    形式化验证是一种通过数学证明确保系统行为符合预期的技术, 近年来已广泛应用于智能合约的安全性和功
                 能正确性验证. 智能合约的形式化验证旨在通过严谨的数学方法排查潜在漏洞, 确保合约在各类场景中的安全性
                 和可靠性   [101] .
                    Bhargavan  等人  [102] 于  2016  年在 PLAS 会议上提出基于形式化验证的框架, 专门用于验证智能合约的安全性
                 和功能正确性. 该框架通过将智能合约翻译为              F  语言  (F*), 在源代码和字节码级别进行形式化分析. 研究团队开发
   352   353   354   355   356   357   358   359   360   361   362