Page 358 - 《软件学报》2026年第1期

揭晚晴 等: 智能合约与 DeFi 协议漏洞检测技术综述 355

了 Solidity 到 F*的翻译工具和 EVM 字节码的反编译器, 确保在不同级别上对合约进行形式化验证. 此研究为智
能合约形式化验证提供了一套完整的工具链, 奠定了该领域进一步发展的基础.
Kalra 等人 [103] 提出了 ZEUS, 在延续文献 [102] 工作的基础上, 进一步丰富了形式化验证的方法. ZEUS 结合了
抽象解释和符号模型检测, 用于智能合约的验证. 该工具通过将智能合约转换为 LLVM bitcode 的中间表示, 结合
抽象解释和符号模型检测技术进行验证. 抽象解释用于计算数据域上的循环和函数摘要, 而符号模型检测则在缩
减的状态空间中进行验证, 以确保智能合约的安全性. ZEUS 通过精确的分析和有效的状态空间缩减, 显著提升了
智能合约验证的准确性和扩展性, 特别是在处理复杂合约时表现优异.
文献 [104] 提出的 KEVM 是基于 K 框架构建的 EVM 形式化语义模型. K 框架是一种用于定义可执行语义规
范的重写系统, 研究团队通过该框架定义了 EVM 的语法、状态配置和执行规则, 构建了完整的 EVM 形式化语
义. KEVM 的创新之处在于其不仅通过了所有官方测试套件, 成为首个完整的 EVM 可执行规范, 还扩展了多种形
式化分析工具, 包括调试器、符号执行引擎和演绎验证器, 这为 EVM 的形式化分析提供了强有力的支持.
后续还有基于其他特征进行形式化验证的研究, 如基于静态程序切片框架的 HoRStify [41] . HoRStify 通过分析
程序依赖图, 捕捉智能合约中变量和节点之间的依赖关系, 并通过逻辑编码和约束霍恩子句定义安全性模式, 以验
证合约的安全属性.
3.1.1.2 符号执行
符号执行是一种在智能合约漏洞检测中广泛应用的技术, 其核心是将程序变量抽象为符号输入, 并通过模拟
程序的执行路径, 分析可能导致漏洞的输入条件 [105] .
Luu 等人 [5] 于 2016 年提出了 Oyente, 这是首个使用符号执行技术检测智能合约漏洞的工具. Oyente 直接处
理 EVM 字节码, 通过构建控制流图和执行符号状态, 利用 Z3 求解器分析路径约束, 从而检测交易顺序依赖、时
间戳依赖、异常处理不当和重入漏洞等问题. 在此基础上, Tsankov 等人 [68] 提出的 Securify 通过将 EVM 字节码反
编译为静态单赋值形式的无栈表示, 推导出语义事实, 以验证合约的安全性. 尽管 Securify 在处理数值属性推理上
有局限, 但它有效减少了用户在分类警告时的工作量, 成为智能合约安全分析中的重要工具.
后续的研究继续丰富了符号执行检测方法, 如 TEETHER [77] 和 SAILFISH [55] 系统. Krupp 等人 [77] 开发了
TEETHER, 这是首个能够自动识别智能合约漏洞并生成攻击载体的工具. TEETHER 通过逆向工程字节码, 构建控
制流图, 使用符号执行分析关键指令, 并生成可利用的攻击路径. Bose 等人 [55] 提出了 SAILFISH 系统, 专注于检测
智能合约中的状态不一致性漏洞. SAILFISH 采用混合分析方法, 通过轻量级探索阶段识别潜在漏洞, 并在精炼阶
段通过符号求解和值摘要分析验证漏洞的真实性.
3.1.1.3 污点分析
污点分析是一种程序分析技术, 旨在追踪数据从源头到达目标之间的流动情况. 在智能合约漏洞检测中的应
用, 通过标记和跟踪“污点 (可能受外部输入影响的数据)”, 污点分析可以帮助识别检测可能导致安全问题的路径 [106] .
Torres 等人 [107] 于 2018 年提出了 Osiris 工具, 专门用于检测以太坊智能合约中的整数溢出漏洞. 该工具基于
智能合约的字节码构建控制流图, 利用符号执行模拟合约的执行路径, 检测可能的整数溢出操作. 为了减少误报,
Osiris 使用污点分析技术追踪未经验证的输入 (污点) 在合约中的传播路径, 如果这些污点影响到了溢出操作, 该
操作便被标记为潜在漏洞.
Ethainter 工具 [108] 用于检测以太坊智能合约中的复合信息流漏洞. Ethainter 在信息流分析的基础上, 结合了污
点分析技术, 详细建模合约中的数据清理机制, 追踪未清理的数据在合约中的传播路径, 从而识别出可能绕过守卫
机制的漏洞. 同样是基于信息流分析, SmartACE 框架 [109] 用于验证复杂智能合约, 尤其是那些涉及大量用户的合
约. 在污点分析阶段, SmartACE 利用局部抽象技术, 有效地捕捉潜在的漏洞路径, 从而提高了合约验证的效率和精度.
后续也出现了针对特定漏洞的污点分析检测方法, 如 Ghaleb 等人 [78] 提出的 AChecker 工具, 专注于检测智能
合约中的访问控制漏洞, 尤其是那些缺乏明确访问控制策略说明的合约. AChecker 首先通过静态数据流分析识别
出合约中的访问控制检查点和相关状态变量, 然后利用跨过程的上下文敏感污点分析, 追踪用户输入对这些关键
指令或状态变量的影响.