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。



coinpionex