Blockchain Smart Contract Threat Detection Technology Based on Symbolic Execution

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.