Quantifying secure composability of smart contracts

Abstract

Since its inception in 2008, distributed ledger technology (DLT), has enabled a suite of financial services to be offered without relying on trusted intermediaries. In contrast to traditional finance, decentralized finance (DeFi) built upon DLT empowers users to execute peer-to-peer electronic transactions in a trustless enivironment. Account-based blockchain models, such as Ethereum, implement DeFi using smart contracts—self-executing digital agreements—programmed to encode and execute in-tended financial mechanisms. These smart contracts function as “bricks of lego”,enabling developers to construct complex DeFi services by composing individual components. These compositions introduce new, complex inter-dependencies andvulnerabilities which, owing to the transparent and public nature of the ledger, makes them susceptible to exploitation by malicious participants. The subject of economic exploitation is a recurring issue and has been studied in the literature as Maximal Extractable Value (MEV). Surprisingly enough, existing studies on compositionality are few. The notion of secure composability in the "Clockwork Finance" paper by Babel et al. suffers from usability and algorithmic issues, while failing to specify the contracts from which MEV is extracted and incorrectly classifying as not composable contracts that have intended MEV. While the notion of “MEV non-interference” introduced in the "DeFi composability" paper by Bartoletti et al. addresses these drawbacks and checks whether the contracts that will be deployed suffer a loss when adversaries manipulate their dependencies, it is limited. Since the notion is qualitative, it does not provide information about the degree of interference caused and possible upper bounds to the loss suffered by a compound contract. This thesis performs an exploratory study of quantitative notions for secure composability of smart contracts, eventually arriving at MEV interference. Our "MEV interference" captures various security properties one would deem desirable. We study the theoretical properties of this notion and apply it to study paradigmatic contract compositions of Lending Pools, Automated Market Makers, and Betting contracts.