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, ofering a novel perspective and potential foundation for developing verification techniques against such attacks.
Reentrancy remains one of the most critical and extensively studied vulnerabilities in the domain of smart contracts. It refers to a subtle yet highly dangerous class of bugs that arise when a contract issues an external call to another contract, and the callee, before the original execution flow is complete, calls back into the initiating contract. If the contract’s internal state has not been properly updated prior to the external call, such re-entries can manipulate the state in unintended ways, leading to potentially severe consequences.
This vulnerability is particularly concerning in decentralized environments such as Ethereum, where smart contracts operate autonomously and are entrusted with managing significant financial assets without centralized oversight. The infamous DAO attack in 2016 stands as a stark example of the risks posed by reentrancy: an attacker exploited this very flaw to drain millions of dollars worth of Ether, severely undermining trust in the early Ethereum ecosystem. Since then, reentrancy has become a canonical example underscoring the importance of rigorous security practices in smart contract development.
In response to the threat of reentrancy, a broad spectrum of tools and techniques has been developed
to detect and mitigate related vulnerabilities. These range from static analysis methods [
However, distinguishing between contracts that are merely syntactically vulnerable and those that are truly exploitable remains a subtle and unresolved problem. A contract may exhibit reentrant behavior at the code level, yet remain unexploitable under realistic execution scenarios [19]. This gap highlights the growing need for rigorous, semantics-driven methods that can more accurately diferentiate benign from truly dangerous behaviors, especially in the context of complex inter-contract interactions and dynamic asset transfers.
To address this gap, we investigate the application of formal verification methods to the problem of reentrancy detection, with a particular focus on noninterference, a foundational concept in security that ensures the absence of unauthorized information flow between distinct components of a system. Noninterference was originally introduced in the setting of multi-level secure systems [20], and has since evolved through various formalizations and extensions [21, 22, 23], adapting to new contexts such as distributed computing and programming language semantics.
Among the diferent approaches to verifying noninterference, one of the most tractable and compositional methods is based on unwinding conditions. These conditions ofer a structured and modular framework for reasoning about security properties, providing suficient criteria to ensure that no illicit lfow of information occurs during system execution [ 24, 25, 26, 27]. This makes them particularly wellsuited for analyzing complex behaviors such as reentrancy, where the interaction between components and the timing of state updates play a critical role.
In this work, we investigate how unwinding conditions can be efectively leveraged to reason about reentrancy vulnerabilities in smart contracts. To this end, we build on a simplified concurrent imperative language originally proposed in [25, 27], extending it to capture key features of account-based blockchain platforms such as Ethereum. In particular, we enrich the language with constructs that model contracts performing value transfers during execution, that is an essential aspect of smart contract semantics. Our abstraction deliberately omits low-level implementation details in order to focus on the core mechanisms of inter-contract interaction and monetary flow, enabling a clean and precise formal analysis of potential reentrancy behaviors.
As a concrete application of our approach, we present a formal case study based on an auction contract, a widely used and security-sensitive pattern in decentralized applications. This case study demonstrates how our formalization can be used to systematically identify potential reentrancy vulnerabilities, assess their exploitability, and analyze the efectiveness and limitations of common mitigation strategies. Our work builds on [28], which exploits similar noninterference-based reasoning in the context of Maximal Extractable Value (MEV) [29, 30] attacks. In contrast, we apply a similar formal approach to uncover and analyze reentrancy vulnerabilities, highlighting how these reasoning principles extend naturally to this distinct class of threats.
Our findings demonstrate that the noninterference framework, and in particular the application of unwinding conditions, ofers a powerful and principled foundation for reasoning about reentrancy in smart contracts. By formalizing the contract semantics and systematically analyzing the conditions under which re-entrant behavior can occur, we gain deeper insight into the nature of this vulnerability and the structural safeguards required to mitigate it efectively.
Structure of the paper. The remainder of the paper is organized as follows. Section 2 introduces a simplified concurrent imperative language designed to model contracts that perform value transfers during execution. In Section 3, we present the notion of noninterference and explain how the concept of downgrading can be used to represent the intentional release of sensitive information. Section 4 provides a detailed formalization of the Auction contract within our language, illustrating how the noninterference property is instantiated and how downgrading helps distinguish between secure and potentially vulnerable scenarios. Finally, Section 5 concludes the paper.
In this section, we present an extension of the imperative concurrent language introduced in [27], aimed at capturing the behavior of account-based smart contracts, such as those written in Solidity.
Let Z be the set of integer numbers, T = {true, false} be the set of boolean values, L be a set of lowlevel locations and H be a set of high-level locations, with L ∩ H = ∅. We also assume a distinguished family of special locations, denoted , used to access the balance associated with a contract . These balance variables are readable within the program but are not directly writable, their value can only be updated indirectly through external interactions, such as contract calls that transfer funds. As with standard storage locations, balance variables are divided into high-level and low-level subsets, denoted by B and B respectively, with B ∩ B = ∅.
The set Aexp of arithmetic expressions is defined by the grammar:
::= | | | 0 + 1 | 0 − 1 | 0 * 1 where ∈ Z, ∈ L ∪ H and ∈ B ∪ B . We assume that arithmetic expressions are total. The set Bexp of boolean expressions is defined by:
::= true | false | (0 = 1) | (0 ≤ 1) | ¬ | 0 ∧ 1 | 0 ∨ 1 where 0, 1 ∈ Aexp.
We say that an arithmetic expression is confidential , denoted by ∈ high, if there is a high-level location which occurs in it. Otherwise we say that is public, denoted by ∈ low. Similarly, we say that a boolean expression is confidential , denoted by ∈ high, if there is a confidential arithmetic expression which occurs in it. Otherwise we say that is public, denoted by ∈ low. This notion of confidentiality, both for arithmetic and boolean expressions, is purely syntactic. Notice that a high-level expression can contain low-level locations, i.e., its value can depend on the values of low-level locations. This reflects the idea that a high-level user can read high- and low-level data.
The syntax of our language is organized into three primary categories: contracts, programs, and statements. A contract is defined as a tuple of programs, each representing a possible execution entry point. Programs, in turn, consist of sequences of statements. This structured syntax enables the modeling of smart contracts that perform value transfers and interact with other contracts via the call operator, efectively capturing the essential semantics of contract interaction and asset flow. Formally, the syntax is defined as: ::= ::= ⟨1, .., ⟩ | 0; 1 | if() {0} else {1} | while() { } | await() {} | co 1|| . . . || oc | call ( ′, ) ::= skip | := | 0; 1 contracts programs statements where ∈ Aexp, ∈ L ∪ H, and ∈ Bexp. Notice that, as in [31], in the body of the await operator only sequences of assignments are allowed.
The operational semantics of our language is based on the notion of state. A state is a function which assigns to each location, both standard and balance location, an integer, i.e., : L ∪ H ∪ B ∪ B →− Z. Given a state , we denote by [/] (resp., [ /]) the state ′ such that ′() = (resp., ′( ) = ) and ′( ) = ( ) for all ̸= (resp., ̸= ). Moreover, we denote by the restriction of to the low-level locations and, given the states and , we write = for = . ⟨skip, ⟩ l→ow ⟨end, ⟩ ⟨0, ⟩ → ⟨0′, ′⟩ ⟨0; 1, ⟩ → ⟨0′; 1, ′⟩
0′ ̸≡ end ⟨, ⟩→ true ⟨if() {0} else {1}, ⟩ → ⟨0, ⟩
⟨, ⟩→ true ⟨while() { }, ⟩ → ⟨ ; while() { }, ⟩ ∈
∈ ⟨, ⟩→ true ⟨await() {}, ⟩ ⟨, ⟩ ⇝ 2 ⟨end, ′⟩ ∈ 1 1∪ 2 ⟨end, ′⟩ → ⟨, ⟩ → ⟨′, ′⟩
⟨co 1|| . . . |||| . . . || oc, ⟩ → ⟨co 1|| . . . ||′|| . . . || oc, ′⟩ ⟨, ⟩ →
⟨ := , ⟩ → ⟨end, [/]⟩
∈ ⟨0, ⟩ → ⟨end, ′⟩ ⟨0; 1, ⟩ → ⟨1, ′⟩
⟨, ⟩→ false ⟨if() {0} else {1}, ⟩ → ⟨1, ⟩
∈ ⟨, ⟩→ false ⟨while() { }, ⟩ → ⟨end, ⟩
∈ ⟨, ⟩→ false
⟨await() {}, ⟩ → ⟨await() {}, ⟩
∈ ⟨co end|| . . . ||end|| . . . ||end oc, ⟩ l→ow ⟨end, ⟩ ∃. ∈ ∃′. ′ ∈ ′ () → (′) → ′
⟨, ⟩ → 0 ⟨call ( ′, ), ⟩ → ⟨ ′, [′/′ + 0][/ − 0]⟩ ≥ 0 ∈ ∃. ∈ ∃′. ′ ∈ ′ () →
⟨, ⟩ → 0 ⟨call ( ′, ), ⟩ → ⟨end, ⟩ < 0 ∈ of the evaluation operation is assumed.
Given an arithmetic expression ∈ Aexp and a state , the evaluation of in , denoted by ⟨, ⟩ → with ∈ Z, is defined in the standard way. Similarly, ⟨, ⟩ → with ∈ Bexp and ∈ {true, false}, denotes the evaluation of a boolean expression in a state . In both cases, atomicity
To model the behavior of Ethereum smart contracts, we assume that the execution of a contract is initiated by an external user through a call. In our formalism, contract execution begins with a designated entry-point program, typically named Main. We represent this interaction as an implicit call of the form call (Main, ), where is the argument passed to the contract. This models the external invocation of a contract, as commonly occurs in Ethereum when users send transactions to trigger contract logic. Since all contract behavior ultimately unfolds through the execution of individual programs, we focus our operational semantics on programs rather than entire contracts. This modular view allows us to capture the core dynamics of execution, including inter-contract interactions and value transfers, while maintaining a clear and tractable the semantic model.
Let Prog be the set of programs of our language. The operational semantics of programs is defined in terms of state transitions. A transition from a program and a state has the form ⟨, ⟩ → ⟨ ′, ′⟩ where ′ is either a program or the special symbol end (denoting termination) and ∈ {high, low} stating that the transition is either confidential or public. The operation 1 ∪ 2 returns low if both 1 and 2 are low otherwise it returns high. Let P = Prog ∪ {end} and Σ be the set of all the possible states. The operational semantics of ⟨, ⟩ ∈ P ×
Σ is the labelled transition system (LTS) defined by structural induction on according to the rules depicted in Table 1. Intuitively, the semantics of the sequential composition impose that a program of the form 0; 1 behaves like 0 until 0 terminates and then it behaves like 1. To describe the semantics of a program of the form while() { } we have to distinguish two cases: if is true, then the program is unravelled to ; while() { }; otherwise it terminates. As far as the await operator is concerned, if is true then await() { } terminates executing in one indivisible action, i.e., it is not possible to observe the state changes internal to the execution of , while if is false then await() { } loops waiting for to become true. In a parallel composition of the form co 0|| . . . ||oc any of the can move, and the termination is reached only when all the ’s have terminated. Finally, we define the call call ( ′, ) operator, which describes how a program can invoke some other program ′ while transferring some amount of currency from the caller’s balance to the callee’s balance ′ , where and ′ are the contracts to which and ′ belong respectively. In other words, the call command can be used to transfer some amount of currency and invoke a program ′ on another contract. In this case, the specified amount is subtracted from the caller’s balance and added to the callee’s balance. The execution then continues in the callee’s context.
to denote ⟨, ⟩ ⇝
⟨ ′, ′⟩ with ∈ {low, high}.
We use the following notations. We write ⟨, ⟩ → ⟨ ′, ′⟩ to denote ⟨, ⟩ → ⟨ ′, ′⟩ with ∈ {low, high} and ⟨0, 0⟩ → ⟨, ⟩. The notation ⟨0, 0⟩ ⇝
low ⟨, ⟩ with ≥
0 for ⟨0, 0⟩ → ⟨1, 1⟩ → · · · → ⟨ − 1, − 1⟩ → ⟨, ⟩ stands for ⟨0, 0⟩ → ⟨, ⟩ for some ≥ 0 with all the transitions labelled with low; similarly ⟨0, 0⟩ ⇝ ⟨, ⟩ stands for ⟨0, 0⟩ → ⟨, ⟩ for some ≥ 0 with at least one of the transitions labelled with high. Finally, we write ⟨, ⟩ ⇝ ⟨ ′, ′⟩ high
Notice that the operational semantics defined in Table 1 is non-deterministic, since in the case of parallel composition there are many possible evolutions.
In [27], we introduced an imperative concurrent language, inspired by the one presented in [31], and we investigated several notions of noninterference aimed at ensuring secure information flow in multi-level systems. In such systems, users are classified into diferent security levels, typically high (e.g., system administrators) and low (e.g., standard users), and noninterference guarantees that no information lfows from high-level entities to low-level ones. Such a flow would, in efect, result in the unintended disclosure of confidential information.
However, recognizing that a strict prohibition of all high-to-low flows can be overly rigid and impractical in many real-world scenarios, we also proposed a downgrading mechanism in [27]. This mechanism allows for explicitly authorized, limited information flows from high to low, enabling a more flexible and context-aware approach to enforcing security.
To keep the presentation simple and accessible, we avoid relying on complex observational equivalences such as bisimulation. Instead, we adopt a more direct approach by observing only the final values of low-level variables at the end of program execution.
Intuitively, when analyzing a program that manipulates both low and high-level variables, our goal is to ensure that the behavior of does not allow high-level activities to influence the low-level outcomes. In other words, no matter how the high-level variables are modified during execution, potentially due to interactions with high-level users or components, the values of the low-level variables should remain unafected. If modifications to high-level variables result in observable changes to low-level ones, this constitutes an information flow, or more precisely, interference.
The key idea is to reason about the security of in isolation, by showing that its execution is secure in any possible context, regardless of the actions performed by external high-level entities. This principle is formalized in [27] through the notion of a generalized unwinding condition, which characterizes classes of secure programs that are parametric with respect to: • a binary relation =. which equates two states if they are indistinguishable for a low-level observer; • a binary reachability relation ℛ on P ×
Σ which associates to each pair ⟨, ⟩ all the pairs ⟨, ⟩ which, in some sense, are reachable from ⟨, ⟩.
low-level observer; • a binary relation ≑ which equates two pairs ⟨, ⟩ and ⟨, ⟩ if they are indistinguishable for a A pair ⟨, ⟩ satisfies (an instance of) our unwinding framework (i.e., there are no flows of information from high to low) if any high-level step ⟨, ⟩ h→igh ⟨, ⟩ performed by a pair ⟨, ⟩ reachable from ⟨, ⟩ has no efect on the observation of a low-level user. This is achieved by requiring that all the . elements in the set {⟨, ⟩ | = } (whose states are low-level equivalent) may perform a transition reaching an element of the set {⟨, ⟩ | ⟨, ⟩ ≑ ⟨, ⟩} (whose elements are all indistinguishable for a low-level observer). We use the notation ℛ(⟨, ⟩) to denote the set of pairs reachable from ⟨, ⟩, i.e., ℛ(⟨, ⟩) = {⟨, ⟩ | ⟨, ⟩ℛ⟨, ⟩}.
. (=, ℛ, ≑) d=ef {⟨, ⟩ ∈ Prog × Σ | ∀ ⟨, ⟩ ∈ ℛ(⟨, ⟩)
high if ⟨, ⟩ → ⟨, ⟩ th.en ∀ ∈ Σ such that = , ∃ ⟨, ⟩ : ⟨, ⟩ → ⟨, ⟩ and ⟨, ⟩ ≑ ⟨, ⟩}
We will now apply the concept of generalized unwinding in one of its simplest forms, which will serve as a suficient foundation for our analysis in the subsequent section focusing on our case study. As far as the relation =. is concerned, it is quite natural to consider two states to be equivalent when . they assign the same values to the low-level variables, i.e., we consider = to be the relation =. The relation ℛ is the notion of reachability we rely on, i.e., ⇝ is defined by the operational semantics. In [27], we introduced the concept of low-level bisimulation to define what the low-level user can observe. Specifically, we utilized low-level bisimulation to instantiate the equivalence relation denoted by ≑. Bisimulation is the appropriate notion to employ when it is assumed that the low-level user can observe the values of low-level variables at any point during the execution. Also other more involved forms of approximating equivalences such as the one presented in [32] could be used for our aims. However, for the sake of simplicity in our current presentation, we make the assumption that the low-level user can only observe the values of variables at the end of the execution. We are aware of the fact that this is not a good choice when non-terminating programs are considered. Formally this means that we instantiate ≑ as ≈ defined as follows.
Definition 2 (≈ ). Let ⟨, ⟩ and ⟨, ⟩ be two pairs. It holds that ⟨, ⟩ ≈ ⟨, ⟩ if and only if whenever ⟨, ⟩ ⇝ ⟨end, ′⟩, there exists a pair ⟨end, ′⟩ such that ⟨, ⟩ ⇝ ⟨end, ′⟩ with ′ = ′, and vice-versa (i.e., ≈ is symmetric).
Now that we have gathered all the necessary components, our objective is to demonstrate that a program does not exhibit interference. In other words, for all possible states , the pair ⟨, ⟩ belongs to (=, ⇝ , ≈ ).
As shown in our previous work [27], when a program does not belong to a given unwinding class, it is possible to construct a malicious environment in which information can flow from high to low. This observation implies that even by analyzing the program in isolation, we can anticipate and identify potential security vulnerabilities. Conversely, if a program does belong to an unwinding class, then no information leaks can occur—regardless of how the environment behaves.
One of the key strengths of the unwinding approach lies in its ability to pinpoint the exact points in the program where information flow might arise. As illustrated in Figure 1, such flows are triggered when transitions involving high-level data are executed.
Example 1. In order to provide some more intuition on the meaning of the unwinding condition, let us consider the followning toy example.
≡ := 0; if( > 0){ := } else {skip} Let be high-level and be low-level. Apparently, when we reach the if test the value of the high-level variable is 0, so the else branch is always taken and the value of the high-level variable is not revealed.
high ⟨, ⟩ →− ↑ ↓ = ↑ ↓ ⟨, ⟩ →− ⟨ , ⟩ ⇝ ↑ ↓ ≈ ↑ ↓ ⟨ , ⟩ ⇝ ⟨end, ′⟩ ↑ ↓ ′ = ′ ↑ ↓ ⟨end, ′⟩
However, this program does not satisfy our unwinding condition as one can observe taking for instance which assigns value 0 to and that is [/1]. As a matter of fact, when the if test is reached we have to consider the possibility that another program running in parallel with has modified the value of , thus allowing to take the if branch and reveal the value of the variable to the low-level user.
As observed by numerous researchers, the notion of noninterference, while foundational, can be overly restrictive in many practical scenarios. By definition, noninterference enforces a strict absence of any information flow from high to low levels. However, in real-world applications, programs often require controlled release, or downgrading, of sensitive information. Common examples include password validation, access-controlled data retrieval, and computations in spreadsheets involving both public and confidential inputs [22, 33].
The intuitive concept of downgrading conceals several subtle challenges at the implementation level. It naturally leads to critical questions such as: Who is authorized to perform downgrading? What information can be downgraded? Where and when is downgrading permissible? In our previous work [27], we addressed these concerns by introducing a set of high-level expressions and proposing a delimited notion of noninterference. This refined model allows for the controlled downgrading of designated expressions at any point during program execution.
In this paper, we focus on a notion of downgrading that is tied to the specific point during execution at which the downgrading takes place. This choice is consistent with our use of unwinding conditions to identify precise execution points in a smart contract where potential reentrancy vulnerabilities may occur. To support this approach, we introduce a function, downgrade, which maps any arithmetic or boolean expression to itself while explicitly lowering its confidentiality level to low. As a result, program instructions involving downgrade are treated as declassified in the operational semantics and are not considered dangerous within the unwinding test.
Example 2. We consider again the program of Example 1. If we know that revealing to the low-level user the value of is not dangerous, and it is necessary (e.g., the system administrator needs to send to the user a message), then we can modify the program as follows:
≡ := 0; := downgrade(); if( > 0){ := } else {skip} If is low-level, the only point where we should check the unwinding condition, is the second assignment instruction. However, since the downgrade operator is used, when the assignment is executed a low-level transition is performed and the unwinding condition is satisfied.
We are now ready to model a smart contract implementing an auction by using our language. The original contract written in Solidity is depicted in Table 2 and is taken from [34].
address payable public seller; uint public endTime; address public highestBidder; uint public highestBid; mapping(address => uint) public bids; constructor(uint _startingBid, uint _duration) { seller = payable(msg.sender); highestBid = _startingBid; endTime = block.timestamp + (_duration * 1 seconds); function bid() external payable { require(block.timestamp < endTime, "Bidding time expired"); require(msg.value > highestBid, "Value must be greater than highest"); require(bids[msg.sender] == 0, "You have already placed a bid"); bids[msg.sender] = msg.value; highestBidder = msg.sender; highestBid = msg.value; function withdraw() public { require(block.timestamp >= endTime, "Auction not ended"); uint amt = bids[msg.sender]; (bool success, ) = payable(msg.sender).call{value: amt}(""); bids[msg.sender] = 0; require(success, "Transfer failed."); function end() external { require(msg.sender == seller, "Only the seller"); require(block.timestamp >= endTime, "Auction not ended"); (bool success, ) = seller.call{value: highestBid}(""); require(success, "Transfer failed.");
In our model, a contract is a tuple of programs, thus we define:
We will show that the code of this contract is subject to malicious reentrancy attacks due to the way it is implemented. The contract contains two main procedures: Bid and Withdraw, defined as follows: 1: Program Bid 2: PrevBid := Bids[Sender]; 3: if (CallValue ≤ HighestBid ∨ PrevBid ̸= 0) then 4: 5: 6:
skip else
HighestBidder := Sender; 7: HighestBid := CallValue; 8: Bids[Sender] := CallValue 1: Program Withdraw 2: Amt := Bids[Sender]; 3: call(Receive, Amt); 4: Bids[Sender] := 0 ◁ -= Amt, += Amt
We denote variables using capitalized identifiers. In all examples, we omit the caller program in the subscript of the call primitive, as it is implicitly understood to be the program from which the call originates. Thus, any call of the form call( ′, ) should be interpreted as being issued by the currently executing program, typically the one enclosing the call. The identifiers highlighted in red represent high locations, from which unwanted information flows may originate; conversely, those highlighted in green represent low locations that may be afected by such flows. A few identifiers have a special meaning: Sender refers to the identifier of the user invoking the current smart contract, while CallValue denotes the amount of money transferred by the caller via the call primitive.
Each bid is accepted only if the Sender has not already placed a bid, and the ofered amount (CallValue) exceeds the current HighestBid. If both conditions hold, the bid is recorded and the highest bidder is updated accordingly. Our model faithfully reproduces the fund transfer mechanism used in Solidity on Ethereum, where transferring money to another contract is done by invoking a call method that implicitly dispatches a receive() function defined in the target contract. The same happens in our language: the Withdraw procedure allows participants to reclaim their funds by calling a Receive function with the amount previously bid.
The call to Receive within the Withdraw procedure is crucial to understand the mechanisms undergoing reentrancy. It serves two purposes: triggering the execution of the target program (Receive) and transferring funds from the balance of the caller contract to the balance of the callee contract. Notably, balances are associated with contracts, not programs, whereas the call primitive manipulates programs, not contracts. Being contracts just tuples of programs, though, it is easy to reconstruct which contract a given program belongs to.
In the comment, the and are two placeholders indicating, respectively, the balance of the caller contract and the callee contract, whatever they are upon execution. The examples in the sections below will show how those two placeholders become contract names when a contract is run.
We now introduce another contract, which implements the code of a user participating to the auction. Such contract does not exploit the reentrancy vulnerability and is an example of a harmless interaction consisting of the following two programs:
Harmless ≡ ⟨ Main, Receive⟩ where the implementation are: 1: Program Main 2: call(Bid, 100); 3: call(Withdraw, 0) 1: Program Receive 2: skip ◁ Harmless -= 100, ReentrantAuction += 100
In the Main program, a user wishing to participate in the auction places a bid with an amount of 100. This amount is transferred from the balance of Harmless to that of ReentrantAuction, since the former contains the calling context and the latter contains the Bid program. In other words, that call could be rewritten in our formal language as: callMain(Bid, 100) where Main ∈ Harmless ∧ Bid ∈ ReentrantAuction ⟨Main, [ReentrantAuction/200, Harmless/100]⟩
↓ ⟨Bid, [ReentrantAuction/200, Harmless/100]⟩
↓ ⟨Withdraw, [ReentrantAuction/300, Harmless/0, Bids[Sender]/100]⟩
↓ ⟨Receive, [ReentrantAuction/200, Harmless/100, Bids[Sender]/100]⟩
↓ ⟨Withdraw, [ReentrantAuction/200, Harmless/100, Bids[Sender]/100]⟩ hence, the two balances involved are Harmless and ReentrantAuction.
The following line performs a call with zero amount, which reduces to a simple program invocation and produces no efect on balances. When invoking Withdraw, the user expects to receive money via the execution of the Receive program supplied. The dummy implementation of Receive is key to understanding why the contract is harmless and does not allow reentrancy attacks. Since our example mimicks the same callback mechanism undergoing in Solidity, which allows the Receive function to perform any arbitrary logic, implementing it as a skip ensures that it solely receives the funds without triggering any additional operation.
When running this code, once the Withdraw program is invoked, the caller’s balance appearing in the comment of the Withdraw function in the previous section refers to ReentrantAuction, and the callee’s balance to Harmless. Hence, the caller’s balance is decreased by the transferred amount, while the callee’s balance is increased by the same amount.
The execution of the Harmless contract starts from the Main program:
↓ ⟨skip, [ReentrantAuction/200, Harmless/100, Bids[Sender]/0]⟩
Consider now a malicious setup where the Receive programs are written by an attacker and embedded in the following contract:
Whereas the Main program is unchanged from the previous section, the Receive implementation difers, as it exploits a reentrant call to Withdraw to steal money.
1: Program Receive 2: call(Withdraw, 0) Reentrancy takes place via repeated, mutually recursive calls between Withdraw and Receive, which gradually deplete the caller’s balance until it reaches zero, at which point execution halts. The following trace shows this process in action. We focus on a state in which the variables have the following values: (ReentrantAuction) = 200; (Attacker) = 100; ⟨Main, [ReentrantAuction/200, Attacker/100]⟩ ↓ . . .
↓ ⟨Bid, [ReentrantAuction/200, Attacker/100]⟩
execution of Main ↓ . . . execution of Bid ↓ ⟨Withdraw, [ReentrantAuction/300, Attacker/0, Bids[Sender]/100]⟩ ↓ . . .
↓ ⟨Receive, [ReentrantAuction/200, Attacker/100, Bids[Sender]/100]⟩ execution of Withdraw #1 ↓ . . . execution of Receive #1 ↓ ⟨Withdraw+Receive, [ReentrantAuction/200, Attacker/100], Bids[Sender]/100⟩
In order to avoid the attacker from being able to leverage a reentrancy attack, the Withdraw program should be edited as follows: 1: Program Withdraw 2: Amt := Bids[Sender]; 3: Bids[Sender] := 0; 4: call(Receive, Amt) ◁ SafeAuction -= Amt, Attacker += Amt
The only change lies in the position of the line that resets the bid to zero: it has now been moved before the call to Receive.
With reference to the Solidity code in Table 2, this means to apply the same simple fix: 1 function withdraw() public { 2 require(block.timestamp >= endTime, "Auction not ended"); 3 uint amt = bids[msg.sender]; 4 bids[msg.sender] = 0; // attackers reach this before and prevent further payments 5 (bool success, ) = payable(msg.sender).call{value: amt}(""); 6 require(success, "Transfer failed."); 7 }
This reordering is suficient to prevent the reentrancy attack, as an attacker invoking the modified Withdraw procedure recursively would find the Bids[Sender] location already cleared, and thus be unable to extract further funds. As a result, any subsequent calls to Receive would transfer zero value only.
Let us update the auction contract embedding the new, safer version of the Withdraw as well as the original Bid shown in the previous section:
And let the contract invoking the auction be the same malicious Attacker contract defined above. Its execution produces the following trace, in which no information flow compromises the caller’s balance. Reentrancy attacks are rendered harmless by the assignment to zero occurring before the call, efectively neutralizing any attempt to extract additional funds.
⟨Main, [SafeAuction/200, Attacker/100]⟩ ↓ . . .
↓ ⟨Bid, [SafeAuction/200, Attacker/100]⟩
execution of Main ↓ . . . execution of Bid ↓ ⟨Withdraw, [SafeAuction/300, Attacker/0, Bids[Sender]/100]⟩ ↓ . . .
↓ ⟨Receive, [SafeAuction/200, Attacker/100, Bids[Sender]/0]⟩ ↓ . . .
↓ ⟨Withdraw+Receive, [SafeAuction/200, Attacker/100, Bids[Sender]/0]⟩ ↓ . . .
execution of Receive #1 execution of Withdraw #1 ↓ ⟨Withdraw+Receive, [SafeAuction200, Attacker/100, Bids[Sender]/0]⟩ ↓ . . .
↓ ⟨skip, [SafeAuction/200, Attacker/100, Bids[Sender]/0]⟩ execution of Withdraw #2 and Receive #2 execution of Withdraw #n and Receive #n
The last state transition proves that the balance associated to the malicious contract Attacker has not increased, and the original amount of money stored in the balance associated to the SafeAuction contract is unchanged.
We now present a simplified version of a crowdfunding contract written in Solidity. At first glance, the withdraw function appears vulnerable to a reentrancy attack, as it invokes the call function to transfer Ether to an external address receiver before updating the contract’s internal state, a well-known red flag in smart contract security. However, in this case, the receiver address is hardcoded and not dynamically computed, ensuring that no malicious contract can exploit the callback. Furthermore, the function includes an access control check that restricts its execution to the contract’s owner. Additionally, the function transfers the entire contract balance in a single call, leaving no residual funds that an attacker could repeatedly steal through reentrant invocations. As a result, despite following a pattern commonly associated with reentrancy vulnerabilities, the contract is secure. This example highlights the limitations of pure noninterference and underscores the importance of taking into account the execution context when evaluating smart contract security. bool open; // flag that closes the Crowdfund address receiver; // receiver of the donated funds address owner; constructor (address payable receiver_) { receiver = receiver_; owner = msg.sender; open = true; function donate() public payable {
require (open); function withdraw() public { require (open); require (msg.sender == owner); (bool succ,) = receiver.call{value: address(this).balance}(""); open = false; require(succ); In our model, we define the CrowdFund contract as follows:
and we consider the Main and Receive programs of the Owner and the Receiver:
The execution starts from the Main program belonging to the Owner contract, which then invokes the Withdraw of the Crowdfund contract and finally the Receive of the Receiver. 1: Program Main 2: call(Withdraw, 0) 1: Program Receive 2: skip We provide only the implementation of Withdraw, as the Donate function is straightforward. ◁ CrowdFund -= Balance, Receiver += Balance
In this case, we use of the downgrade operator that lowers the confidentiality level of Balance, so when the call is executed, it is treated as declassified and is therefore not considered dangerous in the unwinding test, i.e., the unwinding condition is satisfied.
The case study presented in this article demonstrates that the non-interference framework is particularly well-suited for capturing the vulnerability known as reentrancy in smart contracts. By applying the unwinding conditions, we were able to systematically identify and understand potential reentrancy vulnerabilities in an auction contract, highlighting the efectiveness of this formal approach.
As future work, we propose to develop a proof system in the style of [35] for the analysis of smart contracts, which will enable formal verification of the absence of reentrancy vulnerabilities. Additionally, we aim to implement a tool based on the non-interference framework as in [36] to facilitate automated analysis of smart contracts, thereby enhancing security and reliability in blockchain applications.
This study was carried out within the PE0000014 - Security and Rights in the CyberSpace (SERICS) and received funding from the European Union Next-GenerationEU - National Recovery and Resilience Plan (NRRP) – MISSION 4 COMPONENT 2, INVESTIMENT 1.3 – CUP N. H73C22000890001. This work has been also partially supported by the Research Project INDAM GNCS 2025 - CUP E53C24001950001 “Modelli e Analisi per sistemi Reversibili e Quantistici (MARQ)” and by the Project PRIN 2020 - CUP N. 20202FCJMH "NiRvAna - Noninterference and Reversibility Analysis in Private Blockchains". This manuscript reflects only the authors’ views and opinions, neither the European Union nor the European Commission can be considered responsible for them.
The authors used AI-based tools (ChatGPT, Grammarly) exclusively for language editing purposes (grammar, spelling, and style). The scientific content, analysis, and conclusions are entirely the work of the authors, who take full responsibility for the integrity and accuracy of the manuscript. [4] P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. Buenzli, M. Vechev, Securify: Practical security analysis of smart contracts, in: Proceedings of the 2018 ACM SIGSAC conference on computer and communications security, 2018, pp. 67–82. [5] B. Mueller, Smashing smart contracts, in: 9th HITB Security Conference, 2018. [6] B. Jiang, Y. Liu, W. K. Chan, Contractfuzzer: Fuzzing smart contracts for vulnerability detection, in: Proceedings of the 33rd ACM/IEEE international conference on automated software engineering, 2018, pp. 259–269. [7] T. D. Nguyen, L. H. Pham, J. Sun, Y. Lin, Q. T. Minh, sfuzz: An eficient adaptive fuzzer for solidity smart contracts, in: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, 2020, pp. 778–788. [8] C. Schneidewind, I. Grishchenko, M. Scherer, M. Mafei, ethor: Practical and provably sound static analysis of ethereum smart contracts, in: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, 2020, pp. 621–640. [9] Y. Xue, M. Ma, Y. Lin, Y. Sui, J. Ye, T. Peng, Cross-contract static analysis for detecting practical reentrancy vulnerabilities in smart contracts, in: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020, pp. 1029–1040. [10] Z. Liao, Z. Zheng, X. Chen, Y. Nan, Smartdagger: a bytecode-based static analysis approach for detecting cross-contract vulnerability, in: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, 2022, pp. 752–764. [11] Y. Wu, X. Xie, C. Peng, D. Liu, H. Wu, M. Fan, T. Liu, H. Wang, Advscanner: Generating adversarial smart contracts to exploit reentrancy vulnerabilities using llm and static analysis, in: Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, 2024, pp. 1019–1031. [12] B. Boi, C. Esposito, S. Lee, Smart contract vulnerability detection: The role of large language model (llm), ACM SIGAPP Applied Computing Review 24 (2024) 19–29. [13] C. Laneve, A. Spanò, D. Ressi, S. Rossi, M. Bugliesi, Assessing code understanding in llms, in: C. Ferreira, C. A. Mezzina (Eds.), Formal Techniques for Distributed Objects, Components, and Systems, Springer Nature Switzerland, Cham, 2025, pp. 202–210. [14] Z. Liu, P. Qian, X. Wang, Y. Zhuang, L. Qiu, X. Wang, Combining graph neural networks with expert knowledge for smart contract vulnerability detection, IEEE Transactions on Knowledge and Data Engineering 35 (2021) 1296–1310. [15] L. Guo, H. Huang, L. Zhao, P. Wang, S. Jiang, C. Su, Reentrancy vulnerability detection based on graph convolutional networks and expert patterns under subspace mapping, Computers & Security 142 (2024) 103894. [16] M. Rizzo, D. Ressi, A. Gasparetto, S. Rossi, A comparison of machine learning techniques for ethereum smart contract vulnerability detection, in: D. Porello, C. Vinci, M. Zavatteri (Eds.), Proceedings of the 6th International Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, OVERLAY 2024, Bolzano, Italy, November 28-29, 2024, volume 3904 of CEUR Workshop Proceedings, CEUR-WS.org, 2024, pp. 119–126. [17] J. Yu, X. Yu, J. Li, H. Sun, M. Sun, Smart contract vulnerability detection based on multimodal feature fusion, in: International Conference on Intelligent Computing, Springer, 2024, pp. 344–355. [18] M. Rizzo, A. Spanò, L. Benetollo, D. Ressi, A. Gasparetto, S. Rossi, Advanced large language models prompting strategies for reentrancy classification and explanation in smart contracts, in: D. Ressi, S. Rossi, F. Tiezzi, W. Knottenbelt (Eds.), Proceedings of the 4th EAI International Conference on Blockchain Technology and Emerging Applications BLOCKTEA 2025, Venice, Italy, September 18-19, 2025, Springer – LNICST series, 2025. [19] D. Perez, B. Livshits, Smart contract vulnerabilities: Vulnerable does not imply exploited, in: 30th
USENIX Security Symposium (USENIX Security 21), 2021, pp. 1325–1341. [20] J. A. Goguen, J. Meseguer, Security policies and security models, in: 1982 IEEE Symposium on Security and Privacy, 1982, IEEE Computer Society, 1982, pp. 11–20. doi:10.1109/SP.1982. 10014. [21] R. Focardi, S. Rossi, Information flow security in dynamic contexts, J. Comput. Secur. 14 (2006)