Clockwork Finance：智能合约中经济安全性的自动化分析

我们引入了 Clockwork Finance Framework (CFF)，这是一个通用形式化验证框架，用于对组合的去中心化金融智能合约的经济安全属性进行机械化推理。CFF 具有三个关键属性。它是合约完备的，意味着它可以对任何智能合约平台及其所有合约进行建模——无论是图灵完备的还是其他的。它以渐近常数模型开销实现这一点。它在构造上也是攻击穷尽的，意味着它可以自动且机械地提取跨建模合约对用户加密货币的所有可能经济攻击。得益于这些属性，CFF 可以支持多个目标：开发者对合约的经济安全分析、用户对 DeFi 交易风险的分析、费用用户体验以及机器人或矿工对套利机会的优化。因为 CFF 提供可组合性，它可以通过对任何所需的可能交互的智能合约模型集进行推理来支持这些目标。我们将 CFF 实例化为以太坊合约的可执行模型，该模型结合了最先进的演绎验证器。基于先前的工作，我们引入了可提取价值，这是组合 DeFi 合约中经济安全性的一个新形式化概念，它既是 CFF 的基础，也具有普遍意义。我们构建了以太坊中四个流行的已部署 DeFi 协议的模块化、人类可读、可组合的 CFF 模型：Uniswap、Uniswap V2、Sushiswap 和 MakerDAO，截至2022年3月，它们代表了总计240亿美元的价值。我们使用这些模型以及其他一些常见模型（如闪电贷、空投和投票）进行实验，证明 CFF 是实用的，并且可以从真实世界的交易活动中驱动有用的、基于数据的 EV 洞察。在没有任何显式编程的攻击策略的情况下，CFF 在近期平均每月发现预期5600万美元的 EV。