不变性驱动开发的呼吁

编写智能合约需要比大多数其他软件工程领域更高级别的安全保证。行业已从简单的ERC20代币发展到利用领域特定算法并处理重大货币价值的复杂多组件DeFi系统。这种演变释放了巨大潜力，但也引入了不断升级的黑客攻击事件。

我们需要向不变性驱动开发进行范式转变，以推动行业走向更安全的未来。通过将不变性——必须始终成立的关键属性——嵌入软件开发生命周期的每个阶段，您可以显著增强智能合约的健壮性。

在这篇博客文章中，我们将探讨不变性驱动开发的含义、为什么它至关重要，以及如何采用这种方法来提升您的安全实践并构建更健壮的智能合约。

什么是不变性？

不变性驱动开发的核心是定义和维护不变性：关于程序必须始终成立的陈述，无论其状态或执行路径如何。这些不变性充当系统的支柱，确保其逻辑和功能完整性。

在智能合约中，不变性可以根据应用程序采取多种形式。例如：

• ERC20供应量：一个ERC20不变性是用户的余额绝不能超过代币的总供应量
• 自动化做市商(AMMs)：在使用x * y = k公式的系统（如Uniswap）中，该公式充当交换的不变性，确保每个交易后这个等式仍然成立（假设没有费用）
• 借贷协议：计算随时间累积利息的函数的不变性是它是一个递增的单调函数（例如，返回值随时间增加而增加）

不变性通常可以分为两种类型：

函数级不变性通常关注特定计算，通常不需要改变状态（例如Solidity中的pure或view函数）。例如，上述借贷不变性（计算利息的函数是递增单调函数）可以通过函数级不变性表达。

系统级不变性跨越整个系统的状态和转换，例如确保其资产始终大于或等于其负债。系统级不变性的一个例子是确保没有用户的代币余额大于总供应量。

如果您熟悉模糊测试或形式化验证，您已经熟悉不变性。然而，正如下一节所示，不变性不仅限于这些技术；您还可以在以下上下文中使用它们：

• 通过外部工具进行监控，监视破坏不变性的交易
• 链上不变性，直接在智能合约内执行，并在用户与合约交互时充当后置条件
• 手动审查，代码审查侧重于验证关键不变性

如果您想了解更多关于在模糊测试背景下开发不变性的信息，请参阅我们"构建安全合约"网站上的模糊测试页面和我们的模糊测试研讨会。

安全研究人员使用不变性评估合约已有多年；我们的公开报告包含超过六年历史的不变性，它们的使用在我们的大多数安全审查中至关重要。如今，我们的许多竞争对手都遵循我们的方法，突显了其效率。然而，尽管在安全社区取得了成功，软件工程师仍然很少使用不变性。这是我们希望在未来几年改变的情况。

不变性不是一次性的考虑——它们应该指导您智能合约开发的每一步。以下是如何在流程的每个步骤中应用它们。

设计不变性

您越早开始思考和记录不变性，它们对项目的影响就越显著。在编写任何代码之前，在协议的初始设计期间就开始识别不变性。提出以下问题：

• 主要不变性是什么？ 让您的团队识别10个最重要的不变性，以便他们在项目开发的每个阶段都能牢记它们。如果他们无法回答，那么请投入更多时间来识别它们。
• 这些不变性将如何检查？ 如何检查不变性将影响代码的设计。例如，将被监控的不变性需要发出相关事件，而将在链上运行的不变性可以从特定的代码隔离中受益。
• 这些不变性将如何指定并与代码保持同步？ 您的规范很可能会随着代码和项目需求的变化而发展。确保它们保持同步的过程对协议的长期成功至关重要。

此阶段不需要特殊工具——只需基本的笔记和文档。使用此模式作为基线：

英文描述可以像口头描述一样简单。然而，对于复杂不变性的良好实践是通过类似Hoare三元组的格式（前置条件、命令、后置条件）来描述它们。尽管名称听起来很正式，但Hoare三元组只是捕获三个关键元素：

• 前置条件：关于操作前状态/参数的假设
• 命令：要测试的操作
• 后置条件：操作后必须为真的内容

从概念上讲，这与遵循Arrange、Act、Assert或Given、When、Then设计模式相同（如果您熟悉它们）。

例如，x * y = k不变性可以按照此模式表达；参见ToB1：

图1：不变性示例

如果您正在寻找创建不变性的灵感，可以在我们的属性仓库中找到一组预定义的不变性。

实施和测试不变性

智能合约开发生命周期中最长的部分是开发和测试。在这里，开发代码、创建和更新不变性以及一般测试之间的迭代过程至关重要。

例如，识别函数级不变性将帮助您为代码库设计适当级别的模块化，以便以更易于测试的方式分离组件。

在此阶段，您可以使用的工具包括：

• 模糊测试器（例如Medusa、Echidna和Foundry）
• 形式化验证工具（例如Halmos、Certora和KEVM）
• 手动审查

不变性通常可以用Solidity编写（如下所示）或用特定领域语言（如Certora Prover的CVL）编写。

1
2
3
4
5
6
7
8

// 用户余额不得超过总供应量
function test_ERC20_userBalanceNotHigherThanSupply() public {
    assertLte(
        balanceOf(msg.sender),
        totalSupply(),
        "User balance higher than total supply"
    );
}

图2：ToB0：任何用户的余额绝不能超过代币的总供应量（properties/ERC20BasicProperties.sol#L18-L25）

在部署后，随着代码库的发展，继续在每次代码更改/PR时测试不变性。CloudExec将帮助您在云中持续运行模糊测试器，而fuzz-utils将把模糊测试发现转换为Foundry单元测试。

工具的选择将取决于不变性和代码库；请参阅我们描述何时使用模糊测试与形式化验证的博客文章。如果某些不变性足够简单——或者相反，太复杂而无法用工具测试——彻底的文档和单元测试将至关重要。

链上不变性

一些不变性可以成为链上代码的一部分。这些不变性可以作为合约执行的后置条件。Uniswap的x * y = k就是这种不变性的一个例子。链上不变性是一个强大的工具：它们提供强有力的保证，并且在防止黑客攻击方面非常有效。

然而，使每个不变性都成为链上代码的一部分可能不可行。一些不变性需要复杂的计算（例如，无界循环迭代），这会增加gas成本或不变性本身出现错误的风险。一个破坏不变性的例子是我们Uniswap V3报告中的一个问题（TOB-UNI-005），该问题可能允许恶意用户耗尽任何Uniswap池。这个问题突显了链上不变性是一把双刃剑，具有独特的 benefits 和风险。这就是为什么在设计阶段识别潜在的链上不变性以确定哪些适合合约代码并对其特别关注至关重要。

验证不变性

准备好不变性列表供第三方或内部代码评估（安全审查、错误竞赛或漏洞赏金）将帮助安全工程师理解系统的关键部分并专注于最重大的风险。这是不变性驱动开发闪耀的一个例子：您可以更快地让安全工程师熟悉您的代码库，并更好地理解代码审查覆盖率。

在此阶段，您将拥有与实施期间相同的工具：模糊测试器、形式化验证工具和手动审查。这种方法的一个例子是我们的Uniswap V4报告，我们通过自动化技术（模糊测试、形式化方法和自定义静态分析）测试了100个不变性。每种技术都针对正确的不变性进行了定制：

图3：我们Uniswap V4报告的自动化测试部分

要了解我们如何为此项目创建模糊测试工具，请观看我们下周关于如何为Uniswap V4设计不变性的演示。日期和时间将在X上公布。

监控不变性

了解系统的哪些方面对监控至关重要可能具有挑战性。这是不变性驱动开发方法闪耀的另一个领域：不变性指示了这些方面。

像Hexagate和Tenderly这样的解决方案让您通过事件和交易分析监控不变性（请注意，不变性必须适应遵循工具的自定义API）。您还可以利用链上模糊测试器（包括Echidna和Medusa）使用实际值持续压力测试用Solidity编写的不变性。

在这里，不变性必须是您事件响应策略的一部分。对于要监控的每个不变性，您必须定义以下内容：

• 如何解释和调试不变性被破坏的原因
• 您组织中的谁具有适当的知识
• 您可以采取哪些行动（例如，暂停系统、更改参数、升级合约）

遵循我们的事件响应建议进行相应规划，并考虑通过举办SEAL战争游戏来验证您的流程，模拟由破坏不变性触发的安全事件。

为什么不变性驱动开发强大

大多数智能合约黑客攻击涉及业务逻辑或领域特定问题。开发人员应该防范这些问题，而不变性驱动开发旨在解决它们。

通过在整个开发过程中集成不变性，您将：

• 立即检测错误
• 澄清协议的核心假设
• 减少攻击面
• 简化代码审查和监控

最终，您将转变心态，将安全作为优先事项。

不变性驱动开发不仅仅是一种技术——它是一种开发心态。它是关于通过开发集成安全方法并推动设计决策以降低风险。我们希望看到多个团队在未来采用这种方法。如果您需要帮助识别和测试您的不变性，请联系我们。