【Libra 技术解读】详解move语法、解释器和介绍器

发布时间:2019-06-24          作者:超哥


 

本文将主要介绍:

move语法、解释器和验证器

快搬好小板凳来听课咯!

 

move语法

白皮书使用了一种半形式化(semi-formal)的描述语言进行了描叙。至于这套描述语言,主要符号解释如下:

  • =: 定义

  • ::= : 赋值

  • ⇀: 映射

  • ×: product type,也就是表示结构体

  • ∈: 表示属于某个类型或者集合中的一个元素

通过这些符号,Move定义了如下的语法类型:

Global state: 地址到账户的map,账户由Resource和Module构成。形式化定义如下:


Modules:由名字,结构体声明以及过程声明组成, 可以简单理解为c++的class。module通过ModuleId被外部索引(访问),结构体通过structId被外部索引,结构体声明是一个<kind, FieldName->非引用类型>的product类型。


Module定义了资源的作用域,类似于c++的namespace的功能。其中Module内置了几个重要的函数用来进行类型操作:

  • Pack and Unpack 用于从非受限类型创建和销毁模块的资源;

  • MoveToSender/MoveFrom 在当前账户地址下面发布或者删除对应的资源;

  • BorrowField :获得结构体的一个字段的引用

Types: 包含基本类型(bytes是fixed-size字符串,AccountAddress是256bits),结构体类型,非引用类型,以及


在Module里面除去被声明为资源的类型(标记了resource kind),其余的类型统称为unrestricted types(不受限类型)。资源类型的变量或者字段只能被move,并且资源类型变量的引用不能被解引用,也不能被重复赋值。另外an unrestricted struct不能包含restricted field,原因很简单, unrestricted 结构体被赋值或者复制的时候,如果有restricted字段,那这个字段不会实际被操作到。

Values:


Move支持引用,引用是短暂的,因此不能被用来定义结构体的字段,也不能引用引用,应用的声明周期就是交易脚本的执行过程。通过Borrow{Loc, Field, Global}可以分别可以获得局部变量,结构体变量或者全局变量的引用(敲黑板,请学习rust)。

另外因为struct里不能存储reference,所以可以保证struct一定是一个tree而不会有backedge。这也是move比rust简化的最重要的一点,正因此move不需要复杂的lifetime。 因此Resource同样也不可能出现图结构。这样确实大大简化了语言的处理。

Procedures and transaction scripts:


过程的签名包含函数的访问控制修饰符,参数类型和返回值类型。过程声明包括一个过程签名,局部变量和一系列的指令,(作者认为,这个声明理解为定义(definition)更合适一些)。一个交易脚本是一个不关联具体module的过程,因此他不会被复用,交易脚本操作的全局状态转换,这些状态的修改要么全部成功,要么全部失败。

ProcedureID标识一个过程,被moduleId和过程签名唯一确定,并且Call指定将其作为第一个参数,进行调用。这也就意味着函数调用是静态可确定(staticly determined)的,不存在什么函数指针或者函数表。同时模块内的过程依赖是无环的,加上模块本身的没有动态指派,这样就加强了执行期间的函数调用的不可变性:也就是一个procedure在执行过程的call frame必然是相邻的。因此也防止了类似于以太坊里面的re-entrancy攻击(这个就是有名导致分叉出ETC的攻击)。

 

move解释器

Move的字节码指令在一个栈式的解释器进行执行,栈式虚拟机的好处是易于实现和控制,对硬件环境的要求较少,非常适合区块链场景。同时文中也提到,相对寄存器式的解释器, 栈式解释器在不同的变量之间进行copy和move更容易控制和检测。

解释器的定义如下:


解释器由一个Value Stack,Call Stack以及全局变量引用计数器和一个GasUnits(类似以太坊的Gas Limits)组成。CallStackFrame包含了一个过程执行的所有上下文信息以及指令编号(指令会被唯一编码,减少代码体积,常规处理方法)。Locals是一个变量名到运行时候的Value的map。

字节码解释器支持过程调用(废话啊)。当在一个过程中执行Call指令调用其他的过程的时候,会创建一个新的CallStackFrame对象,然后将对应的调用参数存储到Locals上面,最后解释器开始以此执行新的合约的指令。执行过程遇到分支指令的时候,会在本过程内部(也就是Basic Block之前的跳转)发生一个静态跳转,所谓静态跳转实际上是指跳转的offset是事先已经确定好的,不会像evm一样动态跳转。这也就是之前提到的no dynamic dispath。最后调用return结束调用,同时返回值放在栈顶。

Gas衡量的思路跟EVM是一样的,每个指令有对应的Gas Units,执行一次,减去对应指令的Gas消耗,直到减到0或者所有指令执行完成。

Move的指令包括6大类:

  • 变量操作: CopyLoc/MoveLoc实现数据从本地变量到栈的拷贝和移动,StoreLoc是讲数据存回来到本地

  • 常量/数值/逻辑操作

  • Pack/Unpack/MoveToSender/MoveFrom/BorrowField 等资源操作,具体的解释可以看前一篇文章

  • 引用相关的指令,包括ReadRef/WriteRef/ReleaseRef/FreezeRef, 其中FreezeRef转换一个可变引用到一个不可变引用

  • 控制流结构,包括call和return,branch,BranchIfTrue,BranchIfFalse等

  • 区块链特定的操作,包括获得交易脚本的sender或者创建一个账号等指令。

详细的指令列表在白皮书的Appendix A已经列出。

 

Bytecode验证器

验证器我们在很多编译器里面都能看到,例如普遍使用的SMT证明器Z3. 验证器的核心功能就是在编译阶段保证语言(合约)的安全特性能够得到满足和增强。验证器静态验证是合约脚本发布的必经步骤。

验证器的状态如下:


对于一段可能包含多个module的交易脚本,进行验证,验证结果返回ok,或者各种不满足条件的报错。

Move的模块的二进制格式里面编码了一系列实体的集合,这些实体都放在一个table里面, 包括常量,类型签,结构体定义以及过程定义。检测过程主要有三类:

  • 结构体合法检查: 保证字节码的table的完整性(well-formed), 检测的错误非法的table index, 重复的资源实体以及非法的类型签名,例如引用了一个引用等

  • 过程定义的语义检测:包括参数类型错误,悬垂索引以及资源重复定义。

  • 链接时错误,非法调用内部过程,或者链接一个声明和定义不匹配的流程。

下面重点解释下语义检测和链接时错误检测。

Control-flow graph construction

验证器会首先创建一个bytescode的BasicBlock的控制流图,一个BasicBlock可以理解为中途没有分支指令的指令块。

Stack balance checking

检测栈里面被调用者的访问范围,保证合约的被调用者不能访问到调用者的栈空间。例如一个过程被执行的时候,调用者首先在CallStackFrame里面初始化局部变量,然后将局部变量放入到栈里面,假设当前栈的高度是n,那么有效的bytecode必须满足不变性: 当到达basic block的结束的时候,栈的高度依然还是n。验证器主要是通过分析每个基本块的指令对栈的可能影响,保证不操作高度低于n的栈空间。这里有一个例外就是,一个以return结尾的block,他退出的时候高度必须是n+m,其中m是过程返回值的个数。(这个特殊的操作有点匪夷所思,难道是把栈的高度默认放在了过程的第一个参数,退出的时候这样可以进一步的进行检测?后面确认了,确实是因为目前不支持多返回值,所以才加在一起)。

Type checking

在二进制格式里面,局部变量的类型是定义好的,但是栈的value确实需要推导的。在每个基本快这种推导和类型检测独立执行的,因为前面保证了调用过程访问的栈的高度是合法的,因此,这个时候就能安全的推导栈里面变量的类型了。具体检测就是给Value Stack维护了一个对应的Type Stack,执行的时候TypeStack也跟这指令执行进行pop和push。

Kind checking

kind和type的区别是type可能包含别名。 kind的检查主要检资源是满足

  • 不可双花

  • 不可销毁

  • 必有归属(返回值必须被接受)

对于非资源类型的话,就没有这些限制了。

reference checking

引用的语法包括可变引用,不可变引用。所以引用检测结合了动态和静态分析。 静态分析利用类似rust类型系统的borrow checking机制,保证:1. 所以引用必须指向的是一个已经被分配的存储上,防止悬空; 2. 所有的引用都有安全的读写权限,引用访问既可以共享,也可以排斥(也就是有限的读写权限)。

为了保证2点, BorrowGlobal调用的时候会动态的对全局变量的引用进行了计数, 解释器会对每个发布了的资源进行判断,如果被borrow或者move了,再次引用就会报错。

Linking with global state

链接的时候还需要对链接的对象和声明是否匹配,过程的访问控制等做再次的检查。

 

以上就是目前Move的大部分的静态验证了。可以看到每个流程都有非常严格的分析和限制,最大程度的保证Resouce的安全转移和访问。

 

最后将虚拟机所有的状态和转移总结如下:

Move虚拟机通过执行区块交易里面的脚本实现全局状态Σ的转移。E表示交易脚本产生的针对某个账户的状态修改集(可以理解为XuperChain的读写集):

虚拟机会顺序执行区块的每个交易,产生一系列的E,并且前一个E在后面交易执行的时候是生效的。

当前vm是串行执行交易,然后产生一系列的读写集。 但是Move在设计的时候,已经考虑到了预测执行产生读写集,然后合并的时候根据资源的access path(可以对比与XuperChain的读写集版本)进行冲突检测来解决冲突。。

最后将讲到了未来的规划,重点还是完善类型系统,提供更多类库支持。

这个白皮书分享系列到此为止,可以整体可以看到,Move通过借助logic type,module。 system在资源的转移控制上面做了大量的静态检测来保证资产转移的安全,相对EVM来说,避免了很多问题,Libra主网上线之后,在DeFi领域可能应该会对以太坊的DeFi Dapp造成不小的冲击。