In the context of Blockchains and Decentralized Finance the notion of Maximal Extractable Value (MEV) is attracting more and more attention. MEV is the maximum gain that users-including miners and validators-can obtain by interacting with a smart contract and with its dependencies. Such profits witness attacks that also exploit strategic transaction manipulations (e.g., reordering transactions in blocks) and distort the meaning of smart contracts. The use of the notion of noninterference for modeling and analysing MEV attacks has recently been proposed in the literature. Noninterference aims to capture unwanted information flows in multi-level systems. Various definitions of noninterference have been presented, and among these those based on unwinding conditions allow the possible flows to be specifically located in a system. In this paper we investigate the use of such unwinding conditions to analyze MEV. We exploit a simple case study-the Bet contract-to highlight the advantages and disadvantages of our proposal.
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
technology1[
Despite the security assurances provided by blockchain technology, DeFi smart contracts possess
inherent vulnerabilities as highlighted in recent s6t]u.dWieitsh[ in the DeFi ecosystem, decentralized
exchanges (DEXs) play a central role by facilitating trustless transactions through smart contract
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 [
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 dependencies7[]. This potential for profit attracts not only legitimate users but also malicious actors who exploit strategic transaction manipulations, such as reordering transactions within block to manipulate the outcomes of smart contracts. These actors often employ automated bots to engage in frontrunning, exploiting transactional intricacies for potent8]i.alNgoatianbsle[ examples of MEV exploitation include instances of decentralized exchange (DEX) arbitrage, where participants exploit price diferences across decentralized exchange protoc9o].lsSu[ch 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 introd1u0c,1e1d,[
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 study1[
Structure of the paper. The structure of the paper is as follows: In Se1c,twioenpresent the case study of the Bet contract. Sect2ioinntroduces 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 diferentiate secure scenarios from potentially risky ones. Finally, Section 4 discusses related work and concludes the paper.
In this section we briefly introduce the main functionalities of a betting service, as also detailed in
[
We explore two instances of the oracle contract, with the first being an Automated Market Maker (AMM) inspired by the Uniswap protocol (shetet,ps://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, difers from the AMM contract in terms of rate setting. In the AMM, the rate is afected 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 unafected by variations in wallet values resulting from user interactions.1Fiilglursterates the primary functionalities of the Bet contract and its potential interactions with either AMM or Exchange.
As detailed in1[
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 gre enin Figure1). Such flow of information comes from the high level variable representing the exchange rate (denoted byina rFeigdure1), i.e., from a variable whose value can be altered by other contracts. Our approach ofers 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.
In [16] we considered an imperative concurrent language, inspired by the one introd1u9c]eadnidn [ proposed diferent 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 mechanism16in]. [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.
Letℤ be the set of integer number=s, { true,false} be the set of boolean valu esb,e a set of low level locations anℍd be a set of high level locations, w∩itℍh = ∅ . The setAexp of arithmetic expressions is defined by the grammar: ∶∶= | |
0 + 1 | 0 − 1 | 0 ∗ 1 . We assume that arithmetic expressions are total. TBheexspeotf boolean where ∈ ℤ and ∈ ∪ ℍ expressions is defined by: where 0, 1 ∈ Aexp.
∶∶= true| false| ( 0 = 1) | ( 0 ≤ 1) | ¬ | 0 ∧ 1 | 0 ∨ 1
We say that an arithmetic expres si oisnconfidential , denoted by ∈ high, if there is a high level location which occurs in it. Otherwise we sa y tishpautblic, denoted by ∈ low. Similarly, we say that a boolean expressionis confidential , denoted by ∈ high, if there is a confidential arithmetic expression which occurs in it. Otherwise we say tihsaptublic, 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 setProg 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 i1n9[], in the body of thaewait operator only sequences of assignments are allowed.
The operational semantics of our language is based on the nosttiaoten. oAf stat e is a function which assigns to each location an integer∶, i .∪e.ℍ, ⟶ ℤ . Given a state, we denote by [ /] the state′ such that′( ) =
and ′( ) = ( ) restriction ofto the low level locations and we w=rite for = .
for al l ≠ . Moreover, we denote by the
Given an arithmetic expressi o∈n Aexp and a stat e, the evaluation oifn , denoted by⟨, ⟩ → with ∈ ℤ , is defined in the standard way. Similarl⟨y,,⟩ → with ∈
denotes the evaluation of a boolean expressiinona 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 symebnodl (denoting termination) a n∈d{ high, low} stating that the transition is either confidential or public. The operation1∪ 2 returnlsow if both 1 and 2 arelow otherwise it returhnisgh. Letℙ = Prog∪{end} and Σ be the set of all the possible states. The operational sema⟨n, t⟩ic∈s ℙof× Σ is thelabelled transition system (LTS) defined by structural induction onaccording to the rules depicted in T1aibnle the Appendix. Intuitively, the semantics of the sequential composition imposes that a program of the form 0; 1 behaves lik e 0 unti l 0 terminates and then it behaves li1k. eTo describe the semantics of a program of the forwmhile() {}
we have to distinguish two cases:iisftrue, then the program is unravelled t;o while() {} ; otherwise it terminates. As far asatwhaeit operator is concerned, if is true thenawait() {}
terminates executi ngin one indivisible action, i.e., it is not possible to observe the state changes internal to the execu t,iwohniolef if is false thenawait() {} loops waiting for to become true. Finally, in a parallel composition of thceof or0m|… | oc any of the can move, and the termination is reached only when a l l’sthhaeve terminated.
We use the following notations. We w⟨r, i⟩te→ ⟨
low {low, high} and ⟨ 0, 0⟩ →
⟨ , ⟩ with ≥ 0 for⟨ 0, 0⟩ → ⟨ 1, 1⟩ → ⋯ → ⟨ −1 , −1 ⟩ → ⟨ , ⟩.
The notatio⟨n 0, 0⟩ ⇝ ⟨ , ⟩ stands for⟨ 0, 0⟩ → ⟨ , ⟩ for some ≥ 0 with all t hetransitions high ⇝ labelled witlhow; similarly⟨ 0, 0⟩ ⟨ , ⟩ stands for⟨ 0, 0⟩ → ⟨ , ⟩ for some ≥ 0 with at least one of thetransitions labelled whitihgh. Finally, we writ⟨e, ⟩ ⇝ ⟨ ′, ′⟩ to denote ′, ′⟩ to denote⟨, ⟩ → ⟨ ′, ′⟩ with ∈
⇝ ⟨ ′, ′⟩ with ∈ { low, high}.
Notice that the operational semantics defined in T1aibslneon-deterministic, since in the case of parallel composition there are many possible evolutions.
Intuitively, when we analyze a prog ratmhat 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 unafected. 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 prograamnd 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 1[
low level observer; • a binary relatio≑nwhich equates two pai⟨r,s⟩ and ⟨, ⟩ if they are indistinguishable for a A pair⟨, ⟩ satisfies (an instance of) our unwinding framework (i.e., there are no flows of informahigh →
⟨, ⟩ tion from high to low) if any high level ⟨s ,t ⟩ep 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 s{e⟨ t,⟩ | ≐ } reaching an element of the {s⟨e, t⟩ | ⟨, ⟩ ℛ(⟨, ⟩) = {⟨ , ⟩ | ⟨, ⟩ℛ⟨ , ⟩}
. low level observer). We use the notaℛtio(⟨n, ⟩)
to denote the set of pairs reachable ⟨fr,o⟩m , i.e., (whose states are low level equivalent) may perform a transition ≑ ⟨, ⟩}
(whose elements are all indistinguishable for a Definition 1. (Generalized Unwinding) Let≐ be a binary relation ovΣe,rℛ and≑ be two binary relations oveℙr× Σ. We define the unwinding class (≐, ℛ, ≑) by: (≐, ℛ, ≑) = {⟨, ⟩ ∈
Prog × Σ ∣ ∀ ⟨ , ⟩ ∈ ℛ(⟨, ⟩) def 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 suficient foundation for our analysis in the subsequent section focusing on our case study. high ⟶ ⟨, ⟩ ⇝ ⟨ end, ′⟩ ⟨, ⟩ = ↑ ↓ ↑ ↓ ⟨, ⟩ ⟶ ⟨, ⟩ ⇝ ⟨ ↑ ↓ ≈ ↑ ↓ ↑ ↓ ↑ ↓ ′ = ′ end, ′⟩ they assign the same values to the low level variables, i.e., we c≐ontsoidbeer the relatio=n. The relationℛ is the notion of reachability we rely on⇝,i.eis., 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 presente2d0]inco[uld 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 instantia≑taes ≈ defined as follows. ⟨, ⟩ ⇝ ⟨
end, ′⟩, there exists a pa⟨iernd, ′⟩ such that⟨, ⟩ ⇝ ⟨ Definition 2 (≈ ). Let⟨, ⟩ and⟨, ⟩ be two pairs. It holds th⟨,a⟩t≈ ⟨, ⟩
if and only if whenever 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, tsthaetpeasir⟨, ⟩ 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 wor1k6],[ 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 Fig2u,rseuch 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){ ∶= } Let be high level and be low level. Apparently, when we reach the if test the value of the high level variable i0s, 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 valu0eto 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 pa ralhlaesl with modified the value of , thus allowing to take the if branch and reveal the value of the vtaoriable the low level user.
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 reledaoswenogrrading of
sensitive information (e.g., password checking, information purchase, and spreadsheet computation)
[
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 previous1w6]o, rwke[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 cdaowllnegdrade that maps any arithmetic or boolean expression to itself, while altering its confidentialitylloewv. eClotnosequently, the operational semantics of program instructions invodlovwinnggrade are declassified to the low level, and they are not considered as dangerous in the unwinding test.
Example 2. We consider again the progr amof Example1. If we know that revealing to the low level user the value ofis not dangerous, and it is necessary (e.g., the system administrator needs to send to the user a message), then we can modify the pro graasmfollows: ≡ ∶= 0; ∶= downgrade( ); if( > 0){ ∶= } If is low level, the only point where we should check the unwinding condition, is the second assignment instruction. However, since dtohwengrade 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 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 Eth 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, BetOwnerWalBletWEtahlelre.,tWe highlight the variabBleetWalleitn green as it is the variable we aim to safeguard from MEV attacks, meaning it will be designated as low-level.
Zero
The Bet program continuously runs until the deadline set by the Bet_Contract owner in the variable Deadline is expired. It waits for the Player to be ‘NULL’ and for PotBet to be non zero. The condition for Player to be ’NULL’ ensures that another user is not already placing a bet. Additionally, PotBet must be non-zero, indicating that the Player program has initialized the variables PotBet and SenderBet. If the PotBet is valid, the program updates the variables Player, PlayerWalletEther, and BetWalle.t 1: Program Bet 2: while (Deadline> BlockNum) do 3: await (Player = ‘NULL’ ∧ PotBet ≠0d)o 4: skip 5: if (PotBet= BetWalle)tthen 6: Player∶= SenderBet; 7: PlayerWalletEth∶e=r PlayerWalletEth−erPotBet; 8: BetWalle∶t= BetWalle+t PotBet 9: else 10: 11:
PotBet∶= 0;
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 BetRAamtemaRnadteEthe.rIf the latter is greater than the former, the player receives the entire vBaeltuWe aolflte.htTehe variable AmmRateEtheris 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.
1: Program Win 2: while (Deadline> BlockNum) do 3: await ( SenderWin = Playerd)o 4: skip 5: if (BetRate< AmmRateEthe)rthen 6: PlayerWalletEth∶e=r PlayerWalletEth+erBetWalle;t 7: BetWalle∶t= 0 8: 9: 1: Program Constructor 2: await ( InitialPot ≠0 ∧ BetRate ≠0 ∧ Deadline ≠0 ∧ Oracle ≠0 ∧ Tokedno≠0) 3: GetToken 4: if (Token≠ ‘Ether’∧ OracleGetToke=n (‘Ether’ , Token)) then 5: BetOwner∶= SenderConstruct;or 6: BetOwnerWalletEth∶e=rBetOwnerWalletEth−eIrnitialPo; t 7: BetWalle∶t= BetWalle+t InitialPot 8: else 9: else
SenderWin∶= ‘NULL’ It’s worth noting that we explicitly designate the vBaertiWaballeleats low-level anAdmmRateEther 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 variablAemmRateEthe.r
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 varAimabmlReaitseEthe,rwe 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 levBeeltvWarailalbelte equal to0. However, if we modify only the high level variaAbmlmeRateEtherprior to the execution of line 5, the program ends wiBtehtWallebteing non-zero. This discrepancy is suficient 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 ofer 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 toke ns and may fluctuate, the value fo r 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 variablAemmRateEthe,rwhich is used in the Win program within the Bet_Contract. Similarly, in the code, variables designated in red are considered high-level. SpeAcmificmaRllayt, eT1 and AmmRateT2 must be high-level because they correspond to the varAimabmlReateEtherused in the Win program. Furthermore, the variabAlmesmWalletT1andAmmWalletT2also need to be high-level, their significance will become clear upon examining the Swap program.
1: Program GetRate 2: while true do 3: await ( T ≠‘NULL’) do 4: skip 5: if (T = ‘T1’) then 6: AmmRateT1 ∶= AAmmmmWWaalllleettTT12; 7: T ∶= ‘NULL’ 8: else if (T = ‘T2’) then 9: AmmRateT2 ∶= AAmmmmWWaalllleettTT21; 10: T ∶= ‘NULL’ 11: else 12:
T ∶= ‘NULL’
The Swap program enables token exchange based on the constant prKo.dTuhcte 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 whetherAmmWalletT2holds adequate tokens to satisfy this amount. If it does, the program increases AmmWalletT1by the specified AmountToSwap and decreaseAsmmWalletT2accordingly to maintain
ZeroAMM
As far as the levels of the variables are concerned,AsminmcReateT1 and AmmRateT2 have to be high level, in order to ensure that the program Swap satisfies the unwinding condition, thYe variable has to be high too (see line 7). This in turn impliesAtmhmaWtalletT1andAmmWalletT2have to be high (see lines 8,9, 16, 17). Finally, this requires to the vaKriatoblbee 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 LT notation outlined in Sect2i.o1n.Specifically, we will show how two executions of the same program starting with the same low level variable values can end with diferent values for the low level variable BetWalle.tLet us consider the program:
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 PotBeBtetoWtahllee.tIn 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 st atien which the variables have the following values: AmmWalletEthe=r 600; AmmWalletT2= 600; AmmRateEther= 1
AmountToSwap= 300; TokenToSwap=T2
BetWalle=t 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 Conversely, if Win is executed prior to Swap, and then Swap follows, the outcome difers: These two executions result in a distinct value for the low levelBveatrWiaabll e,tindicating a potential MEV attack. In fact, in the second execution the BvaetrWiabalelehtas not been modified and reaches the end with val1u0e. 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 diferent 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 a miner, they can ensure a favorable outcome, thereby enabling the occurrence of a MEV attack, as highlighted in18[].
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.
1: Program SetRate 2: while true do 3: await (NewRate ≠0 ∧ SenderSetRate = ExchangeOwndeor) 4: skip 5: ExchangeRate∶= NewRate; 6: NewRate∶= 0; 7: SenderSetRat∶e= ‘NULL’
Let us modify the Win program at line 5 by replacing the varAimabmlReateEtherwith the variable ExchangeRat.eOur analysis on the Bet contract is not afected. 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 diferent 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 exchang rate. With the Exchange contract, only the owner holds the authority to adjust the exchange rate, re dering any attempts by adversaries to influence the exchange contract inefective in altering the rate. However, it is essential to recognize that within this framework, there exists a potential information lfow 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 difers from the owner of the Exchange contract. To diferentiate 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 licnokd:e repositor.y
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 Bartoletti1e8t] (asle.eianl[so AppendixB), 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, 1u8n]l.ikCeleinar[ly 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 dificult 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.
This work has been partially supported by the Project PRIN 2020 “Nirvana - Noninterference and Reversibility Analysis in Private Blockchains”, and by the project SERICS (PE00000014) under the MUR National Recovery and Resilience Plan funded by the European Union - NextGenerationEU.
Wesley, 2000. [16] A. Bossi, C. Piazza, S. Rossi, Compositional information flow security for concurrent programs, 2023, pp. 2499–2516. doi:10.1109/SP46215.2023.10179346.
A. Operational Semantics
⟨skip, ⟩ l→ow ⟨end, ⟩ ⟨ 0, ⟩ → ⟨ 0′, ′⟩ ⟨ 0; 1, ⟩ → ⟨ 0′; 1, ′⟩
0′ ≢ end ⟨if() { 0} else { 1}, ⟩ → ⟨ 0, ⟩ ⟨, ⟩→ true ⟨, ⟩→ true ⟨while() {}, ⟩
→ ⟨; while() {}, ⟩ ⟨, ⟩→ true ⟨, ⟩ ⟨await() {}, ⟩ →1∪ 2 ⟨end, ′⟩
⇝2 ⟨end, ′⟩ ∈ 1 ⟨ , ⟩ → ⟨ ′, ′⟩ ∈ ∈ ⟨, ⟩ →
⟨ ∶= , ⟩ → ⟨end, [ /]⟩
∈ ⟨ 0, ⟩ → ⟨end, ′⟩
⟨ 0; 1, ⟩ → ⟨ 1, ′⟩ ⟨, ⟩→ false ⟨if() { 0} else { 1}, ⟩ → ⟨ 1, ⟩ ⟨, ⟩→
false ⟨while() {}, ⟩ → ⟨end, ⟩
∈ ⟨, ⟩→
false ⟨await() {}, ⟩ → ⟨await() {}, ⟩ ∈ ∈ ⟨co 1| … | | … | oc, ⟩ → ⟨co 1| … | ′| … | oc, ′⟩ ⟨co end| … |end| … |end oc, ⟩ l→ow ⟨end, ⟩
In [
MEV(|Δ, †Δ) = MEV†Δ(|Δ, †Δ). (2)