A quantitative notion of economic security for smart contract compositions

Emily Priyadarshini; Massimo Bartoletti

REVIEW 5 major objections 4 minor 27 references

A quantitative notion of economic security for smart contract compositions

T0 review · 5 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper introduces MEV interference, a quantitative measure of how much an adversary's ability to manipulate a surrounding smart-contract context amplifies economic losses to newly deployed contracts.

desk verdict A quantitative MEV-interference ratio with real proofs, but the lending-pool example silently assumes Cmin<1 and needs fixing. read the letter →

arxiv 2505.19006 v1 pith:IUDZLN5U submitted 2025-05-25 cs.CR

Emily Priyadarshini , Massimo Bartoletti This is my paper · ORCID

classification cs.CR

keywords smartcontractsDeFiMEVeconomicsecuritynon-interferenceoraclemanipulationquantitativelendingprotocols

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper introduces a quantitative security notion, MEV interference, that measures how much an adversary's ability to manipulate the surrounding context amplifies economic losses to newly deployed smart contracts. It extends the earlier binary MEV non-interference relation into a continuous scale from 0 to 1, where zero means the context adds nothing to an attack and one means all extractable loss comes from manipulating the context. The paper proves basic properties of the measure (boundedness, monotonicity, wallet independence, and invariance under front-running under certain conditions) and applies it to archetypal DeFi compositions, producing closed-form interference formulas for airdrop, exchange, bet, and lending-pool contracts. A sympathetic reading is that this provides the first quantitative, state-dependent way to rank how dangerous a context is to a set of contracts, rather than merely classifying a composition as secure or insecure.

What carries the argument

The load-bearing object is the MEV interference ratio of Definition 1, which compares two 'local MEV' quantities over the same target contracts: the maximum loss adversaries can inflict when restricted to calling only the target contracts, versus when they may also call the surrounding context. The ratio is normalized into [0,1] by subtracting from 1 the restricted-to-unrestricted loss ratio, and it is set to 0 when the unrestricted loss is 0. Every theorem in the paper is a statement about how this ratio behaves when the context is widened or when the adversary's callable set is changed, and the use cases are closed-form evaluations of the ratio for concrete contracts.

What would settle it

Find a real or constructible smart-contract composition with a reentrant or cyclic call graph in which an adversary can route an internal call from a target contract back into the context, and show that the unrestricted MEV then exceeds what the paper's formula assigns to any well-formed state; this would break Lemma A.3, which Theorem 3 uses.

Watch

Extended reading notes

Core claim

Definition 1 defines the MEV interference of a state S on contracts ∆ as I(S⇝∆) = 1 − MEV_{†∆}(S|∆,†∆) / MEV(S|∆,†∆), and 0 when the unrestricted loss is zero. The numerator is the maximum wealth loss an adversary can inflict on ∆ by calling only contracts in ∆; the denominator allows calls to any contract in the composition, including ∆'s dependencies in the context S. The ratio measures how much of ∆'s exposure is due to the context. The paper proves that I agrees with the existing MEV non-interference notion of [6] (I = 0 iff non-interferent), that it is monotone in the context (Theorem 1), independent of non-adversarial wallet balances (Theorem 2), and preserved under front-running when the target's dependencies are sender-agnostic and token-independent (Theorem 3). In the use cases, the measure quantifies oracle-manipulation and under-collateralized-loan attacks with explicit formulas, showing, for example, that a richer adversary sometimes needs the context less, while the interference can be near 1 when price manipulation is required.

Load-bearing premise

The model assumes contract call graphs are acyclic and states are well-formed, meaning a contract can only call contracts deployed before it; this rules out reentrancy and cyclic dependencies, and the compositionality proofs (especially Lemma A.3 and Theorem 3) rely on there being no internal calls crossing the boundary between the context and the target contracts.

Editorial extensions

If this is right

A composition with I(S⇝∆)=0 is economically non-interferent in the sense of [6], so the binary criterion becomes the zero case of a continuous scale.
Adding more contracts to the context can only increase or preserve the measured interference, never decrease it (Theorem 1).
Non-adversarial users' token balances do not affect the measured interference, so analyses can ignore all wallets except the adversary's (Theorem 2).
If the target's dependencies are sender-agnostic and token-independent from other contracts, front-running the target with extra contracts does not change its measured interference (Theorem 3).
For archetypal DeFi compositions, the measure yields closed-form expressions that quantify how AMM reserve sizes, collateralization thresholds, and adversary wealth affect the severity of oracle-manipulation and under-collateralized-loan attacks.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A natural next step is to make the mempool a parameter of the restricted MEV, which the authors flag as future work; doing so would make I depend on pending user transactions and could rank compositions by attackable surface in real time.
The same ratio could be adapted to other damage metrics beyond token wealth, such as loss of user funds or protocol insolvency, by replacing the wealth function in Equation (1).
Because I(S⇝∆)=1 whenever the target has no independent exposure, the measure deliberately saturates; comparing two different attacks by raw loss amounts would require pairing I with the unrestricted MEV, not replacing it.
Testable conjecture implied by the examples: for constant-product AMMs, I decreases as the adversary's capital grows in the Airdrop/Exchange case but increases in the AMM/Bet and AMM/Lending cases, suggesting the direction of the wealth effect depends on whether the context is a source of funding or of price manipulation.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Short version: the quantitative MEV interference definition is a real, useful extension of the qualitative non-interference notion from [6], and the main structural theorems are actually proved rather than hand-waved. It deserves a serious referee. But the showcase lending-pool example has a parameter bug that should be fixed before publication.

The new thing is Definition 1: I(S⇝∆) = 1 − MEV_†∆(S|∆,†∆)/MEV(S|∆,†∆), with the zero case handled. This gives a state-dependent, quantitative measure of how much the context amplifies losses to newly deployed contracts, and it collapses to the old binary non-interference notion exactly when I=0. Theorem 1 (monotonicity under adding contracts), Theorem 2 (irrelevance of non-adversary wallets), and Theorem 3 (preservation under front-running by sender-agnostic, token-independent contracts) are meaningful statements. The proofs in Appendix A are real proofs built on the local-MEV lemmas from [6]; the dependency is legitimate, not circular. The use cases illustrate the intended semantics, including the airdrop/fee example where I ≤ r/100, which is easy to read and correct.

The soft spots are in the examples, not in the core definition. Example 6 silently assumes Cmin < 1. For any standard lending protocol, Cmin > 1, and the displayed restricted MEV n(1/Cmin − 1) is negative. Since MEV is a maximum loss and the adversary can always choose to do nothing, the true value is 0 in that regime. The closed form for I then exceeds 1, contradicting Lemma 1(iii). The derivation would only be consistent for an already under-collateralized protocol, which is not the attack scenario the text describes. This needs a fix and an explicit parameter range. Example 5 has a smaller presentation issue: the main text states equalities, while Appendix B derives inequalities after flooring integer arithmetic; the formulas should be marked as bounds. Also, the partial-order/no-reentrancy assumption is load-bearing for Lemma A.3 and Theorem 3; the footnote dismissal of reentrancy as removable by programming patterns is not backed by a proof, and should be stated as a modeling restriction rather than a non-issue.

Who is this for: people doing static analysis or risk assessment of DeFi compositions. It is an incremental but solid contribution, not a paradigm shift. My recommendation: send it to peer review. The central definition and theorems deserve referee time; the example bugs are locatable and fixable. I would ask for a corrected Example 6, a bounds-clear Example 5, and a more honest statement about the call-graph restriction.

Referee Report

5 major / 4 minor

Summary. The paper introduces MEV interference, I(S⇝∆) = 1 − MEV_{†∆}(S|∆,†∆) / MEV(S|∆,†∆) (with value 0 when the denominator is 0), as a quantitative, state-dependent measure of how much an adversary can amplify the economic loss of a set of contracts ∆ by manipulating their context S. The paper proves fundamental properties: I is always between 0 and 1 (Lemma 1), it is monotone under widening the context (Theorem 1), it is independent of non-adversarial user wallets (Theorem 2), and it is preserved when the context is extended with sender-agnostic, token-independent contracts (Theorem 3). It then applies the notion to archetypal compositions: Airdrop/Exchange, FeeManager/Airdrop, AMM/Bet, and AMM/LendingPool, with the last intended to quantify under-collateralized loan attacks enabled by oracle manipulation.

Significance. If the formal results are correct, the paper offers a clean, parameter-free quantitative refinement of the qualitative MEV non-interference notion of [6], with plausible applications to DeFi risk assessment. The definition is transparent, state-dependent, and does not rely on fitted parameters or circular reasoning. The theorems are supported by proofs in Appendix A, although those proofs depend on the well-formedness assumption of Section 2. The significance of the applications is not yet established, because several of the worked examples contain arithmetic or modeling errors that change the claimed conclusions.

major comments (5)

[Section 4, Example 2 (Listing 1.2)] The restricted MEV in Example 2 is computed as the amount transferred to the adversary rather than the loss of ∆. In a withdrawal of x=n from AirdropFee, the contract transfers n−fee to the caller and fee to the FeeManager owner, so the wealth of ∆ decreases by n regardless of the fee. By Eq. (3), MEV_{†∆}(S|∆,†∆)=n, hence I(S⇝∆)=0, contradicting the displayed I≤r/100. This is a misapplication of Definition 1 in the paper's own illustrative example.
[Section 5, Example 4 (Airdrop/Exchange)] The MEV formulas count the gross ETH output of the swap instead of the net wealth loss of Exchange. When M swaps x:T and receives x·r:ETH, Exchange gains x:T and loses x·r:ETH, so by Eq. (1) its loss is x(r−1), not x·r. Draining the Airdrop gives an unrestricted loss bounded by min((n_M+n_A)(r−1), n_E), not min((n_M+n_A)r, n_E), so the displayed piecewise expression for I is incorrect.
[Section 5, Example 5 (AMM/Bet)] The restricted MEV displayed as an equality, (2br0/(rr1)−b−1) for r0/(rr1)≥1/2, conflicts with the stated exact real-arithmetic assumption in Section 5 and with Appendix B, which derives the expression as an inequality after applying flooring. Under exact arithmetic the term should be 2br0/(rr1)−b, and the subsequent I formula should be a genuine equality rather than the bound derived in the appendix. The main text must either consistently use exact arithmetic or explicitly present the formulas as upper bounds.
[Section 5, Example 6 (AMM/Lending Pool)] The restricted MEV n(1/Cmin−1) is negative whenever Cmin>1, contradicting the nonnegativity of MEV (Eq. (3), Lemma A.1(5)) and causing the displayed I to exceed 1 (e.g., Cmin=1.5, n=10, r=10), which contradicts Lemma 1(iii). For standard collateralization Cmin>1 the true restricted MEV is 0 because the adversary can simply abstain from borrowing, while the unrestricted attack can still be profitable. The formulas are valid only in the unstated regime Cmin<1, and in that regime the described borrowing is available even without oracle manipulation. Moreover, the derivation maximizes t(x), the borrowed amount, rather than the actual loss t(x)+x−n; the derivative of the loss contains an extra +1 term, so x=(4n−r)/5 does not maximize the loss. The example needs to be reworked with explicit parameter ranges and max(0,·) truncation.
[Section 2 / Appendix A (Lemma A.3, Theorem 3)] The well-formedness assumption that the call relation ≺ is a partial order and the resulting exclusion of reentrancy are load-bearing: Lemma A.3 and Theorem 3 rely on there being no internal calls across the Γ/Γbar boundary. The footnote claims that reentrancy can always be removed by programming patterns, but gives no proof or reference, and for arbitrary existing compositions this is not evident. The paper should either relax the assumption or state this restriction prominently as a limitation in Section 6.

minor comments (4)

[Section 4, after Lemma 1] The word 'minumum' should be 'minimum'.
[Section 5, Example 5] The closing sentence claims that the Bet/Exchange composition has zero MEV interference, but this is not derived anywhere in the example and needs a one-line justification or a reference.
[Appendix B, Example 6] In the second derivative computation, the term '-4(r+x^3)' appears to be a typo for '-4(r+x)^3'.
[Section 6] The phrase 'analysequalitative' should be 'analyse qualitative'.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Definition 1 is a new quantitative measure, and its consistency with the prior qualitative notion is a design property by construction, not a derived prediction; all theorems are proved from stated MEV axioms.

full rationale

The paper's central object, MEV interference I(S⇝∆), is defined directly in Definition 1 as 1 minus the ratio of restricted local MEV to unrestricted local MEV. The consistency claim that I=0 iff S and ∆ are non-interferent according to [6] is an immediate consequence of the definition, presented as a design property rather than as an independently derived result; this is not a circular derivation because no prediction is being extracted from an input that already contains it. The local MEV quantities and their basic properties (Lemma A.1, Lemma A.2) are imported from prior work [6] with stated assumptions; these are external supporting results that do not include the target ratio, so the self-citation is legitimate evidence rather than a load-bearing circular chain. Lemma 1 and Theorems 1-3 are proved from those lemmas and the definitions, with no fitted parameters, no data-fitting, and no reliance on a uniqueness theorem imported from the same authors. No ansatz is smuggled in via citation, and the quantitative measure is not a mere renaming of the earlier binary non-interference notion. The apparent arithmetic inconsistencies in Example 6 (e.g., negative restricted MEV for standard collateralization Cmin>1, and interference values exceeding 1 in contradiction of Lemma 1(iii)) are correctness concerns about the example computations, not circularity of the framework. Under the stated model assumptions, the derivation chain is self-contained, so the circularity score is 0.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The framework is built on standard MEV assumptions and imports local-MEV properties from prior work. It introduces no new entities. The main definitions are new but do not require hidden fitted parameters.

assumptions (6)

domain assumption The blockchain state is well-formed: contracts contain all their dependencies, and the call graph ⊑ is a partial order (no cycles).
Introduced in Section 2; used throughout proofs (e.g., Lemma A.3, Theorem 3) to rule out internal calls across contract boundaries and reentrancy.
domain assumption The adversary fully controls transaction selection and ordering (standard MEV adversary).
Section 3 threat model, following [3].
domain assumption Contracts cannot mint or burn tokens, and can only transfer tokens to user accounts.
Section 2; guarantees finite wealth and monotonic properties of MEV.
domain assumption Prices of native crypto-assets are constant.
Section 6 limitation; relied on in the wealth definition Eq (1) and use-case computations.
domain assumption Properties of local MEV as stated in Lemma A.1 of this paper (imported from [6]).
Used without proof in proofs of Lemmas 1-2 and Theorem 1; they come from Bartoletti et al. [6].
standard math All token amounts are finite and transitions are deterministic.
Section 2; ensures the maxima in Eqs (2)-(3) exist.

how reviews work

0 comments

Cite this review

Pith. "Pith review of A quantitative notion of economic security for smart contract compositions." pith.science (2026). https://pith.science/paper/IUDZLN5U

@misc{pith2026250519006,
  author       = {Pith},
  title        = {Pith review of: A quantitative notion of economic security for smart contract compositions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IUDZLN5U}},
  note         = {Machine review of arXiv:2505.19006}
}

read the original abstract

Decentralized applications are often composed of multiple interconnected smart contracts. This is especially evident in DeFi, where protocols are heavily intertwined and rely on a variety of basic building blocks such as tokens, decentralized exchanges and lending protocols. A crucial security challenge in this setting arises when adversaries target individual components to cause systemic economic losses. Existing security notions focus on determining the existence of these attacks, but fail to quantify the effect of manipulating individual components on the overall economic security of the system. In this paper, we introduce a quantitative security notion that measures how an attack on a single component can amplify economic losses of the overall system. We study the fundamental properties of this notion and apply it to assess the security of key compositions. In particular, we analyse under-collateralized loan attacks in systems made of lending protocols and decentralized exchanges.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

27 extracted references · 13 canonical work pages

[6]

In: Financial Cryptography and Data Security (FC 2024)

Bartoletti, M., Marchesin, R., Zunino, R.: DeFi composability as MEV non- interference. In: Financial Cryptography and Data Security (FC 2024). LNCS, vol. 14745. Springer (2025),https://doi.org/10.1007/978-3-031-78679-2_20

work page doi:10.1007/978-3-031-78679-2_20 2025
[1]

In: ACM Asia Conference on Computer and Communications Security (ASIA CCS)

Arora, S., Li, Y., Feng, Y., Xu, J.: SecPLF: Secure protocols for loanable funds against oracle manipulation attacks. In: ACM Asia Conference on Computer and Communications Security (ASIA CCS). ACM (2024).https://doi.org/10.1145/ 3634737.3637681

arXiv 2024
[2]

In: ACM SIG- PLAN Symposium on Principles of Programming Languages (POPL)

Assaf, M., Naumann, D.A., Signoles, J., Totel, E., Tronel, F.: Hypercollecting se- mantics and its application to static analysis of information flow. In: ACM SIG- PLAN Symposium on Principles of Programming Languages (POPL). pp. 874–887. ACM (2017).https://doi.org/10.1145/3009837.3009889

arXiv 2017
[3]

In: IEEE Symposium on Security and Privacy

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

arXiv 2023
[4]

In: ACM SIGSAC Conference on Computer and Communications Security (CCS)

Babel, K., Javaheripi, M., Ji, Y., Kelkar, M., Koushanfar, F., Juels, A.: Lanturn: Measuring economic security of smart contracts through adaptive learning. In: ACM SIGSAC Conference on Computer and Communications Security (CCS). pp. 1212–1226. ACM (2023).https://doi.org/10.1145/3576915.3623204

arXiv 2023
[5]

In: Workshop on Trusted Smart Contracts

Bartoletti, M., Chiang, J.H., Lluch-Lafuente, A.: SoK: Lending Pools in Decentral- ized Finance. In: Workshop on Trusted Smart Contracts. LNCS, vol. 12676, pp. 553–578. Springer (2021).https://doi.org/10.1007/978-3-662-63958-0_40

doi:10.1007/978-3-662-63958-0_40 2021
[7]

In: Financial Cryptogra- phy and Data Security

Bartoletti, M., Zunino, R.: A theoretical basis for MEV. In: Financial Cryptogra- phy and Data Security. LNCS, Springer (2025), to appear

work page 2025
[8]

In: ACM SIGSAC Conference on Computer and Communications Se- curity (CCS)

Chen, T., Zhang, Y., Li, Z., Luo, X., Wang, T., Cao, R., Xiao, X., Zhang, X.: To- kenscope: Automatically detecting inconsistent behaviors of cryptocurrency tokens in Ethereum. In: ACM SIGSAC Conference on Computer and Communications Se- curity (CCS). pp. 1503–1520. ACM (2019).https://doi.org/10.1145/3319535. 3345664

doi:10.1145/3319535 2019

Show all 27 references

[9]

Clark, D., Hunt, S., Malacaria, P.: A static analysis for quantifying information flow in a simple imperative language. J. Comput. Secur.15(3), 321–371 (2007). https://doi.org/10.3233/JCS-2007-15302

2007 doi
[10]

In: IEEE Symp

Daian, P., Goldfeder, S., Kell, T., Li, Y., Zhao, X., Bentov, I., Breidenbach, L., Juels, A.: Flash boys 2.0: Frontrunning in decentralized exchanges, miner ex- tractable value, and consensus instability. In: IEEE Symp. on Security and Privacy. pp. 910–927. IEEE (2020).https:/...

2020
[11]

In: IEEE Sym- posium on Security and Privacy

Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Sym- posium on Security and Privacy. pp. 11–20. IEEE Computer Society (1982). https://doi.org/10.1109/SP.1982.10014

1982
[12]

In: Crypto Valley Conference on Blockchain Technology (CVCBT)

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

2020
[13]

In: ACM Conference on Advances in Financial Technologies (AFT)

Gudgeon, L., Werner, S., Perez, D., Knottenbelt, W.J.: DeFi protocols for loan- able funds: Interest rates, liquidity and market efficiency. In: ACM Conference on Advances in Financial Technologies (AFT). pp. 92–112 (2020).https://doi.org/ 10.1145/3419614.3423254

2020
[14]

CEUR Workshop Proceedings, vol

Guesmi, S., Piazza, C., Rossi, S.: Noninterference analysis for smart contracts: Would you bet on it? In: Distributed Ledger Technology Workshop (DLT). CEUR Workshop Proceedings, vol. 3791. CEUR-WS.org (2024) 16

2024
[15]

In: Financial Cryptography and Data Security Workshops

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

2022 doi
[16]

ACM Trans

Kitzler, S., Victor, F., Saggese, P., Haslhofer, B.: Disentangling Decentralized Fi- nance (DeFi) compositions. ACM Trans. Web17(2), 10:1–10:26 (2023).https: //doi.org/10.1145/3532857

2023 doi
[17]

Theoretical Computer Science538, 124–139 (2014).https://doi.org/https:// doi.org/10.1016/j.tcs.2014.04.022

Klebanov, V.: Precise quantitative information flow analysis - a symbolic approach. Theoretical Computer Science538, 124–139 (2014).https://doi.org/https:// doi.org/10.1016/j.tcs.2014.04.022

2014 doi
[18]

In: ACM SIGSOFT International Symposium on Software Testing and Analysis

Kong, Q., Chen, J., Wang, Y., Jiang, Z., Zheng, Z.: DeFiTainter: Detecting price manipulation vulnerabilities in DeFi protocols. In: ACM SIGSOFT International Symposium on Software Testing and Analysis. p. 1144–1156 (2023).https://doi. org/10.1145/3597926.3598124

2023
[19]

In: International School on Formal Methods for the Design of Computer, Com- munication, and Software Systems (SFM)

K¨ opf, B., Rybalchenko, A.: Automation of quantitative information-flow analysis. In: International School on Formal Methods for the Design of Computer, Com- munication, and Software Systems (SFM). LNCS, vol. 7938, pp. 1–28. Springer (2013).https://doi.org/10.1007/978-3-642-38874-3_1

2013 doi
[20]

Mackinga, T., Nadahalli, T., Wattenhofer, R.: TW AP oracle attacks: Easier done than said? In: IEEE International Conference on Blockchain and Cryp- tocurrency (ICBC). pp. 1–8. IEEE (2022).https://doi.org/10.1109/ICBC54727. 2022.9805499

2022
[21]

In: Financial Cryptography

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

2021 doi
[22]

CoRRabs/2411.01230(2025).https://doi.org/10.48550/ arXiv.2411.01230

Wu, K.W.: Strengthening DeFi security: A static analysis approach to Flash Loan vulnerabilities. CoRRabs/2411.01230(2025).https://doi.org/10.48550/ arXiv.2411.01230

2025 doi arXiv
[23]

CoRRabs/2104.15068 (2021),https://arxiv.org/abs/2104.15068

Wu, S., Wang, D., He, J., Zhou, Y., Wu, L., Yuan, X., He, Q., Ren, K.: DeFiRanger: Detecting price manipulation attacks on defi applications. CoRRabs/2104.15068 (2021),https://arxiv.org/abs/2104.15068

2021 arXiv
[24]

CoRRabs/2407.01204(2024),https://arxiv.org/ abs/2407.01204 17 A Proofs: properties of MEV interference We start by recalling from [6] a few useful properties of local MEV

Yao, S., Ni, H., Myers, A.C., Cecchetti, E.: SCIF: A language for compositional smart contract security. CoRRabs/2407.01204(2024),https://arxiv.org/ abs/2407.01204 17 A Proofs: properties of MEV interference We start by recalling from [6] a few useful properties of local MEV. ...

2024 arXiv
[25]

This is becauseMhas no way to force other users to spend their tokens in the attack sequence

ifD⊆D ′, thenMEV D (S ,C)≤MEV D′(S ,C) 3.MEV D (W|Γ ,C)≤MEV D (W|∆,C)ifΓ⪯∆ 4.MEV D (W|Γ ,C) = MEV D (W|Γ ,C∩ †Γ) = MEVD∩†Γ (W|Γ ,C) 5.0≤MEV D (S ,C)≤$ C (S) Lemma A.2 states that the only user wallets that need to be taken into account to estimate the MEV are those of the adve...
[26]

the contracts inC ′ are sender-agnostic; 2.C ′ ⊆D
[27]

deps(D)∩deps(C)and deps(D)\deps(C)are token independent inS. Proof.First, note that the inequality MEV D∩deps(C) (S ,C)≤MEV D (S ,C) fol- lows from Item 2 of Lemma A.1, so we just need to show that: MEVD (S ,C)≤MEV D∩deps(C) (S ,C) To do so, let ⃗X∈κ D (M)∗ be a sequence of tr...

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.

[1] [6]

In: Financial Cryptography and Data Security (FC 2024)

Bartoletti, M., Marchesin, R., Zunino, R.: DeFi composability as MEV non- interference. In: Financial Cryptography and Data Security (FC 2024). LNCS, vol. 14745. Springer (2025),https://doi.org/10.1007/978-3-031-78679-2_20

work page doi:10.1007/978-3-031-78679-2_20 2025

[2] [1]

In: ACM Asia Conference on Computer and Communications Security (ASIA CCS)

Arora, S., Li, Y., Feng, Y., Xu, J.: SecPLF: Secure protocols for loanable funds against oracle manipulation attacks. In: ACM Asia Conference on Computer and Communications Security (ASIA CCS). ACM (2024).https://doi.org/10.1145/ 3634737.3637681

arXiv 2024

[3] [2]

In: ACM SIG- PLAN Symposium on Principles of Programming Languages (POPL)

Assaf, M., Naumann, D.A., Signoles, J., Totel, E., Tronel, F.: Hypercollecting se- mantics and its application to static analysis of information flow. In: ACM SIG- PLAN Symposium on Principles of Programming Languages (POPL). pp. 874–887. ACM (2017).https://doi.org/10.1145/3009837.3009889

arXiv 2017

[4] [3]

In: IEEE Symposium on Security and Privacy

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

arXiv 2023

[5] [4]

In: ACM SIGSAC Conference on Computer and Communications Security (CCS)

Babel, K., Javaheripi, M., Ji, Y., Kelkar, M., Koushanfar, F., Juels, A.: Lanturn: Measuring economic security of smart contracts through adaptive learning. In: ACM SIGSAC Conference on Computer and Communications Security (CCS). pp. 1212–1226. ACM (2023).https://doi.org/10.1145/3576915.3623204

arXiv 2023

[6] [5]

In: Workshop on Trusted Smart Contracts

Bartoletti, M., Chiang, J.H., Lluch-Lafuente, A.: SoK: Lending Pools in Decentral- ized Finance. In: Workshop on Trusted Smart Contracts. LNCS, vol. 12676, pp. 553–578. Springer (2021).https://doi.org/10.1007/978-3-662-63958-0_40

doi:10.1007/978-3-662-63958-0_40 2021

[7] [7]

In: Financial Cryptogra- phy and Data Security

Bartoletti, M., Zunino, R.: A theoretical basis for MEV. In: Financial Cryptogra- phy and Data Security. LNCS, Springer (2025), to appear

work page 2025

[8] [8]

In: ACM SIGSAC Conference on Computer and Communications Se- curity (CCS)

Chen, T., Zhang, Y., Li, Z., Luo, X., Wang, T., Cao, R., Xiao, X., Zhang, X.: To- kenscope: Automatically detecting inconsistent behaviors of cryptocurrency tokens in Ethereum. In: ACM SIGSAC Conference on Computer and Communications Se- curity (CCS). pp. 1503–1520. ACM (2019).https://doi.org/10.1145/3319535. 3345664

doi:10.1145/3319535 2019