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