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.

翻译：去中心化金融（DeFi）服务通常通过组合多种智能合约构建而成。虽然可组合性是DeFi成功的关键驱动因素，但它也带来了安全风险：攻击者可能利用新部署合约与现有合约之间的交互造成经济损失。我们提出MEV非干扰性——一种针对DeFi可组合性的形式化安全概念，要求新部署合约集合的最大可提取价值不会因与现有区块链状态交互而增加。为支撑该概念，我们定义了局部MEV，这是一种聚焦于特定受害合约集合损失的新型经济攻击衡量指标。我们研究了有界财富与无界财富两种对抗模型，并建立了充分条件与局部性原理，从而实现对安全可组合性的模块化推理。我们将该框架应用于代表性DeFi组合体（包括交易所、AMM、期权、借贷池、路由器和套利合约），展示了它如何区分安全组合与脆弱组合。我们的研究结果为推理DeFi组合的经济安全性提供了形式化基础。