注：今日，DeFi安全审计公司Trail of Bits披露了Aave假贷协议此前存在的一个严重缝隙，在发现到该问题后，Aave迅速修正了该缝隙，然后避免了一场危机。
原文来自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功能；
初始化可晋级合约
这种可晋级形式的一个约束是，署理不能依赖逻辑合约的结构函数（Constructor）进行初始化。因此，状态变量和初始设置有必要在公共初始化函数中履行。
在LendingPool中，初始化函数设置提供者地址（_addressesProvider）：
initializer调节器防止屡次调用initialize，它要求满足以下条件为true：
以下：
-
初始化答应在相同买卖中屡次调用调节器（因此有多个initialize函数）；
-
isConstructor（）是署理履行代码所需的；
-
revision > lastInitializedRevision 答应在合约晋级时再次调用初始化函数；
尽管它经过署理，预期可正常工作，可是（3）也答应任何人直接在逻辑合约上调用initialize函数。一旦逻辑合约被布置：
-
revision将为0x2(LendingPool.sol#L56)；
-
lastInitializedRevision将为0x0；
而缝隙是：任何人都能够在LendingPool逻辑合约中设置_addressesProvider。
恣意delegatecall
LendingPool.liquidationCall直接托付调用（delegatecall）由_addressProvider回来的地址：
这答应任何人发动LendingPool逻辑合约，设置受控地址提供者，并履行恣意代码，包含selfdestruct。
运用缝隙的场景：任何人都能够损坏假贷池逻辑合约。下面是一个简化的视觉表明：
缺乏存在检查
就问题自身而言，已经是很严重了，因为任何人都能够损坏逻辑合约，并阻挠署理履行假贷池代码。
然而，在署理合约中运用OpenZeppelin会加重这一问题的严重性。咱们在2018年撰写的一篇博客文章中着重，没有代码的合约托付调用（delegatecall）能在不履行任何代码的情况下回来成功。尽管咱们开始宣布正告，但OpenZeppelin并未在其署理合约中修正回退函数：
假如署理托付调用（delegatecall）了一个已损坏的假贷池逻辑合约，则署理将回来成功，而不会履行任何代码。
由于Aave能够更新署理以指向另一个逻辑合约，因此这种缝隙运用不会耐久。但在可运用此缝隙的时刻范围内，任何调用该假贷池的第三方合约，都将表现为某些代码已被履行，但实践却并未履行。这将打破很多外部合约的基本逻辑。
受影响的合约
-
一切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)
修正及主张
走运的是，在咱们陈述这个缝隙之前，还没有人运用它。Aave对其两个版别的假贷池调用了initialize函数，然后确保了合约的安全：
-
LendingPool V1: 0x017788dded30fdd859d295b90d4e41a19393f423 修正时刻: 2020年12月4日 07:34:26 PM +UTC
-
LendingPool V2: 0x987115c38fd9fd2aa2c6f1718451d167c13a3186 修正时刻: 2020年12月4日 07:53:00 PM +UTC
长期而言，合约布置者应：
-
在一切逻辑合约中添加一个结构函数（constructor ）以使initialize函数无效；
-
检查delegatecall署理fallback函数中是否存在合约；
-
仔细检查delegatecall陷阱，并运用slither-check-upgradeability；
形式化验证合约并不是防弹的
Aave的代码库经过了形式化验证，区块链领域的一个趋势是，人们会以为安全特性是圣杯。用户可能会尝试根据这些特性的存在与否，对各种合约的安全性进行排序。咱们以为这是危险的，它会导致过错的安全感。
Aave形式化验证陈述列出了 LendingPool 视图函数（例如，它们没有副作用）以及池操作（例如，操作成功后回来true且不复原）的特点。例如，已验证的特点之一是：
然而，假如逻辑合约遭到损坏，则该特点可能会被损坏。那怎么才干对此进行验证？尽管咱们无法访问定理证明或所运用的设置，但很可能证明proof没有考虑可晋级性，或许prover不支持杂乱的合约交互。
这在代码验证中是很常见的。你能够经过对整体行为的假设来证明目标组件中的行为，可是在多合约设置中证明特点是具有挑战性和耗时的，因此有必要进行权衡。
形式化验证技术很棒，可是用户有必要意识到它们掩盖范围很小，并且可能会错失进犯前言。另一方面，自动化工具和人工检查可协助开发人员以较少的资源来提升代码库的安全性。了解每种解决方案的长处和局限性，对开发人员和用户而言都至关重要。当时的问题就是一个很好的比如，Slither能够在几秒钟内发现这个问题，受过练习的专家可能会很快指出它，而要用安全特性来检测，则需要付出很大的精力。
总结
Aave做出了积极反应，并在发现问题后迅速修正了该缝隙。危机避免了，但最近遭受黑客进犯的其他受害者却没有那么走运。在布置代码并将其暴露于对抗性环境之前，咱们主张开发者：
-
检查这儿的检查表和练习；
-
将Slither添加到你的持续集成管道中并查询其一切陈述；
-
给安全公司适当的时刻来检查你的系统；
-
请注意可晋级性，至少请检查合约晋级反形式，合约搬迁的工作方式，以及运用OpenZeppelin的可晋级性；
咱们希望经过共享此信息以及与此问题相关的Slither检测器来防止相似的过错。
视野开拓
在 20 世纪 80 年代早期农业改革期间 ，地方领导人对民间自发的农业生产“单干“和“包产到户＂的立场和态度，往往是决定此类经济活动是否能顺利存在的重要原因之一。时任安徽省委书记的万里和当时四川省委的负责人就是对此类经济活动表示支持的地方领导人的代表人物。当时民间有谚云：“ 要吃米 ，找万里 ……＂。-《权力结构、政治激励和经济增长》
