Abstract:

The exploitation of reentrancy vulnerabilities represents one of the most destructive attacks among the security issues related to smart contracts. Existing methods often suffer from high false negative rates. To address these issues, this paper proposes a reentrancy vulnerability detection method based on symbolic execution. This method utilizes static symbolic execution technology. By simulating the execution of Ethereum virtual machine instructions and connecting the public function control flow subgraph-which may be invoked multiple times by external contracts-to the control flow graph of the called contract, the system is capable of repeated simulations. The complete control flow graph of the intrusion attack, combined with contract state consistency detection, enables the detection of three different types of reentrancy vulnerabilities: same function, cross-function, and cross-contract types. The detection tool Lucifer, designed based on this method, was compared with related works such as Oyente, Securify, DefectChecker, and Sailfish using known label datasets, vulnerability injection datasets, custom datasets, and real Ethereum smart contract datasets. Experimental results show that Lucifer ranks first or second in terms of false positive rate, false negative rate, and fault tolerance, with an accuracy rate of 100% in some detection cases. Comprehensive evaluation indicators show that Lucifer's detection rate surpasses that of existing tools and that it has better identification capabilities for certain specific reentrancy contracts, particularly those involving mutex locks and function modifiers. Although Lucifer's detection time was longer, it remained within a controllable range, and no detection timeout were encountered.

Key words: smart contract, reentrancy vulnerability detection, symbolic execution, control flow graph, contract state consistency

摘要：

在智能合约安全问题中, 利用重入漏洞是最具破坏性的攻击之一。针对目前相关检测工作漏报率和误报率高的问题, 提出一种基于符号执行的重入漏洞检测方法。该方法基于静态符号执行技术, 在模拟以太坊虚拟机指令执行过程中, 通过将可能被外部合约多次调用的公有函数控制流子图连接到被调用合约的控制流图, 构建出能够模拟重入攻击的完全控制流图, 再结合合约状态一致性检测, 实现同函数、跨函数和跨合约等3种不同类型的重入漏洞检测。基于该方法设计的检测工具Lucifer与相关工作Oyente、Securify、DefectChecker、Sailfish在已知标签数据集、漏洞注入数据集、自定义数据集和以太坊智能合约真实数据集上进行对比, 实验结果表明, Lucifer在误报率、漏报率和容错性上均分别获得第一或者第二的成绩, 部分检测情形准确率达到100%, 由综合评价指标可以看出, Lucifer的检测率优于现有检测工具, 在对于部分特定重入合约的情形尤其在与互斥锁和函数修饰符有关的重入漏洞的识别中有较好的识别能力, 在检测时长上, Lucifer的检测时间较久但也在可控范围, 并未出现检测超时。

关键词: 智能合约, 重入漏洞检测, 符号执行, 控制流图, 合约状态一致性