Skip to content

Latest commit

 

History

History
195 lines (122 loc) · 14.5 KB

4-2-2-字节码验证器.md

File metadata and controls

195 lines (122 loc) · 14.5 KB
Raw

字节码验证器

原文链接：https://developers.libra.org/docs/crates/bytecode-verifier
译者：humyna
日期：2019.09.23
版权及转载声明：本文采用知识共享署名-非商业性使用-禁止演绎 4.0 国际许可协议进行许可。

概述

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

已编译的模块中每个函数体各自被单独验证，同时信任模块中函数签名的正确性。检查每个函数签名与其定义是否匹配是一项单独的职责。一个函数体是一系列字节码指令。这个指令序列在下面描述的几个阶段中检查。

CFG施工

通过将指令序列分解为一组基本块来构造控制流图。每个基本块包含一个连续的指令序列；所有指令集在块之间进行分区。每个块以分支或return指令结束。分解成块保证分支目标落在某个块的开始处。分解还试图确保生成的块是最大的。然而，分析的完整性soundness并不取决于极大性。

堆栈安全

块的执行发生在局部变量数组和堆栈的上下文中。函数的参数是局部变量数组的前缀。跨函数调用传递参数和返回值都是通过堆栈完成的。当函数开始执行时，其参数arguments已经加载到其参数parameters中。假设函数开始执行时堆栈高度为_n_;那么有效的字节码必须强制执行执行器落在基本块开始处堆栈高度为n的不变量。此外，在return指令处，堆栈高度必须是_n_ + k，其中_k_，s.t.k>= 0是返回值的数量。分析的第一阶段检查通过分别分析每个块、计算块中的每个指令对堆栈高度的影响、检查高度是否不低于n来检查是否维护了这个不变量，在n或n+k处（依赖块的最终指令和函数的返回类型）保留在块的末尾。

类型安全

分析的第二阶段检查是否使用适当类型的参数调用每个操作（原语或定义的函数）。操作数是位于局部变量或堆栈上的值。字节码中已提供函数的局部变量类型。但是，堆栈值的类型将被推断。该推断和每个操作的类型检查可以分别对每个块完成。由于每个块开始处的堆栈高度是n，并且在块执行期间不会低于n，因此我们只需要对从n开始的堆栈后缀建模，以便对块指令进行类型检查。我们使用一个类型堆栈来建模这个后缀，当块中的指令流被处理时，类型会被压入和弹出。只有类型堆栈和局部变量的已知静态类型才需要对每个指令进行类型检查。

资源安全

资源代表区块链上的资产。 因此，对这些类型存在某些限制，这些限制不适用于正常值。 直观地说，资源值无法复制，必须在交易结束时使用（这意味着他们能全局存储中转移或被销毁）。 具体而言，存在以下限制：

  • CopyLoc 和 StLoc 要求本地类型不是资源类型。
  • WriteRef, Eq, 和 Neq 要求引用的类型不属于资源类型。
  • 在函数结束时 (到达 Ret的时候), 任何类型为资源类型的局部变量都不能为空，即该值必须已从本地移出。

如上面提到的，围绕 Ret 的最后一条规则意味着资源必须是：

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

MoveToSender 和 Unpack 都位于声明资源的模块内部。

引用安全

引用在字节码语言中是一等的first-class。函数可以通过以下几种方式获得新的引用:

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

引用安全性检查的目的是确保没有空引用。下面是空引用的一些例子:

  • 局部变量 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 。

设置分析

引用安全分析设置为流分析（或抽象解释）。为抽象地执行基本块的代码定义了一个抽象状态。维护一个从基本块到抽象状态的映射。如果在基本块B的开头有一个抽象状态S，B的抽象执行将导致状态S’。此状态s'将传播到b的所有继承者，并记录在映射中。如果一个块已经存在一个状态，则新传播的状态“连接”到现有状态。如果连接失败，将报告错误。如果连接成功，但抽象状态保持不变，则不会进行进一步传播。否则，状态将被更新并通过块再次传播。在抽象状态通过块传播期间处理指令时，也可能报告错误。

抽象状态. 

抽象状态有三个组件：

  • 从局部变量到抽象值的部分映射。不在此映射范围内的局部变量不可用。可用性是被初始化的概念的概括。由于被移动，局部变量在初始化之后可能变得不可用。抽象值是 应用_Reference_(n)（对于引用类型的变量）或值 Value(ns)（对于值类型的变量），其中_n_是nonce， _ns_是一组nonces。nonce是一个常量，用于表示引用。设 Nonce 表示所有nonce的集合。如果局部变量 l 映射到 Value(ns)，则意味着有未完成的引用指向存储在 l 中的值。对于 ns 中的每个成员 n，必须有一个局部变量 l 映射到 Reference(n)。如果局部变量 x 映射到 Reference(n)并且局部变量 y 和 z 分别映射到 Value(ns1)和 Value(ns2) ，那么 n 可能是 ns1 和 ns2 的成员。这仅仅意味着分析是有损的。 l 映射到 Value（{}）时的特殊情况意味着没有对 l 的引用，因此 l 可能被销毁或移动。
  • 局部变量到抽象值的部分映射本身并不足以检查字节码程序，因为字节码所处理的值可以是大的嵌套结构，其有指向值中间的引用。可以扩展指向值中间的引用以生成另一个引用。应该允许一些扩展，但其他扩展不应该被允许。为了跟踪引用之间的相对扩展，抽象状态有第二个组件。此组件是从nonce到以下两种借用信息之一的映射：
    • 一组nonces 【humyna注：此处原文格式错误】
    • 字段集到nonces集nonces的映射

当前实现将此信息存储为具有不相交域的两个单独的映射：

  • 从 Nonce 到 Set <Nonce>的映射_borrowed_by_ 
  • 从_Nonce _到 Map<Field，Set<Nonce>> 的映射 fields_borrowed_by
    • 如果 n2 在 borrowed_by [n1]，则表示由 n2 表示的引用是由 n1 表示的引用的扩展名。
    • 如果_n2 _在 fields_borrowed_by [n1][f] 中 ，则由 n2 表示的引用是由 n1 表示的引用的扩展f的扩展。 基于这一直觉，通过采用对应于 fields_borrowed_by[n] 域中所有字段的所有nonce集的并集，将一个 nonce n 从 fields_borrowed_by 的域移动到 borrowed_by 的域是一个合理的过度近似。
  • 要在块中的指令之间传播抽象状态，还必须对堆栈上的值和引用进行建模。我们之前已经描述了如何将可用的堆栈后缀建模为类型堆栈。我们现在将此堆栈的内容扩充为包含一个类型和一个抽象值的结构。我们维护不变量，即堆栈上的非引用值不能对它们进行挂起。因此，如果堆栈上存在一个抽象值_Value_(ns) ，则ns为空。

值和引用

让我们深入看看值和引用（包括共享和排他的）是如何被建模的。

  • 一个非引用值被建模为 Value(ns)，其中ns是表示借用引用的一组nonce。仅当ns为空时，此值的销毁/移动/复制才被视为安全的。堆栈上的值通常满足此属性，但局部变量中的值可能不满足。
  • 引用被建模为_Reference_(n)，其中 n 是随机数。 如果引用被标记为共享，则始终允许读访问，并且永远不允许写访问。 如果引用 Reference(n) 被标记为独占，则仅当 n 没有借用时才允许写访问，如果从 n 借用的所有随机数驻留在被标记的引用中，则允许读访问和共享。 此外，构造引用的规则保证了引用标记共享的扩展也必须被标记为共享。 这些检查共同提供了前面提到的参考透明性。
  • 一个引用被建模为引用_Reference_(n)，其中n是nonce。如果引用标记为共享，则始终允许读取访问，永不允许写入访问。如果引用 Reference(n) 被标记为排他，则仅当n没有借用时才允许写访问；如果从n借用的所有nonce都位于标记为共享的引用中，则允许读访问。此外，用于构造引用的规则保证标记为共享的引用的扩展也被标记为共享。这些检查共同提供了前面提到的引用透明性的属性。

目前，字节码语言不包含任何用于共享引用的直接构造函数。 BorrowLoc 和 BorrowGlobal 创建排他引用。 BorrowField 创建从源引用继承其标记的引用。Move（当应用于包含引用的局部变量时）将引用从局部变量移动到堆栈。FreezeRef 用于将现有的排他引用转换为共享引用。在将来，我们可能会添加一个生成共享引用的 BorrowGlobal 版本。

**报错。**如前所述，检查人在以下某种情况下报告错误：

  • 在通过块传播抽象状态期间，不能证明指令是安全的。
  • 通过不同传入边传播到块中的抽象状态的联接失败。

让我们深入看看上面错误报告的第二个原因。请注意，表示可用堆栈后缀的类型和抽象值对的堆栈在块的开头是空的。因此，连接只发生在表示可用局部变量和借用信息的抽象状态上。只有当两个边上的可用局部变量集不同时，联接才会失败。如果可用变量集是相同的，则连接本身是简单的——借用集是逐点连接的。不过，有两个微妙之处值得一提：

  • 沿着两条边的抽象状态中使用的一组nonces可能彼此没有任何连接。 由于实际的nonce值并不重要，因此在执行连接之前，将nonces映射到固定整数（包含nonces的局部变量的索引）。
  • 在连接期间，如果一个nonce n 位于一侧的 borrowed_by 域和 另一侧的 fields_borrowed_by 域中，则 n 在执行连接之前从 fields_borrowed_by 移动到 borrowed_by。

借用引用

每个引用构造函数 — BorrowLoc, BorrowField, BorrowGlobal, FreezeRef, 和 CopyLoc — 都是通过生成新的nonce来建模的。 当 BorrowLoc 借用局部变量中的值时，BorrowGlobal 借用了全局值。 BorrowField，FreezeRef 和 CopyLoc （应用于包含引用的本地值）从源引用借用。 由于每个新的nonce与所有以前生成的nonce不同，因此分析保持不变量，即所有可用的局部变量和引用类型的堆栈位置具有表示其抽象值的不同nonce。 另一个重要的不变量是借用信息中引用的每个随机数必须驻留在表示局部变量或堆栈位置的某个抽象值中。

引用释放

全局和局部的引用由 ReleaseRef 操作释放。 从函数的局部变量中返回具有未释放引用的函数值是错误的。 必须显示释放所有引用。 因此，使用 StLoc 操作覆盖可用引用是错误的。

当被操作ReadRef, WriteRef, Eq, Neq, 和 EmitEvent 消费时，引用将隐式释放。

全局引用

全局引用的安全性取决于静态和动态分析的组合。 静态分析不区分全局和本地引用。 但动态分析区分它们并对全局引用执行引用计数，如下所示：字节码解释器将维护一个从一个地址和完全限定的资源类型对到一个 union（Rust枚举）的映射 M ，包含以下值：

  • Empty
  • RefCount(n) 某值n（计数） n >= 0

解释器对以下操作执行额外的状态更新和检查。在下面的代码中，assert失败表名一个程序员的错误，panic失败表明解释器中的内部错误。

MoveFrom(addr) {
    assert M[addr, T] == RefCount(0);
    M[addr, T] := Empty;
}

MoveToSender(addr) {
    assert M[addr, T] == Empty;
    M[addr, T] := RefCount(0);
}

BorrowGlobal(addr) {
    if let RefCount(n) = M[addr, T] then {
        assert n == 0;
        M[addr, T] := RefCount(n+1);
    } else {
        assert false;
    }
}

CopyLoc(ref) {
    if let Global(addr, T) = ref {
        if let RefCount(n) = M[addr, T] then {
            assert n > 0;
            M[addr, T] := RefCount(n+1);
        } else {
            panic false;
        }
    }
}

ReleaseRef(ref) {
    if let Global(addr, T) = ref {
        if let RefCount(n) = M[addr, T] then {
            assert n > 0;
            M[addr, T] := RefCount(n-1);
        } else {
            panic false;
        }
    }
}

上面规则没有说明的一个微妙之处是，当应用于全局引用时，BorrowField 和 FreezeRef 保持引用计数不变。 因为这些指令消耗了堆栈顶部的引用，同时在堆栈顶部生成了它的扩展。 类似地，由于 ReadRef ，WriteRef，Eq，Neq 和 EmitEvent 消费堆栈顶部的引用，它们将引用计数减少1。

模块代码结构

*
├── invalid_mutations  # Library used by proptests
├── src                # Core bytecode verifier files
├── tests              # Proptests