Flashbots 核心贡献者等人发表新论文，研究 DeFi 智能合约经济安全的形式化验证框架 CFF

链闻消息，Flashbots 核心贡献者 Philip Daian、康奈尔大学计算机安全博士生 Kushal Babel 和 Mahimna Kelkar 以及康奈尔理工学院教授 Ari Juels 共同发布关于 Clockwork Finance Framework （CFF）的新论文，这是一种 DeFi 智能合约经济安全的形式化验证框架。论文中表示，CFF 具有三个关键特性，合约完备、以渐近最优的模型大小实现、在构造上穷举攻击。CFF 可以支持多个目标，开发者对合约的经济安全性分析、用户对 DeFi 交易风险的分析、机器人或矿工对套利机会的优化。

此外，CFF 框架引入了一个新的 DeFi 合约经济安全概念，可提取价值 （EV）。团队成员通过对 Uniswap、Uniswap V2、SushiSwap 和 MakerDAO 构建了模块化的、可读的、可组合的 CFF 模型，验证了在没有明确编程攻击策略的情况下，CFF 平均每月发现 5600 万美元的 EV。