保护Uniswap v4：形式化验证和恶意Hook保护

介绍

在这篇博文中，我们将探讨 Certora 如何利用形式化验证来保护 Uniswap v4 免受恶意 hook 的侵害。我们还将探讨 Certora 独特的工具 Certora Prover 如何精确地定义和证明正确性规则，从而确保智能合约的强大安全性。

我们在之前的博文中建立了 Uniswap v4 威胁模型，详细说明了围绕 恶意 hook，资不抵债风险 和各种潜在攻击途径的漏洞。我们还介绍了其他审计公司发现的错误，强调了 Certora 的安全方法 如何应对这些挑战。

让我们探讨一下使用 Certora Prover 进行形式化验证如何加强 Uniswap v4 的防御，从而提供全面的保护，以抵御隐藏的威胁。

从模糊测试开始进行形式化验证

模糊测试和形式化验证中最大的挑战之一是考虑代码的安全性保证属性。幸运的是，当 Certora 审计开始时，Uniswap 团队已经使用 Foundry 开发了许多测试。

其中一项特别的测试，名为 test_fuzz_swap_beforeSwap_returnsDeltaSpecified，包括一项断言，用于检查掉期期间收到的金额是否与指定的金额匹配。此项测试在模糊测试期间成功通过。

然后，当我们的团队在此测试上运行 Certora Prover 时，根据相应的 CVL 规则，该断言被违反。

违规发生的原因是路由器可能在执行测试之前具有原生 token 余额。因此，它将全部余额发送给掉期接收者。这意味着用户将收到掉期的收益以及路由器中任何先前存在的资金。

无论 buzzer 运行多长时间，模糊测试工具都无法找到这种情况。问题源于测试的设置，特别是其初始条件。幸运的是，CVL 和 Certora Prover 不会从特定的起始状态开始，因此它们可以考虑路由合约具有非零原生余额的情况，并提供一个反例。

此测试用例有些人为，并且发现的违规行为并不表示代码中存在错误，而是测试中的不精确。Certora Prover 从比模糊器更通用的前提条件开始。

尽管如此，如果我们忽略这种情况，Prover 验证了其 CVL 形式的测试。这样做的好处是双重的：测试经过改进以考虑任何初始状态，并且还被证明可以与任何测试输入一起使用。相比之下，模糊器仅覆盖有限范围的可能输入。

超越 Solidity：展示 Uniswap v4 协议的有趣属性

用户可以使用 Certora 验证语言 (CVL) 简洁地表达规则，这些规则是智能合约的强大而全面的测试。尽管这些规则可能很简短，但它们的安全性优势非常大。使用 CVL 的优势之一是其语法与 Solidity 或 Forge 测试的语法非常相似。你可以使用 CVL 而不是 Solidity 编写测试，同时利用 Certora Prover 的功能进行形式化验证。

我们将展示我们证明的一个规则示例，以及它如何针对我们的一个担忧提供保证：恶意 hook 的潜在利用。

我们 之前描述过 恶意 hook 如何操纵有利于他们的会计，从而误导 Pool Manager 相信它欠用户（或 hook 合约）的价值超出预期价值。假设标准的无 hook 会计反映了原始的 Uniswap v3 逻辑，基于分段常数乘积池。在这种情况下，我们要求 hook 和用户的总会计等同于默认会计，对于 hook 引入的任何逻辑。换句话说，hook 不得为自己或用户创建“额外”余额。

hook 可以对其自身和用户应用任意余额变更。由于其任意性，该规则还考虑了默认 hook，该 hook 在没有权限时不会应用任何余额变更。

在此规则中，我们从 Pool Manager 调用 swap() 函数两次，使用相同的初始状态（由规则主体中的 initState 表示，它反映了此测试中涉及的所有合约的存储状态）。两种情况的唯一区别是我们提供给 swap 函数的任意 hook 数据字节参数。

与其他编程语言或模糊测试程序中的标准变量声明不同，在这些声明中，值通常会被初始化或随机化，CVL 的行为有所不同。在 CVL 中，所有声明的变量（除非在声明期间显式分配一个值）都是完全任意的。这意味着它们可以采用其类型的任何值，但要受到用户通过 require 语句指定的约束。

但是，这里缺少一些东西。我们尚未定义 hook 合约，或者它如何根据我们提供的输入来计算余额增量。好消息是，我们不需要指定这些细节。CVL 提供了一项独特的功能，允许我们用非确定性行为替换合约调用和返回值。在 CVL 术语中，将函数调用替换为未指定的值称为概括。我们在验证 Uniswap v4 时广泛使用了这种技术。概括越通用，规则证明的适用性就越广泛，从而增强其正确性的保证。

无论 hook 在实践中的功能如何，我们都会将其返回的数据替换为可能在不同调用之间变化的任意值。下面的两个并行场景可能看起来等效，但由于 hook 的随机行为，它们在幕后的行为有所不同。尽管 hook 增量不同，但两次调用的共享状态保持一致，包括池密钥、合约状态和虚拟余额。

规则流程如下：

1. 从初始状态使用任意函数参数调用 swap()。
2. 在交换两个池 token 之后，获取池 hook 地址和 msg.sender 的货币增量。
3. 从原始初始状态再次调用 swap()，使用不同的 hook 参数，就像没有调用第一个 swap() 一样。
4. 获取此第二种情况的货币增量。
5. 断言对于两种情况下的两种池 token，hook 地址和 msg.sender 的货币增量之和是相同的。

规则：
在给定相同初始状态的情况下，货币增量之和与 hook 的行为无关。

rule swap_hook_sender_deltas_sum_is_preserved() {
    /// 环境 (env) 是包含区块链和交易上下文的内部结构。
    env eA;
    env eB;
    /// 在两种情况下，msg.sender 都是相同的。
    require eA.msg.sender == eB.msg.sender;

    /// 声明 swap 参数（通用）
    PoolManager.PoolKey key;
    IPoolManager.SwapParams params;
    address hookAddress = key.hooks;
    PoolManager.PoolId poolId = PoolGetters.toId(key);

    bytes hooksA;   /// 场景 A 的 Hook 数据。
    bytes hooksB;   /// 场景 B 的 Hook 数据。

    /// 这是一个存储“检查点”，可以随时恢复到此。
    storage initState = lastStorage;

   /// 有必要消除在swap之前hook的影响，这样它就不会改变
   /// 交换的数量。
   require !CVLHasPermission(hookAddress, BEFORE_SWAP_RETURNS_DELTA_FLAG());

    swap(eA, key, params, hooksA) at initState;

    /// 获取场景 A 的虚拟余额状态（掉期后）。
    int256 deltaSender0_A = PoolGetters.currencyDelta(e1.msg.sender, key.currency0);
    int256 deltaSender1_A = PoolGetters.currencyDelta(e1.msg.sender, key.currency1);
    int256 deltaHook0_A = PoolGetters.currencyDelta(hookAddress, key.currency0);
    int256 deltaHook1_A = PoolGetters.currencyDelta(hookAddress, key.currency1);

    /// 从规则的初始状态在场景 B 中调用 swap。
    swap(eB, key, params, hooksB) at initState;

    // 获取场景 B 的虚拟余额状态（掉期后）。
    int256 deltaSender0_B = PoolGetters.currencyDelta(e1.msg.sender, key.currency0);
    int256 deltaSender1_B = PoolGetters.currencyDelta(e1.msg.sender, key.currency1);
    int256 deltaHook0_B = PoolGetters.currencyDelta(hookAddress, key.currency0);
    int256 deltaHook1_B = PoolGetters.currencyDelta(hookAddress, key.currency1);

    /// 断言对于两种情况下的两种 token，货币增量之和是相等的。
    assert
        deltaSender0_B + deltaHook0_B == deltaSender0_A + deltaHook0_A
        &&
        deltaSender1_B + deltaHook1_B == deltaSender1_A + deltaHook1_A;
}

Certora Prover 使用 SMT 求解器成功证明了此规则。这种验证的含义是什么？

不管 hook 在掉期操作期间返回的数据如何，都可以保证 hook 地址和用户 (msg.sender) 的货币增量之和被保留，并且保持等于默认情况下的增量（朴素 hook），该增量基于标准的 Uniswap v3 逻辑。因此，如果我们确信归因于用户的增量是准确的，我们可以自信地说，任何 hook 都无法产生偏离正确值的增量。

细心的读者可能会争辩说，仅凭此规则不足以确保免受恶意 hook 的攻击。例如，我们尚未考虑不同 token 的其他用户的虚拟余额。这种说法是有效的，并且我们有一个额外的规则，确保 swap() 函数仅更改 msg.sender 和 hook 的余额，特别是对于池中涉及的两种 token。

主要的点是，有时仅凭一个规则无法完全消除潜在的攻击途径。至关重要的是要了解有助于有效证明的一组假设和断言。

结论

在这篇博文中，我们重点介绍了使用形式化验证来增强模糊测试覆盖范围的好处，并演示了其识别非平凡边界情况的能力。我们还说明了如何在 CVL 中实现规则以检测通用 hook 的不当行为。我们的努力成功地证明了一个关键属性，无论 hook 的实现如何，该属性都成立。这强调了形式化验证在保护智能合约和确保借贷协议或去中心化交易所 (DEX)（如 Uniswap）中的资金偿付能力方面的巨大潜力。

我们将很快在外部 Git 存储库中发布一套全面的 v4-core CVL 规则，详细说明有关 Pool Manager 内正确处理资金的重要属性。

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