Introduction

Decentralized Finance (DeFi) is revolutionizing the landscape of the global digital economy by amalgamating decentralization and distribution principles with traditional financial services. This integration operates within a decentralized framework, leveraging digital assets primarily through blockchain technology [1,2,3]. Such pioneering methods engender an alternative financial system distinguished by its emphasis on decentralization, fostering innovation, promoting interoperability, and ensuring transparency [4]. Ethereum, renowned for its sophisticated smart contract functionality, stands as the cornerstone technology supporting various DeFi services. Smart contracts serve as automated enforcers of contractual terms, allowing for intricate interactions between parties without the need for intermediaries [5].

Despite the security assurances provided by blockchain technology, DeFi smart contracts possess inherent vulnerabilities as highlighted in recent studies [6]. Within the DeFi ecosystem, decentralized exchanges (DEXs) play a central role by facilitating trustless transactions through smart contracts, eliminating the need for centralized intermediaries. Automated Market Maker (AMM) protocols, a prominent feature of DEXs, have garnered significant attention in the wake of increased interest in blockchain technology. These protocols operate on a peer-to-pool basis, wherein liquidity providers contribute assets to liquidity pools, enabling users to exchange assets at algorithmically determined prices [4].

In the realm of Blockchains and Decentralized Finance (DeFi), the concept of Maximal Extractable Value (MEV) is gaining increasing attention. MEV represents the maximum potential gain that users, including miners and validators, can achieve through interactions with a smart contract and its associated dependencies [7]. This potential for profit attracts not only legitimate users but also malicious actors who exploit strategic transaction manipulations, such as reordering transactions within blocks, to manipulate the outcomes of smart contracts. These actors often employ automated bots to engage in frontrunning, exploiting transactional intricacies for potential gains [8]. Notable examples of MEV exploitation include instances of decentralized exchange (DEX) arbitrage, where participants exploit price differences across decentralized exchange protocols [9]. Such attacks not only compromise the integrity of smart contracts but also distort their intended functionality.

Recent literature has proposed utilizing the concept of noninterference for modeling and analyzing MEV attacks. Noninterference aims to identify and mitigate undesired information flows within multilevel systems. Various definitions of noninterference have been introduced [10,11,12,13], with those based on unwinding conditions particularly useful for pinpointing potential information flows within a system [14,15,16]. Our study builds upon prior research, particularly drawing from the contributions by Babel et al. in [17] and by Bartoletti et al. in [18]. Specifically, Bartoletti et al. 's work introduces a novel concept of secure composability for smart contracts, aiming to safeguard compound contracts from economic harm caused by adversaries interfering with their dependencies.

In this paper, our investigation centers on the application of unwinding conditions to analyze the Maximal Extractable Value (MEV). Our approach involves a meticulous examination of a straightforward case study-the Bet contract-with the aim of elucidating both the strengths and limitations of our methodology. Specifically, we utilize a simple imperative concurrent language, as introduced in a previous study [14,16] for security verification, to identify vulnerabilities within DeFi smart contracts that are susceptible to MEV interferences. Through the presentation of the Bet contract case study, we spotlight scenarios where particular conditions affect MEV noninterference, thereby emphasizing potential sources of vulnerability within DeFi services. Differently from the proposal of [18], we exploit the formalization of noninterference in terms of unwinding conditions. This allows us to abstract from the environment, namely the specific implementations of smart contracts that interact with the one under examination. This abstraction enables a more comprehensive evaluation of MEV vulnerabilities within DeFi systems.

Structure of the paper. The structure of the paper is as follows: In Section 1, we present the case study of the Bet contract. Section 2 introduces the concept of noninterference for an imperative concurrent language and outlines the use of downgrading to capture the release of sensitive information. Section 3 details the modeling of the Bet contract within our imperative language, including the capture of the noninterference property and the application of downgrading functionality to differentiate secure scenarios from potentially risky ones. Finally, Section 4 discusses related work and concludes the paper.

The Bet Contract Case Study

In this section we briefly introduce the main functionalities of a betting service, as also detailed in [18], which serves as a straightforward case study in this paper to demonstrate how to instantiate noninterference expressed through unwinding conditions for detecting MEV attacks. Specifically, the Bet contract we consider enables individuals to place bets on the exchange rate between a given token and Ether. This contract is parameterized based on an oracle contract responsible for providing token price information. Upon deployment, the owner initiates the bet contract with an initial pot of Ether; for joining, a player is required to contribute an amount of Ether equal to the pot. Prior to the deadline, the player can withdraw the pot if the oracle exchange rate is greater than the bet rate defined by the Bet contract owner. Subsequently, after the deadline elapses, the pot is transferred to the owner's wallet.

We explore two instances of the oracle contract, with the first being an Automated Market Maker (AMM) inspired by the Uniswap protocol (see, https://uniswap.org/). This AMM allows users to both add liquidity for two tokens and execute swaps between the held tokens. Additionally, the contract enables the querying of token pairs and exchange rates. In contrast, the second oracle contract, referred to as the Exchange contract, differs from the AMM contract in terms of rate setting. In the AMM, the rate is affected by the fluctuations in the total amount of tokens staked in the AMM wallet, equating to the division of the total amount of one token by the total amount of the paired token. Conversely, in the Exchange contract, the rate is solely determined by the owner and remains unaffected by variations in wallet values resulting from user interactions. Figure 1 illustrates the primary functionalities of the Bet contract and its potential interactions with either AMM or Exchange.

As detailed in [18], MEV attacks become feasible when the Bet contract employs AMM as its oracle. In this scenario, an attacker can place a bet and subsequently interact with the AMM contract before executing the function to claim the win. By doing so, the attacker alters the exchange rate, thereby influencing the outcome of the bet. This vulnerability is not limited to regular users; its success rate significantly increases when the attacker is a miner with the ability to dictate transaction order within blocks. Conversely, if the Bet contract relies on the Exchange contract as its oracle, the attacker cannot modify the rate, even if interaction with the Exchange contract occurs.

In the forthcoming sections, we will show that when we use noninterference for modeling this attack the wallet of the bet contract is going to play the role of the low level variable over which we observe a flow of information (denoted by a green 𝐿 in Figure 1). Such flow of information comes from the high level variable representing the exchange rate (denoted by a red 𝐻 in Figure 1), i.e., from a variable whose value can be altered by other contracts. Our approach offers the advantage of focusing solely on the bet contract and identifying potentially dangerous instructions within it. Then, a thorough analysis of the oracles becomes imperative to distinguish between the two scenarios.

Noninterference and Downgrading over a Concurrent Imperative Language

In [16] we considered an imperative concurrent language, inspired by the one introduced in [19] and proposed different notions of noninterference with the aim of ensuring that in multi-level systems, where users are categorized as high (e.g., system administrators) and low (e.g., standard users) no information flow occurs from the high level to the low one. A flow of information from high to low could in fact represent the public disclosure of private data.

Recognizing that completely preventing any potential flow might be overly restrictive in many scenarios, we also proposed a downgrading mechanism in [16]. This mechanism enables explicit allowance of delimited flows, providing a nuanced approach to managing information flow within the system.

In this section, we provide a brief overview of those papers. However, to maintain simplicity in our presentation, we refrain from utilizing specific observational equivalences, like, e.g., bisimulation. Instead, we solely focus on observing the values of low-level variables at the end of the execution.

The Language

Let ℤ be the set of integer numbers, 𝕋 = {true, false} be the set of boolean values, 𝕃 be a set of low level locations and ℍ be a set of high level locations, with 𝕃 ∩ ℍ = ∅. The set Aexp of arithmetic expressions is defined by the grammar:

𝑎 ∶∶= 𝑛 | 𝑋 | 𝑎 0 + 𝑎 1 | 𝑎 0 − 𝑎 1 | 𝑎 0 * 𝑎 1

where 𝑛 ∈ ℤ and 𝑋 ∈ 𝕃 ∪ ℍ. 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 both high and low level data.

The set Prog of programs of our language is defined as:

𝑆 ∶∶= skip | 𝑋 ∶= 𝑎 | 𝑆 0 ; 𝑆 1 𝑃 ∶∶= 𝑆 | 𝑃 0 ; 𝑃 1 | if(𝑏) {𝑃 0 } else {𝑃 1 } | while(𝑏) {𝑃} | await(𝑏) {𝑆} | co 𝑃 1 | | … | |𝑃 𝑛 oc

where 𝑎 ∈ Aexp, 𝑋 ∈ 𝕃 ∪ ℍ, and 𝑏 ∈ Bexp. Notice that, as in [19], 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 an integer, i.e., 𝜎 ∶ 𝕃 ∪ ℍ ⟶ ℤ. Given a state 𝜎 , we denote by 𝜎[𝑋 /𝑛] the state 𝜎 ′ such that 𝜎 ′ (𝑋 ) = 𝑛 and 𝜎 ′ (𝑌 ) = 𝜎(𝑌 ) for all 𝑌 ≠ 𝑋 . Moreover, we denote by 𝜎 𝐿 the restriction of 𝜎 to the low level locations and we write 𝜎 = 𝑙 𝜃 for 𝜎 𝐿 = 𝜃 𝐿 .

Given an arithmetic expression 𝑎 ∈ Aexp and a state 𝜎, the evaluation of 𝑎 in 𝜎 , denoted by ⟨𝑎, 𝜎 ⟩ → 𝑛 with 𝑛 ∈ ℤ, 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 of the evaluation operation is assumed.

Our operational semantics is expressed 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 ℙ = Prog∪{end} and Σ be the set of all the possible states. The operational semantics of ⟨𝑃, 𝜎 ⟩ ∈ ℙ × Σ is the labelled transition system (LTS) defined by structural induction on 𝑃 according to the rules depicted in Table 1 in the Appendix. Intuitively, the semantics of the sequential composition imposes 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. Finally, 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.

We use the following notations. We write ⟨𝑃, 𝜎⟩ → ⟨𝑃 ′ , 𝜎 ′ ⟩ to denote ⟨𝑃, 𝜎 ⟩ 𝜖 → ⟨𝑃 ′ , 𝜎 ′ ⟩ with 𝜖 ∈ {low, high} and ⟨𝑃 0 , 𝜎 0 ⟩ → 𝑛 ⟨𝑃 𝑛 , 𝜎 𝑛 ⟩ with 𝑛 ≥ 0 for ⟨𝑃 0 , 𝜎 0 ⟩ → ⟨𝑃 1 , 𝜎 1 ⟩ → ⋯ → ⟨𝑃 𝑛−1 , 𝜎 𝑛−1 ⟩ → ⟨𝑃 𝑛 , 𝜎 𝑛 ⟩.

The notation ⟨𝑃 0 , 𝜎 0 ⟩ low ⇝ ⟨𝑃 𝑛 , 𝜎 𝑛 ⟩ stands for ⟨𝑃 0 , 𝜎 0 ⟩ → 𝑛 ⟨𝑃 𝑛 , 𝜎 𝑛 ⟩ for some 𝑛 ≥ 0 with all the 𝑛 transitions labelled with low; similarly ⟨𝑃 0 , 𝜎 0 ⟩ high ⇝ ⟨𝑃 𝑛 , 𝜎 𝑛 ⟩ stands for ⟨𝑃 0 , 𝜎 0 ⟩ → 𝑛 ⟨𝑃 𝑛 , 𝜎 𝑛 ⟩ for some 𝑛 ≥ 0 with at least one of the 𝑛 transitions labelled with high. Finally, we write ⟨𝑃, 𝜎 ⟩ ⇝ ⟨𝑃 ′ , 𝜎 ′ ⟩ to denote

⟨𝑃, 𝜎⟩ 𝜖 ⇝ ⟨𝑃 ′ , 𝜎 ′ ⟩ with 𝜖 ∈ {low, 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.

Noninterference

Intuitively, when we analyze a program 𝑃 that involves both low and high-level variables, our objective is to ensure that regardless of how the high-level variables are modified during execution by other high-level components, which represent interactions with high-level users, the values of the low-level variables remain unaffected. Put simply, if actions performed by other components on the high-level variables lead to changes in the low-level ones, it signifies an unwanted information flow, or interference. In essence, we focus solely on the program 𝑃 and aim to demonstrate its security in any possible context or environment -meaning, irrespective of the actions taken by high-level users. This concept is formalized in [16], where a generalized unwinding condition defines classes of 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 ℙ × Σ which associates to each pair ⟨𝑃, 𝜎 ⟩ all the pairs ⟨𝐹 , 𝜓 ⟩ which, in some sense, are reachable from ⟨𝑃, 𝜎⟩. • a binary relation ≑ which equates two pairs ⟨𝑃, 𝜎⟩ and ⟨𝑄, 𝜃⟩ if they are indistinguishable for a low level observer;

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 ⟨𝐹 , 𝜓 ⟩ high → ⟨𝐺, 𝜑⟩ performed by a pair ⟨𝐹 , 𝜓 ⟩ reachable from ⟨𝑃, 𝜎 ⟩ has no effect 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., ℛ(⟨𝑃, 𝜎⟩) = {⟨𝐹 , 𝜓 ⟩ | ⟨𝑃, 𝜎⟩ℛ⟨𝐹 , 𝜓 ⟩}.

Definition 1. (Generalized Unwinding)

Let ≐ be a binary relation over Σ, ℛ and ≑ be two binary relations over ℙ × Σ. We define the unwinding class 𝒲 (≐, ℛ, ≑) by:

𝒲 (≐, ℛ, ≑) def = {⟨𝑃, 𝜎⟩ ∈ Prog × Σ | ∀ ⟨𝐹 , 𝜓 ⟩ ∈ ℛ(⟨𝑃, 𝜎 ⟩) if ⟨𝐹 , 𝜓 ⟩ high → ⟨𝐺, 𝜑⟩ then ∀ 𝜋 ∈ Σ such that 𝜋 ≐ 𝜓 , ∃ ⟨𝑅, 𝜌⟩ ∶ ⟨𝐹 , 𝜋⟩ → ⟨𝑅, 𝜌⟩ and ⟨𝐺, 𝜑⟩ ≑ ⟨𝑅, 𝜌⟩}

We will now apply the concept of generalized unwinding in one of its simplest forms, which will serve as a sufficient 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 [16], 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 [20] could be used for our aims. However, for the sake of simplicity in our current presentation, we make the assumption that the lowlevel 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.

⟨𝐹 , 𝜓 ⟩ high ⟶ ⟨𝐺, 𝜑⟩ ⇝ ⟨end, 𝜑 ′ ⟩ ↑ ↑ ↑ ↓ ↓ ↓ 𝜋 = 𝑙 𝜓 ≈ 𝑙 𝜑 ′ = 𝑙 𝜌 ′ ↑ ↑ ↑ ↓ ↓ ↓ ⟨𝐹 , 𝜋⟩ ⟶ ⟨𝑅, 𝜌⟩ ⇝ ⟨end, 𝜌 ′ ⟩

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 viceversa (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 𝒲 (= 𝑙 , ⇝, ≈ 𝑙 ). Through our case study, we will illustrate that when this condition is not met, it may lead to MEV interferences.

As demonstrated in our previous work [16], when a program does not belong to an unwinding class, it is possible to define a malicious environment wherein information flows from high to low. This means that by analyzing the program in isolation, we can pinpoint potential hazardous scenarios. In other words, when a program belongs to an unwinding class, no adverse consequences can arise, regardless of the actions taken by the environment. One of the main advantages of the unwinding approach is its ability to identify the specific points within the program that could potentially lead to information flows. As illustrated in Figure 2, such flows occur when high-level transitions are executed.

In the context of MEV interference, this approach aids in identifying the specific dependencies of the contract that require deeper analysis. When scrutinizing these dependencies reveals that no adverse outcomes can occur, it is possible to leverage the concept of downgrading, thereby permitting controlled information flows.

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. 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.

Downgrading

As noted by numerous researchers, the concept of noninterference can be overly limiting in numerous practical scenarios. Noninterference models the complete absence of information flow from high to low levels. However, in reality, many programs do require some form of release or downgrading of sensitive information (e.g., password checking, information purchase, and spreadsheet computation) [12,21].

The intuitive concept of downgrading masks certain intricate issues at the implementation level. For example, it raises questions like "who can perform downgrading, " "what elements can be downgraded, " "where downgrading can occur, " and so forth. In our previous work [16], we introduced a collection of high-level expressions and proposed a delimited notion of noninterference that permits the downgrading of such expressions at any stage during the execution.

In this paper, we opt to focus on a notion of downgrading that pertains to the precise point within the execution where the downgrading occurs. This aligns with our approach of using unwinding conditions to pinpoint specific points in the execution of a smart contract where potential MEV interferences may arise. To achieve this, we introduce a function called downgrade that maps any arithmetic or boolean expression to itself, while altering its confidentiality level to low. Consequently, the operational semantics of program instructions involving downgrade are declassified to the low level, and they are not considered as dangerous in 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.

Back to the Bet Contract

We are now ready to model the Bet contract case study within our imperative language. In our model, the Bet contract is defined as the parallel composition of its functionalities, namely:

Bet_Contract ≡ co Constructor | | Bet | | Win | | Close oc .

Since our language provides only basic instructions and lacks object-oriented features, we exploit the await operator to enforce the desired order of execution. For instance, the Constructor should execute first. Additionally, in our code, we denote variables using strings that begin with capital letters, while constants are enclosed in quotation marks.

The Constructor program is responsible for deploying the Bet_Contract. Let us assume a program named Owner initializes the variables InitialPot, Rate, Token, Oracle, and Deadline. Additionally, the variable OracleGetToken contains the returned value of the GetToken program, which is a part of the oracle contract, and it is used to check that the oracle contract allows the exchange between Ether and Token. Another program, Zero, assigns zero values to the variables InitialPot, Rate, Token, Oracle, and Deadline. The Constructor program awaits the initialization of the variables InitialPot, Rate, Token, Oracle, and Deadline. Subsequently, it verifies that the oracle program can exchange Ether and Token. If this is the case, it updates the variables BetOwner, BetOwnerWalletEther, BetWallet. We highlight the variable BetWallet in green as it is the variable we aim to safeguard from MEV attacks, meaning it will be designated as low-level. SenderBet ∶= 0 Similar to the Bet program, the Win program runs continuously until the deadline expires. It awaits the current player, whose name is stored in the variable Player, to claim victory. This indicates that when the player wishes to claim, they will use another program to modify the value of the variable SenderWin. Upon this action, the Win program compares the variables BetRate and AmmRateEther. If the latter is greater than the former, the player receives the entire value of the BetWallet. The variable AmmRateEther is highlighted in red because its value is determined and modified within the oracle program (AMM or Exchange in our example). We lack control over its value, making it a potential source of MEV attacks. SenderWin ∶= 'NULL' It's worth noting that we explicitly designate the variable BetWallet as low-level and AmmRateEther as high-level, while no specific designation is made for the other variables. In this scenario, we can consider them as low-level by default, which is equivalent to solely focusing on potential MEV attacks stemming from the variable AmmRateEther.

At this point, we have all the necessary ingredients to assess whether the program Bet_Contract meets our unwinding condition. Assuming that the only high-level variable is AmmRateEther, we observe that the sole high-level transition is triggered by line 5 of the Win program. When this transition occurs we reach a state which leads to the end of the program with the low level variable BetWallet equal to 0. However, if we modify only the high level variable AmmRateEther prior to the execution of line 5, the program ends with BetWallet being non-zero. This discrepancy is sufficient to infer that Bet_Contract fails to satisfy the unwinding condition, indicating interference from high to low and highlighting a potential source of MEV attacks.

This small example provides insight into the functionality of unwinding conditions, demonstrating their ability to analyze the program of interest independently of the blockchain environment in which it will ultimately operate. Additionally, unwinding conditions offer the benefit of identifying the precise instructions and variables within the code that could potentially be exploited as attack vectors.

However, we cannot draw a conclusion on the reliability of the Bet_Contract solely based on this analysis. It is imperative to delve deeper into the oracle programs to assess whether the potential attacks are indeed feasible. If these attacks are not deemed "realistic", we can then utilize the downgrading mechanism and consider the Bet_Contract as "secure".

Let us now examine the scenario where the oracle program is the AMM contract. Specifically, we will analyze its core functionalities, particularly operations that significantly impact the token's rate. An Automated Market Maker (AMM) is a decentralized finance (DeFi) algorithmic trading protocol that enables the automatic exchange of cryptographic tokens through the use of liquidity pools. Unlike traditional order book-based exchanges, AMMs provide liquidity through these pools, with prices determined algorithmically based on the token ratios within the pool. Automated Market Makers (AMMs) employ mathematical formulas to determine token prices within liquidity pools. The two predominant AMM formulas are the Constant Product Market Maker (CPMM) and the Constant Sum Market Maker (CSMM). In our case study, we use an AMM instance based on CPMM, which is expressed by the formula 𝐾 = 𝑋 * 𝑌 , where 𝑋 represents the amount of token T1 in the AMM, and 𝑌 represents the amount of token T2 in the AMM. This implies that the ratio of token quantities directly influences the price of one token relative to another. Furthermore, the formula ensures that, while the values for tokens 𝑋 and 𝑌 may fluctuate, the value for 𝐾 remains constant during trades or liquidity deposits.

The program GetRate returns the exchange rate between the two tokens T1 and T2, ensuring the constant product of their quantities as defined earlier. This program computes and provides the value of the variable AmmRateEther, which is used in the Win program within the Bet_Contract. Similarly, in the code, variables designated in red are considered high-level. Specifically, AmmRateT1 and AmmRateT2 must be high-level because they correspond to the variable AmmRateEther used in the Win program. Furthermore, the variables AmmWalletT1 and AmmWalletT2 also need to be high-level, their significance will become clear upon examining the Swap program. AmmRateT1 ∶= AmmWalletT1 AmmWalletT2 ;

T ∶= 'NULL' 8:

else if (T = 'T2') then 9:

AmmRateT2 ∶= AmmWalletT2 AmmWalletT1 ; T ∶= 'NULL' The Swap program enables token exchange based on the constant product K. The swapping operation is governed by the values of AmountToSwap and TokenToSwap specified by the sender. If the sender chooses to exchange AmountToSwap of token T1 for token T2, the program initially computes the corresponding amount required for AmountToSwap in T2. Subsequently, it verifies whether AmmWalletT2 holds adequate tokens to satisfy this amount. If it does, the program increases AmmWalletT1 by the specified AmountToSwap and decreases AmmWalletT2 accordingly to maintain the constant stored in the variable K. The same process occurs vice-versa if the sender chooses to swap T2 for T1. We posit the existence of a program, ZeroAMM, which is presumed to initialize the AmountToSwap and TokenToSwap variables to zero. AmmWalletT2 ∶= AmmWalletT2 + AmountToSwap;

ZeroAMM

As far as the levels of the variables are concerned, since AmmRateT1 and AmmRateT2 have to be high level, in order to ensure that the program Swap satisfies the unwinding condition, the variable Y has to be high too (see line 7). This in turn implies that AmmWalletT1 and AmmWalletT2 have to be high (see lines 8,9,16,17). Finally, this requires to the variable K to be high (see line 5).

We already observed that line 5 of the Win program causes a flow of information witnessing a possible MEV attack. Now that we possess a deeper understanding of the AMM contract, we can demonstrate the interference resulting from the interaction with the AMM contract, utilizing the LTS notation outlined in Section 2.1. Specifically, we will show how two executions of the same program starting with the same low level variable values can end with different values for the low level variable BetWallet. Let us consider the program:

Bet+Amm ≡ co Bet_Contract | | Amm_Contract oc

In particular, let us assume that we have reached the execution of:

co (co Bet | | Win | | Close oc) | | Amm_Contract oc

Moreover, the Player has been set to 'BOB'and he has already added his PotBet to the BetWallet. In this context, we designate the T1 token held within the AMM contract to represent Ethereum's native cryptocurrency, Ether. Thus, we denote AmmWalletT1 as AmmWalletEther and AmmRateT1 as AmmRateEther. We focus on a state 𝜎 in which the variables have the following values: AmmWalletEther = 600; AmmWalletT2 = 600; AmmRateEther = 1 AmountToSwap = 300; TokenToSwap=T2 BetWallet = 10; BetRate = 2; SenderWin = 'BOB' If the execution sequence begins with the code of the Swap program, followed by GetRate, which are part of the Amm_Contract, and concludes with the selection of Win, the resulting outcome is as These two executions result in a distinct value for the low level variable BetWallet, indicating a potential MEV attack. In fact, in the second execution the variable BetWallet has not been modified and reaches the end with value 10. Notice that we are not delving into the specific identities of the player and the user initiating the Swap. Nor we are assuming their ability to influence the scheduling order. We are simply observing two different low-level behaviors. Further analysis is required to ascertain the potential transformation of the first execution into a MEV attack. Naturally, if the player of the Bet contract also interacts with the AMM and possesses the authority to dictate transaction order as a miner, they can ensure a favorable outcome, thereby enabling the occurrence of a MEV attack, as highlighted in [18].

Let us now examine the scenario where we leverage the Exchange contract instead of relying on the AMM contract. In this case only the owner has the authority to modify the rate. Below, we model the pivotal functionality of the Exchange contract, wherein the rate is altered. SenderSetRate ∶= 'NULL' Let us modify the Win program at line 5 by replacing the variable AmmRateEther with the variable ExchangeRate. Our analysis on the Bet contract is not affected. We still observe that the unwinding condition is not satisfied witnessing a possible MEV attack. However, in this very simple example one can assume that when the player in the Bet contract is different from the owner of the Exchange contract, the player cannot be sure to win the bet. So, we can exploit the downgrading mechanism and modify the Win program as follows. Player ∶= 'NULL' In this specific scenario, the noninterference property remains unscathed when utilizing the Exchange contract as a price oracle, given that the adversary lacks the ability to manipulate the exchange rate. With the Exchange contract, only the owner holds the authority to adjust the exchange rate, rendering any attempts by adversaries to influence the exchange contract ineffective in altering the rate. However, it is essential to recognize that within this framework, there exists a potential information flow through interactions with the Exchange contract, particularly when the owner of the Exchange contract coincides with the owner or player of the Bet contract. This introduces the possibility of interference. However, interference does not arise when the player in the Bet contract differs from the owner of the Exchange contract. To differentiate this secure scenario from the potentially risky one described earlier, we rely on the Downgrading functionality embedded in our language.

The code implementation for this example encompasses smart contracts for Bet, AMM, and Eexchange functionalities. Furthermore, we've developed a USDC ERC20 token to enable a hands-on exchange experience with our custom token. The complete implementation in solidity can be found on GitHub via the following link: code repository.

Conclusion

In this paper, we explore the application of unwinding conditions to analyze Maximal Extractable Value (MEV) within the context of the Bet contract. Our investigation utilizes a simple imperative concurrent language to model the Bet contract, shedding light on scenarios where specific conditions impact MEV noninterference. This underscores potential vulnerabilities within decentralized finance (DeFi) services. This is a first step, while an in depth analysis of the relationships between unwinding conditions and MEV is left as future work.

Comparing our approach with the contribution of Bartoletti et al. in [18] (see also Appendix B), our focus lies in formalizing noninterference through unwinding conditions. By employing unwinding conditions, we abstract from the environment, enabling us to disregard the specific implementations of possible smart contracts interacting with the one under examination, unlike in [18]. Clearly this is an advantage from the computational point of view, since it allows us to analyse smaller system. Moreover, this approach facilitates the identification of critical points within the program that may lead to information flows, thereby enhancing the security analysis of smart contracts. On the other side, a second stage analysis of the dependencies is necessary in order to discard unrealistic sources of attacks.

Furthermore, the Bet contract case study presented in this paper illustrates the practical application of our methodology in identifying and mitigating MEV attacks. Overall, our work contributes to the comprehension and mitigation of MEV vulnerabilities in smart contracts within the realm of decentralized finance. As future work we also plan to apply our framework.

As future work we also plan to define our framework on fragments of languages for smart contracts, such as solidity, in order to avoid possible discrepancies introduced relying on an intermediate language. This is a difficult task due to the richness of languages for smart contracts. However, object oriented features would avoid us the use of programming tricks, such as the use of the away operator, for avoiding unwanted interleaving behaviors.

A. Operational Semantics

Table 1

The operational semantics.

B. MEV and Local MEV in [18]

In [18], the author delineates two notions of MEV. The first, termed global MEV, relies on the entire blockchain state 𝑆 to determine the value of MEV extracted from a contract Δ. This criterion introduced by Babel et al. in [17], referred to as 𝜀-composability, asserts that contracts Δ are composable in a blockchain state 𝑆 if adding Δ to 𝑆 does not afford the adversary a "significantly higher" Maximal Extractable Value (MEV). Formally, denoting by MEV(𝑆) the maximal value adversaries can extract from 𝑆, and with 𝑆|Δ representing the blockchain state 𝑆 extended with contracts Δ, the composability criterion of Babel et al. is expressed as:

Δ is 𝜀-composable in 𝑆 if MEV (𝑆|Δ) ≤ (1 + 𝜀) MEV (𝑆)(1)

where 𝜀 parameterizes the "not significantly higher" condition above. However, this approach has limitations as elucidated in [18]. For instance, utilizing the MEV of the entire state S as a baseline for comparison complicates the interpretation of the concrete security guarantee of ε-composability.

The second notion of MEV, introduced by Bartoletti et al., is Local MEV, termed MEV non-interference. This concept measures the maximal economic loss that adversaries can induce on a given set of contracts, unlike global MEV, which applies solely to the entire blockchain state. By adapting the definition of non-interference property to the DeFi setting, they stipulate that the MEV extractable from Δ (the public output) should remain unaffected by the dependencies of Δ (the private inputs). Formally, MEV non-interference holds when the MEV extractable from the contract accounts in Δ(i.e., †∆) using any contract in S | ∆ is exactly the same MEV that can be extracted using only the contracts in ∆. They introduce the following definition: