Abstract: Ensuring the security of smart contracts against reentrancy vulnerabilities is critical,particularly for contracts with locking mechanisms,which are often overlooked by existing techniques based on symbolic execution,fuzz testing and model checking.A model-checking-based approach for automatic reentrancy vulnerability detection in smart contracts named ReChecker was presented,categorizing contracts as either with or without locking mechanisms.By utilizing the Check-Effect-Interaction (CEI) pattern and lock mechanisms,ReChecker modeled smart contract source code as a Labelled Transition System (LTS) using an Abstract Syntax Tree (AST).It then formalized reentrancy safety properties through Linear Temporal Logic (LTL) formulas based on execution order and access control.Utilizing the Process Analysis Toolkit (PAT),ReChecker automated vulnerability detection for both locked and lock-free smart contracts.Experimental results on three datasets demonstrated that ReChecker outperformed five baseline methods,improving accuracy by 10.83% and reducing false negatives and false positives by 12% and 17.5%,respectively.

Key words: smart contracts, reentrancy vulnerability, model checking, abstract syntax tree, labeled transition system, linear temporal logic

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

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