Paper 2021/1147

Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts

Kushal Babel, Cornell Tech
Philip Daian, Cornell Tech
Mahimna Kelkar, Cornell Tech
Ari Juels, Cornell Tech
Abstract

We introduce the Clockwork Finance Framework (CFF), a general purpose, formal verification framework for mechanized reasoning about the economic security properties of composed decentralized-finance (DeFi) smart contracts. CFF features three key properties. It is contract complete, meaning that it can model any smart contract platform and all its contracts—Turing complete or otherwise. It does so with asymptotically constant model overhead. It is also attack-exhaustive by construction, meaning that it can automatically and mechanically extract all possible economic attacks on users’ cryptocurrency across modeled contracts. Thanks to these properties, CFF can support multiple goals: economic security analysis of contracts by developers, analysis of DeFi trading risks by users, fees UX, and optimization of arbitrage opportunities by bots or miners. Because CFF offers composability, it can support these goals with reasoning over any desired set of potentially interacting smart contract models. We instantiate CFF as an executable model for Ethereum contracts that incorporates a state-of-the-art deductive verifier. Building on previous work, we introduce extractable value (EV), a new formal notion of economic security in composed DeFi contracts that is both a basis for CFF and of general interest. We construct modular, human-readable, composable CFF models of four popular, deployed DeFi protocols in Ethereum: Uniswap, Uniswap V2, Sushiswap, and MakerDAO, representing a combined 24 billion USD in value as of March 2022. We use these models along with some other common models such as flash loans, airdrops and voting to show experimentally that CFF is practical and can drive useful, data-based EV-based insights from real world transaction activity. Without any explicitly programmed attack strategies, CFF uncovers on average an expected $56 million of EV per month in the recent past.

Metadata
Available format(s)
PDF
Category
Applications
Publication info
Published elsewhere. 44th IEEE Symposium on Security and Privacy 2023
DOI
10.1109/SP46215.2023.00036
Keywords
DeFi securitysmart contractscomposability
Contact author(s)
babel @ cs cornell edu
phil @ cs cornell edu
mahimna @ cs cornell edu
History
2023-05-18: last of 2 revisions
2021-09-10: received
See all versions
Short URL
https://ia.cr/2021/1147
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2021/1147,
      author = {Kushal Babel and Philip Daian and Mahimna Kelkar and Ari Juels},
      title = {Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts},
      howpublished = {Cryptology ePrint Archive, Paper 2021/1147},
      year = {2021},
      doi = {10.1109/SP46215.2023.00036},
      note = {\url{https://eprint.iacr.org/2021/1147}},
      url = {https://eprint.iacr.org/2021/1147}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.