Modeling Reentrancy in Smart Contracts through Noninterference

Reentrancy is a well-known vulnerability in smart contracts for blockchain platforms, allowing malicious actors to repeatedly call a contract before previous executions are completed, often leading to unexpected and harmful behavior. In this paper, we propose the use of the notion of noninterference to model and analyze reentrancy attacks. Originally developed to characterize unwanted information flows in multi-level security systems, noninterference provides a rigorous framework for reasoning about the absence of illicit interactions between components. Among the various formulations of noninterference, those based on unwinding conditions are particularly well-suited for our analysis, as they enable the precise localization of information flows within a system. We investigate how these conditions can be applied to detect and understand reentrancy vulnerabilities in smart contracts, offering a novel perspective and potential foundation for developing verification techniques against such attacks.