ReenSAT: Reentrancy Vulnerability Detection in Smart Contracts Using Semantic-Enhanced SAT Evaluation

Reentrancy, a specific vulnerability in smart contracts, frequently leads to security incidents. However, existing detection tools encounter challenges related to low precision, limited mainly by eight typical false positive (FP) types. To address these challenges, we proposed enriching the control flow to construct a constraint reentrancy control flow graph (CRCFG) at the source code level. The CRCFG includes specific control flows interacting with attackers and corresponding constraint relationships. This enhancement facilitates modeling of the reentrancy process and leverages Boolean satisfiability (SAT) solvers for vulnerability detection, thereby enhancing the precision of the detection. Specifically, first, we present the concepts of five different kinds of basic blocks to build a CRCFG. Then, we encode the CRCFG by converting it into a conjunctive normal form file. Finally, we call a SAT solver to examine all scenarios in the CRCFG and determine the presence of reentrancy vulnerabilities. Based on the above-mentioned steps, we developed a tool, ReenSAT, to detect reentrancy vulnerabilities. We conducted experiments on a verified real-world dataset. Experimental results show that ReenSAT outperforms state-of-the-art tools by an impressive <bold xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">34.72%</b> in precision, while effectively addressing eight typical types of false positives within these tools. In addition, when processing complex large contract datasets, ReenSAT's vulnerability detection efficiency outperforms that of most state-of-the-art tools.