精确定义 Smart Contract— Solidity的语意正规化 - 区块链技术 - BitMere

Solidity 作为一个程序语言，写出来的Smart Contract 就跟所有程序一样，有时候会有 Bug。然而 Smart Contract 上的 Bug 很可能比一般程序中的 Bug 还要严重，因为一旦放到链上就再也无法被修改了，最知名的莫过于 DAO attack。于是有人将脑筋动到另一个依然还未被广泛应用的领域上——正规验证（Formal Verificatinon，也有人称为形式化验证）
本篇文章介绍的内容则是正规验证前必须的工作，即定义一个语言的语意（semantics）。在一个语言中，一个语句的语义指的是这段指令所代表的「意思」。看到这大家可能会有个疑惑，为什么一个指令的意思需要另外定义？不是全部都写在规格书跟编译程序里了吗？原因是，就算是写在规格中的语法，其真正的意思也时常是没被精确定义的，如果仅是写在规格书中，那一个指令结束后，整个计算机的状态（在 EVM 可以指整个 Ethereum 的 Global State）常是无法被确定的，必须了解编译行为、以及编译后的 bytecode 才能了解会发生什么事。然而一个好的程序语言，应该让程序设计师只看高阶的程序代码就能判断会及不会发生什么行为。
什么是正规语意？以伪码与 Hoare Logic 为例
一个典型用 Hoare Logic 进行分析的程序会具有三元的结构 {P}C{Q}，不严谨的解释是对于一个程序 C，其执行前的状态 P （前件）会在执行后变成状态 Q（后件）。状态 P,Q 都是由命题构成集合。
我们先看一句简单的指令：
x := x+1
这个指令做的事很简单，「将 x 加上 1 后赋值给自己」。但在撰写程序时我们其实是对这个指令执行前与执行后会发生的事已经在脑内有许多的预设了，才会写下这样的程序。而 Hoare Logic 正是将这些脑内的预设写下来。例如，若我在写下这行程序时，我确信执行前的 x 的值为 42，那在一个语法没有其他作用的程序语言中，这行程序执行完 x 的值会变为 43。在Hoare Logic 中可以写成 {x=42}x := x+1{x=43}。
我们再看另一行程序
y := x
若在写这行程序时我们已经想好 x 的值会是 43，那执行完 y 应当要是 43。写成 Hoare Logic 便是 {x=43}y := x{y=43}。
当我们发现第一个程序的后件与第二个程序的前件相同，便能将上面两行程序连接起来，而变成 {x=42}x := x+1; y := x{y=43}。
从而在写一个程序时，我们若总是在每个小程序前后加上前件与后件（P 与 Q），最后在将所有程序组合起来时，就能确切知道这个程序在给定一个执行前的状态下，执行后必然会发生什么事。
在设计一个语言时，若我们所有最基本的单元操作的前后件都写出来，那就可以想象我们能设计一套工具去判断整个程序执行前后一定会发生的事，而不会有如 C 语言中的 undefined behavior 或需要看 bytecode 才能确定的行为。
MatchingLogic 与 K-framework
K Framework 是一个用来定义程序语言的工具，其运用的是Hoare Logic 的延伸—— Matching Logic。在 K Framework 中，定义一个语言需要三个基本的组件：语法（syntax）、配置（configuration）与规则（rule）。
定义程序语法用的（K 的）语法是 BNF，若写过 functional 语言或读过计算理论的人可能会很熟悉，简单来说就是将一个语言中的所有可能出现的语法以递归的方式定义清楚，以这篇论文中定义 Solidity 的语法方式为例子：
K := uintm | address | K[n]
T := uintm | address | T[n] | T[] | mapping K T| ?T???T? | contract | ref T
这部分只列出所有 Solidity 可能出现的型别，若要完整定义语言还需列出如 contract、pragma 等关键词。
而 Solidity 写成 K Framework 的语法实在太长了，这里就先以一个官网范例中简单的语言 IMP 为例子（简写自 imperative，相对于 declarative 语言。其实定义纯 functional 的 declarative 语言相对简单，也是官方提供的第一个范例，但读者应该更熟悉如 Solidity 或 C 等imperative 语言因此也用此举例）
IMP 以 K Framework 定义的 Syntax 如下

由此可以看出，对于任何一个指令 Stmt，他都必需是 Stmt 所定义的形式中其中一种。如 while(1){x=1+1;} 是合法的Stmt，因为他符合 “while”"(" BExp “)” Block 的形式，而这是因为 while 中的 1 符合BExp 的形式，而且 x=1+1 符合Stmt 中 Id"=" AExp “;” 的形式，因为 1+1 符合 AExp … 依此类推。
而配置（configuration）则是将语言执行中会用到或改变的状态（state）写下来，这些配置可以是内存、计数器等。如果是完全没有副作用的语言那可能不需要定义这种状态（完全不需要输入输出的 declarative 语言可能就用不到，如K Framework 在 tutorial 中定义的小语言LAMBDA）。然而一般实务上使用的语言一定用到外部的状态，状态也能称为环境（enviroment），可以理解为从语言中看不出来，但在执行时会用到与造成影响的对象。
如在 C 中直接修改内存的操作，虽然语法上只是一个指令（指令执行的结果在后续程序中拿来使用），但实际上对「内存」这个状态造成了影响。以 Solidity 来说实体的state 就是 Storage 与Memory。真正需要定义的 state 其实细分非常多，如Type Space（从变量名称到 Type 的对应关系）、NameSpace（变量名称到内存位置的对应关系）、Storage 与Memory（从内存位置对应到其上的值）等。
配置可以是巢状的，也就是说一个配置中可以包含其他配置。例如一个 thread 中有一个 stack，一支程序可以有好几个 thread，就用得到这样的配置。
IMP 中的 configuration 长这样：

与庞大的语言比起来这是非常简单的 configuration。语法是 XML，一个 configuration 的空间称为一个 cell，这里有两个 cell，k 与 state。k 里面放的是程序代码本身，而state 则储存了如变量等需要记录的状态。T 可以暂时不理会。$PGM 是 KFramework 的变量，意思是程序代码要放在这个 cell 中（程序代码也是环境的一部分！如在 C 中程序代码也是 data 的一部分，甚至能写出能读写自己的程序代码区块的程序），:Pgm 说明这个程序代码同时必须是符合 Syntax 中定义好的 Pgm 的形式才行。
configurations 也定义好后，就要写规则。规则就是最重要的「程序如何执行」的原则。在 K Framework 定义的语言中，一行指令会做出什么操作，一定要是明确写出的一条规则才行，否则就会无法执行。一条规则的形式是「可被执行的程序」加上其「被执行成的结果」，另外能加上附加条件以及其会对环境（配置）造成的影响。如现在有条简单的规则：
rule while (B) S => if (B) {S while (B) S} else {}
这条规则是在说明，任何符合 while (B) S 形式的语法都能执行为 if (B) {Swhile (B) S} else {}。=>这个动作可以称为重写（Rewrite），因为这规则的意思其实就是「将左边的程序重写成右边的程序」，再将重写后的程序继续依照其他规则执行（重写）下去。
再看另一条规则：
rule X = I:Int; => . … … X |-> (_ => I) …
这条规则是在说，在 k 这个 configuration 中，当出现 X=I 形式时（I 必须为 Int），其会被重写为什么都没有（. 在 K Framework 中是 nothing 的意思）。在中开头没有 …，结尾却有，意思是若要使用这条规则，X=I 的形式必须出现在程序的开头。而state 中 X 所对应到的值会被取代为 I。（|-> 是变量名称与值的对应关系，_ 是本来所对应到的值，但因为不需要用到本来的值所以用 _）
到这边为止应该可以看出，规则跟上面讲的 Hoare Logic 其实非常像！只是我们将前件后件写成了 Rewrite 的规则，{P}S{Q} 被转换成了 S∧P ? T∧Q 这样的形式（T 是 Rewrite 后的程序代码）。
K-framework中被正规化的 Solidity
写了这么多，这篇跟本还没讲和 Solidity 有关的内容。的确，光是介绍 K Framework 就花了很多功夫，在开头提及的论文中，南洋理工与新加坡科技设计大学的人将 Solidity 的基本语意实作在 K Framework 中，写了 50 个configuration 以及 200多条 rule（2000+ 行），目前已经可以在 KFramework 中执行。在执行过程中，我们就能做动态的测试，判断 cell 中会不会出现预期以外的值。
我们就看其中一条简单的 rule。

（注意这里的水平分隔上下就是?的左右）
Elementary-TypeName 这条规则中，pcsContractPart 是一个定义在 K Framework 的函数，会被展开为一个可以被重写的形式。（在中的）程序代码若是符合一个变量宣告的形式，contract cell 中的许许多多配置就能够方式如上的操作。以 uint public data = 10; 为例，uint 可以代入 X（ElementaryTypeName）、public 代入 Y（Specifiers）、data 代入 Z（Id），10 代入 E。当出现符合这样规则的程序后，这行指令的下一步可以被「重写」为什么都不剩（.K，「.」开头为 nothing 的意思）。同时，在这个程序执行时的状态，也就是configuration 中：
cname（合约名称）必须有符号 C。
vname （记录变量数量）中的数字 N 会增加 1。
vId （记录第 N 个变量的变量名称）会多出一条 N 到 Z 的对应。
variables （从变量名称到变量地址的对应）会多一个 Z 到 !Num 的对应，!Num 是告诉 K 产生一个新的数字作为地址。
typename （记录从变量名称到 Type 的对应）多一条 Z 到 X 的对应。
cstore （记录从地址到值的对应）多一条 !Num 到 E 的对应。
需要注意的是，每个 cell 中的前件都要成立，这个规则才适用。如果前件为 nothing（「.」开头），那就代表这个 cell 没有前件。例如，若 contract cell 中没有 C 这个合约名称，这条规则就不能被使用。如果一行指令没有任何规则能被套用，程序就会执行不下去。
结语
语意正规化后，离正规验证其实还有段距离。若我们想要验证一个程序的正确性，我们得先将我们所认为的「正确」的条件（specification）给列出来。例如，在一个扣款的合约中，钱包被扣除的数字必须只能有一次，我们就能另外写程序检查在存有钱包金额的那个 cell 中，是不是一定只会减少某个数字。但这样的程序要怎么写又是另一个大工程，其中牵扯到将 Matching Logic 转换成可以被验证的逻辑模型等问题。已经有人将 EVM 实作在 KFramework 中（注意不是 Solidity，在计算理论中，要描述一个完整的程序语言与描述一台电脑是等价的，EVM 同理也能以 K Framework 描述），并配合 Z3 证明器写了用来证明 Smart Contract 的工具，里面附有一些已经证明好的 Smart Contract 与他们的 specification，有兴趣的人可以了解一下。