Abstract
Smart contracts, self-executing agreements on blockchain networks, have revolutionized decentralized applications and finance. However, their immutability and direct handling of digital assets make them prime targets for sophisticated cyberattacks. Reentrancy, a critical vulnerability exemplified by the infamous DAO hack, allows an attacker to repeatedly call back into a vulnerable contract before the initial transaction is complete, leading to unauthorized fund depletion. Traditional smart contract auditing methods, such as manual review and dynamic testing, often struggle to identify subtle reentrancy patterns due to the vast state space and complex execution flows. This paper proposes a formal verification approach leveraging symbolic execution to systematically detect reentrancy vulnerabilities in Ethereum smart contracts. Our methodology models smart contract execution paths symbolically, identifying potential reentrant calls and analyzing path constraints to determine exploitability. We evaluate the approach on a diverse dataset of vulnerable and non-vulnerable contracts, demonstrating its high efficacy in precisely pinpointing reentrancy attack vectors. The results highlight the superior detection capabilities of formal verification over conventional techniques, offering a robust solution for enhancing the security and trustworthiness of blockchain ecosystems.
