什么是Solidity正規(guī)驗(yàn)證

Solidity作為一個(gè)程序語言，寫出來的Smart Contract就跟所有程序一樣，有時(shí)候會(huì)有Bug。然而Smart Contract上的Bug很可能比一般程序中的Bug還要嚴(yán)重，因?yàn)橐坏┓诺芥溕暇驮僖矡o法被修改了，最知名的莫過于DAO attack。于是有人將腦筋動(dòng)到另一個(gè)依然還未被廣泛應(yīng)用的領(lǐng)域上— —正規(guī)驗(yàn)證（Formal Verificatinon，也有人稱為形式化驗(yàn)證）。

本篇文章介紹的內(nèi)容則是正規(guī)驗(yàn)證前必須的工作，即定義一個(gè)語言的語意（semantics）。在一個(gè)語言中，一個(gè)語句的語義指的是這段指令所代表的「意思」。看到這大家可能會(huì)有個(gè)疑惑，為什么一個(gè)指令的意思需要另外定義？不是全部都寫在規(guī)格書跟編譯器里了嗎？原因是，就算是寫在規(guī)格中的語法，其真正的意思也時(shí)常是沒被精確定義的，如果僅是寫在規(guī)格書中，那一個(gè)指令結(jié)束后，整個(gè)電腦的狀態(tài)（在EVM可以指整個(gè)Ethereum的Global State）常是無法被確定的，必須了解編譯行為、以及編譯后的bytecode才能了解會(huì)發(fā)生什么事。然而一個(gè)好的程式語言，應(yīng)該讓程式設(shè)計(jì)師只看高階的程式碼就能判斷會(huì)及不會(huì)發(fā)生什么行為。

什么是正規(guī)語意？以虛擬碼與Hoare Logic 為例

一個(gè)典型用Hoare Logic進(jìn)行分析的程式會(huì)具有三元的結(jié)構(gòu){ P } C { Q }，不嚴(yán)謹(jǐn)?shù)慕忉屖菍?duì)于一個(gè)程式C，其執(zhí)行前的狀態(tài)P（前件）會(huì)在執(zhí)行后變成狀態(tài)Q（后件）。狀態(tài)P ， Q都是由命題構(gòu)成集合。

我們先看一句簡單的指令：x ：= x+1

這個(gè)指令做的事很簡單，「將x加上1后賦值給自己」。但在撰寫程式時(shí)我們其實(shí)是對(duì)這個(gè)指令執(zhí)行前與執(zhí)行后會(huì)發(fā)生的事已經(jīng)在腦內(nèi)有許多的預(yù)設(shè)了，才會(huì)寫下這樣的程式。而Hoare Logic正是將這些腦內(nèi)的預(yù)設(shè)寫下來。例如，若我在寫下這行程式時(shí)，我確信執(zhí)行前的x的值為42，那在一個(gè)語法沒有其他作用的程式語言中，這行程式執(zhí)行完x的值會(huì)變?yōu)?3。在Hoare Logic中可以寫成{ x =42} x ：= x +1{ x =43}。

我們?cè)倏戳硪恍谐淌?/p>

y ：= x

若在寫這行程式時(shí)我們已經(jīng)想好x的值會(huì)是43，那執(zhí)行完y應(yīng)當(dāng)要是43。寫成Hoare Logic便是{ x =43} y ：= x { y =43}。

當(dāng)我們發(fā)現(xiàn)第一個(gè)程式的后件與第二個(gè)程式的前件相同，便能將上面兩行程式連接起來，而變成{ x =42} x ：= x +1; y ：= x { y =43}。

從而在寫一個(gè)程式時(shí)，我們?nèi)艨偸窃诿總€(gè)小程式前后加上前件與后件（P與Q），最后在將所有程式組合起來時(shí)，就能確切知道這個(gè)程式在給定一個(gè)執(zhí)行前的狀態(tài)下，執(zhí)行后必然會(huì)發(fā)生什么事。

在設(shè)計(jì)一個(gè)語言時(shí)，若我們所有最基本的單元操作的前后件都寫出來，那就可以想像我們能設(shè)計(jì)一套工具去判斷整個(gè)程式執(zhí)行前后一定會(huì)發(fā)生的事，而不會(huì)有如C 語言中的undefined behavior 或需要看bytecode 才能確定的行為。

Matching Logic 與K-framework

K Framework是一個(gè)用來定義程式語言的工具，其運(yùn)用的是Hoare Logic的延伸— — Matching Logic。在K Framework中，定義一個(gè)語言需要三個(gè)基本的元件：語法（syntax）、配置（configuration）與規(guī)則（rule）。

定義程式語法用的（K的）語法是BNF，若寫過functional語言或讀過計(jì)算理論的人可能會(huì)很熟悉，簡單來說就是將一個(gè)語言中的所有可能出現(xiàn)的語法以遞回的方式定義清楚，以這篇論文中定義Solidity的語法方式為例子：

K ：= uintm | address | K［ n ］

T ：= uintm | address | T［ n ］ | T［］ | mapping KT| ? T ??? T ? | contract | ref T

這部分只列出所有Solidity 可能出現(xiàn)的型別，若要完整定義語言還需列出如contract、pragma 等關(guān)鍵字。

而Solidity 寫成K Framework 的語法實(shí)在太長了，這里就先以一個(gè)官網(wǎng)范例中簡單的語言IMP 為例子（簡寫自imperative，相對(duì)于declarative 語言。其實(shí)定義純functional 的declarative 語言相對(duì)簡單，也是官方提供的第一個(gè)范例，但讀者應(yīng)該更熟悉如Solidity 或C 等imperative 語言因此也用此舉例）

IMP 以K Framework 定義的Syntax 如下

module IMP-SYNTAX

syntax AExp ：：= Int | Id

| AExp “/” AExp

》 AExp “+” AExp

| “（” AExp “）”

syntax BExp ：：= Bool

| AExp “《=” AExp

| “！” BExp

》 BExp “&&” BExp

| “（” BExp “）”

syntax Block ：：= “{” “}”

| “{” Stmt “}”

syntax Stmt ：：= Block

| Id “=” AExp “;”

| “if” “（” BExp “）” Block “else” Block

| “while” “（” BExp “）” Block

》 Stmt Stmt

syntax Pgm ：：= “int” Ids “;” Stmt

syntax Ids ：：= List{Id，“，”}

endmodule

由此可以看出，對(duì)于任何一個(gè)指令Stmt，他都必需是Stmt所定義的形式中其中一種。如while（1）{x=1+1;}是合法的Stmt，因?yàn)樗稀皐hile” “（” BExp “）” Block的形式，而這是因?yàn)閣hile中的1符合BExp的形式，而且x=1+1符合Stmt中Id “=” AExp “;”的形式，因?yàn)?+1符合AExp …依此類推。

而配置（configuration）則是將語言執(zhí)行中會(huì)用到或改變的狀態(tài)（state）寫下來，這些配置可以是記憶體、計(jì)數(shù)器等。如果是完全沒有副作用的語言那可能不需要定義這種狀態(tài)（完全不需要輸入輸出的declarative 語言可能就用不到，如K Framework 在tutorial 中定義的小語言LAMBDA）。然而一般實(shí)務(wù)上使用的語言一定用到外部的狀態(tài)，狀態(tài)也能稱為環(huán)境（enviroment），可以理解為從語言中看不出來，但在執(zhí)行時(shí)會(huì)用到與造成影響的對(duì)象。如在C 中直接修改記憶體的操作，雖然語法上只是一個(gè)指令（指令執(zhí)行的結(jié)果在后續(xù)程式中拿來使用），但實(shí)際上對(duì)「記憶體」這個(gè)狀態(tài)造成了影響。以Solidity 來說實(shí)體的state 就是Storage 與Memory。真正需要定義的state 其實(shí)細(xì)分非常多，如Type Space（從變數(shù)名稱到Type 的對(duì)應(yīng)關(guān)系）、Name Space（變數(shù)名稱到記憶體位置的對(duì)應(yīng)關(guān)系）、Storage 與Memory（從記憶體位置對(duì)應(yīng)到其上的值）等。

配置可以是巢狀的，也就是說一個(gè)配置中可以包含其他配置。例如一個(gè)thread 中有一個(gè)stack，一支程式可以有好幾個(gè)thread，就用得到這樣的配置。

IMP 中的configuration 長這樣：

configuration 《T》

《k》 $PGM:Pgm 《/k》

《state》 .Map 《/state》

《/T》

與龐大的語言比起來這是非常簡單的configuration。語法是XML，一個(gè)configuration的空間稱為一個(gè)cell，這里有兩個(gè)cell，k與state。k里面放的是程式碼本身，而state則儲(chǔ)存了如變數(shù)等需要記錄的狀態(tài)。T可以暫時(shí)不理會(huì)。$PGM是K Framework的變數(shù)，意思是程式碼要放在這個(gè)cell中（程式碼也是環(huán)境的一部分！如在C中程式碼也是data的一部分，甚至能寫出能讀寫自己的程式碼區(qū)塊的程式），：Pgm說明這個(gè)程式碼同時(shí)必須是符合Syntax中定義好的Pgm的形式才行。

configurations 也定義好后，就要寫規(guī)則。規(guī)則就是最重要的「程式如何執(zhí)行」的原則。在K Framework 定義的語言中，一行指令會(huì)做出什么操作，一定要是明確寫出的一條規(guī)則才行，否則就會(huì)無法執(zhí)行。一條規(guī)則的形式是「可被執(zhí)行的程式」加上其「被執(zhí)行成的結(jié)果」，另外能加上附加條件以及其會(huì)對(duì)環(huán)境（配置）造成的影響。如現(xiàn)在有條簡單的規(guī)則：

rule while （B） S =》 if （B） {S while （B） S} else {}

這條規(guī)則是在說明，任何符合while （B） S形式的語法都能執(zhí)行為if （B） {S while （B） S} else {}。=》這個(gè)動(dòng)作可以稱為重寫（Rewrite），因?yàn)檫@規(guī)則的意思其實(shí)就是「將左邊的程式重寫成右邊的程式」，再將重寫后的程式繼續(xù)依照其他規(guī)則執(zhí)行（重寫）下去。

再看另一條規(guī)則：

rule 《k》 X = I:Int; =》 。 .。.《/k》 《state》。.. X |-》 （_ =》 I） 。..《/state》

這條規(guī)則是在說，在k這個(gè)configuration中，當(dāng)出現(xiàn)X=I形式時(shí)（I必須為Int），其會(huì)被重寫為什么都沒有（。在K Framework中是nothing的意思）。在《k》 《/k》中開頭沒有 。..，結(jié)尾卻有，意思是若要使用這條規(guī)則，X=I的形式必須出現(xiàn)在程式的開頭。而state中X所對(duì)應(yīng)到的值會(huì)被取代為I。（|-》是變數(shù)名稱與值的對(duì)應(yīng)關(guān)系，_是本來所對(duì)應(yīng)到的值，但因?yàn)椴恍枰玫奖緛淼闹邓杂胈）

到這邊為止應(yīng)該可以看出，規(guī)則跟上面講的Hoare Logic其實(shí)非常像！只是我們將前件后件寫成了Rewrite的規(guī)則，{ P } S { Q }被轉(zhuǎn)換成了S ∧ P ? T ∧ Q這樣的形式（T是Rewrite后的程式碼）。

K-framework 中被正規(guī)化的 Solidity

寫了這么多，這篇跟本還沒講和Solidity 有關(guān)的內(nèi)容。的確，光是介紹K Framework 就花了很多功夫，在開頭提及的論文中，南洋理工與新加坡科技設(shè)計(jì)大學(xué)的人將Solidity 的基本語意實(shí)作在K Framework 中，寫了50 個(gè)configuration 以及200 多條rule（2000+ 行），目前已經(jīng)可以在K Framework 中執(zhí)行。在執(zhí)行過程中，我們就能做動(dòng)態(tài)的測試，判斷cell 中會(huì)不會(huì)出現(xiàn)預(yù)期以外的值。

我們就看其中一條簡單的rule。

（注意這里的水平分隔上下就是? 的左右）

Elementary-TypeName這條規(guī)則中，pcsContractPart是一個(gè)定義在K Framework的函數(shù)，會(huì)被展開為一個(gè)可以被重寫的形式。（在《k》中的）程式碼若是符合一個(gè)變數(shù)宣告的形式，contract cell中的許許多多配置就能夠方式如上的操作。以u(píng)int public data = 10;為例，uint可以代入X（ElementaryTypeName）、public代入Y（Specifiers）、data代入Z（Id），10代入E。當(dāng)出現(xiàn)符合這樣規(guī)則的程式后，這行指令的下一步可以被「重寫」為什么都不剩（.K，「?！归_頭為nothing的意思）。同時(shí)，在這個(gè)程式執(zhí)行時(shí)的狀態(tài)，也就是configuration中：

· cname（合約名稱）必須有符號(hào) C

· vname （記錄變數(shù)數(shù)量）中的數(shù)字N 會(huì)增加 1

· vId （記錄第N 個(gè)變數(shù)的變數(shù)名稱）會(huì)多出一條N 到Z 的對(duì)應(yīng)

· variables （從變數(shù)名稱到變數(shù)地址的對(duì)應(yīng)）會(huì)多一個(gè)Z 到 ！Num 的對(duì)應(yīng)，！Num 是告訴K 產(chǎn)生一個(gè)新的數(shù)字作為地址

· typename （記錄從變數(shù)名稱到Type 的對(duì)應(yīng)）多一條Z 到X 的對(duì)應(yīng)

· cstore （記錄從地址到值的對(duì)應(yīng)）多一條 ！Num 到E 的對(duì)應(yīng)。

需要注意的是，每個(gè)cell 中的前件都要成立，這個(gè)規(guī)則才適用。如果前件為nothing（「?！归_頭），那就代表這個(gè)cell 沒有前件。例如，若contract cell 中沒有C 這個(gè)合約名稱，這條規(guī)則就不能被使用。如果一行指令沒有任何規(guī)則能被套用，程式就會(huì)執(zhí)行不下去。

結(jié)語

語意正規(guī)化后，離正規(guī)驗(yàn)證其實(shí)還有段距離。若我們想要驗(yàn)證一個(gè)程式的正確性，我們得先將我們所認(rèn)為的「正確」的條件（specification）給列出來。例如，在一個(gè)扣款的合約中，錢包被扣除的數(shù)字必須只能有一次，我們就能另外寫程式檢查在存有錢包金額的那個(gè)cell中，是不是一定只會(huì)減少某個(gè)數(shù)字。但這樣的程式要怎么寫又是另一個(gè)大工程，其中牽扯到將Matching Logic轉(zhuǎn)換成可以被驗(yàn)證的邏輯模型等問題。已經(jīng)有人將EVM實(shí)作在K Framework中（注意不是Solidity，在計(jì)算理論中，要描述一個(gè)完整的程式語言與描述一臺(tái)電腦是等價(jià)的，EVM同理也能以K Framework描述），并配合Z3證明器寫了用來證明Smart Contract的工具，里面附有一些已經(jīng)證明好的Smart Contract與他們的specification，有興趣的人可以了解一下。