#bytecode #verifier #instructions #run-time #generation #module #generate

已撤回 测试生成

用于生成字节码验证器和Move VM运行时测试的工具

0.3.2 2022年8月23日
0.3.1 2022年8月13日
0.2.1 2022年7月22日
0.1.6 2022年7月5日
0.1.4 2022年5月24日

#42 in #verifier

Apache-2.0

1.5MB
32K SLoC


id: bytecode-test-generation title: 字节码测试生成工具 custom_edit_url: https://github.com/move-language/move/edit/main/language/testing-infra/test-generation/README.md

字节码测试生成工具

概述

此工具可以生成已知有效或已知无效的Move字节码程序。已知有效意味着程序是有效的,因为它根据Move字节码语言的正式规范构建。已知无效的字节码程序是以受控方式偏离规范的。

生成的模块将由Move字节码验证器进行检查,然后在VM运行时上运行。如果模块包含已知有效的字节码,我们应该期望程序将通过字节码验证器。如果它没有通过验证器,这表明字节码验证器中存在错误或失败的指令的正式规范是不正确的。同样,它也应该在VM运行时上成功运行。

如果模块包含已知无效的字节码,我们应该期望验证器将拒绝该模块。如果验证器没有拒绝该模块,这再次表明字节码验证器中存在错误或正式规范是不正确的。同样对于VM运行时。

使用方法

构建和配置

要构建此工具

  • cargobuild

src/config.rs 中有配置选项(以及它们行为的说明)。大多数情况下,这些选项应保留为提供的默认值。

运行

该工具期望最多两个参数

  • --iterations:应生成和测试的程序数量
  • --output:(可选)如果提供,这是导致错误的模块将被序列化并保存的路径。如果没有提供,失败案例将记录到控制台。

此外,还有一个可选的标志 RUST_LOG,用于控制调试信息的详细程度。它从 error(信息最少)到 debug(信息最多)。此标志最常用的设置是 info,它将打印统计信息,如迭代次数、已验证和执行程序的次数等。

要运行工具

  • RUST_LOG=info cargo run-- --iterations N--outputPATH

架构

该工具通过抽象地模拟虚拟机的状态,并按该抽象状态模拟字节码指令来工作。抽象状态定义在 abstact_state.rs 中。它由虚拟机栈、局部变量和借用图的类型级建模组成。

指令是用它们的先决条件和效果来定义的。这些定义在 summaries.rs 中找到,并使用在 transitions.rs 中定义的宏。指令的先决条件是针对给定抽象状态为真或假的谓词。例如,Bytecode::Add 指令要求栈中包含两个整数。这是通过说 Bytecode::Add 的先决条件是

  • state_stack_has!(0, Some(SignatureToken::U64))
  • state_stack_has!(1, Some(SignatureToken::U64)) 来建模的,其中索引 0 和 1 指的是栈的顶部两个元素。

指令的效果描述了指令如何修改抽象状态。对于 Bytecode::Add,效果是执行两个栈弹出操作,并将一个 SignatureToken::U64 推送到栈上。

通过这种方式,我们能够完全捕获每个指令的需求和执行方式。这些信息用于生成有效的字节码程序。

字节码程序的生成按以下步骤进行

  1. lib.rs 中,生成器循环首先初始化一个 ModuleBuilder
  2. ModuleBuilder,定义在 ../utils/src/module_generator.rs 中,生成模块定义
  3. ModuleBuilder 调用在 bytecode_generator.rs 中定义的 generator 来填充模块内的函数体
  4. generatorcontrol_flow_graph.rs 中构建一个控制流图(CFG)。CFG 的每个块都被分配一个有效的起始和结束抽象状态。
  5. generator 根据以下算法填充 CFG 的块
    1. 给定起始抽象状态 AS1,设 candidates 为所有预条件在 AS1 中得到满足的指令列表
      • 如果希望生成无效的指令,则让 x 预条件为 false
    2. 根据栈高度启发式算法从 candidates 中选择候选指令 instr
      • 栈高度启发式算法选择在栈高度较小时增加栈的指令,在栈高度较大时减少栈的指令
    3. instr 的效果应用于 AS1,生成 AS2
    4. 如果栈为空,则终止,否则从步骤 a 重复使用 AS2

这会导致生成一个模块。然后,将模块提交给字节码验证器,并记录字节码验证器的行为(即无验证错误、一些验证错误、恐慌、崩溃)。同样,与 VM 运行时(除了运行时错误而不是验证错误)。根据此工具构建时的配置,如果模块导致验证错误、恐慌或崩溃,则模块将被打印出来或序列化到磁盘。

这将持续到工具调用时指定的迭代次数。

其他文件

  • error.rs 定义了一个错误结构体,用于传递错误信息。
  • tests/ 包含一系列文件,用于测试每个字节码指令的预条件和效果

扩展工具

对这个工具最常见的变化或扩展可能是更改指令的预条件和效果。要执行此操作,请遵循以下步骤

  1. 检查 transitions.rs 中是否已定义一个宏来捕获您想要的预条件/效果
  2. 如果宏已经定义,只需将其添加到 summaries.rs 中要更改的指令的摘要中即可
  3. 如果不存在合适的宏,请在 transitions.rs 中定义它。查看该文件中的其他宏以获取示例。
  4. transitions.rs 中的宏可以访问 AbstractState 的公共字段和函数。如果您的宏需要访问更多内容,请在 abstract_state.rs 中添加一个新的辅助方法,然后在宏中调用它。

依赖关系

~27–41MB
~617K SLoC