Lib.rs

id: bytecode-verifier title: 字节码验证器 custom_edit_url: https://github.com/move-language/move/edit/main/language/move-bytecode-verifier/README.md

概述

字节码验证器包含一个静态分析工具，用于拒绝无效的Move字节码。它检查栈使用、类型、资源和引用的安全性。

在信任模块中函数签名正确性的同时，分别验证编译模块中每个函数的正文。检查每个函数签名是否与其定义匹配是另一个责任。函数的正文是一系列字节码指令。以下阶段检查这一指令序列。

控制流图构建

通过将指令序列分解为基本块的集合来构建控制流图。每个基本块包含一系列连续的指令；所有指令被分配到各个块中。每个块以分支或返回指令结束。将分解为块保证了分支目标仅落在某些块的开始处。分解还试图确保生成的块是最大的。然而，分析的正确性并不依赖于最大性。

栈安全性

代码块的执行是在栈和局部变量数组的环境中进行的。函数的参数是局部变量数组的开头。参数和返回值通过栈在函数调用之间传递。当一个函数开始执行时，其参数已经加载到其参数中。假设当函数开始执行时栈的高度为 n，那么有效的字节码必须强制执行以下不变性：当执行到达基本块的开始时，栈高度为 n。此外，在返回指令中，栈高度必须是 n+k，其中 k（满足 k>=0）是返回值的数量。分析的第一阶段通过分别分析每个块、计算块中每条指令对栈高度的影响、检查高度不会低于 n，并在块结束时留在 n 或 n+k（取决于块的最终指令和函数的返回类型）来检查这个不变性。

类型安全

分析的第二阶段检查每个操作（原始或定义的函数）是否使用适当的参数调用。操作的运算符位于局部变量或栈中的值。函数的局部变量类型已在字节码中提供。然而，栈值的类型是推断出来的。这种推断和每个操作的类型检查可以针对每个块分别进行。由于每个块开始时的栈高度为 n，并且在块执行过程中不会低于 n，我们只需要为类型检查块指令的栈后缀（从 n 开始）建模。我们使用类型栈来模拟这个后缀，类型在处理块中的指令流时被推入和弹出。我们只需要类型栈和局部变量的静态已知类型来类型检查每条指令。

资源安全

资源代表区块链的资产。因此，对这些类型有一些限制，这些限制不适用于普通值。直观地说，资源值不能被复制，必须在交易结束时使用（这意味着它们被移动到全局存储或销毁）。具体来说，以下限制适用：

• CopyLoc 和 StLoc 要求局部变量的类型不是资源类型。
• WriteRef、Eq 和 Neq 要求引用的类型不是资源类型。
• 在函数结束时（当到达 Ret 时），没有类型的局部变量是空的，即值必须已从局部变量中移出。

如上所述，这条关于 Ret 的最后规则意味着资源 必须 已经被

• 通过 MoveTo 移动到全局存储。
• 通过 Unpack 销毁。

这两个 MoveTo 和 Unpack 都在声明资源的模块内部。

引用安全

引用在字节码语言中是一等公民。新鲜引用可以通过多种方式使函数可用：

• 输入参数。
• 从局部变量中的值的地址。
• 从地址中的全局发布值的地址。
• 从一个包含结构的引用中获取字段的地址。
• 从函数返回值。

引用安全检查的目的是确保没有悬垂引用。以下是一些悬垂引用的例子

• 局部变量 y 包含了对局部变量 x 中值的引用；然后 x 被移动。
• 局部变量 y 包含了对局部变量 x 中值的引用；然后 x 绑定到新的值。
• 引用了一个尚未初始化的局部变量。
• 从函数中返回局部变量中的值引用。
• 引用 r 是对全局发布值 v 的引用；然后 v 被取消发布。

引用可以是独占的或共享的；后者允许只读访问。引用安全性检查的次要目标是确保在字节码程序的执行上下文中，包括整个评估堆栈和所有函数帧，如果存在两个包含引用的不同的存储位置 r1 和 r2，使得 r2 扩展 r1，则以下两个条件都成立

• 如果 r1 被标记为独占的，则它必须是无效的，即无法到达一个控制位置，其中 r1 被解引用或修改。
• 如果 r1 是共享的，则 r2 也是共享的。

上述两个条件建立了引用透明性的属性，这对于可扩展的程序验证很重要，其大致形式如下：考虑以下代码片段 v1 = *r; S; v2 = *r，其中 S 是一个任意的计算，它不通过语法引用 r 执行任何写入（并且不对任何扩展 r 的 r' 执行写入）。然后 v1 == v2。

*
├── invalid-mutations  # Library used by proptests
├── src                # Core bytecode verifier files
├── tests              # Proptests