形式验证的三大误解

形式验证（FV）在智能合约领域从未实现其潜在的广泛应用，主要有三个普遍的误解：

1. 使用起来很困难

2. 仅适用于简单系统

3. 不能作为安全工具使用

我们展示了我们的规范语言，CVL，如何打破这些误解。

Certora 实现的主要工具是 Certora Prover。该工具使用 formal verification（形式验证）来证明在 Solidity 编写的智能合约上的属性。

形式验证是数学上检查程序的行为是否符合其规范的过程。这是提升智能合约安全性的一种推荐技术。关于 formal verification 的理论更加详细的解释可以在我们的 白皮书 中找到。

这一切听起来很不错，为什么不是每个人都在使用形式验证来编写或审计智能合约呢？

这可能部分由于一些关于形式化技术的持久性误解，使其看起来太难以实施或者效果不足。本文回顾了这些误解，并解释了它们为何不应成为担忧的原因。

误解一 — 使用形式验证需要博士学位

有一种普遍的误解认为，编写形式规范由于涉及数学和逻辑而十分困难。

使用我们的规范语言 Certora Verification Language (CVL) 编写可以像编写单元测试一样简单。

让我们从一个例子开始：

contract ERC20 is IERC20, IERC20Metadata {
  function transferFrom(address sender, address recipient, uint256 amount)
    public virtual override returns (bool) {
    …
  }
  {…}
}

我们可能感兴趣的其中一个属性是 转账的完整性。这意味着 transferFrom 函数不影响发送者和接收者的余额总和。

以下是用 CVL 编写该属性的时候规则的样子：

rule integrityOfTransfer(address sender, address recipient, uint256 amount) {
  env e;
  uint256 balanceSender = balanceOf(e, sender);
  uint256 balanceReceiver = balanceOf(e, receiver);
  transferFrom(sender, receiver, amount);
  assert balanceSender + balanceReceiver == balanceOf(e, sender) + balanceOf(e, receiver);
 }

a). 初始化 env e，它表示与环境相关的 Solidity 全局变量，例如 msg.sender（请参见 文档）。

b). 获取发送者和接收者的余额。

c). 断言总和未被 transferFrom 函数所影响。

Certora Prover 将使用 formal verification 在所有有效输入和初始状态上测试该规则。就我们的情况而言，这意味着：

1. 所有可能的初始存储状态将得到检查。
2. 所有有效的发送者和接收者地址将被检查。
3. 任何转账金额将被检查。

如你所见，该规则看起来就像一个简单的单元测试。然而，它仍然包含了 FV 的全面性，这在验证智能合约代码的正确性时可能至关重要。

误解二 — 形式验证无法证明基本不变性

上面的例子可以被认为是简单的，也许不足以让你相信在实际代码中和更复杂的属性上使用 CVL 的力量。

2022年5月，Maker的形式验证团队发现了使用形式验证工具的可用性和必要性。使用 Certora Prover，他们发现了其协议中的一个问题。这个问题自2019年11月第一次发布以来便存在（更多细节请见 这里）。

多抵押 DAI (MCD) 是 Maker 实现的稳定币。该协议的一个最关键属性是不变性，称为 DAI 的基本方程。此不变性确保 DAI 的余额始终由债务支撑。这个不变性可以通过方程表达：

DAI 的基本方程

Maker团队在他们的 规范 中实现了这个不变性，使用 CVL 编写。他们惊讶地发现，在已经部署了近三年的代码中，这个不变性并不总是成立。幸运的是，这个错误是不可被利用的，资金也没有面临风险。然而，这例子展示了为什么 FV 工具应被用来确保重要协议的属性对所有可能的输入和状态有效。

误解三 — 形式验证无法发现复杂的漏洞

尽管我们只谈到了 Certora FV 工具来检查特定于被检查协议的属性，但这还不够。一次好的安全审计还必须检查智能合约代码中常见但危险的漏洞。

一年前，ChainSecurity 团队提出了一个新颖的漏洞只读重入。此漏洞最初是在 Curve 协议中发现的。随后在其他多个合约中也发现了该漏洞，估计由于这一攻击向量，风险超过了 1 亿美元。

只读重入攻击的示意图

此漏洞允许潜在攻击者将易受攻击合约的脏状态暴露给第三方被利用的合约。由于视图函数通常缺乏重入保护，因此这种可能性存在，因为它们不会改变状态。

检查此漏洞的一个属性可能是：

每次调用外部函数时，所有视图函数返回有效状态。

在这种情况下，有效状态 是函数的初始状态或函数的最终状态。

在 CVL 中编写这个规则是直接的，如下代码片段所示：

ghost bool no_ro_reentrancy;

rule no_read_only_reentrancy(method f)
{
  env e;
  env e_external;
  calldataarg data;
  require no_ro_reentrancy;
  require before_func1 == view_func_caller(e_external);
  f(e, data);
  require after_func1 == view_func_caller(e_external);
  assert no_ro_reentrancy, "发现了一个只读重入漏洞";
}

在这里，我们使用一个参数规则来对我们的合约的任何外部方法 f 运行我们的规则，并在 Solidity 原始代码中使用包装函数 view_func 来调用任何视图函数。

我们在 Curve 协议上检查了此属性，它发现了不仅是特定易受攻击的代码行，还发现了返回不一致状态的特定视图函数。FV 的全面性和精确性无疑使其成为讨论代码安全时不可或缺的工具。

结论

在本文中，我们展示了三个例子，表明我们的语言 CVL 是可访问和直观的，同时依然具备足够的表达力，以检查非常有趣的属性和漏洞。

许多更多的示例可以在我们的 示例 仓库中找到。

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