圣杯 - 形式化验证提升 DeFi 协议的安全性

Certora 最近通过对 Euler V2 Vault 实现 的一个关键属性进行 形式化验证（formally verifying），提升了 DeFi 安全的标准。在这篇文章中，我们讨论了形式化验证如何提供对 DeFi 协议的强保证，发现开发者未知的稀有漏洞，并且涉及的规范可能比漏洞本身更容易理解。

作为一个例子，我们详细讨论了我们最近对 Euler 的“圣杯”不变性的证明：即在价格不变的情况下，Euler V2 协议上的账户保持健康的性质。我们展示了这一不变性如何可以排除对 Euler V1 系统的先前攻击，以及它如何消除对安全第一的 Euler V2 的未知问题。我们的完整规范可以在 这里 获得。

通过验证排除未知的未知

确保智能合约安全的一个挑战是，安全在本质上是不对称的：攻击者只需找到一个未知的漏洞，而系统防御者需要排除所有可能的攻击向量。这个挑战与来自认知科学的一个概念 Johari 窗口 有很好的联系。在社会科学中，它是一种帮助人们更好理解他们与他人的关系以及他人如何看待他们的方式——对于我们来说，有些信息是自己知道的，有些则是别人知道的。我们可以将其类比于安全性：有些行为是我们知道的（或不知道的），而有些行为是其他人知道的，比如白帽黑客，最后，还有最危险的类别——那些所有人都不知道的行为！

在 DeFi 中，最常见的安全实践之一是邀请白帽黑客审计协议的代码，并试图发现漏洞。这非常有价值，因为它有助于揭示表面下的隐藏区域：审计员知道但系统设计者不知道的问题。然而，智能合约及其交互是复杂的，还有未知的——那些过于微妙以至于审计员无法通过手动审查或甚至广泛测试发现的漏洞。

然而， 形式化验证 让我们能够以原则性和可操作的方式解决未知的问题。形式化验证是使用数学的正式方法证明或反驳系统相对于某一属性的正确性。相比手动审计或测试技术，形式化验证给我们提供了强有力的保证，即这一属性在所有可能的状态、输入和交互中始终成立。除这种保证外，当证明失败时，我们还会从 Certora Prover 获得一个具体的反例，这可能是一个少见触发的漏洞——即连白帽黑客也可能找不到的未知的未知。

如下面的图所示，形式化验证可以应用于设计周期的任何地方。例如，可以使用高层验证工具如 TLA+ 验证系统设计，或使用如 Certora 的证明器对实现进行验证。对实现的验证生成一个验证报告，以补充人为审计员的工作。在开发过程中，合约可以在每次更改时作为持续集成的一部分进行重新验证，相关的可升级合约可以在部署之前和之后通过 CI 得到保护。

图：形式化验证与 DeFi 系统设计过程

然而，形式化验证所提供的保证只强于规范——要真正排除未知的问题，我们需要制定全面的规范，描述关键系统不变性，而不是简单地重申实现细节。

借贷协议

在深入探讨借贷协议的关键安全属性之前，让我们回顾一下这些协议是如何工作的。借贷协议本身是某个基础资产（ERC20）合约上的一个账户。借贷者将一定数量的这种资产存入协议中（将这笔钱转移到协议中）以换取协议的股份。通过同意借出这笔钱，他们的股份积累利息。借款人存入一些担保品（另一种 ERC20 资产），以换取他们所借的基础资产的数量。借款人会积累债务利息，最终必须偿还所借款项及其债务。担保品用于激励偿还，通常借款人必须 超额担保，即存入的担保品的价值必须高于他们所借款项的价值。

借贷协议的关键属性

借贷协议的两个关键安全属性是偿付能力和账户健康。偿付能力 是指协议的参与者都可以将他们的钱提回；换句话说，协议拥有足够的资产来覆盖所有借贷者。账户健康 确保所有借款账户都是超额担保的。账户健康的一个关键指标是贷款价值比（LTV），即已借款金额与已存担保品金额的比例。当该值小于 1 时，账户处于健康状态（并且是超额担保的）。某些协议或治理者可能更加严格，为账户定义了一个更低的 LTV 才能够被认为是健康。

Euler vault 的“圣杯”属性与账户健康相关：借贷协议中的任何操作都不应该使用户变得不健康。也就是说，借款人不能通过承担超过其担保品的债务而使自己变得不健康；任何其他参与者也不应该能够使借款人不健康。对此有两个已知的例外行为。账户可能变得不健康：

• 由于资产价格变化（例如，如果担保品代币的价值下降）
• 由于利息累积

然而，一个不健康的账户不能采取行动以恶化其健康状况（例如，通过借入更多）。

这两个属性之间的关系是什么？偿付能力关系到协议的整体资产，而圣杯规则关系到个别账户的位置。一个安全的借贷协议应该同时强制执行这两个属性，实际上一个的实现可能与另一个相关。然而，通常情况下，一个并不意味着另一个。通过考虑虚构的系统我们可以看到这一点：

• 偿付能力存在而所有账户健康缺失—— 一个允许账户不健康的系统，如果其他账户的担保品弥补了其未担保的部分
• 账户健康存在而偿付能力缺失—— 一个系统可能对所有操作要求单个账户的健康检查，但却不正确地跟踪其底层资产总量

正因为如此，我们证明了 Euler V2 vault 的偿付能力和圣杯规则。

值得注意的是，这两个属性都涉及系统的输出行为，而不是实现细节，且有多种系统设计可以实现这两个属性。安全规范设计的一项关键实践是将规范与实现细节进行区分——处理行为的更广泛、更抽象的属性比简单重申实现细节，更有可能捕获未知的缺陷。

圣杯的探索：规范与证明

我们对于圣杯规则的证明策略基于协议状态转换系统中转变的归纳。作为基础情况，我们证明所有账户最初都是健康的。然后我们展示，如果任意一个账户在任意配置下是健康的，那么在一次转换后，它仍然保持健康。这些转换包括协议的公共函数。

稍微详细一些，我们为单个转换证明的是借款人或任何其他参与者都不能使借款人的健康状态变为不健康，除了上述提到的两个例外：1）价格变化和 2）利息累积。

让我们看看如何在 Certora 的验证语言 CVL 中对其进行规范。

此代码段比我们的完整规范简单了一些，完整规范在 这里 可用，但它展示了关键概念。首先，我们声明代表任意 EVM 状态、任意函数参数和任意账户的变量。然后我们保存此账户初始状态是否健康，执行任何 vault 函数，然后再次检查账户的健康状态。我们证明，如果该账户最初是健康的，那么在后续状态中也是健康的。

由于 Euler V2 的系统设计和实现都着重于安全性，我们能够在不对实现做任何更改的情况下证明圣杯规则。

Euler V1 攻击

为什么这个属性被称为圣杯？它与允许对 Euler V1 系统进行复杂和高明攻击的漏洞密切相关，而如果有“圣杯”属性，就可以避免此攻击。攻击的详细描述见 Coinbase 文章。简而言之，这一攻击依赖于：

• 递归借贷
• 攻击者的捐赠使其自身不健康
• 自我清算

其背后的漏洞根本上源于开发周期后期新增功能的健康检查不正确。

攻击步骤如下：

第 1 步： 攻击者从 AAVE 发起了 2.1 亿美元的闪电贷

第 2 步： 攻击者将闪电贷的收益作为担保品存入 Euler Vault。

第 3 步： 攻击者请求基于其担保品铸造股份

第 4 步： 攻击者调用 donateToReserves，将他们的担保品捐赠给 Vault 的储备

• 这是利用潜在漏洞的地方
• 为捐赠账户进行的 LTV 检查在函数调用开始时提前进行，而在余额变化之前执行
• 调用成功，允许攻击者违反协议，导致其有资格被清算！

第 5 步： 攻击者利用他们控制的清算合约清算他们的用户账户。清算对清算者合约（他们控制）是有利可图的

第 6 步： 清算合约提取清算收益

第 7 步： 攻击者利用自己清算的收益偿还闪电贷，并获利

我们可以看到，脆弱的 donateToReserves 函数 并未 强制执行圣杯规则，因为它可能结束于捐赠者的不健康状态（并且函数不会回滚）。

然而，Euler V2 设计确实具备圣杯属性。让我们看看其系统设计如何强制执行这一点。

安全的 Euler V2 设计

第 1 步： 用户不会直接调用 vault。它们在 EVC 上执行一个调用或批处理，请求 EVC 代表它们执行一个或多个 vault 操作。在 call/batch 实现中，EVC 设置一个 onBehalfOfAccount 地址，以跟踪调用者的权限

第 2 步： EVC 代表用户账户调用所请求的 vault 操作。这通过执行 EVM 级别的 call 操作来调用 Vault 的这个方法

第 3 步： Vault 对任何有可能因操作而影响余额的账户进行健康检查。这些检查被排队，以便稍后执行，因为 EVK 的批处理功能——多个 vault 操作可以依次执行。该批处理允许暂时使账户不健康，只要所需的健康检查在整个批处理完成时成功。

第 4 步： Vault 执行所请求的操作（例如 deposit, withdraw, redeem 等），可能影响一个或多个账户的余额

第 5 步： 控制流返回到 EVC 的 call/batch/permit 方法（请记住：我们是在从 EVC 通过低级调用操作进入 Vault 的）

第 6 步： EVC 对所有已被 Vault 排队检查的账户执行状态检查。（更详细地说：这是通过调用 restoreExecutionContext 进行的）通过将健康检查推迟到 调用的最后，过早进行健康检查的风险也得到缓解。健康检查发生在所有操作结果产生之后，如果任何账户变得不健康，将导致调用回滚。

Euler V2 的圣杯

这里解释一下这个调用图如何强制我们的属性。假设用户发出一个借款超过担保品的调用，这将导致他们的 LTV 超过 1。在这次排队的状态检查执行时（第 6 步），检查将失败，导致整个调用回滚。

你可能会想：为什么我们不直接检查每个函数是否进行了健康检查？这是有几个原因。首先，这样做过于保守，因为并非所有的 vault 操作都能使账户变得不健康，我们希望避免产生额外的、浪费 gas 的检查。其次，我们不希望依赖人工审计来指定每个 vault 调用可能影响哪些账户。通过更多地信任更宽泛的规范，我们有更大的机会超越人类所能发现的。因此，我们的属性还将捕获其他一些严重漏洞：

• 如果状态检查仅排队给其他无关账户
• 如果对进行状态检查的模块初始化函数进行了更改，遗漏了这项检查
• 如果从 EVC 获取的存储的 onBehalfOfAccount 是错误的

接下来，让我们更详细地查看我们的验证设置和我们所做的一些假设。

验证设置

类似 Certora Prover 的验证工具，基于 满足性模态理论 (SMT) 的工具，自动化程度很高。但它们可能会遇到 超时问题，即工具为提供解决方案花费太久或根本无法做到。这是因为在底层，它们是 基于一个 NP-hard 的问题! 解决此问题的一种关键方法是进行 模块验证， 将证明目标拆分为多个子问题。通常，这通过证明一个较小的中间理论来完成，然后在其他证明或假设中使用。

我们为 Euler Vault Kit 进行模块验证的两个关键方式。第一是利用 Euler 的设计，该设计已经是模块化的——顶层合约分为不同功能部分的模块。我们分别验证每个模块。第二，我们验证了 Euler 的 Ethereum Vault Connector (EVC)，然后利用这些假设证明 vault 的圣杯规则。

验证设置如下图所示。我们实际上验证的每个模块下面的合约略有不同——相反，我们构造一个从感兴趣的模块、风险管理器和一个抽象验证工具继承而来的合约。每个模块都需要一个风险管理器，因为它实现相关的健康检查功能。抽象验证工具有助于我们归集和重用定义、工具函数和假设。

验证假设

我们的规范还依赖于一些假设和我们对其他系统组件证明的一些属性。首先，我们依赖一些关于 Ethereum Vault Connector 的假设，该连接器同样由 Euler 开发并且我们单独验证：

• 调用 Vault 的唯一方式是通过 call/batch（直接或通过重新路由）
• call/batch 函数始终执行所有排队的健康检查

我们假设协议治理者完全可信，将选择合理的价格预言机、底层资产和计价资产。我们还假设 LTV 值的以下属性都是由治理强制实施的： setLTV，我们也证明过：

• 清算 LTV 大于借款 LTV
• LTV 小于 1

我们还假设所有预言机报价（单个代币的价值）小于 2**230，以避免溢出；这在实践中极不可能被超出。

关键要点

我们通过形式化验证能够提供强有力的保证，确保 Euler V2 的账户保持健康。形式化验证能够排除未知的漏洞，但验证的有效性取决于规范。编写良好的规范需要时间和努力；最好是在设计过程中尽早开始。描述总体系统行为的规范比单纯重申实现细节更有可能捕获未知错误。现有的形式化验证工具，如 Certora Prover，也可以以高度自动化的方式验证诸如账户健康和偿付能力等关键属性。

[1]:  致谢：Doug Hoyte, Euler 的联合创始人

• 原文链接： certora.com/blog/the-hol...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～