免责声明：马洛安全公司这篇文章中的内容是 "按原样 "提供的，没有任何形式的保证。本文件中的任何内容都无意成为专业建议，包括但不限于金融、投资、法律或税务建议。Input Output Global不对您使用或依赖本文件中的任何信息负责。
简介
在大多数区块链中，智能合约是一个计算机程序，一旦满足某些预定义的条件就会自动执行。在Cardano中，它有点不同，因为智能合约的执行发生在提交给Cardano节点的外部交易中。但是，无论它在引擎盖下如何工作，智能合约对许多行业都很有用：金融、房地产、商业和其他许多行业。
使用智能合约的交易可能涉及大量价值的移动和转移，这可能是不良行为者的一个珍贵目标。同样，由于编码中的缺陷或漏洞，这些价值可能被锁定，或完全丢失。
要避免任何不希望看到的结果，需要实施一个强大的安全框架，这涉及到开发商、交易所和任何其他处理智能合约的各方的设计原则、审计和最佳实践的结合。
Marlowe是一个由Input Output Global（IOG）创建的工具和语言的生态系统，它增加了来自整个Cardano技术社区的不断增长的资源，以便在Cardano区块链上开发金融和交易智能合约。
Marlowe套件的设计和开发都是以安全为中心的。例如，Marlowe的创造者已经建立了功能限制，确保合同是有限的，并且总是终止的。Marlowe还避免了某些编程结构，以防止不希望出现的结果，例如递归和循环。第三方Tweag在Marlowe部署到主网上之前进行了静态和动态审计。所有这些安全功能的结果，以及其他许多功能，是一个安全的智能合约创建和开发平台。
本文深入探讨了Marlowe的安全性，解释了安全审计的结果，以及团队如何应对这些结果，内置的功能限制，部署中包含的安全分析工具，以及使用Marlowe时必须采取的一些预防措施和注意事项。
本文件的结构
本文件分为六个定义明确的部分：
- 智能合约审计
- 基于智能合约的攻击
- Tweag审计
- Marlowe中内置的安全增强功能限制
- 交易验证
- 货币政策
作为一个整体，本文意在全面了解智能合约审计的重要性以及目前存在的基于智能合约的不同类型的攻击，然后再具体深入探讨Marlowe工具套件如何利用审计和强大的安全原则来维护一个安全的智能合约开发环境。
智能合约审计
概述
智能合约固有的自主性和某些交易中涉及的相对高风险意味着确保一致性和安全性是最重要的。这需要准确了解智能合约在执行时的行为，以便发现和解决任何潜在的缺陷或故意的恶意代码。从安全角度对智能合约进行审计是防止后续失败或损害的最佳方式。审计在部署前彻底检查智能合约的代码和条件，以确保合约的行为符合预期。
审计方法
尽管智能合约审计的方法可能不同，而且因项目而异，但智能合约可以使用人工或自动方法进行分析。通常情况下，大多数项目采用两者的组合。
文件收集
在审计过程开始之前，审计人员可能会花一些时间收集任何与项目有关的文件。这可能包括技术文件，白皮书，代码库，以及任何其他可能与审计过程有关和有帮助的材料。
手工审计
这种形式的智能合约审计涉及一群人分析每一行代码、合约逻辑、合约架构和任何内置的安全措施，以确保高效的设计和正确性。除了揭示编码错误外，人工审计还可能发现设计缺陷。人工审计往往被认为是一种非常彻底和准确的方法。
自动审计
与人工审计不同，自动审计通常采取以软件为中心的测试方法。专有的或现成的软件审计工具可能有助于发现错误，但某些漏洞可能不会变得明显。
由于这些方法的互补性，最佳的审计实践涉及手动和自动审计的结合，以确保所有潜在的缺陷、错误和漏洞被发现和纠正。
审计后的行动
一旦审计过程完成，审计师将产生一份报告，详细说明他们的发现。这些可能包括按严重程度分类的错误和一系列建议。
合同错误可分为以下几种：
- 严重：这种类型的缺陷可能会阻止合同和/或协议的安全运行。
- 重大：编码或逻辑中的某些错误可能导致资金损失，或协议状态不受控制。
- 中等：虽然资金可能没有风险，但这些类型的错误可能影响合同的性能或可靠性。
- 轻度：这种分类通常包括对安全影响很小或没有影响的低效率代码。信息性：通常指的是编码风格或最佳实践问题。
智能合约审计的优势
虽然审计对任何应用程序都很重要，但对于在区块链上运行的智能合约和去中心化应用程序（DApps）来说尤其重要，因为这些去中心化的账本具有不可改变的性质。
智能合约审计的优势包括：主动识别风险，避免潜在的高成本错误，整体上有一个更好的开发环境，以及获得关于漏洞的洞察力，以及如何消除它们。
主动识别风险
部署未经审计的智能合约是一场赌博，任何开发者或公司都不应该这样做。一些智能合约可能涉及大量资金，如果丢失或受损，可能导致更大的责任。通过积极主动地努力补救这些风险，大大降低了发生严重错误的可能性。
避免潜在的昂贵的错误
由于编码/逻辑错误或由于合同中的恶意干扰，资金被永远锁定，这是任何客户或开发者都不愿意经历的。经济损失只是其中的一个方面。也可能有严重的法律后果。
一个更好的整体开发环境
审计软件不仅是推荐的，而且是一种要求。保证一个应用程序或一套应用程序的安全，并遵循最佳实践，可以加强提供，创造一个更健康的开发环境。
获得对漏洞的洞察力，以及如何消除这些漏洞
在软件开发中，预防胜于修补。而当涉及到智能合约时，由于区块链的不可更改性，没有机会进行修补。彻底的审计将产生许多关于代码、合同的逻辑、架构和许多其他参数的信息，使开发人员能够完善和产生最佳的合同。
基于智能合约的攻击
重入式攻击
在这种攻击中，一个智能合约函数通过调用第二个合约暂时放弃了对交易的控制，第二个合约开始对第一个合约进行递归提款调用，在第一个合约更新其状态之前耗尽其资金。这些类型的攻击之所以成为可能，是因为智能合约编码中存在的漏洞。2016年的DAO事件涉及到一个重入式攻击。
Cardano区块链的设计使重入式攻击成为可能。因为Cardano使用EUTXO模型，智能合约是原子性的，不会互相调用，这使得重入成为不可能。
前端入侵
一些区块链设计允许智能合约和交易在被链上确认之前，可以公开查看一段时间。这些悬而未决的交易在整个网络的内存池中共享，这使对手能够看到合同的预期结果。这样一个能看到待定交易的对手可以引入一个新的交易，因为他知道这样做会在待定交易的基础上获得利润，而牺牲其他用户的利润。从本质上讲，对手操纵交易的执行顺序对他们自己有利。
虽然这种类型的事件在其他区块链上是一个大问题，但没有证据表明Cardano（以及延伸到Marlowe）会受到前面运行的入侵。
Oracle操纵
甲骨文将区块链连接到外部系统，智能合约可能会根据从甲骨文收到的数据执行。这种对外部系统的依赖性意味着，如果甲骨文收到的输入在被送入甲骨文之前被操纵，智能合约执行的安全性和完整性可能会受到影响。
其他常见的基于智能合约的安全漏洞包括算术错误、整数溢出和下溢、智能合约可见性设置和时间戳操纵。
特威格的审计
本节重点介绍Tweag安全审计的结果，Marlowe团队的回应，以及Marlowe设计中的安全原则。
特威格安全审计的主要发现和内部回应
特威格对Marlowe语言进行了手动和自动审计，发现了几个问题。
高严重性的发现包括负数存款的处理，防止 “双重满足”，状态不变性的执行，正式规范与Plutus实现之间的实施差异，以及货币保存定理的证明。
负存款的处理
存款收入的计算方法是将存款输入相加，不管它们是否为负数，而语义学认为它们是零存款。再加上没有对结束的马洛状态进行余额检查，这使得结束的余额与支付给马洛验证人的价值不同。这可以被一个允许负数存款的Marlowe合同所利用。
内部回应
这个问题已经通过在Marlowe语义验证器中添加一个针对负数存款的防护措施来解决。该防护措施确保验证器对负数存款的语义与Marlowe的Isabelle语义一致。具体来说，一个负数的存款被视为零的存款。因此，一个负的存款不会减少Plutus数据中的任何账户余额，而且内部余额的总和将与UTXO中持有的Marlowe语义脚本地址的值相匹配。
防止双重满足
尽管Marlowe验证器防止了在同一事务中运行的多个Marlowe验证器脚本副本之间的双重满足，但在同一事务中Marlowe验证器与另一个Plutus验证器一起运行的情况下，它没有防止。
内部响应
现在，通过强制要求Marlowe验证器是唯一在交易中运行的Plutus脚本，以防止双重满足。这允许Marlowe合同与其他Plutus脚本协调，但只在不可能有双重满足的情况下。一些基于属性的测试被添加进来，以检查这种缓解的正确性。
状态不变性的强制执行
最初，Marlowe验证器对自己的正确操作做了乐观的假设，并且没有检查某些不变式，以减少Plutus的执行成本。
内部回应
Marlowe语义验证器现在严格执行初始和最终状态的不变性，确保正数的账户、不重复的状态条目（账户、选择和绑定值）以及总的内部值与脚本UTXO的值相匹配这三个状态不变性。
正式规范与Plutus实现之间的实施差异
审计揭示了正式规范与实际的Plutus实现之间的一些差异。具体来说，就是语言上的差异和对Isabelle、Haskell和Plutus Tx的效率考虑。
形式化的规范是用Isabelle编写的，这是一种形式化方法的语言，而实际的Marlowe实现是用Haskell和Plutus Tx编写的。Marlowe团队尽可能地遵循Isabelle的规范，但是由于语言的不同，一些偏差是不可避免的。例如，Marlowe实现的某些方面在Isabelle中是低效的，所以为了实现更高效的Haskell，必须进行修改。
内部回应
这个问题通过代码分析和基于属性的测试得到了缓解
货币保全定理的证明
货币保全定理只考虑了资产的数量，而没有考虑其类型。这意味着该证明不会考虑这样的情况：例如，一个合同可以收到20个Ada和15个Djed并偿还20个Djed和15个Ada。
内部回应
对Isabelle代码的修订弥补了这个问题。具体来说，增加了一个新的MultiAssets类型，并重构了Isabelle代码（没有修改解释器），以证明资产被保留下来。
Marlowe的内置安全增强功能限制
Marlowe具有几个限制，以确保某些安全风险不会发生。
-
合同是有限的
-
合同会终止
-
合同有明确的有效期
-
合同结束时没有资产被保留
-
价值是保存的
除了这些限制之外，为了确保安全，Marlowe没有使用一些编程语言结构： -
不允许递归
-
不支持循环
-
不允许定义函数或宏
-
超时必须是数字常数
-
只有Case continuations可以被merkleized。Faustus编程语言放宽了上面的一些限制，但它可以编译成安全的Marlowe。
-
安全分析工具
Marlowe团队设计的marlow-cli运行分析工具可以检查一个Marlowe合约与Cardano分类账规则的兼容性。
Cardano账本有内置的限制，可以阻止Marlowe合同在链上运行，即使合同本身对Marlowe语言有效。例如，账本对角色和代币名称的长度进行了限制，还限制了Plutus的执行成本。任何违反这些规则的合同都不会在链上运行，即使该合同可能是正确构建的。同样，虽然合同可能在Playground上运行，但如果合同违反了分类账的限制，它们也不会在链上运行。了解更多关于内置分类账设计限制的信息。
主要启示：Playground是关于语言的，而Runtime是关于在Cardano区块链上具体实现Marlowe合约的。如果有人在其他区块链上实现Marlowe，你仍然可以使用Playground，但你不能在其他区块链上使用Runtime。
注意：如果数据点不适合在链上，合同会被锁定，但Marlowe套件包括评估这种风险的工具。这些工具应该在部署合约之前使用。
交易验证
有两种类型的Plutus验证器脚本参与验证UTXO支出：
语义验证器
支付验证器
安全实践表明，除非交易的内容和影响已被审查并被充分理解，否则不应签署交易。在Marlowe环境中，这意味着验证Marlowe合同，它的输入和它的状态。它还意味着确保所使用的角色铸币策略（如果有的话）和Marlowe验证器是正确的。
下面的安全考虑适用于两种验证器脚本类型。
语义验证器
在签署一个Marlowe交易之前，应该充分理解以下概念：
- 该交易是否运行一个Marlowe合约？
- 它的角色铸币政策是什么（如果有的话）？
- 角色代币是如何分配的（如果有的话）？
- 当前的合约和它的状态是什么？
- 哪些输入正被应用于该合约？
- 交易中还发生了什么？
该交易是否操作一个Marlowe合同？
Plutus验证器脚本是所有指定版本的Marlowe合同的通用解释器，这意味着一个Marlowe合同的UTXO驻留在一个脚本哈希中。验证一个交易从一个将Marlowe脚本哈希值作为其支付部分的地址支出，就可以确认真正的Marlowe验证器将运行以验证该特定UTXO的支出。通过编译验证器并计算其哈希值，可以从第一原理上计算出Marlowe验证器的脚本哈希值，前提是这个存储库中的Marlowe脚本源代码是可以信任的。
它的角色造币策略（如果有的话）是什么？
铸币政策是创建特定代币类型的代币的规则集，其铸币政策的哈希值可以识别。这被称为造币政策ID。铸币政策决定了是否可以创建新的代币，或者已经创建的代币是否就是全部。
例如，Marlowe合同的各方，如贷款人和借款人，可以用两种方式表示：
通过地址：地址类型的每一方都对应于一对公钥和私钥的实例，这对公钥和私钥大概由其中一方的钱包持有。使用地址来代表各方比使用角色更简单、更便宜。为了认证自己，由地址代表的各方只需要签署需要他们认证的交易（即那些为该方执行存款或选择）。
通过角色令牌：每一个角色类型的当事人都对应着一个存储在链上的令牌。对于一个合同使用角色令牌作为认证，该合同需要声明其角色令牌的铸币政策ID是它想作为角色令牌的铸币政策ID。在这种情况下，由铸币政策ID识别的令牌的每个资产名称都代表不同的一方。为了验证交易，角色令牌所有者只需要将其作为需要验证角色令牌所有者的交易的一部分。有可能存在不止一个具有相同资产名称的令牌，所以从技术上讲，除非你拥有具有该方资产名称的角色令牌的所有实例，否则你不会拥有一个角色方。
角色代币是如何分配的？
如果一个合同只使用地址来代表各方，那么角色的铸币政策就不是一个问题。地址的缺点是它们不能被证明地转移，所以一旦知道了一个地址的私钥，你就不能表明你已经忘记它并删除它。从地址接收者的角度来看，地址始终是不安全的。拥有安全地址的唯一方法是自己生成。
优势或作用是，由于代币被视为链上的原生资产，它们可以像ada或任何其他资产一样被转让。但是，任何拥有具有正确造币政策ID和资产名称的代币的人都可以作为它所代表的一方，所以你需要确保你是唯一拥有这种代币的人，否则你就不能真正控制这一方了。
当然，你可以通过自己铸造角色代币来确保你是唯一拥有该代币的人（Marlowe Runtime会在合约创建过程中安全地完成这一过程）。如果有其他人铸造了角色代币或创建了合约，你需要确保：
你拥有所有控制该方的现有代币
不能再创建这样的代币（因为铸币政策不允许）。
如果造币政策足够简单，检查这个的最简单方法是使用Marlowe扫描器来找出合同的角色造币政策ID。然后，使用Cardano explorer来检查铸币政策背后的政策是什么（以确保不能产生更多的角色），并检查已经铸币的现有角色的当前分布情况（换句话说，谁拥有哪些代币）。
当前的合约及其状态是什么？
合同的交易前状态是在与正在从Marlowe脚本地址花费的UTXO相关的Plutus数据中定义的。这个数据集必须在交易中提供，并且必须包含以下内容：
- 合同内部账户的余额
- 在合同执行过程中，到此为止的选择历史
- 合同中绑定的变量的当前值
- 合同中尚待执行的部分
数据可以从无符号的交易主体中提取出来，并使用函数Plutus.V2.Ledger.Api.fromData将其反序列化为Language.Marlowe.Core.V1.Semantics.MarloweData。
另一种方法：
- 命令行工具marlowe log --show contract将显示合同的链上历史。
- 这个在线工具也可以查看合同和链上状态
- 一个REST API提供了通过marlowe log --show获得的相同信息。
什么输入被应用到合同上？
与从Marlowe脚本地址支出UTXO相关的Plutus赎回者定义了应用于合同的输入，以及在交易主体中指定的交易的槽位有效期间隔。输入是一个由零个或多个存款、选择和通知组成的序列。使用像Marlowe Playground或marlow-cli run prepare这样的工具，可以分析将这个输入应用到合约的后果。
赎回者可以从未签名的交易主体中提取，并使用函数Plutus.V2.Ledger.Api.fromData将其反序列化为Language.Marlowe.Scripts.MarloweInput。命令行工具marowe-cli util slotting将计算出有效性间隔中提到的槽与合同中的POSIX时间之间的关系。
交易中还发生了什么？
未签署的交易可能包含了Marlowe合同规定之外的其他支出和支付。这可以用工具cardano-cli transaction view来检查。
货币政策
通常情况下，应该使用货币政策（像Marlowe Runtime中支持的那些）来强制执行单一的造币事件和每个角色的单一代币。这些政策确保角色代币是真正的不可伪造的代币（NFT），所以角色代币持有者是可以验证的唯一可以作为合同中的当事人的人。
铸造多份特定角色代币的货币政策，或具有开放铸造政策的政策，支持非标准的用例。例如，铸造每个角色代币的两个副本，并将其分配给同一方，如果包含 "热 "角色代币的钱包无法访问，该方可以将一个代币放入冷库作为备份。一些新颖的众包合同可能涉及到将角色（通过相同的角色代币，甚至在合同开始后也可能被铸造）分配给许多参与者。最后，Plutus合约对角色代币的铸造政策可以与一个或多个Marlowe合约的运作相协调。
角色代币
角色代币可以授权Marlowe交易中的存款和选择。授权使用角色代币比用公钥授权更灵活，因为角色代币（以及因此参与Marlowe合约）可以在钱包之间转移或转移给其他人。
Marlowe验证器脚本并不强制执行任何特定的角色令牌的货币政策，以实现新的使用案例。然而，在基于角色的Marlowe合同中，授权的安全性确实严重依赖于角色代币的货币政策。这意味着货币政策和代币的链上支付都应该在参与Marlowe合约之前进行仔细的审查。验证一个简单脚本的货币政策需要从区块链上检索脚本并研究它。验证Plutus脚本的货币政策包括获取和研究该脚本的Plutus源代码，并对源代码进行哈希运算以检查货币政策ID。
鸣谢： Joseph Fajen、Brian Bush和Omer Husain都对本文做出了宝贵的贡献。