#参考 #指令 #字节码 #堆栈 #验证器 #分析 #签名

已删除 mv-bytecode-verifier

Move字节码验证器

0.1.0 2022年5月22日

#43#验证器

Apache-2.0

1MB
18K SLoC


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

概述

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

编译模块中每个函数的主体在信任模块中函数签名正确性的同时单独进行验证。检查每个函数签名是否与定义匹配是一个单独的责任。函数的主体是一系列字节码指令。此指令序列在以下几个阶段进行检查。

控制流图构建

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

堆栈安全性

块的执行在堆栈和局部变量数组的环境中发生。函数的参数是局部变量数组的开头。参数通过堆栈在函数调用之间传递。当一个函数开始执行时,其参数已经加载到其参数中。假设函数开始执行时的堆栈高度为 n;那么有效的字节码必须强制执行一个不变量,即当执行落在基本块的开头时,堆栈高度为 n。此外,在返回指令时,堆栈高度必须是 n+k,其中 k,s.t. k>=0 是返回值的数量。分析的第一阶段通过单独分析每个块,计算块中每个指令对堆栈高度的影响,检查高度不会低于 n,并且块结束时留在了 nn+k(取决于块的最后一个指令和函数的返回类型)来检查此不变量是否得到维持。

类型安全性

分析的第二阶段检查每个操作(无论是原始操作还是定义好的函数)是否使用了适当类型的参数。操作的操作数位于局部变量或栈上。函数的局部变量类型已经在字节码中提供。然而,栈上值的类型需要推断。这种推断和每个操作的类型检查可以针对每个代码块单独进行。由于每个代码块开始时的栈高度是 n,并且在代码块执行过程中不会低于 n,所以我们只需要为类型检查代码块的指令建模从 n 开始的栈后缀。我们使用一个类型栈来建模这个后缀,其中类型在处理代码块中的指令流时被推入和弹出。只需要类型栈和局部变量的静态已知类型来检查每个指令。

资源安全

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

  • CopyLocStLoc 要求局部变量的类型不是资源类型。
  • WriteRefEqNeq 要求引用的类型不是资源类型。
  • 在函数结束时(当达到 Ret 时),没有类型为资源类型的局部变量可以空,即值必须已从局部变量中移出。

如上所述,围绕 Ret 的最后一条规则意味着资源 必须 已经

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

MoveToUnpack 都在声明资源的模块内部。

引用安全

在字节码语言中,引用是一等公民。新引用以多种方式对函数可用

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

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

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

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

  • 如果 r1 被标记为独占,则它必须是不可激活的,即无法到达引用 r1 被取消引用或修改的控制位置。
  • 如果 r1 是共享的,则 r2 也是共享的。

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

分析设置

引用安全分析被设置为流分析(或抽象解释)。为基本块的代码抽象执行定义了一个抽象状态。维护一个从基本块到抽象状态映射。给定一个基本块 B 开始时的抽象状态 SB 的抽象执行导致状态 S'。此状态 S' 被传播到 B 的所有后继,并在映射中记录。如果已经为块存在状态,则新生成的传播状态与现有状态“合并”。如果合并失败,则报告错误。如果合并成功但抽象状态保持不变,则不再进行进一步传播。否则,状态被更新并再次通过块传播。在通过块传播抽象状态时处理指令时,也可能报告错误。

错误。 如前所述,检查器在以下情况之一中报告错误

  • 无法证明指令在通过块传播抽象状态时是安全的。
  • 通过不同传入边传播到块中的抽象状态的合并失败。

这个模块是如何组织的?

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

依赖项

~4MB
~67K SLoC