原文來自Trail of Bits：
12月3日，知名DeFi借貸協議Aave部署了V2版本，儘管我們並沒有被雇傭來查看其代碼，但在次日，我們還是對其進行了簡單審查。很快，我們就發現了一個影響Aave V1和V2版本合約的漏洞，並報告了該問題。在將我們的分析發送給Aave的一小時內，他們的團隊修復了該漏洞，以減輕潛在影響。如果該漏洞被利用，這一問題將破壞Aave，並影響外部DeFi合約中的資金。
據悉，有5家不同的安全公司審查了Aave代碼庫，其中有一些使用了形式化驗證。然而，這個漏洞並沒有被這些公司注意到。這篇文章描述了這一問題，以及“該漏洞是如何逃過檢測”等其它的一些經驗教訓。此外，我們也在開發一種新的Slither檢測器，它可以識別這一漏洞，從而為以太坊社區提高安全性。
漏洞
Aave使用了delegatecall代理模式，這一點我們在過去的文章中已經詳細討論過了。簡單來看，每個組件被分成了兩個合約：（1）包含實現的邏輯合約，（2）包含數據並使用delegatecall與邏輯合約進行交互的代理。在邏輯合約上執行代碼時，用戶與代理合約進行交互。這是delegatecall代理模式的簡化表示：
在Aave中，LendingPool（LendingPool.sol）是使用delegatecall代理的可升級組件。
而我們發現的漏洞依賴於這些合約中的兩個功能：
可以直接調用邏輯合約的函數，包括初始化函數；借貸池具有其自己的delegatecall功能；
1
初始化可升級合約
這種可升級模式的一個限制是，代理不能依賴邏輯合約的構造函數（Constructor）進行初始化。因此，狀態變量和初始設置必須在公共初始化函數中執行。
在LendingPool中，初始化函數設置提供者地址（_addressesProvider）：
initializer調節器防止多次調用initialize，它要求滿足以下條件為true：
以下：
初始化允許在相同交易中多次調用調節器（因此有多個initialize函數）；isConstructor（）是代理執行代碼所需的；revision > lastInitializedRevision 允許在合約升級時再次調用初始化函數；
雖然它通過代理，預期可正常工作，但是（3）也允許任何人直接在邏輯合約上調用initialize函數。一旦邏輯合約被部署：
revision將為0x2(LendingPool.sol#L56)；lastInitializedRevision將為0x0；
而漏洞是：任何人都可以在LendingPool邏輯合約中設置_addressesProvider。
2
任意delegatecall
LendingPool.liquidationCall直接委託調用（delegatecall）由_addressProvider返回的地址：
這允許任何人啟動LendingPool邏輯合約，設置受控地址提供者，並執行任意代碼，包括selfdestruct。
利用漏洞的場景：任何人都可以破壞借貸池邏輯合約。下面是一個簡化的視覺表示：
3
缺乏存在檢查
就問題本身而言，已經是很嚴重了，因為任何人都可以破壞邏輯合約，並阻止代理執行借貸池代碼。
然而，在代理合約中使用OpenZeppelin會加劇這一問題的嚴重性。
我們在2018年撰寫的一篇博客文章中強調，沒有代碼的合約委託調用（delegatecall）能在不執行任何代碼的情況下返回成功。儘管我們最初發出警告，但OpenZeppelin並未在其代理合約中修復回退函數：
如果代理委託調用（delegatecall）了一個已破壞的借貸池邏輯合約，則代理將返回成功，而不會執行任何代碼。
由於Aave可以更新代理以指向另一個邏輯合約，因此這種漏洞利用不會持久。但在可利用此漏洞的時間範圍內，任何調用該借貸池的第三方合約，都將表現為某些代碼已被執行，但實際卻並未執行。這將打破很多外部合約的基本邏輯。
4
受影響的合約
所有AToken（Aave代幣）：AToken.redeem調用pool.redeemUnderlying（AToken.sol#L255-L260)。由於調用什麼也不做，用戶將燒掉他們的AToken，而不會收到他們的底層資產；WETHGateway(WETHGateway.sol#L103-L111):存款會存儲在網關中，然後任何人都可以竊取存款資產；任何基於Aave信用委託v2（MyV2）的代碼庫(MyV2CreditDelegation.sol)；
如果我們發現的問題被利用，則Aave之外的很多合約都會受到各種方式的影響。確定一份完整的名單是困難的，我們沒有試圖這樣做。這一事件凸顯了DeFi可組合性的潛在風險，以下是我們找到的一些受影響的合約：
DefiSaver v1 (AaveSaverProxy.sol)DefiSaver v2 (AaveSaverProxyV2.sol)PieDao – pie oven (InterestingRecipe.sol#L66)
5
修復及建議
幸運的是，在我們報告這個漏洞之前，還沒有人利用它。 Aave對其兩個版本的借貸池調用了initialize函數，從而保證了合約的安全：
LendingPool V1: 0x017788dded30fdd859d295b90d4e41a19393f423 修復時間: 2020年12月4日07:34:26 PM +UTCLendingPool V2: 0x987115c38fd9fd2aa2c6f1718451d167c13a3186 修復時間: 2020年12月4日07:53:00 PM +UTC
長期而言，合約部署者應：
在所有邏輯合約中添加一個構造函數（constructor ）以使initialize函數無效；檢查delegatecall代理fallback函數中是否存在合約；仔細檢查delegatecall陷阱，並使用slither-check-upgradeability；
6
形式化驗證合約並不是防彈的
Aave的代碼庫經過了形式化驗證，區塊鏈領域的一個趨勢是，人們會認為安全特性是聖杯。用戶可能會嘗試根據這些特性的存在與否，對各種合約的安全性進行排序。我們認為這是危險的，它會導致錯誤的安全感。
Aave形式化驗證報告列出了LendingPool 視圖函數（例如，它們沒有副作用）以及池操作（例如，操作成功後返回true且不還原）的屬性。例如，已驗證的屬性之一是：
然而，如果邏輯合約遭到破壞，則該屬性可能會被破壞。那如何才能對此進行驗證？雖然我們無法訪問定理證明或所使用的設置，但很可能證明proof沒有考慮可升級性，或者prover不支持複雜的合約交互。
這在代碼驗證中是很常見的。你可以通過對整體行為的假設來證明目標組件中的行為，但是在多合約設置中證明屬性是具有挑戰性和耗時的，因此必須進行權衡。
形式化驗證技術很棒，但是用戶必須意識到它們覆蓋範圍很小，並且可能會錯過攻擊媒介。另一方面，自動化工具和人工審查可幫助開發人員以較少的資源來提升代碼庫的安全性。了解每種解決方案的優點和局限性，對開發人員和用戶而言都至關重要。當前的問題就是一個很好的例子，Slither可以在幾秒鐘內發現這個問題，受過訓練的專家可能會很快指出它，而要用安全特性來檢測，則需要付出很大的精力。
總結
Aave做出了積極反應，並在發現問題後迅速修復了該漏洞。危機避免了，但最近遭受黑客攻擊的其他受害者卻沒有那麼幸運。在部署代碼並將其暴露於對抗性環境之前，我們建議開發者：
查看這裡的檢查表和訓練；將Slither添加到你的持續集成管道中並調查其所有報告；給安全公司適當的時間來審查你的系統；請注意可升級性，至少請審查合約升級反模式，合約遷移的工作方式，以及使用OpenZeppelin的可升級性；
我們希望通過分享此信息以及與此問題相關的Slither檢測器來防止類似的錯誤。
