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

Solidity作為一個程序語言，寫出來的Smart Contract就跟所有程序一樣，有時候會有Bug。然而Smart Contract上的Bug很可能比一般程序中的Bug還要嚴重，因為一旦放到鏈上就再也無法被修改了，最知名的莫過于DAO attack。于是有人將腦筋動到另一個依然還未被廣泛應(yīng)用的領(lǐng)域上— —正規(guī)驗證（Formal Verificatinon，也有人稱為形式化驗證）。

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

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

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

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

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

我們再看另一行程式

y ：= x

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

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

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

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

Matching Logic 與K-framework

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

定義程式語法用的（K的）語法是BNF，若寫過funcTIonal語言或讀過計算理論的人可能會很熟悉，簡單來說就是將一個語言中的所有可能出現(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 的語法實在太長了，這里就先以一個官網(wǎng)范例中簡單的語言IMP 為例子（簡寫自imperaTIve，相對于declarative 語言。其實定義純functional 的declarative 語言相對簡單，也是官方提供的第一個范例，但讀者應(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

由此可以看出，對于任何一個指令Stmt，他都必需是Stmt所定義的形式中其中一種。如while（1）{x=1+1;}是合法的Stmt，因為他符合“while” “（” BExp “）” Block的形式，而這是因為while中的1符合BExp的形式，而且x=1+1符合Stmt中Id “=” AExp “;”的形式，因為1+1符合AExp …依此類推。

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

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

IMP 中的configuration 長這樣：

configuration 《T》

《k》 $PGM:Pgm 《/k》

《state》 .Map 《/state》

《/T》

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

configurations 也定義好后，就要寫規(guī)則。規(guī)則就是最重要的「程式如何執(zhí)行」的原則。在K Framework 定義的語言中，一行指令會做出什么操作，一定要是明確寫出的一條規(guī)則才行，否則就會無法執(zhí)行。一條規(guī)則的形式是「可被執(zhí)行的程式」加上其「被執(zhí)行成的結(jié)果」，另外能加上附加條件以及其會對環(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 {}。=》這個動作可以稱為重寫（Rewrite），因為這規(guī)則的意思其實就是「將左邊的程式重寫成右邊的程式」，再將重寫后的程式繼續(xù)依照其他規(guī)則執(zhí)行（重寫）下去。

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

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

這條規(guī)則是在說，在k這個configuration中，當出現(xiàn)X=I形式時（I必須為Int），其會被重寫為什么都沒有（。在K Framework中是nothing的意思）。在《k》 《/k》中開頭沒有 。..，結(jié)尾卻有，意思是若要使用這條規(guī)則，X=I的形式必須出現(xiàn)在程式的開頭。而state中X所對應(yīng)到的值會被取代為I。（|-》是變數(shù)名稱與值的對應(yīng)關(guān)系，_是本來所對應(yīng)到的值，但因為不需要用到本來的值所以用_）

到這邊為止應(yīng)該可以看出，規(guī)則跟上面講的Hoare Logic其實非常像！只是我們將前件后件寫成了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è)計大學的人將Solidity 的基本語意實作在K Framework 中，寫了50 個configuration 以及200 多條rule（2000+ 行），目前已經(jīng)可以在K Framework 中執(zhí)行。在執(zhí)行過程中，我們就能做動態(tài)的測試，判斷cell 中會不會出現(xiàn)預(yù)期以外的值。

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

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

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

· cname（合約名稱）必須有符號 C

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

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

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

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

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

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

結(jié)語

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