不变性驱动开发的需求

本文介绍了不变性驱动开发(Invariant-Driven Development)在智能合约安全中的重要性。通过在软件开发生命周期的每个阶段嵌入不变性——必须始终保持的关键属性,从而显著提高智能合约的鲁棒性。文章阐述了不变性的定义、类型,以及如何在设计、实现、测试、验证和监控等阶段应用不变性驱动开发,以构建更安全的智能合约。

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

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

在这篇博文中,我们将探讨不变量驱动的开发意味着什么,为什么它至关重要,以及你如何采用这种方法来提升你的安全实践并构建更健壮的智能合约。

什么是 Invariants (不变量)?

从核心上讲,不变量驱动的开发涉及定义和维护 Invariants (不变量):关于程序的状态的陈述,无论其状态或执行路径如何,这些陈述都必须始终成立。 这些 Invariants (不变量) 充当系统的支柱,确保其逻辑和功能完整性。

在智能合约中,Invariants (不变量) 可以采用多种形式,具体取决于应用程序。 例如:

  • ERC20 供应量: ERC20 的一个 Invariant (不变量) 是,用户的余额永远不能超过代币的总供应量。
  • Automated market makers (AMMs) (自动化做市商): 在使用 x * y = k 公式(如 Uniswap)的系统中,该公式充当交换的 Invariant (不变量),确保此等式在每次交易后都保持为真(假设没有费用)。
  • Lending protocol (借贷协议): 计算随时间推移获得的利息的函数的 Invariant (不变量) 是它是一个递增的单调函数(例如,返回值随着时间的增加而增加)。

Invariants (不变量) 通常可以分为两种类型:

  • 函数级别 Invariants (不变量) 通常侧重于特定的计算,并且通常不需要更改状态(例如,Solidity 中的 pureview 函数)。 例如,上面描述的借贷 Invariant (不变量)(计算利息的函数是一个递增的单调函数)可以通过函数级别的 Invariant (不变量) 来表示。
  • 系统级别 Invariants (不变量) 跨越整个系统的状态和转换,例如确保其资产始终大于或等于其负债。 系统级别 Invariant (不变量) 的一个例子是确保没有用户的代币余额大于总供应量。

如果你熟悉模糊测试或形式化验证,那么你已经熟悉 Invariants (不变量) 了。 然而,如下一节所示,Invariants (不变量) 并不局限于这些技术; 你还可以在以下情况下使用它们:

  • 监控,通过外部工具,监视违反 Invariants (不变量) 的交易
  • On-chain Invariants (链上不变量),它们直接在智能合约中执行,并在用户与合约交互时充当后置条件
  • Manual reviews (人工审查),代码审查侧重于验证关键 Invariants (不变量)

如果你想了解更多关于在模糊测试的上下文中开发 Invariants (不变量) 的信息,请参阅我们的 Building Secure Contracts 网站上的 模糊测试页面 和我们的 模糊测试研讨会

多年来,安全研究人员一直使用 Invariants (不变量) 来评估合约; 我们的公共报告包含六年多前的 Invariants (不变量),它们的使用在我们的大多数安全审查中至关重要。 如今,我们的许多竞争对手都遵循我们的方法,突显了其效率。 然而,尽管 Invariants (不变量) 在安全社区中取得了成功,但软件工程师仍然很少使用它们。 这就是我们希望在未来几年内改变的。

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

设计 Invariants (不变量)

你越早开始思考和记录 Invariants (不变量),它们对你的项目的影响就越大。 在编写任何代码之前,首先在协议的初始设计期间识别 Invariants (不变量)。 提出以下问题:

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

此阶段不需要特殊的工具——只需要基本的笔记和文档记录即可。 使用此架构作为基线:

ID Invariant (不变量) Components (组件) Testing strategy (测试策略)
<英语描述> <涉及的合约/函数> <模糊测试、形式化验证、单元测试、人工审查>

英语描述可以像你口头描述它一样简单。 然而,对于复杂的 Invariants (不变量) 来说,一个好的做法是通过类似于 Hoare Triple (霍尔三元组) 的格式(前置条件、命令、后置条件)来描述它们。 尽管 Hoare Triple (霍尔三元组) 的名称听起来很正式,但它只是捕获了三个关键要素:

  • Pre-condition (前置条件):关于操作前的状态/参数的假设
  • Command (命令):要测试的操作
  • Post-condition (后置条件):操作后必须为真的内容

从概念上讲,如果你熟悉 Arrange, Act, AssertGiven, When, Then 设计模式,这与遵循它们相同。

例如,x * y = k Invariant (不变量) 可以按照此架构表示; 请参阅 ToB1:

ID Invariants (不变量) Components (组件) Testing Strategy (测试策略)
ToB0 任何用户的余额都不得超过代币的总供应量 MyToken 模糊测试
ToB1 - 如果池没有费用(前置条件)<br>- 调用交换函数(命令)<br>- x * y = k 没有改变(后置条件) MyAMM 模糊测试
ToB2 计算随时间推移获得的利息的函数是一个递增的单调函数 Lending.compute_interest 形式化验证

图 1:Invariants (不变量) 示例

如果你正在寻找创建 Invariants (不变量) 的灵感,可以在我们的 properties 仓库中找到一组预定义的 Invariants (不变量)。

实现和测试 Invariants (不变量)

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

例如,识别函数级别的 Invariants (不变量) 将帮助你为你的代码库设计合适的模块化级别,以一种使它们更易于测试的方式分离组件。

在此阶段,你可以使用的工具有:

Invariants (不变量) 通常可以用 Solidity(如下所示)或 Certora Prover 的领域特定语言(如 CVL)编写。

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

图 2:ToB0:任何用户的余额都不得超过代币的总供应量(properties/ERC20BasicProperties.sol#L18-L25

随着你的代码库在部署后不断发展,请继续在每次代码更改/PR 上测试 Invariants (不变量)。 CloudExec 将帮助你在云中持续运行你的模糊器,而 fuzz-utils 将把模糊测试结果转换为 Foundry 单元测试。

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

On-chain Invariants (链上不变量)

一些 Invariants (不变量) 可以成为链上代码的一部分。 这些 Invariants (不变量) 可以充当合约执行的后置条件。 Uniswap 的 x * y = k 就是这种 Invariant (不变量) 的一个例子。 On-chain Invariants (链上不变量) 是一种强大的工具:它们提供强大的保证,并且非常有效地防止黑客攻击。

然而,可能无法使每个 Invariant (不变量) 都成为链上代码的一部分。 一些 Invariants (不变量) 需要复杂的计算(例如,无界循环迭代),这会增加 Gas 成本或 Invariants (不变量) 本身出现 Bug 的风险。 一个失效的 Invariant (不变量) 的例子是我们 Uniswap V3 报告 中的一个问题 (TOB-UNI-005),该问题可能允许恶意用户耗尽任何 Uniswap 池。 这个问题也强调了 On-chain Invariants (链上不变量) 是一把双刃剑,具有独特的优点和风险。这就是为什么在设计阶段识别潜在的 On-chain Invariants (链上不变量) 以确定哪些适合合约代码并特别注意它们至关重要。

验证 Invariants (不变量)

准备好用于供第三方或内部代码评估(安全审查、Bug 竞赛或 Bug 赏金)的 Invariants (不变量) 列表将帮助安全工程师了解系统的关键部分,并专注于最重要的风险。 这是不变量驱动的开发的一个闪光点:你可以更快地让安全工程师了解你的代码库,并更好地了解代码审查范围。

在此阶段,你将拥有与实施阶段相同的工具:模糊器、形式化验证工具和人工审查。 这种方法的一个例子是我们的 Uniswap V4 报告,我们在其中通过自动化技术(模糊测试、形式化方法和自定义静态分析)测试了 100 个 Invariants (不变量)。 每种技术都针对正确的 Invariant (不变量) 量身定制:

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

要了解我们如何为该项目创建模糊测试工具,请观看我们下周介绍如何为 Uniswap V4 设计 Invariants (不变量) 的演示文稿。 日期和时间将在 X 上公布。

监控 Invariants (不变量)

知道系统的哪些方面至关重要以进行监控可能具有挑战性。 这是不变量驱动的开发方法的另一个亮点:Invariants (不变量) 指示了这些方面。

诸如 HexagateTenderly 之类的解决方案允许你通过事件和交易分析来监控 Invariants (不变量) (请注意,必须调整 Invariants (不变量) 才能遵循这些工具的自定义 API)。 你还可以利用 On-chain fuzzer (链上模糊器)(包括 EchidnaMedusa)来持续压力测试用 Solidity 编写的 Invariants (不变量) 与实际值。

在这里,Invariants (不变量) 必须成为你的事件响应策略的一部分。 对于要监控的每个 Invariant (不变量),你必须定义以下内容:

  • 如何解释和调试 Invariant (不变量) 为何被破坏
  • 你的组织中谁具有适当的知识
  • 你可以使用的操作(例如,暂停系统、更改参数、升级合约)

请遵循我们的 事件响应建议 进行相应规划,并考虑通过主持 SEAL 兵棋推演 来模拟由 Invariant (不变量) 损坏触发的安全事件来验证你的流程。

为什么 Invariant (不变量) 驱动的开发如此强大

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

通过在整个开发过程中集成 Invariants (不变量),你将:

  • 立即检测到 Bug
  • 阐明你的协议的核心假设
  • 减少攻击面
  • 简化代码审查和监控

最终,你将改变你的思维模式,将安全作为优先事项。

Invariants (不变量) 驱动的开发不仅仅是一种技术——它是一种开发思维模式。 它是关于通过开发集成一种安全方法,并推动设计的决策以降低风险。 我们希望看到更多的团队在未来采用这种方法。 如果你需要帮助识别和测试你的 Invariants (不变量),请 联系我们

  • 原文链接: blog.trailofbits.com/202...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
Trail of Bits
Trail of Bits
https://www.trailofbits.com/