Aave is a leading DeFi lending protocol that has evolved from a P2P lending model to a liquidity pool-based system。
AAVE 于 2017 年启动，在 DeFi 的世界中，自 2017 年以来人气一直很高的这个领域被视为 OG。Aave，或者说它的前身 ETHLend，最初是一个 P2P 贷款协议，但在 2020 年初转变为基于流动性池的协议。那时，Certora 是一家拥有主要人才和先进但尚不成熟技术的小公司，渴望提升以保护防止漏洞为重心的创新协议的安全性。
Aave V1：旅程的开始
在 2020 年 1 月，我们开始审查已经上线的 V1 协议。审查首先通过对合同进行特征描述并制定组件及其交互的规范来进行。这次接触让 Aave 团队首次了解了形式验证及其防止可能对用户体验产生重大影响的错误的能力。这标志着两个公司之间一段漫长而牢固的合作关系的开始，这一关系一方面加强了 Aave 的安全性，另一方面提升了 Certora Prover 的能力。
早期阶段：保护 Aave V2
八个月过去后，Aave 开始计划发布他们新的改进版本的成功协议。在最终开发阶段，Aave 联系了 Certora，询问是否有时间参与对预部署代码的安全保护，这是一个“向左转移”的做法，可以通过更早找到代码漏洞来减少安全测试的成本和干扰。我们感到受宠若惊，并凭借显著改善的方法论、经验和技术，欣然接受了这项工作，希望证明形式验证在智能合约安全方面的有效性。
在接下来的一个季度中，我们与开发团队紧密合作，以更好地理解并正式描述系统。Aave 作为一个将安全性视为最高优先级的顶尖团队，与我们耐心而渴望地合作，结果很快就显现出来。审查包括 20 个合同，包含超过 5,500 行代码，发现了十个 显著独特的漏洞，这些都是 Certora 发现的。在部署之前识别出这些漏洞，避免了 ranging from 统计错误的 totalSupply 报告到资产损失的影响。该努力还产生了 25 条集成到 CI（持续集成检查）中的规范规则。因此，Aave V2 确实证明了其随着时间的推移而展示出的韧性。
自 2020 年 11 月部署以来，该协议保持了数十亿美元的资金未被攻击，最高 TVL 达到超过 180 亿美元。
继续旅程：保护 Aave V3
一年后，2021 年 11 月，Aave 再次准备发布该协议的新改进版本。V3 具有很大的潜力，承诺显著提高资本效率，更广泛的风险和控制机制，以及额外备受期待的功能。为了审查代码和寻找漏洞这一极为重要的使命，Aave 联系了不下于六家顶尖安全公司，其中包括 Certora。
前一年，Certora Prover 获得了一些关键的新能力。我们的安全专家对一组经过深思熟虑的规范规则进行了为期两个月的形式验证。高复杂性使得审查努力变得更慢更困难，并迫使我们只验证了一部分合同。尽管如此，我们在选定的合同中实施了 45 条规范规则，并发现了五个 显著的代码漏洞，Aave 在部署前进行了修复。
该协议已在多个 L2 链和随后以太坊主网上部署迄今为止，TVL 超过 20 亿美元，证明了其免疫力。
持续的安全性和灵活性：现在
在 2022 年 3 月，Aave 和 Certora 之间建立起了良好的历史和理解，我们转向 DAO 提供我们的服务。提案包括由 Certora Prover 技术辅助的专用安全咨询，以及建立和管理一个负责通过形式验证方法审查代码的安全社区的全部责任。在得到 DAO 的强力支持，一个新时代开始了。在随后的半年中，我们荣幸地参与了一些重要合约的开发过程，如：
aStETH，其 TVL 约为 10 亿美元- 关键治理 V2 桥接到多个 L2 链
- AAVE Token V3， 在 V3 治理系统中发挥核心作用
在成功的贡献期后，DAO 决定将其对我们服务的使用延长一年。自那时起，我们感到自己在保护协议的一些最关键的操作和组件中发挥了不可或缺的角色：
在这段持续贡献和合作的时期，我们：
- 报告了 12 个显著漏洞，防止了可能使协议及其用户损失数十亿美元
- 审查了超过 120 个合同，包含超过 40,000 行代码，撰写了超过 800 条规范规则，并在每次代码增加时通过数百次 CI 运行对其进行了验证
- 组织并管理六次社区行动，以保护关键智能合约，同时赋能 Aave 社区为可扩展安全开发做出贡献，发放近 400,000 美元的奖励以激励高质量的规范撰写和漏洞发现。
在对协议的贡献之路上，我们与开发实体进行了无数次关于各种合同设计和实施的讨论。我们通过提出问题和要求一致的答案来推动开发者更好地理解他们的代码和设计。我们以时时可用的方式陪伴开发，专业性满满地为他们在任何必要的问题上提供咨询，无论是代币上市有效负载的审查，还是重大关键新组件的审查，或是事件响应。我们的咨询创建了一个直接的开发反馈循环，从而有机地改善了当前和未来版本的代码设计和安全性。
在与 DAO 的合作中，我们为 Aave 提供了持续高质量的安全保障，同时允许灵活的智能合约开发，促进协议的繁荣。
技术统计
在其他方面，我们：
- 审查了 169 个智能合约，包含 51,289 行 Solidity 代码（我们的技术分析字节码，通常更大）
- 在与 AAVE 长期合作中，防止了 28 个显著漏洞在部署前
- 报告了六个额外显著漏洞，涉及多个正在开发中的合约
- 通过提供每周快速响应提升了开发的频率
- 撰写了形式属性（可以在 这里 找到）并使用 Certora Prover 技术形式验证代码中的大部分内容
- 分配 $383,500 用于外部安全研究人员使用 Certora Prover 审查代码，以支持 6 项不同的努力
我们咨询 Aave 和 BGD 处理现场事件，这对 Aave 这种规模的 DeFi 协议来说是一项艰巨的任务。在某一次具体事件中，我们的团队能够迅速辩驳白帽黑客的潜在攻击，并为 DAO 节省资金，也避免了恶意代码的引入，这始终是安全漏洞的潜在源头。我们还向 BGD 提供了几种潜在的实时威胁，并讨论了可能的补救措施。
结论：一种合作的遗产
Aave 是当前 DeFi 领域中最成功的协议之一。然而，它也是整个 Web3 生态系统中最复杂的借贷系统之一。其复杂性，加上其高 TVL 的增长，提升了 安全风险，并需要与顶尖安全专业人士进行合作。
Certora 利用专业的安全研究人员，他们专注于 Aave 的代码基础。我们的持续合作为 Aave 安全的每个方面提供几乎立即可用的安全咨询，包括事件响应。我们通过将开发者的设计方法转变为以规范和安全为核心，从而改善了协议的设计，这将系统的预期行为和在代码中使用的基本假设形成文档。
我们的形式验证技术降低了智能合约的风险。形式验证生成可再利用的通用而强大的规范测试，以检查每次新代码在协议中的引入，从而防止部署新漏洞。
