The security of smart contracts, which are an important part of blockchain technology, has attracted much attention. In particular, reentrancy vulnerability, which is hidden and complex, poses a great threat to smart contracts. In order to improve the existing detection methods, which exhibit low efficiency and accuracy, in this paper, we propose a smart contract threat detection technology based on symbolic execution. In this method, first, the recursive descent algorithm is used to recover the basic blocks of contract code and control flow diagram, and static type inference is performed for static single assignment (SSA) variables. Then, the control flow diagram is encoded into constrained horn clause (CHC) constraints in combination with the symbolic execution technology. Model checking is conducted for the generated constraints using an automatic theorem prover based on the abstraction refinement technique for fast static detection of common security threats in smart contracts. Compared with existing detection methods, the method proposed in this paper allows the detection of both the checks-effects-interactions pattern and the vulnerability in relation to reentrant locks. It can simulate the state changes of reentrant locks as well as other global variables in multiple recursive transactions. The experimental results show that this method significantly increases both detection efficiency and accuracy, improving the security of smart contracts.

翻译：智能合约作为区块链技术的重要组成部分，其安全性已引起广泛关注。特别是隐蔽且复杂的重入漏洞，对智能合约构成重大威胁。针对现有检测方法效率低、准确率不足的问题，本文提出一种基于符号执行的智能合约威胁检测技术。该方法首先采用递归下降算法恢复合约代码的基本块和控制流图，并对静态单赋值（SSA）变量进行静态类型推断；随后结合符号执行技术，将控制流图编码为约束非Horn子句（CHC）约束集。利用基于抽象精化技术的自动定理证明器对生成的约束进行模型检测，实现对智能合约常见安全威胁的快速静态检测。与现有检测方法相比，本文方法既能检测检查-效果-交互模式，又能检测与重入锁相关的漏洞，可模拟多递归交易中重入锁及其他全局变量的状态变化。实验结果表明，该方法显著提升了检测效率与准确率，有效增强了智能合约的安全性。