pith. sign in

arxiv: 2606.05418 · v1 · pith:APHOSUOQnew · submitted 2026-06-03 · 💻 cs.CR · cs.SE

A formal framework for the economic security of DeFi compositions

Massimo Bartoletti , Riccado Marchesin , Roberto Zunino This is my paper

Pith reviewed 2026-06-28 05:15 UTC · model grok-4.3

classification 💻 cs.CR cs.SE
keywords DeFiMEVcomposabilitysmart contractseconomic securityformal methodsblockchainnon-interference
0
0 comments X

The pith

MEV non-interference requires that new DeFi contracts do not increase the maximal extractable value obtainable through interactions with existing blockchain state.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines MEV non-interference as a formal property for safe DeFi composition: newly deployed contracts must not allow greater economic extraction when they interact with the pre-existing blockchain state. It supports this with local MEV, a measure focused on losses to a designated set of victim contracts, and analyzes two models of adversary wealth. Sufficient conditions and locality principles are given to support modular checks of composability. The framework is applied to exchanges, AMMs, lending pools and similar services to classify which compositions remain secure and which become vulnerable.

Core claim

We introduce MEV non-interference, a formal security notion for DeFi composability requiring that the maximal extractable value from a set of newly deployed contracts is not increased by interactions with the existing blockchain state. To support this notion, we define local MEV, a novel measure of economic attacks that focusses on the loss of a given set of victim contracts. We study two adversarial models, with bounded and unbounded wealth, and establish sufficient conditions and locality principles that enable modular reasoning about secure composability. We apply the framework to representative DeFi compositions, including exchanges, AMMs, options, lending pools, routers, and arbitrage c

What carries the argument

MEV non-interference: the property that maximal extractable value from new contracts does not increase due to interactions with existing blockchain state, supported by the definition of local MEV that isolates losses to specific victim contracts.

If this is right

  • Compositions satisfying the sufficient conditions can be checked for security without examining the entire existing blockchain state.
  • Designers can use the locality principles to add new contracts while preserving the non-interference property of prior ones.
  • The distinction between secure and vulnerable compositions applies directly to common services such as AMMs, lending pools, and arbitrage routers.
  • Both bounded-wealth and unbounded-wealth analyses are available, allowing security arguments under different resource assumptions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same non-interference check could be applied to protocol upgrades that alter existing contracts rather than only new deployments.
  • Automated static analysis tools could be built to verify the sufficient conditions on contract source code before deployment.
  • The framework might be extended to quantify the exact increase in extractable value when non-interference fails, rather than only detecting its presence.

Load-bearing premise

The two adversarial models of bounded and unbounded wealth together with the definitions of local MEV and MEV non-interference suffice to capture the relevant economic attacks arising in real DeFi compositions.

What would settle it

A concrete DeFi composition in which interactions with existing state demonstrably increase the maximal extractable value beyond the local MEV of the new contracts, yet the framework still classifies the composition as satisfying non-interference.

read the original abstract

Decentralized Finance (DeFi) services are usually constructed by composing a variety of smart contracts. While composability is a key driver of the success of DeFi, it also creates security risks: adversaries may exploit interactions between newly deployed contracts and the pre-existing ones to inflict economic losses. We introduce MEV non-interference, a formal security notion for DeFi composability requiring that the maximal extractable value from a set of newly deployed contracts is not increased by interactions with the existing blockchain state. To support this notion, we define local MEV, a novel measure of economic attacks that focusses on the loss of a given set of victim contracts. We study two adversarial models, with bounded and unbounded wealth, and establish sufficient conditions and locality principles that enable modular reasoning about secure composability. We apply the framework to representative DeFi compositions, including exchanges, AMMs, options, lending pools, routers, and arbitrage contracts, showing how it distinguishes secure compositions from vulnerable ones. Our results provide a formal foundation for reasoning about the economic security of DeFi compositions.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 0 minor

Summary. The paper introduces MEV non-interference as a formal security notion for DeFi composability, requiring that the maximal extractable value from a set of newly deployed contracts is not increased by interactions with the existing blockchain state. It defines local MEV as a measure focused on losses to a given set of victim contracts, studies adversarial models with bounded and unbounded wealth, establishes sufficient conditions and locality principles enabling modular reasoning, and applies the framework to representative compositions (exchanges, AMMs, options, lending pools, routers, arbitrage contracts) to distinguish secure from vulnerable ones.

Significance. If the results hold, the work supplies a formal foundation for economic security reasoning in DeFi compositions. The definitions of MEV non-interference and local MEV, together with the locality principles and concrete applications to standard DeFi primitives, constitute a modeling contribution that supports modular analysis and could aid protocol design and verification.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the paper, accurate summary of the contributions, and recommendation to accept. We are pleased that the formal notions of MEV non-interference and local MEV, along with the locality principles and applications to DeFi primitives, are recognized as providing a foundation for modular economic security reasoning.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper introduces new formal definitions (MEV non-interference, local MEV) and two adversarial models (bounded/unbounded wealth) as modeling primitives, then derives sufficient conditions and locality principles from them. No equations reduce a claimed prediction or result to a fitted input by construction, no self-citation is load-bearing for the central claims, and no ansatz or uniqueness theorem is smuggled in. The applications to DeFi compositions (exchanges, AMMs, etc.) are direct uses of the definitions rather than statistical predictions. This is a self-contained formal modeling contribution whose soundness does not rely on circular reductions.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

Review performed on abstract only; ledger entries are therefore provisional and limited to what is stated in the abstract.

axioms (1)
  • domain assumption Blockchain state and contract interactions can be modeled as a formal system in which maximal extractable value is well-defined.
    Required for the definitions of MEV non-interference and local MEV to be meaningful.
invented entities (2)
  • MEV non-interference no independent evidence
    purpose: Formal security property for composability
    Newly introduced notion whose independent evidence would require concrete proofs or case studies not visible in the abstract.
  • local MEV no independent evidence
    purpose: Measure of economic loss focused on victim contracts
    Newly introduced measure whose independent evidence would require concrete proofs or case studies not visible in the abstract.

pith-pipeline@v0.9.1-grok · 5718 in / 1236 out tokens · 20654 ms · 2026-06-28T05:15:29.762895+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

32 extracted references · 15 canonical work pages

  1. [1]

    Defi Pulse: What is DeFi? understanding Decentralized Finance, www.defipulse.com/blog/what-is-defi (2019)

    2019

  2. [2]

    Werner, D

    S. Werner, D. Perez, L. Gudgeon, A. Klages-Mundt, D. Harz, W. J. Knottenbelt, SoK: Decentralized Finance (DeFi), in: ACM Conference on Advances in Financial Technologies, (AFT), ACM, 2022, pp. 30–46.doi:10.1145/3558535.3559780

    work page doi:10.1145/3558535.3559780 2022

  3. [3]

    Kitzler, F

    S. Kitzler, F. Victor, P. Saggese, B. Haslhofer, A systematic investigation of DeFi compositions in Ethereum, in: Financial Cryptography and Data Security Workshops, Vol. 13412 of LNCS, Springer, 2022, pp. 272–279.doi:10.1007/978-3-031-32415-4\_18

    work page doi:10.1007/978-3-031-32415-4 2022

  4. [4]

    Kitzler, F

    S. Kitzler, F. Victor, P. Saggese, B. Haslhofer, Disentangling Decentralized Finance (DeFi) composi- tions, ACM Trans. Web 17 (2) (2023) 10:1–10:26.doi:10.1145/3532857

    work page doi:10.1145/3532857 2023

  5. [5]

    Flash boys 2.0: Frontrunning in decentralized exchanges, miner extractable value, and consensus instability

    P. Daian, S. Goldfeder, T. Kell, Y. Li, X. Zhao, I. Bentov, L. Breidenbach, A. Juels, Flash boys 2.0: Frontrunning in decentralized exchanges, miner extractable value, and consensus instability, in: IEEE Symp. on Security and Privacy, IEEE, 2020, pp. 910–927.doi:10.1109/SP40000.2020.00040

    work page doi:10.1109/sp40000.2020.00040 2020

  6. [6]

    Gudgeon, D

    L. Gudgeon, D. Pérez, D. Harz, B. Livshits, A. Gervais, The decentralized financial crisis, in: Crypto Valley Conference on Blockchain Technology (CVCBT), IEEE, 2020, pp. 1–15.doi:10.1109/ CVCBT50464.2020.00005

    arXiv 2020

  7. [7]

    Furucombo website,https://furucombo.app(September 2023)

    2023

  8. [8]

    In: IEEE S&P (2023).https://doi.org/10.1109/SP46215.2023.10179435

    K. Babel, P. Daian, M. Kelkar, A. Juels, Clockwork finance: Automated analysis of economic security in smart contracts, in: IEEE Symposium on Security and Privacy, IEEE Computer Society, 2023, pp. 622–639.doi:10.1109/SP46215.2023.00036

    work page doi:10.1109/sp46215.2023.00036 2023

  9. [9]

    J. A. Goguen, J. Meseguer, Security policies and security models, in: IEEE Symposium on Security and Privacy, IEEE Computer Society, 1982, pp. 11–20.doi:10.1109/SP.1982.10014

    work page doi:10.1109/sp.1982.10014 1982

  10. [10]

    P. Y. A. Ryan, S. A. Schneider, Process algebra and non-interference, in: IEEE Computer Security Foundations Workshop, IEEE Computer Society, 1999, pp. 214–227.doi:10.1109/CSFW.1999.779775

    work page doi:10.1109/csfw.1999.779775 1999

  11. [11]

    P. Y. A. Ryan, J. D. McLean, J. K. Millen, V. D. Gligor, Non-interference: Who needs it?, in: IEEE Computer Security Foundations Workshop, IEEE Computer Society, 2001, pp. 237–238.doi:10.1109/ CSFW.2001.930149

    arXiv 2001

  12. [12]

    Backes, B

    M. Backes, B. Pfitzmann, Computational probabilistic non-interference, in: European Symposium on Research in Computer Security (ESORICS), Vol. 2502 of LNCS, Springer, 2002, pp. 1–23.doi:10. 1007/3-540-45853-0\_1. 41

    2002

  13. [13]

    Giacobazzi, I

    R. Giacobazzi, I. Mastroeni, Abstract non-interference: parameterizing non-interference by abstract interpretation, in: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, 2004, pp. 186–197.doi:10.1145/964001.964017

    work page doi:10.1145/964001.964017 2004

  14. [14]

    Bartoletti, R

    M. Bartoletti, R. Zunino, A theoretical basis for MEV, in: Financial Cryptography and Data Security, LNCS, Springer, 2025, pp. 225–242.doi:10.1007/978-3-032-07035-7\_14

    work page doi:10.1007/978-3-032-07035-7 2025

  15. [15]

    K. Qin, L. Zhou, B. Livshits, A. Gervais, Attacking the DeFi ecosystem with Flash Loans for fun and profit, in: Financial Cryptography, Vol. 12674 of LNCS, Springer, 2021, pp. 3–32.doi:10.1007/ 978-3-662-64322-8_1

    2021

  16. [16]

    Flashbots,flashbots.net(2021)

    2021

  17. [17]

    Blackshear, E

    S. Blackshear, E. Cheng, D. L. Dill, V. Gao, B. Maurer, T. Nowacki, A. Pott, S. Qadeer, D. Rain, S. Russi, T. Sezer, R. Zakian, Zhou, Move: A language with programmable resources, 2019. URLhttps://api.semanticscholar.org/CorpusID:201681125

    2019

  18. [18]

    Angeris, T

    G. Angeris, T. Chitra, Improved price oracles: Constant Function Market Makers, in: ACM Conference on Advances in Financial Technologies (AFT), ACM, 2020, pp. 80–91,https://arxiv.org/abs/2003. 10001.doi:10.1145/3419614.3423251

    work page doi:10.1145/3419614.3423251 2020

  19. [19]

    Angeris, H.-T

    G. Angeris, H.-T. Kao, R. Chiang, C. Noyes, T. Chitra, An analysis of Uniswap markets, Cryptoeco- nomic Systems 1 (1) (2021).doi:10.21428/58320208.c9738e64

    work page doi:10.21428/58320208.c9738e64 2021

  20. [20]

    J. Xu, N. Vavryk, K. Paruch, S. Cousaert, SoK: Decentralized exchanges (DEX) with automated market maker (AMM) protocols, ACM Comput. Surv. (nov 2022).doi:10.1145/3570639

    work page doi:10.1145/3570639 2022

  21. [21]

    Bartoletti, J

    M. Bartoletti, J. H. Chiang, A. Lluch-Lafuente, A theory of Automated Market Makers in DeFi, Logical Methods in Computer Science 18 (4) (2022).doi:10.46298/lmcs-18(4:12)2022

    work page doi:10.46298/lmcs-18(4:12)2022 2022

  22. [22]

    Aave v1 flashloan receiver interface,https://github.com/aave/aave-protocol/ blob/efaeed363da70c64b5272bd4b8f468063ca5c361/contracts/flashloan/interfaces/ IFlashLoanReceiver.sol#L11(2020)

    2020

  23. [23]

    Guesmi, C

    S. Guesmi, C. Piazza, S. Rossi, Noninterference analysis for smart contracts: Would you bet on it?, in: Distributed Ledger Technology Workshop (DLT), Vol. 3791 of CEUR Workshop Proceedings, CEUR- WS.org, 2024. URLhttps://ceur-ws.org/Vol-3791/paper12.pdf

    2024

  24. [24]

    Priyadarshini, M

    E. Priyadarshini, M. Bartoletti, A quantitative notion of economic security for smart contract compositions, in: Financial Cryptography Workshops, Springer-Verlag, p. 147–163.doi:10.1007/ 978-3-032-00492-5\_11

  25. [25]

    Bartoletti, R

    M. Bartoletti, R. Marchesin, R. Zunino, DeFi composability as MEV non-interference, CoRR abs/2309.10781 (2023).arXiv:2309.10781,doi:10.48550/ARXIV.2309.10781. URLhttps://doi.org/10.48550/arXiv.2309.10781

    work page doi:10.48550/arxiv.2309.10781 2023

  26. [26]

    L. Zhou, K. Qin, C. F. Torres, D. V. Le, A. Gervais, High-Frequency Trading on Decentralized On- Chain Exchanges, in: IEEE Symp. on Security and Privacy, IEEE, 2021, pp. 428–445.doi:10.1109/ SP40001.2021.00027

    arXiv 2021

  27. [27]

    UnderstandingtheDAOattack,http://www.coindesk.com/understanding-dao-hack-journalists/

  28. [28]

    A Postmortem on the Parity Multi-Sig library self-destruct,https://goo.gl/Kw3gXi(November 2017)

    2017

  29. [29]

    Bartoletti, S

    M. Bartoletti, S. Lande, M. Murgia, R. Zunino, Verifying liquidity of recursive Bitcoin contracts, Log. Methods Comput. Sci. 18 (1) (2022).doi:10.46298/lmcs-18(1:22)2022. 42 Theorem 2 Theorem 3Theorem 4 Theorem 5 Theorem 6 Theorem 8 Theorem 9 Theorem 10 Theorem 11Theorem 12 Theorem 13 Theorem 15 Theorem 14 Theorem 17 Theorem 18 Figure A.1: Dependencies am...

    work page doi:10.46298/lmcs-18(1:22)2022 2022

  30. [30]

    To show this, letY i be derived from ai:C i.fi(argsi)

    Each transactionY i in ⃗Ycan be funded by the adversary. To show this, letY i be derived from ai:C i.fi(argsi). We have the following cases: •a i =M i. By contradiction, assume that in the state where that transaction is executed,Mi does not have the tokens needed to fund the call toCi. Since the corresponding transactionXj in ⃗X was valid, this means tha...

  31. [31]

    The transactionsY i that are in ⃗Ydue to condition (B) have callee in∂(C,D)by Claim (1), and so their methods aresender-agnosticby assumption (1). So, the fact that in the execution ofY i they are called directly from a user address, while in the execution ofXi they are called from a contract address, does not affect the execution of these calls. Note tha...

  32. [32]

    This difference however does not affect the loss ofC, since Ci,j−1 is not indeps(C)by condition (B)

    The transactionM i:C i,j.fi,j(argsi,j)that are in ⃗Ydue to condition (B) may transfer tokens toM i, while the corresponding callsCi,j−1:C i,j.fi,j(argsi,j)due to the execution of⃗Xmay send these tokens to the senderCi,j−1, thus affecting its gain. This difference however does not affect the loss ofC, since Ci,j−1 is not indeps(C)by condition (B). For the ...