Blockchain Smart Contract Threat Detection Technology Based on Symbolic Execution

TL;DR

This paper introduces a symbolic execution-based method for detecting smart contract vulnerabilities, notably reentrancy, that improves detection accuracy and efficiency over existing techniques.

Contribution

The paper presents a novel symbolic execution approach combined with static analysis and model checking for more effective smart contract threat detection.

Findings

Significantly improved detection accuracy and efficiency.

Able to detect reentrancy vulnerabilities and related patterns.

Simulates state changes in recursive transactions effectively.

Abstract

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.