Verifying Smart Contract Security against Re-entrancy Attacks through Relational Value Analysis

Reentrancy vulnerabilities are a critical security risk in smart contracts, posing a significant threat to the entire blockchain ecosystem. These vulnerabilities arise when a malicious attacker exploits the design of a smart contract to re-enter a function within the execution of another function, thus breaking atomicity and manipulating the smart contract state in unintended ways. While multiple countermeasures have been proposed to fortify smart contracts against re-entrancy based attacks, automatically verifying their effectiveness remains a difficult problem due to the inherent complexity of smart contracts and evolving attack techniques. In this work, we propose RAVEN, a sound and precise approach to verify smart contract safety against re-entrancy attacks automatically. At its core, RAVEN performs a content-sensitive semantic relational value analysis using the polyhedral abstract domain to establish hyper-properties such as absorption and commutativity of different program segments, which are sufficient to ensure safety against re-entrancy. Notably, unlike many prior approaches, we also prove the soundness of RAVEN, thus guaranteeing that contracts deemed as safe by RAVEN would not suffer from classical re-entrancy attacks. We have implemented our approach and evaluated RAVEN against nine state-of-the-art tools using four comprehensive test suites of Solidity smart contracts labeled for re-entrancy. The results demonstrate that RAVEN attains higher precision than existing approaches in detecting both re-entrancy-safe and vulnerable contracts. In particular, RAVEN produced 0/781 false positives on two test suites and 444/21,355 false positives on the remaining two, representing an approximate 77.3% reduction in false positives over prior tools. Moreover, this improvement was achieved with a comparable average analysis time of 141.9 seconds, versus 128.8 seconds for prior tools.