ReChecker:基于模型检测的智能合约重入漏洞检测方法

来源：计算机集成制造系统杂志2026年第3期北京时间：

作者：柴新卓, 刘国玺, 李乐成, 代飞, 黄苾

单位：西南林业大学大数据与智能工程学院

摘要：智能合约的重入漏洞检测是保障其安全性的重要技术手段之一。现有基于符号执行、模糊测试和模型检测方法,只考虑了无锁智能合约,未考虑有锁智能合约的重入漏洞检测。有效建模智能合约并定义重入漏洞的安全性质具有挑战性。本文提出了一种基于模型检测的智能合约重入漏洞检测方法(ReChecker),将智能合约细分为有锁智能合约和无锁智能合约,结合检查-生效-交互模式(CEI)和锁机制,实现对智能合约重入漏洞的自动检测。首先,基于抽象语法树(AST),将智能合约源代码建模为标号迁移系统(LTS);其次,从执行顺序和访问控制视角,使用线性时序逻辑(LTL)公式分别定义了基于CEI模式和基于锁机制的重入漏洞安全性质;然后,在进程分析工具(PAT)的支持下,自动化地检测了有锁智能合约和无锁智能合约是否会发生重入漏洞。最后,为了验证所提方法的有效性,在3个数据集上进行了实验,实验结果表明:相比5种基准方法,ReChecker的准确率平均提升了10.83%,漏报率和误报率平均降低了12%和17.5%。

关键词：智能合约,重入漏洞,模型检测,抽象语法树,标号迁移系统,线性时序逻辑

基金资助：国家自然科学基金资助项目(62262063);云南省基础研究计划资助项目 (202501AS070046);云南省重点研发计划资助项目(202402AD080002-5);云南省高校服务重点产业科技项目(FWCY-ZNT2024020);云南省窦万春专家工作站资助项目(202105AF150013);云南省“兴滇英才支持计划”产业创新人才资助项目(XDYC-CYCX-2022-0009);云南省科协青年科技人才托举工程资助项目;教育部重点实验室开放基金资助项目(EIN2024C004)。