Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A theoretical basis for MEV

Massimo Bartoletti, Roberto Zunino

TL;DR

The paper formalizes Maximal Extractable Value (MEV) on public blockchains by building an abstract, cryptography-inspired model where contracts are state-transition systems, actors hold finite token sets, and wealth is measured additively. It introduces a transaction-deducibility framework ${\kappa_{\mathcal{A}}}$ that captures how adversaries combine private knowledge with mempool data, defines MEV for any actor set ${MEV_{\mathcal{A}}}$, and extends this to a universal MEV via a minimax game with token redistributions ${\approx_{\$}}$, including a variant for 'bad MEV'. The authors prove key properties like existence, monotonicity with respect to mempools and wallets, and finite-mev realizability, then apply the theory to a suite of contracts (e.g., Whitelist, Blacklist, Bank, HTLC, AMM, Crowdfund, Bounty, Lending Pool) to classify MEV-freedom, revealing both MEV-free and attackable cases. By providing formal definitions, proofs, and a benchmark of use cases, the work lays a rigorous foundation for analyzing and mitigating MEV in smart contracts and informs contract design to resist MEV exploitation.

Abstract

Maximal Extractable Value (MEV) refers to a wide class of economic attacks to public blockchains, where adversaries with the power to reorder, drop or insert transactions in a block can "extract" value from smart contracts. Empirical research has shown that mainstream DeFi protocols are massively targeted by these attacks, with detrimental effects on their users and on the blockchain network. Despite the increasing real-world impact of these attacks, their theoretical foundations remain insufficiently established. We propose a formal theory of MEV, based on a general, abstract model of blockchains and smart contracts. Our theory is the basis for proofs of security against MEV attacks.

A theoretical basis for MEV

TL;DR

The paper formalizes Maximal Extractable Value (MEV) on public blockchains by building an abstract, cryptography-inspired model where contracts are state-transition systems, actors hold finite token sets, and wealth is measured additively. It introduces a transaction-deducibility framework that captures how adversaries combine private knowledge with mempool data, defines MEV for any actor set , and extends this to a universal MEV via a minimax game with token redistributions }}$, including a variant for 'bad MEV'. The authors prove key properties like existence, monotonicity with respect to mempools and wallets, and finite-mev realizability, then apply the theory to a suite of contracts (e.g., Whitelist, Blacklist, Bank, HTLC, AMM, Crowdfund, Bounty, Lending Pool) to classify MEV-freedom, revealing both MEV-free and attackable cases. By providing formal definitions, proofs, and a benchmark of use cases, the work lays a rigorous foundation for analyzing and mitigating MEV in smart contracts and informs contract design to resist MEV exploitation.

Abstract

Maximal Extractable Value (MEV) refers to a wide class of economic attacks to public blockchains, where adversaries with the power to reorder, drop or insert transactions in a block can "extract" value from smart contracts. Empirical research has shown that mainstream DeFi protocols are massively targeted by these attacks, with detrimental effects on their users and on the blockchain network. Despite the increasing real-world impact of these attacks, their theoretical foundations remain insufficiently established. We propose a formal theory of MEV, based on a general, abstract model of blockchains and smart contracts. Our theory is the basis for proofs of security against MEV attacks.
Paper Structure (33 sections, 30 theorems, 74 equations, 12 figures, 1 table)

This paper contains 33 sections, 30 theorems, 74 equations, 12 figures, 1 table.

Table of Contents

  1. Introduction
  2. Blockchain model
  3. Maximal Extractable Value
  4. Adversary model
  5. MEV extractable by a given set of actors
  6. Universal MEV
  7. Proving MEV-freedom
  8. Related work
  9. Limitations and conclusions
  10. Long-range attacks
  11. Computational adversaries
  12. Cost of MEV
  13. Good vs. bad MEV
  14. Private order flows
  15. A concrete contract language
  16. ...and 18 more sections

Key Result

Proposition 1

$\mathit{\gamma}_{{\color{ForestGreen}{\tt \mathcal{A}}}_{\color{ForestGreen}{}}}$ is always defined and has a finite integer value, given by $\mathit{\gamma}_{{\color{ForestGreen}{\tt \mathcal{A}}}_{\color{ForestGreen}{}}} = \sum_{{\color{ForestGreen}{\tt A}}_{\color{ForestGreen}{{}}}\xspace\in {\c

Figures (12)

  • Figure 1: A Hash Time Locked Contract.
  • Figure 2: Whitelist, Blacklist and Bank contracts.
  • Figure 3: Syntax of contracts and transactions.
  • Figure 4: Semantics of contracts.
  • Figure 5: A Hash Time Locked Contract.
  • ...and 7 more figures

Theorems & Definitions (58)

  • Definition 1: Contract
  • Definition 2: Wealth
  • Definition 3: Gain
  • Proposition 1
  • Definition 4: Transaction deducibility
  • Proposition 2
  • Definition 5: MEV
  • Proposition 3
  • Proposition 4
  • Proposition 5
  • ...and 48 more