智能合约安全新范式，超越 `require`和`assert`

智能合约安全新范式，超越 require_assert

摘要

不要只为特定的函数写 require 语句；为你的协议写 require 语句。函数遵循检查(requirements)-生效(Effects)-交互(INteractions)+协议不变性(Invariants)或 FREI-PI 模式可以帮助你的合约更加安全，因为它迫使开发人员除了关注函数级别的安全之外，还要关注协议级别的不变性。

动机

2023 年 3 月，Euler Finance 被黑客攻击，损失 2 亿美元。Euler Finance 是一个借贷市场，用户可以存入抵押品并以其为抵押进行借款。它有一些独特的功能，实际上他们是一个可与 Compound Finance 和 Aave 媲美的借贷市场。
你可以阅读关于这个黑客的事后总结这里。它的主要内容是在一个特定的函数中缺少健康检查，允许用户打破借贷市场的基础不变性。

基础不变性（Fundamental Invariants）

大多数 DeFi 协议的核心都有一个不变性，即程序状态的一个属性，它被期望永远是真的。也可能有多个不变性，但一般来说，它们是围绕着一个核心思想建立的。这里是一些例子：

• 如在借贷市场中：用户不能采取任何行动，使任何账户处于不安全或更不安全的抵押品仓位（"更不安全"意味着它已经低于最低安全阈值，因此不能进一步提取）。
• AMM DEX 中：x * y == k，x + y == k，等等。
• 流动性挖矿抵押中： 用户应该只能提取他们存入的抵押代币数量。

Euler Finance 出错的地方不一定是他们增加了功能，没有写测试，或者没有遵循传统的最佳实践。他们对升级进行了审计，并有测试，但还是被漏掉了。核心问题是他们忘记了借贷市场的核心不变性（审计人员也是如此！）。
注：我不是要挑刺 Euler，他们是一个有才华的团队，但这是一个最近的案例。

问题的核心

你可能在想 “嗯，没错。这就是他们被黑的原因；他们忘了一个 require 语句”。是也不是。
但为什么他们会忘记 require 语句呢？

检查-生效-交互 不够好

推荐给 solidity 开发者使用的一个常见模式是 Checks-Effects-Interactions（检查-生效-交互）模式。它对于消除与重入有关的错误非常有用，而且通常会增加开发人员去执行输入验证的的数量。但是，它容易出现只见树木不见森林的