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.

翻译：我们提出钟表金融框架（CFF），这是一个通用形式化验证框架，用于对组合式去中心化金融（DeFi）智能合约的经济安全属性进行机械化推理。CFF具备三个关键特性：一是合约完备性，即能建模任何智能合约平台及其所有合约（无论是否图灵完备），且模型开销渐近恒定；二是构造性攻击穷举，即能自动机械化提取所有针对用户加密货币的、跨建模合约的经济攻击。凭借这些特性，CFF可支持多重目标：开发者对合约的经济安全分析、用户对DeFi交易风险的分析、费用用户体验优化，以及机器或矿工对套利机会的优化。由于CFF具备组合性，它可通过对任意期望的潜在交互智能合约模型集进行推理来支持这些目标。我们将CFF实例化为以太坊合约的可执行模型，该模型整合了最先进的演绎验证器。在前期工作基础上，我们引入可提取价值（EV）这一新型形式化经济安全概念，它既是CFF的基础，也具有普适意义。我们为以太坊中四种主流已部署的DeFi协议（Uniswap、Uniswap V2、Sushiswap和MakerDAO，截至2022年3月总锁仓价值达240亿美元）构建了模块化、可读性强且可组合的CFF模型。结合闪电贷、空投和投票等其他常见模型，实验表明CFF具有实用性，能从真实交易活动中驱动基于数据的、有意义的EV洞察。在未显式编程攻击策略的情况下，CFF近期平均每月可发现预期达5600万美元的可提取价值。