在Compound V3中通过形式化规范检测边缘情况

我们描述了 Compound 新协议 Comet 的有趣正确性规则，并展示了在早期开发中如何使用 Certora Prover 来消除代码中的漏洞

介绍

在当今市场中，大多数 DeFi 借贷活动都涉及提供波动的加密资产并借入单一基础代币。为了应对这种常见的交易模式，Compound 创建了最新的借贷应用程序 Comet，旨在通过优化特定用例来实现更高的资本效率。该合约允许用户将多达 15 种预定义的（波动）资产作为抵押，同时借入一种预定义的币（通常是一种稳定币）。

在开发过程中，Certora 团队与 Compound Labs 合作，使用 Certora 的验证语言（CVL） 编写了正式规范，以描述系统的预期行为，并使用我们的自动化形式验证工具 Certora Prover 检查其实现是否遵循这些规范。Compound 和 Certora 团队指定了 50 条正确性规则，以描述该协议应遵循的重要属性。自动化的形式验证帮助团队在开发期间发现边界情况下的漏洞并在部署前修复这些漏洞，详见 验证报告。

本文其余部分展示了形式验证过程如何在开发过程中发现 Comet 协议中的细微漏洞。由于 Prover 在部署前揭示了漏洞，Compound 开发人员能够在任何资产面临风险之前解决该问题。漏洞已经在提交 4cbb7e6a 中修复。

在此过程中，我们将描述如何应用模块化，这是一种处理导致 Prover 超时的代码的重要技术。

Comet 中的抵押品标志

发现的漏洞是由于不正确处理用户抵押品状态的标志集所导致。我们首先描述这些标志应如何工作。

Comet 为每个用户持有一个数据结构，包含作为抵押品提供的资产列表。此结构以位向量的形式存储，其中每个资产（15 个中的一个）都有一个从 0 到 14 的唯一 assetOffset。位向量称为 assetsIn，assetsIn 的每个位称为一个标志。

struct UserBasic {    …    uint16 assetsIn;    …}/// @notice 用户到基础本金和其他基本数据的映射mapping(address => UserBasic) public userBasic;

此外，对于每种资产，有一个映射存储每个用户提供的抵押品数量：

struct UserCollateral { uint128 balance; …}/// @notice 每个抵押资产的用户抵押数据的映射mapping(address => mapping(address => UserCollateral)) public userCollateral;

使用位向量 assetsIn 允许快速且廉价地计算特定用户作为抵押的资产。主要使用两个函数来操作和访问 assetsIn：

/** @dev 如果给定资产存在非零余额，检查用户是否拥有该资产/function isInAsset(uint16 assetsIn, uint8 assetOffset) virtual internal view returns (bool)

/** @dev 如果用户进入或退出某项资产，则更新 assetsIn 位向量/function updateAssetsIn( address account, AssetInfo memory assetInfo, uint128 initialUserBalance, uint128 finalUserBalance) virtual internal

## 基本属性 — `assetsIn`标志的完整性

我们称一个属性为 **基本的**，如果该属性的违反意味着系统的关键行为不正确。下面是一个基本属性的例子：

> 属性：特定资产的 `userCollateral` 大于零当且仅当相应的标志被设置。

该属性也可以用逻辑符号表示：

> userCollateral\[user\]\[asset\].balance > 0 ⇔
>
> isInAssetsIn(userBasic\[user\].assetsIn, getAssetOffset(asset) )

为什么这个属性是基本的？如上所示，`assetsIn` 用于确定哪些资产作为抵押。如果这个属性不成立，可能会出现多种错误：

- 用户虽然拥有足够的抵押品，但可能无法借款。这意味着系统容易受到拒绝服务攻击。
- 即使用户拥有足够的抵押品，他们也可能被清算。这意味着用户可能在不该失去资产的情况下失去资产。
- 合约在吸收用户的账户时，可能无法将用户的抵押品转回，这导致系统资产的损失。

由于如果这个属性被违反则可能导致多种严重后果，我们希望有保证系统不能违反这个属性。

## 正式指定 `assetsIn` 标志的完整性

使用 Certora Prover 进行形式验证是一种提供此保证的方法。要使用 Prover，我们必须在 [Certora 的验证语言（CVL）](https://docs.certora.com/en/latest/docs/ref-manual/cvl/index.html) 中指定所需的属性。然后，Certora Prover 可以分析智能合约代码以确定其是否满足规范。

给定一个程序和一个属性，Prover 返回三种答案之一：

- **违反** 显示一个具体输入，该输入违反了规范。该输入可能非常罕见，因此通过测试和模糊测试很难找到。
- **证明** 表示数学上不可能违反该规范。
- Prover 也可以 **超时**，无法返回答案。

与单元测试或模糊测试不同，Certora 规范是详尽的：一个属性的证明意味着该属性在 _所有_ 情况下都成立，而不是在固定集或随机样本的可能场景中成立。

在 CVL 中，上述基本属性很容易写。我们已经展示了该属性的逻辑表示：

> userCollateral\[user\]\[asset\].balance > 0 ⇔
>
> isInAssetsIn(userBasic\[user\].assetsIn, getAssetOffset(asset) )

在 CVL 中编写这种属性是简单的。在 CVL 中，应该始终成立的属性可以表示为一个 **不变**：

invariant integrityOfAssetsInFlags(address user, uint8 asset)userCollateral[user][asset].balance > 0 <=> isInAssetsIn(userBasic[user].assetsIn, getAssetOffset(asset))

如果 Prover 能证明该属性，我们就知道它必须在所有可达状态中成立。如果 Prover 找到一个违反判决，我们就知道有一个严重的漏洞，并将得到一个利用该漏洞的示例。不幸的是，由于 Comet 代码库的复杂性，这条规则落入第三类：Prover 在尝试证明时超时。

下一部分解释我们如何解决这个超时以找到证明或违反。

## 使用模块化简化验证

在复杂的系统如 Comet 中，我们使用模块化的方法证明属性（例如，见 [https://github.com/dafny-lang/dafny) ](https://github.com/dafny-lang/dafny)。我们将验证分为两个独立步骤：

- 证明难以推理的低级函数的有用属性
- 使用简单易推理的抽象简化低级函数，遵循已证明的属性

我们现在将详细演示这些步骤。

## 步骤 1：简化 `assetIn()` 和 `updateAssetsIn()`

目前 Prover 对位操作有困难。经过一些调查，我们发现 `assetIn` 和 `updateAssetIn` 函数在 Comet 代码库中被频繁调用，并使用这些难以推理的位操作。

`assetIn` 和 `updateAssetIn` 函数查询和更新包含资产标志的位向量。原则上，这些函数应等同于以下实现，它们使用标准映射而不是位向量：

mapping (uint16 => mapping (address => bool)) assetInState;function isInAsset(uint16 assetsIn, uint8 assetOffset) returns (bool) { return assetInState[assetsIn][indexToAsset[assetOffset]];}function updateAssetsIn( address account, AssetInfo memory assetInfo, uint128 initialUserBalance, uint128 finalUserBalance) override internal { if (initialUserBalance == 0 && finalUserBalance != 0) { // 设置资产的标志 assetInState[assetInAfter][assetInfo.asset] = true; } else if (initialUserBalance != 0 && finalUserBalance == 0) { // 清除资产的标志 assetInState[assetInAfter][assetInfo.asset] = false; }}

虽然此实现效率较低，但对于 prover 而言，推理会容易得多。

利用 CVL 的模块化，我们可以使用这些近似值代替实际的 `assetIn` 和 `updateAssetIn` 来验证其余代码库中的属性。这种简化使得 prover 成功地证明了 `integrityOfAssetsInFlags` 不变性。

## 步骤 2：检查近似

为了证明步骤 1 中的近似合理性，我们辩称，**原则上**，实际和简化的实现应该表现得相同。为检查该假设，我们可以验证这些实现是否满足一些基本正确性属性。例如，这两个函数的一个属性是 `assetIn` 标志根据对 `updateAssetIn` 的调用进行更新。一个典型的单元测试程序将检查特定值：

const tokens = makeProtocol();const user = makeUser();const wethAddress = tokens[‘WETH’].address;// 调用 updateAssetsIn 从 0 值更改为 100updateAssetsInExternal(user.address, wethAddress, 0, 100);// 检查该用户和代币的 isInAsset 返回 true

assert isInAsset(getAssetinOfUser(user.address), tokens[‘WETH’].offset);

使用 CVL，我们可以检查用户地址、代币地址、代币 offset 和余额值的所有可能值上的属性：

rule check_update_UserCollateral( address account, address asset, uint128 initialUserBalance, uint128 finalUserBalance){ updateAssetsIn(account, asset, initialUserBalance, finalUserBalance); bool flagUserAsset = isInAsset(getAssetinOfUser(account), getAssetOffsetByAsset(asset)); assert (initialUserBalance == 0 && finalUserBalance > 0) => flagUserAsset, “余额从 0 更改为非零，但获取器返回了 false”; assert (initialUserBalance > 0 && finalUserBalance == 0) => !flagUserAsset, “余额从非零更改为 0，但获取器返回了 true”;}

由于我们的目标是获得实际实现的正确性保证，因此我们不能在此步骤中使用 `assetIn` 和 `updateAssetIn` 的简化版本。然而，这条规则专注于单个方法的简单属性，因此 Prover 可以及时完成该规则的验证，即使代码包含复杂的位操作。

## Certora Prover 发现的违反

上述步骤 2 非常重要。如果简化版本的代码行为与原版不同，则使用简化版本的证明不适用于真实版本。

实际上，步骤 2 中 `check_update_userCollateral` 规则的验证使我们发现了 Comet 协议中的漏洞。Prover 未能产生证明，而是产生了一个 [反例](https://vaas-stg.certora.com/output/23658/e07dabf38b877c29d91d/?anonymousKey=d0d2558675b84bb0ad284b55ed4fc41316eeb331)，显示该属性 **不成立**：

![](https://img.learnblockchain.cn/2025/04/05/14341810_image.jpg)

在此示例中，我们可以看到用户的余额已从 0 更改为 1。然而，相应的位标志却为 false。在提供的反例中，工具显示了 `assetOffset` 为 8 的情况。

## 违反的原因

一个简单的疏忽导致了这个违反。在早期版本的代码中，协议仅允许 8 种资产而不是 15 种。有些代码仍然基于只有 8 种资产的错误假设。在特别是，以下函数是不正确的：

function isInAsset(uint16 assetsIn, uint8 assetOffset) virtual internal view returns (bool) { return (assetsIn & (uint8(1) << assetOffset) != 0);}

该函数对任何大于或等于 8 的 `assetOffset` 返回 false，而这并不是正确的行为。

一旦发现漏洞，修复变得简单；它在提交 [4cbb7e6a](https://github.com/compound-finance/comet/pull/169/commits/4cbb7e6a3338a288bb95ba4992bd180dcd3721d6) 中得到了修复。Prover 能够验证修补后的实现确实满足预期属性。

## 结论

使用 Certora Prover 进行形式验证是发现智能合约中微妙但重要的漏洞的强大工具。形式验证的一个基本局限性是，总会存在 Prover 超时的情况。然而，我们已展示简化复杂函数并检查简化后有时可以找到漏洞，即使 Prover 最初超时。

>- 原文链接： [medium.com/certora/detec...](https://medium.com/certora/detecting-corner-cases-in-compound-v3-with-formal-specifications-b7abf137fb15)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～