智能合约开发的演进

智能合约领域的过去几周绝对是有趣的。从 SVM 集成的壮观提案到 Vyper 利用削弱 Curve 并几乎摧毁我们的 DeFi 生态系统，很明显，下一波智能合约的需求是什么：由前沿编程语言提供支持的、原生安全且高吞吐量的虚拟机。多年来，重入一直是加密领域最显著的攻击媒介，尤其是在大型 DeFi 黑客攻击中。

Curve 攻击：

最近查看 Curve 攻击，fallback 函数允许多个可重入的 AddLiquidity() 和 RemoveLiquidity() 函数，使攻击者能够退出池子，获得相对于其初始存款的过剩资产，而池子保留了存款前的余额，并且 LP token 的铸造和销毁记录显示出非常准确的值。受影响池子中的流动性被耗尽，因为攻击者重复了此序列。

重入向量

在这种情况下，fallback 函数调用 fund 的 withdrawal 函数，试图利用目标池。当初始交易执行后，攻击者的资源保留在执行序列中时，fallback 函数会循环执行。

The DAO 攻击：

臭名昭著的 DAO 攻击也是一个摧毁行业的事件，它削弱了以太坊的生态系统。

DAO 的 splitDAO 函数，旨在让那些想离开 DAO 并创建自己的“子 DAO”的 token 持有者使用，但在其操作顺序中存在一个缺陷。这个缺陷使它容易受到重入攻击。

1. 初始设置：攻击者首先购买 DAO token 成为 The DAO 的参与者。这意味着他们在 The DAO 中有一些以太币，由他们持有的 token 代表。

2. 恶意合约创建：攻击者不是直接从常规以太坊地址发起攻击，而是精心制作了一个恶意合约。该合约有一个专门设计的 fallback 函数，当合约收到以太币时会被调用。

3. 触发 splitDAO：攻击者从他们的恶意合约中调用 splitDAO 函数来创建一个“子 DAO”。当 The DAO 返回代表攻击者 DAO token 的以太币时（使用 msg.sender.call.value(balance)()），以太币被发送到攻击者的恶意合约，触发其 fallback 函数。

4. 通过 Fallback 函数重入：恶意 fallback 函数在收到以太币后，立即再次调用 splitDAO，请求另一次提款。

5. 状态尚未更新：由于原始合约的状态（设置 shares[msg.sender] = 0）仅在以太币发送后才会发生，并且由于恶意合约在状态更改之前启动了一个新的 splitDAO 调用，因此从 The DAO 的角度来看，攻击者仍然拥有其全部余额。这允许攻击者再次“提取”相同的金额。

6. 递归消耗：从恶意 fallback 函数对 splitDAO 的这种递归调用发生了多次，基本上允许攻击者不断耗尽以太币，直到他们提取的金额是其原始余额的许多倍。

The DAO 合约中的缺陷是操作顺序：

1. 将以太币发送到外部地址。

2. 然后更新内部状态。

这个顺序允许外部地址，特别是如果它是一个具有特定功能的合约（如本例中的恶意 fallback 函数），利用尚未更新的状态。

如果 The DAO 的合约首先更新内部状态，然后发送以太币，那么攻击就不会成为可能。这是因为当恶意 fallback 函数发出其重入调用时，攻击者的余额已经被设置为零。

对于极客来说，这是一个危机代码的简化版本：

function splitDAO(...) {

var balance = shares[msg.sender]; // 获取发送者的余额    shares[msg.sender] = 0; // 将发送者的份额设置为 0    msg.sender.call.value(balance)(); // 将以太币发回给发送者 ...

}

现在怎么办？

行业中的许多开发者已经认识到 Solidity 的缺陷，并转向基于 Rust 的语言。在这些开发者群体中，出现了两个主要的虚拟机：SVM 和 MoveVM。虽然我个人是两者的坚定支持者，并且看到了两者的用例，但从技术角度来看，很明显 Move 语言在性能方面更胜一筹。Move 源自 Rust 语言，由 Facebook 的 Diem 项目设计，Move 被设计成区块链版本的 Rust（可以认为 Move 之于 Rust，就像 React 之于 Javascript）。

Move 安全机制

1. 用例和设计理念：

   • Rust：被设计为一种通用语言，侧重于“安全并发”和“零成本抽象”。专为多个领域而设计，并在人工智能、区块链、Web 开发等领域迅速得到采用。

   • Move：专为区块链设计，特别是 Diem（以前称为 Libra）生态系统。拥有一系列独特的需求，区块链有其自身的特点：不变性、共识机制，尤其是错误的高成本（如 The DAO 事件所示）。

2. 安全机制深度 挖掘：

尽管有革命性的 Anchor 框架，但安全管理资产的任务通常落在开发者肩上：为重入和其他重大错误创造空间。为了解决这个问题，Move 在设计时考虑了以下核心原则：

1. 资源类型：Move 的一个核心特性是它的“资源类型”。资源用于表示数字资产。它们不能被复制或丢弃，只能在存储位置之间移动。这保证了资产不会被意外复制或丢失。

2. 模块系统：Move 使用模块系统，其中每个模块定义资源类型和过程，从而创建一个清晰的命名空间和封装。这允许对行为和数据完整性进行强有力的不变性保证。对于较新的/中级开发者来说，这也允许他们获得直观的开发体验

3. 线性类型系统：类似于 Rust 的所有权系统，Move 的线性类型系统确保一个资源始终只有一个“所有者”。这对于表示数字资产至关重要，因为双重支付是一个问题。它采用线性执行和实用程序系统，从而杜绝了重入攻击的尝试。交易签名者或私钥持有者是 Move 合约中的主要实体，每个函数都模块化。这种设计意味着每个交易都被视为“一次性”请求，并且没有留下任何可以成功重复的空间。例如，调用 fallback() 函数最终可能会通过 RPC，但在执行时被阻止。在这种情况下，一旦私钥持有者签名的交易成功执行，线性执行就会“清除机架”。

4. 字节码验证：此外，Move 通过字节码验证器为其智能合约执行添加了一个额外的安全层，该验证器保证类型和内存安全。字节码验证器使用借用检查方案，该方案允许在任何给定时间只能对一个值进行一次可变引用。为了简化对写操作效果的识别，字节码验证器确保全局存储是基于树的（如 Merkle 根），而不是基于图的。由于缺乏直接结构，基于图的存储系统不稳定且复杂。Move 验证器始终是严格的，即使在存在不受信任的代码的情况下也能发挥这一作用。它可以防止黑客进行多次操作，这些操作可能会导致多个节点崩溃并控制整个帐户余额，这通常被称为重入攻击。

5. 形式化验证：Move 旨在将形式化验证直接集成到其开发过程中。形式化验证使用数学方法来证明代码的正确性，确保智能合约按预期运行。它通过一些根本性的改进来实现这一点

   1. Prover 工具： “Move Prover” 专为在 Move 代码上执行形式化验证而设计。该工具将 Move 字节码转换为逻辑规范，然后由后端求解器检查这些规范，以确保代码符合其规范，确保开发人员可以了解谁在访问智能合约、何时访问以及他们访问的原因。

   2. 行为规范： Move 允许开发者直接在 Move 代码中编写形式规范，与实现一起。这些规范以高级的、声明式的方式表达，允许开发者定义预期的行为、不变量、后置条件和前置条件。从本质上讲，开发者可以指定谁有权访问模块、他们何时有权访问以及他们为什么有权访问。

   3. 丰富的标准库： Move 标准库提供了处理 MOVE token（嘘，剧透）等核心功能，经过广泛的指定和形式化验证，以确保正确性。

   4. 模块化验证： Move Prover 执行模块化验证。这意味着它独立于调用者验证每个函数和过程。这有助于降低验证过程的复杂性，并确保代码的每个部分都是正确的。

   5. Boogie 中间语言： Move Prover 使用 Boogie 语言将 Move 字节码转换为中间表示。Boogie 是一种中间验证语言，它充当高级语言和定理求解器之间的抽象层。这种转换有助于与 Z3 等后端求解器交互，以证明代码的正确性。

   6. 后端求解器： 转换为 Boogie 后，Move Prover 使用 Z3 等强大的定理求解器来检查规范的正确性与转换后的代码。如果求解器发现规范与代码行为之间存在差异，则表明代码中存在潜在错误。

   7. 不变量维护： Move 中形式化验证的一个关键方面是维护不变量，特别是对于资源类型。不变量是在整个代码执行过程中始终成立的条件。通过指定和检查这些不变量，Move 确保像 token 这样的资源得到安全和正确的处理。

Move Prover 概述，由 Ottersec 提供

未来

随着 Move 等前沿框架的兴起，问题围绕着采用展开。我们如何将 Move 带到传统的 EVM 社区，在那里它可以被无缝采用（甚至可以被抽象化）？想象一下，Curve 可以在 SDK 上启动，并且具有内置的证明器和线性逻辑，以防止重入错误。或者，任何面临吞吐量瓶颈的现有 Solidity 游戏都可以无缝地利用并行执行来随意利用 16 万以上的 TPS。我很荣幸能在 Movement Labs 与一个杰出的团队合作，实现这一现实，并使 MoveVM 成为智能合约部署的标准。

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