Canton 上机构金融的智能合约安全：一个完全不同的问题

可以说，现今存在的智能合约安全行业很大一部分是专为以太坊量身定制的。其工具、分类法和威胁模型都假定了一种特定的架构：共享可变状态、公共内存池和开放执行模型。这个基础无疑是出色的，并已帮助保护了数十亿美元的链上资金。然而，Canton Network 为解决机构交易的智能合约提供了另一种架构。这种替代模型正是 Digital Asset 团队通过其智能合约语言 Daml 所提供的。

Daml 专为受监管的金融机构打造并在 Canton Network 上运行，其生态系统参与者近 600 家，其中包括高盛、DTCC、摩根大通、Broadridge、纽约梅隆银行、Citadel Securities 和伦敦证券交易所集团。Canton Network 由 Daml 提供支持，拥有超过 6 万亿美元的链上真实世界资产，已将自己定位为数字全球金融未来的主要参与者。

在我们的研究过程中，我们所发现的拓展了我们对智能合约安全的思考方式，并促使我们为 Daml 智能合约的正确性和安全性创建了三个新的开源工具，如下所述。但这种思维转变始于更好地理解以太坊和 Canton 之间的差异。

两种架构，两个威胁面

以太坊使用基于账户的模型，具有共享的、可变的状态。一个合约有存储槽，任何授权的调用者都可以调用一个函数来修改存储在这些槽中的数据。整个链状态和所有待处理交易都是全局可见的。

这种设计导致了一系列特定且有据可查的漏洞。例如，重入（reentrancy）之所以发生，是因为外部调用可以在调用合约的状态更新完成之前调用任意代码。抢先交易（front-running）和夹心攻击（sandwich attacks）利用公共内存池，在确认之前，所有参与者都可以看到待处理交易。预言机操纵（Oracle manipulation）利用链上价格数据，任何参与者都可以在一笔交易中扭曲这些数据。这些并非随机的错误。每一个都可以追溯到一种架构选择：全局可见状态、公共交易队列以及默认情况下任何合约都可以调用其他合约公共接口的开放执行模型。

另一方面，Canton 使用了截然不同的架构。它使用 Daml 作为其智能合约语言，该语言建立在基于 Haskell 的类型化函数式核心之上（Daml 编译器使用了 GHC 前端的一个分支）。智能合约是用代数数据类型定义的，类型系统在编译时强制执行规则。其执行模型是一个扩展的 UTXO 系统：合约是不可变的，你不会更新它们，而是归档旧的并创建一个新的。交易视图是按接收方加密的，并且 sequencer 和 mediator 协调共识，而从不查看交易内容。通过基于锁的冲突检测协议防止双重花费：如果两笔交易试图归档同一份合约，sequencer 的排序决定优先级，后来的交易将被拒绝。该协议在具有加密承诺和 sequencer 强制排序的两阶段提交方案上运行。

其后果是结构性的。重入不可能发生，因为执行模型不允许在交易中进行任意的外部调用。MEV 提取不可能发生，因为没有公共内存池，并且 sequencer 只能看到加密的有效载荷。sequencer 不能根据其无法读取的内容进行重新排序。预言机操纵的表面比公共区块链更窄：隐私模型限制了攻击者对合约状态的可见性，并且 Canton 生态系统中目前不存在闪电贷工具来放大无资本攻击。mediator 只接收一个通知树（参与者身份、交易树结构、确认响应），而 sequencer 只看到发送者/接收者身份、消息大小和时间。

然而，这并不意味着 Daml 合约没有错误。这意味着这些错误与 Solidity 合约中发现的错误不同。

重要的错误类别

在过去十年中，加密安全社区建立了一个令人印象深刻的漏洞分类法。标准化的合约库、静态分析器、模糊测试器、形式化验证工具、审计方法。这项工作的质量确实很高，但它都不直接适用于基于 Daml 的智能合约。这些检测器检查的是在扩展 UTXO 模型中无法存在的漏洞类别。然而，包括静态分析、基于属性的测试、形式化验证、对抗性威胁建模在内的这些学科仍然完全适用。只是它们需要针对不同的攻击面。

根据我们对 Daml 智能合约的分析，我们能够识别出以下几类错误。

守恒性违规

在一个具有多个转移路径的系统中——用于合并代币的自转移、通过预批准的直接转移、通过锁定持有量的两步转移——总输入量等于总输出量的不变量必须在每个路径中都成立。当有三条路径，每条路径都有不同的中间步骤时，很容易出错。

源于治理控制参数的算术错误

Daml 合约通常包含由治理选择设置的参数：价格字段、费率、每优惠券上限值。这些值会流入算术运算。Daml 在溢出和除以零时会引发 ArithmeticError，这会中止整个交易。如果治理控制的值作为分母出现（并且这种情况经常发生），配置错误可能会导致整个工作流无法运行。这不是代码缺陷。这是代码与配置之间关系的缺陷。代码信任治理过程，而治理过程又由人类操作。

结算逻辑中的时间假设

Daml 的时间模型是 文档 中所说的“略显模糊”。提交的参与者会提出一个账本时间，而 synchronizer 的 sequencer 会分配一个记录时间。协议强制两者之间存在有界偏差，如果差距超过配置的容忍度，交易就会被拒绝。执行截止日期的结算逻辑使用 getTime 需要考虑到这一点：在截止日期边界附近提交的交易可能会被拒绝，不是因为它迟了，而是因为提议时间和记录时间之间的偏差将其推到了容忍度窗口之外。模糊性可以针对每个 synchronizer 进行配置，但任何将账本时间视为精确的挂钟时间的合约逻辑都在做出协议没有明确保证的假设。

跨 synchronizer 时，问题会加剧。文档 明确指出：跨 synchronizer 没有全局因果关系保证。来自不同 synchronizer 的事件可能以任何顺序到达。在一个 synchronizer 上创建、分配给另一个 synchronizer，然后归档的合约可能会以与预期不同的序列发出这些事件。重新分配本身是非原子性的两阶段操作：从源取消分配，分配给目标，在它们之间存在一个“待定分配”的 limbo 状态。虽然 getTime 在交易依赖项上是单调的，但跨 synchronizer 没有全局排序。任何假设跨 synchronizer 边界有序时间戳的结算逻辑都在做出协议不提供的假设。

应用边界处的非确定性排序

Canton 保证因果一致性，而不是全序。多个参与者可以以不同的序列返回同一组合约。选择无序查询的第一个结果的应用程序代码在单节点测试中编译通过，但在生产中会间歇性失败。任何依赖“第一个”或“最旧”而没有在合约字段上明确排序的逻辑都是潜在的缺陷。

上述错误类别未出现在 SWC 注册表或任何现有漏洞分类中。它们是结构上不同的执行模型所产生的结构上不同的错误。

构建验证栈

当我们开始深入研究 Daml 时，它还没有以对抗性为焦点的安全工具。编译器捕获类型错误，linter 检查代码风格。然而，Daml 智能合约中重要的错误类别（例如，守恒性违规、治理触发的算术错误和时间排序错误）都留给了人工审查。为了解决这个问题，我们构建了三个工具：daml-lint、daml-props 和 daml-verify。我们从构建它们中学到的是，并非任何单个技术都是新颖的，而是将这些工具结合使用，每个工具都能捕获其他工具可能遗漏的问题，从而提高对智能合约正确性的信心。

静态分析

第一个工具是 daml-lint，一个用 Rust 编写的静态分析扫描器。该方法遵循 Slither 为 Solidity 建立的模型：AST 遍历检测器，与已知漏洞类别进行模式匹配。

Daml 不公开公共 AST 格式，因此我们使用 haskell-tree-sitter 作为解析器基础（Daml 在语法上与 Haskell 接近），并使用关键字垫片来识别 Daml 特定的声明：template、choice、signatory、observer、ensure、key、maintainer。一个自定义提取层构建了模板、选择及其主体的中间表示（IR）。

IR 存储原始文本和已解析的语句类型。这种双重表示是关键的设计决策。有些检测器需要结构性推理——验证断言是否在 try/catch 块之前。另一些检测器只需要定位除法运算符并检查分母是否受保护。两种表示都可供每个检测器使用。

我们发布了六个检测器，针对上述错误类别：十进制字段上缺少“ensure”子句、无保护的除法、应用程序级别查询中的非确定性排序（通过 Ledger API）、持久合约中的无界字段以及选择参数中缺少正金额断言。注意：Daml 本身没有链上查询原语；这指的是使用 Ledger API 结果的客户端逻辑。

模式匹配对于已知漏洞类别是有效的。但模式是语法的。它们捕捉我们已知要寻找的东西。最重要的错误是语义的。也就是说，它们涉及随时间推移的操作之间的关系。

基于属性的测试

第二个工具是 daml-props，一个用纯 Daml 编写的基于属性的测试框架。该方法遵循 Haskell 的 QuickCheck 和 Solidity 的 Echidna 的谱系，适应 Daml 的约束，不依赖类型类或 IO，并使用 Park–Miller 线性同余生成器作为唯一可用的伪随机数生成器（PRNG）。

核心抽象是有状态序列测试。我们定义一个动作类型，一个将动作应用于状态的执行器，以及一个不变量，它必须在每个步骤之后都成立。该框架生成随机的动作序列，执行它们，检查不变量，当发现违规时，将失败序列收缩到最小复现。

收缩是它与随机测试的不同之处。用一个 47 步的序列识别一个违规是信息丰富的，但将其缩减到 1 步的最小复现是可操作的。

基于属性的测试探索了开发人员意图与代码允许之间的空间。然而，“数百个随机输入”不是“所有输入”，这引出了形式化验证。

形式化验证

第三个工具是 daml-verify，它使用 Z3 prover 来证明关键不变量适用于所有可能的输入。不是一个样本，而是每一个十进制值、每一个时间戳以及输入和输出的每种组合。

我们使用 Z3 变量以 Python 编写 Daml 逻辑的符号模型，然后将属性定义为前置条件-目标对。prover 检查前置条件与目标否定合取的可满足性。如果不可满足（即，不存在满足前置条件但违反目标的输入），则该属性被普遍证明。如果可满足，Z3 会生成一个反例。

我们在四个类别中验证了 14 个属性：

• 守恒性：接收方金额加上发送方变化量等于总输入量，适用于所有转移路径。
• 除法安全性：每次除法都有一个非零分母。这是形式化验证最有价值的地方。
• 时间性：结算截止日期在 synchronizer 边界之间有序。
• 金库：抵押品比率保护成立，清算守恒价值，债务累积是单调的。

我们选择手动模型构建而非自动提取，类似于 Certora 使用其 CVL 规范进行 Solidity 的方法。为了降低模型与代码之间差异的风险，我们构建了一个验证协议：每个模型都与 Daml 源代码逐行检查。

为什么是三个工具？

每个工具都是一个层，可以捕获其他层可能遗漏的东西。

静态分析识别语法模式（已知漏洞类别和结构性反模式），但无法推理操作之间随时间推移的关系。基于属性的测试通过探索输入空间来发现语义错误，但它只检查它生成的输入，“数百个”不是“所有”。形式化验证普遍地证明属性适用于所有输入。然而，它操作的是模型，而不是代码本身，并且其忠实度取决于模型的精确性。

一旦这些层组合起来，差距就会缩小。在我们的测试中，daml-lint 发现了无保护的除法。daml-props 发现了零输入铸币，而 daml-verify 证明了仅靠测试只能近似的守恒属性。

这有一个自然的景深类比。单元测试在开发人员预期的场景中是精确的。基于属性的测试扩大了光圈，以包含没人想到要检查的场景。形式化验证将焦点扩展到整个输入空间。信心需要所有三种焦距。

这意味着什么

Canton Network 上存在一个并行且不断增长的 Daml 智能合约宇宙，许多区块链安全社区的人尚未对其进行审视。它运行着机构赖以生存的关键金融基础设施。它的安全模型与加密世界多年来研究的模型根本不同。公共区块链生态系统中的“智能合约安全”与 Canton Network 之间的差异是巨大的。这两个领域使用相同的词汇——智能合约、账本、代币、结算——但它们指的是不同的架构，面临不同的威胁，需要不同的工具。

验证和安全不仅仅需要一个工具。它需要一个栈。这个栈的价值超过了其各层之和，因为每一层都弥补了其他层的盲点。在金融基础设施中，错过缺陷的成本以真实资本和潜在监管后果来衡量，这种层级组合至关重要。

常见问题

Canton Network 上的智能合约安全与以太坊有何不同？

Canton 使用扩展的 UTXO 模型，具有加密的交易视图和非公共内存池，这消除了以太坊常见的整个漏洞类别，例如重入和 MEV 提取，并由于其隐私模型而显著缩小了预言机操纵面。然而，Canton 引入了其独特的风险面：跨转移路径的守恒性违规、由治理控制参数触发的算术错误以及结算逻辑中的时间排序问题。保护 Daml 智能合约需要专门构建的工具和方法，而不是直接移植以太坊安全工具。

OpenZeppelin 在 Daml 智能合约中发现了哪些错误类别？

根据 OpenZeppelin 的研究，Daml 智能合约中最重要的错误类别是：（1）守恒性违规，即在所有转移路径中总输入量未能等于总输出量；（2）源于治理控制参数的算术错误——特别是无保护的除法，其中配置错误的分母可能导致整个工作流停止；（3）结算逻辑中的时间假设错误，其中账本时间的模糊性和跨 synchronizer 排序可能导致交易被拒绝或处理顺序不正确；以及（4）应用程序边界处的非确定性排序，其中未排序的查询结果导致潜在的、间歇性的生产故障。

为什么保护链上机构金融基础设施需要多层验证方法？

没有单一的验证技术能够覆盖运行金融基础设施的智能合约的全部风险面。静态分析捕获已知的语法漏洞模式，但无法推理操作之间随时间推移的语义关系。基于属性的测试探索意外的输入组合，但只抽样输入空间。形式化验证证明不变量适用于所有可能的输入，但它操作的是模型而不是代码本身。组合所有三层——正如 OpenZeppelin 通过 daml-lint、daml-props 和 daml-verify 所做的那样——才能弥合差距并提供机构级的安全信心。

OpenZeppelin 为 Daml 智能合约安全开发了哪些开源工具？

OpenZeppelin 专门为 Daml 智能合约的正确性和安全性开发了三个开源工具：daml-lint，一个基于 Rust 的静态分析扫描器，带有六个针对 Daml 特定漏洞类别的检测器；daml-props，一个用纯 Daml 编写的基于属性的测试框架，可生成随机动作序列并将故障缩减为最小复现；以及 daml-verify，一个使用 Z3 prover 的形式化验证工具，用于证明关键不变量（涵盖守恒性、除法安全性、时间排序和抵押品管理）适用于所有可能的输入。

随着传统金融转向链上，智能合约安全为何重要？

随着金融机构、资产管理公司和结算基础设施迁移到像 Canton 这样的区块链网络，支撑这些系统的智能合约成为关键的金融基础设施。管理代币化资产或结算逻辑的 Daml 智能合约中的缺陷会带来实际的资本后果和潜在的监管风险。应用严格的、分层的安全评估——针对每个网络的特定架构和威胁面进行调整——是链上金融基础设施所要求的安全标准。

准备好保护你的代码了吗？

申请审计 →

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