胡 凱 白曉敏 高靈超 董愛(ài)強(qiáng)

1(北京航空航天大學(xué)計(jì)算機(jī)學(xué)院 北京 100191)2(北京中電普華信息技術(shù)有限公司 北京 100192)

智能合約的形式化驗(yàn)證方法

胡 凱1白曉敏1高靈超2董愛(ài)強(qiáng)2

1(北京航空航天大學(xué)計(jì)算機(jī)學(xué)院 北京 100191)2(北京中電普華信息技術(shù)有限公司 北京 100192)

(hukai@buaa.edu.cn)

智能合約是一種代碼合約和算法合同，將成為未來(lái)數(shù)字社會(huì)的基礎(chǔ)技術(shù)，它利用協(xié)議和用戶接口，完成合約過(guò)程的所有步驟.總結(jié)了智能合約主要技術(shù)特點(diǎn)和現(xiàn)存的可信、安全等問(wèn)題，提出將形式化方法應(yīng)用于智能合約的建模、模型檢測(cè)和模型驗(yàn)證過(guò)程，以支持規(guī)模化智能合約的生成.研究提出了一個(gè)應(yīng)用于智能合約生命周期的形式化驗(yàn)證框架和驗(yàn)證方法，針對(duì)一個(gè)智能購(gòu)物場(chǎng)景，采用Promela建模語(yǔ)言對(duì)智能購(gòu)物合約進(jìn)行建模，用SPIN進(jìn)行了模型檢測(cè)，驗(yàn)證了形式化方法對(duì)智能合約的作用.

智能合約；形式化方法；建模；驗(yàn)證；SPIN模型檢測(cè)工具

2016年6月17日，運(yùn)行在以太坊公有鏈上的The DAO[1-2]智能合約遭遇攻擊，該合約籌集的公眾款項(xiàng)不斷被一個(gè)函數(shù)的遞歸調(diào)用轉(zhuǎn)向它的子合約，涉及總額300多萬(wàn)以太幣，這是一起嚴(yán)重的智能合約被攻擊事件.The DAO本質(zhì)上是個(gè)VC(風(fēng)險(xiǎn)投資基金)，通過(guò)以太坊籌集到的資金會(huì)鎖定在智能合約中，沒(méi)有哪個(gè)人能夠單獨(dú)動(dòng)用這筆錢(qián).事件是The DAO智能合約本身的腳本漏洞被利用所引發(fā).因此，智能合約的安全、可信問(wèn)題引起大家的關(guān)注，如何編寫(xiě)具有高可靠性、高安全性的智能合約成為目前亟待解決的問(wèn)題.

“智能合約”(smart contract)[3]這個(gè)術(shù)語(yǔ)至少可以追溯到1995年,是由密碼學(xué)家尼克薩博首次提出的.智能合約是能夠自動(dòng)執(zhí)行合約條款的計(jì)算機(jī)程序，他創(chuàng)造性地提出“智能合約就是執(zhí)行合約條款的可計(jì)算交易協(xié)議”.

尼克薩博指出計(jì)算機(jī)代碼可以代替機(jī)械設(shè)備，進(jìn)行更復(fù)雜的數(shù)字財(cái)產(chǎn)交易，未來(lái)的某一天，這些程序甚至可能取代處理某些特定金融交易的律師和銀行，“智能財(cái)產(chǎn)可以將智能合約內(nèi)置到物理實(shí)體的方式，被創(chuàng)造出來(lái)”.比如，房屋出租商將發(fā)現(xiàn)智能合約這種用途很有吸引力，一所房屋的門(mén)鎖，能由被連接到物聯(lián)網(wǎng)上的智能合約打開(kāi),所有門(mén)鎖都是連接互聯(lián)網(wǎng)的.當(dāng)你為租房進(jìn)行了一筆交易時(shí)，存儲(chǔ)在智能手機(jī)中的鑰匙可以為你打開(kāi)房屋,并進(jìn)行自動(dòng)資金轉(zhuǎn)移.雖然智能合約仍然處于初始階段，但是其潛力顯而易見(jiàn)，因?yàn)樗讶伺c法律協(xié)議以及網(wǎng)絡(luò)之間復(fù)雜的關(guān)系程序化了.

智能合約有許多非形式化的定義，尼克薩博給出了一個(gè)簡(jiǎn)短的概念，即“智能合約通過(guò)使用協(xié)議和用戶接口來(lái)促進(jìn)合約的執(zhí)行”；Miller[4]認(rèn)為智能合約就是用程序代碼編寫(xiě)的合約，它的條款由程序來(lái)執(zhí)行；Ethereum的智能合約就是基于區(qū)塊鏈的可直接控制數(shù)字資產(chǎn)的程序[5].

總的來(lái)說(shuō)，一個(gè)智能合約是一套以數(shù)字形式定義的承諾，包括合約參與方可以在上面執(zhí)行這些承諾的協(xié)議.它是能夠自動(dòng)執(zhí)行合約條款的計(jì)算機(jī)程序，被部署在分享的、復(fù)制的賬本上，它可以維持自己的狀態(tài)，控制自己的資產(chǎn)和對(duì)接收到的外界信息或者資產(chǎn)進(jìn)行回應(yīng).承諾指的是合約參與方同意的權(quán)利與義務(wù)，這些承諾定義了合約的本質(zhì)和目的.數(shù)字形式意味著合約不得不寫(xiě)入計(jì)算機(jī)可讀的代碼中.只要參與方達(dá)成協(xié)議，智能合約建立的權(quán)利和義務(wù)，是由一臺(tái)計(jì)算機(jī)或者計(jì)算機(jī)網(wǎng)絡(luò)執(zhí)行完成的.協(xié)議是技術(shù)實(shí)現(xiàn)，在此基礎(chǔ)上，合約承諾被實(shí)現(xiàn)，或者合約承諾實(shí)現(xiàn)被記錄下來(lái).

尼克薩博提出的智能合約理論幾乎與互聯(lián)網(wǎng)(world wide web)同時(shí)出現(xiàn)，但應(yīng)用實(shí)踐卻一直嚴(yán)重地落后于理論.主要面臨2個(gè)方面問(wèn)題:一是智能合約如何來(lái)控制實(shí)物資產(chǎn)保證有效地執(zhí)行合約，計(jì)算機(jī)程序很難控制現(xiàn)實(shí)世界的現(xiàn)金、股份等資產(chǎn)；二是計(jì)算機(jī)很難保證執(zhí)行這些條款以獲得合約方的信任，合約方需要可靠地解釋和執(zhí)行代碼的計(jì)算機(jī)，它無(wú)法親自檢查有問(wèn)題的計(jì)算機(jī)，也無(wú)法直接觀察與驗(yàn)證其他合約方的執(zhí)行動(dòng)作，只有讓第三方審核各方合約執(zhí)行的記錄.而區(qū)塊鏈技術(shù)的出現(xiàn)解決了這些問(wèn)題，從而觸發(fā)了智能合約的應(yīng)用.如今很多區(qū)塊鏈系統(tǒng)，如Ethereum[6]，有可編程的合約語(yǔ)言與可執(zhí)行的基礎(chǔ)設(shè)施，以實(shí)現(xiàn)智能合約.在Ethereum中，智能合約是存儲(chǔ)在區(qū)塊鏈上的腳本，通過(guò)區(qū)塊鏈節(jié)點(diǎn)以分布式的形式執(zhí)行，相當(dāng)于商業(yè)交易、監(jiān)督管理過(guò)程中法律、法規(guī)的執(zhí)行者.智能合約可以按序、安全、可驗(yàn)證的方式實(shí)施特定的流程.

然而，智能合約的生成和執(zhí)行還存在一些問(wèn)題，包括：1)智能合約對(duì)保證資產(chǎn)的安全性提出了更高的要求，合約需要驗(yàn)證合約邏輯屬性的正確性，重要的是能夠自動(dòng)生成可信的可執(zhí)行合約代碼以節(jié)省成本并提高效率；2)智能合約最終會(huì)取代合約文本，因此我們必須保證合約文本與合約代碼的一致性.基于上述問(wèn)題，本文提出將形式化方法應(yīng)用于智能合約的整個(gè)生命周期.

形式化方法[7]是描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù)，用于計(jì)算機(jī)軟件的規(guī)范、開(kāi)發(fā)和驗(yàn)證.將形式化方法用于軟件設(shè)計(jì)，是期望能夠像其他工程學(xué)科一樣，使用適當(dāng)?shù)臄?shù)學(xué)分析以提高設(shè)計(jì)的可靠性和魯棒性.其中，形式化方法中很重要的一步就是形式化驗(yàn)證，形式化驗(yàn)證可以以更正式的方式產(chǎn)生程序.例如，可以進(jìn)行從規(guī)范到程序的屬性或細(xì)化的證明.

近年來(lái)，模型驅(qū)動(dòng)(model-driven)[8]的設(shè)計(jì)與開(kāi)發(fā)方法逐漸受到重視，并被工業(yè)界認(rèn)為是切實(shí)可行的重要方法.該方法將模型作為整個(gè)系統(tǒng)開(kāi)發(fā)過(guò)程的核心元素，在設(shè)計(jì)階段就建立系統(tǒng)的體系結(jié)構(gòu)模型，盡早進(jìn)行驗(yàn)證和分析.同時(shí)，模型的重用以及基于模型轉(zhuǎn)換的自動(dòng)或半自動(dòng)的逐步求精過(guò)程，都有助于降低系統(tǒng)開(kāi)發(fā)時(shí)間和成本.然而，模型驅(qū)動(dòng)的設(shè)計(jì)與開(kāi)發(fā)方法的真正有效使用，需要多方面的支持.首先，需要合適的體系結(jié)構(gòu)建模語(yǔ)言，并要求建模語(yǔ)言對(duì)系統(tǒng)的軟硬件結(jié)構(gòu)、運(yùn)行時(shí)環(huán)境、功能行為以及非功能屬性可表達(dá)；其次，為滿足系統(tǒng)的需求，形式驗(yàn)證與分析方法是重要的手段；最后，基于經(jīng)過(guò)驗(yàn)證和分析的模型，研究自動(dòng)代碼生成技術(shù)，有助于避免手工編碼帶來(lái)的錯(cuò)誤，可以進(jìn)一步提高系統(tǒng)的質(zhì)量屬性.

將形式化方法應(yīng)用于智能合約整個(gè)生命周期的流程包括合約設(shè)計(jì)、自然語(yǔ)言描述、形式化描述、模型驗(yàn)證、自動(dòng)代碼生成和一致性測(cè)試.本文重點(diǎn)探討形式化描述和形式化驗(yàn)證可以更好地生成和執(zhí)行智能合約.其中，形式化描述可以克服自然語(yǔ)言描述的缺點(diǎn)，例如二義性.形式化驗(yàn)證可以檢查合約中是否存在邏輯錯(cuò)誤，可以做可達(dá)性分析、不變性分析、等價(jià)性分析等.

1 智能合約的性質(zhì)

目前，智能合約處在逐漸的發(fā)展中.2015年3月20日，以太坊基金會(huì)發(fā)布了Ethereum項(xiàng)目，它是一個(gè)開(kāi)源數(shù)字貨幣和區(qū)塊鏈平臺(tái)，為開(kāi)發(fā)者提供在區(qū)塊鏈上搭建和發(fā)布智能合約的平臺(tái)，可用來(lái)?yè)?dān)保和交易任何事物.2015年，Linux基金會(huì)發(fā)起一個(gè)推進(jìn)區(qū)塊鏈數(shù)字技術(shù)和交易驗(yàn)證的開(kāi)源項(xiàng)目hyperledger[9]，這是一個(gè)區(qū)塊鏈和智能合約結(jié)合的開(kāi)源平臺(tái)，允許任何人發(fā)行個(gè)人貨幣，通過(guò)權(quán)限控制保證了用戶的隱私和交易的安全性.目前有很多機(jī)構(gòu)和學(xué)者都是基于以上2個(gè)原型系統(tǒng)對(duì)智能合約作更深入的研究.

研究智能合約通過(guò)協(xié)議與用戶界面來(lái)促進(jìn)合約過(guò)程的所有步驟，我們提出了一個(gè)良好的智能合約，它具備以下6個(gè)基本特征：一致性、可定制性、可觀察性、可驗(yàn)證性、自強(qiáng)制性和接入控制.

1) 一致性.智能合約應(yīng)與現(xiàn)有法律一致，必須經(jīng)過(guò)具有專(zhuān)業(yè)法律知識(shí)的專(zhuān)業(yè)人士制定審核，不與現(xiàn)有法律沖突，具有法律效應(yīng).

2) 可定制性.智能合約是可定制的.多個(gè)合約可以合并成一個(gè)復(fù)合或復(fù)雜的合約.

3) 可觀察性.合約方能夠通過(guò)用戶界面去觀察關(guān)于合約的所有狀態(tài)，包括合約本身及合約執(zhí)行過(guò)程的記錄等.

4) 可驗(yàn)證性.合約方執(zhí)行合約的過(guò)程是可驗(yàn)證的.

5) 自強(qiáng)制性.對(duì)于違反合約行為的制裁必須是強(qiáng)制性的，這需要把資產(chǎn)變得數(shù)字化可控，并且由密碼協(xié)議保證其安全.

6) 接入控制.就是指具有相關(guān)合約利益的人才能接觸相應(yīng)的合約信息，即與合約相關(guān)的知識(shí)、控制、執(zhí)行都應(yīng)該作為資產(chǎn)保護(hù)起來(lái)，只有發(fā)生爭(zhēng)執(zhí)時(shí)，才把內(nèi)容提供給第三方檢驗(yàn).

智能合約作為計(jì)算法律學(xué)的一種新技術(shù)，有一個(gè)很重要的特性是當(dāng)條件滿足時(shí)可以自動(dòng)執(zhí)行相應(yīng)動(dòng)作.但這一特性在其他應(yīng)用領(lǐng)域已經(jīng)有類(lèi)似的技術(shù).例如，20世紀(jì)80年代的基于知識(shí)系統(tǒng)都有這一特性.一個(gè)是基于規(guī)則的系統(tǒng)，當(dāng)滿足某個(gè)條件時(shí)，相應(yīng)的規(guī)則就會(huì)被觸發(fā).如果有多個(gè)規(guī)則同時(shí)被觸發(fā)，會(huì)有相應(yīng)的解決機(jī)制協(xié)調(diào)這些規(guī)則的執(zhí)行.一個(gè)是黑板架構(gòu)系統(tǒng)，在這個(gè)系統(tǒng)中，有多個(gè)代理同時(shí)監(jiān)控，當(dāng)某個(gè)條件滿足時(shí)，相應(yīng)的代理會(huì)激活自身的規(guī)則并執(zhí)行.

在Open-Transactions[10]中這樣描述智能合約：一個(gè)智能合約涉及多個(gè)當(dāng)事人，一旦被激活就能自主運(yùn)行，它有可執(zhí)行的代碼；只有被選定的功能可以被激活執(zhí)行；可操縱那些被明確聲明的合法資產(chǎn)；可暫時(shí)存儲(chǔ)資金；合約的狀態(tài)值被不斷地更新、記錄.

下面給出一個(gè)互聯(lián)網(wǎng)智能購(gòu)物合約的例子.基本合約包括商品訂貨、分銷(xiāo)和售后服務(wù).組合的合約用于連接客戶和商家.

基礎(chǔ)合約:

合約1. 貨物訂購(gòu)與分配.

合約方：客戶和商家.

Contract goods_ordering_and_distribution (goods_information, payment, distribution)

BEGIN

IF goods are available and pay is completed and distribution is available

Inform merchant to send the goods to customer, set the terminator= timestamp+one week

ELSE

The transaction failed and returned the money to customer

Wait one week for the acknowledgment message from customer

IF acknowledgment message received

Pay to merchant and quit

IF timeout

The transaction failed and returned the money to customer

END

合約2. 售后服務(wù)合約.

合約方：客戶和商家.

Contract sale_after_service (item_information, payment, terminator)

BEGIN

WHILE (timestamp

Wait for the feedback message from customer

IF merchant received message from customer

SWITCH(message){

Case goods_return message:

IF timestamp

merchant wait for the goods

IF merchant received the goods

merchant return the money back to customer

ELSE

merchant reject and quit

Case goods_exchange message:

IF timestamp

merchant wait for the goods

IF merchant received the goods

merchant send the new goods to customer

Other:

NULL

}

}

QUIT

END

然而，當(dāng)前的智能合約研究還處于初級(jí)階段，應(yīng)用還十分簡(jiǎn)單，甚至是不智能的，智能合約面臨許多可信與安全問(wèn)題.作為一種特殊的程序代碼，除面臨一般軟件面臨的可信和安全問(wèn)題外，智能合約還面臨以下可信和驗(yàn)證方面問(wèn)題：

1) 如何編制合約雙方認(rèn)可的模板框架，誰(shuí)來(lái)編程實(shí)現(xiàn)合約代碼，并保證代碼的正確性及獲得雙方認(rèn)可.

2) 合約驗(yàn)證問(wèn)題. 程序都是有bug的，如明顯地有利于合約的一方，該怎樣進(jìn)行修復(fù)，如何驗(yàn)證合約的邏輯正確并杜絕漏洞.

3) 合約的定制問(wèn)題. 如何制定好的智能合約模板，根據(jù)不同場(chǎng)景定制不同合約，組合多個(gè)合約形成復(fù)合合約.

4) 一致性問(wèn)題. 智能合約代碼執(zhí)行與文本合約具有一致性嗎?不一致的合約是不可信的.

5) 智能合約執(zhí)行過(guò)程中的可控性和可調(diào)度性，要確保執(zhí)行過(guò)程中的可信性和安全性.

下面本文提出采用形式化方法來(lái)研究解決這些問(wèn)題.

2 形式化方法的引入

為解決智能合約上述所提到的問(wèn)題，本文引入形式化方法，將形式化方法應(yīng)用于智能合約生成和執(zhí)行的整個(gè)生命周期.

形式化方法[11]是指用數(shù)學(xué)方法描述和推理基于計(jì)算機(jī)的系統(tǒng)，直觀地說(shuō)，就是規(guī)范語(yǔ)言+形式推理，在技術(shù)上通過(guò)精確的數(shù)學(xué)手段和強(qiáng)大的分析工具得到支持，其表現(xiàn)形式通常有邏輯、離散數(shù)學(xué)、狀態(tài)機(jī)等.規(guī)范語(yǔ)言包括語(yǔ)法、語(yǔ)義以及滿足關(guān)系等，可以分為4類(lèi)：抽象模型規(guī)范法、代數(shù)規(guī)范法、狀態(tài)遷移規(guī)范法和公理規(guī)范法.

形式化方法主要包括形式規(guī)約和形式化驗(yàn)證.形式規(guī)約使用具有精確語(yǔ)法和語(yǔ)義的形式語(yǔ)言刻畫(huà)系統(tǒng)的行為和性質(zhì)，是設(shè)計(jì)系統(tǒng)的約束和驗(yàn)證系統(tǒng)是否正確的依據(jù)；形式化驗(yàn)證則是在形式規(guī)約的基礎(chǔ)上，建立系統(tǒng)行為及其性質(zhì)的關(guān)系，從而驗(yàn)證系統(tǒng)是否滿足期望的關(guān)鍵性質(zhì)，主要包括模型檢測(cè)和定理證明.

模型檢測(cè)[11]是一種重要的自動(dòng)驗(yàn)證和分析技術(shù)，通過(guò)顯式狀態(tài)搜索或隱式不動(dòng)點(diǎn)計(jì)算來(lái)驗(yàn)證有窮狀態(tài)系統(tǒng)是否滿足預(yù)期的性質(zhì).模型檢測(cè)方法目前已經(jīng)涵蓋了并發(fā)系統(tǒng)模型檢測(cè)、實(shí)時(shí)系統(tǒng)模型檢測(cè)、混成系統(tǒng)模型檢測(cè)以及概率模型檢測(cè)等多個(gè)方面.

模型檢測(cè)[12]詳細(xì)探討了模型中的相關(guān)屬性.這不僅對(duì)于有限模型是可以實(shí)現(xiàn)的，而且對(duì)于一些無(wú)限模型也是可以實(shí)現(xiàn)的，其中無(wú)限狀態(tài)集合可以通過(guò)使用抽象或利用對(duì)稱性的優(yōu)點(diǎn)來(lái)表示.通常包括：探索模型中的所有的狀態(tài)和轉(zhuǎn)換，通過(guò)使用智能的和領(lǐng)域特定的抽象技術(shù)在單個(gè)操作中考慮整個(gè)狀態(tài)組，并減少計(jì)算時(shí)間.

基于有限狀態(tài)機(jī)的模型檢驗(yàn)可以全自動(dòng)驗(yàn)證，它可以檢測(cè)模型的不同狀態(tài).定理證明需要在一些關(guān)鍵路徑進(jìn)行手動(dòng)控制，它可以證明程序的正確性.等價(jià)驗(yàn)證主要是驗(yàn)證設(shè)計(jì)的一致性，也就是說(shuō)，設(shè)計(jì)是否滿足需要，或者程序和合約是否相同.

定理證明技術(shù)將系統(tǒng)行為和性質(zhì)都用邏輯方法來(lái)刻畫(huà)，基于公理和推理規(guī)則組成的形式系統(tǒng)，證明系統(tǒng)是否滿足期望的關(guān)鍵性質(zhì).而使用定理證明器來(lái)輔助證明，相當(dāng)于將手工證明變成一系列能夠在計(jì)算機(jī)上自動(dòng)進(jìn)行的符號(hào)演算，能夠?qū)ψC明過(guò)程進(jìn)行正確性檢查，從而提高證明的可信度.常用的定理證明器主要有Coq，PVS，Isabelle等.

圖1 智能合約的MDE流程圖

作為形式化方法的工程實(shí)踐，模型驅(qū)動(dòng)工程(MDE)旨在提高程序規(guī)范中的抽象級(jí)別，并增加程序開(kāi)發(fā)的自動(dòng)化.MDE[8]的思想是使用不同抽象級(jí)別的模型用于開(kāi)發(fā)系統(tǒng)，從而提高程序規(guī)范中的抽象級(jí)別.通過(guò)使用可執(zhí)行模型轉(zhuǎn)換來(lái)增加程序開(kāi)發(fā)中的自動(dòng)化.較高級(jí)別的模型被轉(zhuǎn)換為較低級(jí)別的模型，直到該模型可以使用代碼生成或模型解釋來(lái)執(zhí)行.MDE可以支持智能合約的整個(gè)生命周期，從建模、驗(yàn)證、代碼生成到一致性測(cè)試，應(yīng)用于智能合約的形式化方法流程如圖1所示.

在模型驅(qū)動(dòng)框架下，由于體系結(jié)構(gòu)模型包含的系統(tǒng)特征和信息較多，一般不直接對(duì)體系結(jié)構(gòu)模型進(jìn)行驗(yàn)證和分析，而主要采用模型轉(zhuǎn)換的方式，即將體系結(jié)構(gòu)模型(或子集)轉(zhuǎn)換到另一個(gè)形式模型，或者直接轉(zhuǎn)換到模型檢測(cè)工具或定理證明器，目的是為了重用這些已有的驗(yàn)證和分析能力.

基于模型的代碼自動(dòng)生成[13]概念源于模型驅(qū)動(dòng)架構(gòu) (model driven architecture, MDA).模型到代碼的生成和模型到模型的轉(zhuǎn)換都是MDA模型轉(zhuǎn)換的子集.MDA能夠盡早對(duì)系統(tǒng)進(jìn)行分析與驗(yàn)證，并將驗(yàn)證后符合需求的模型生成代碼，不僅有助于保證系統(tǒng)的質(zhì)量屬性，同時(shí)能夠促進(jìn)應(yīng)用開(kāi)發(fā)的標(biāo)準(zhǔn)化和工業(yè)化，并有效控制開(kāi)發(fā)時(shí)間與成本.

一致性測(cè)試[14]指的是被測(cè)系統(tǒng)與標(biāo)準(zhǔn)的一致性，它是一種黑盒測(cè)試.通過(guò)一致性測(cè)試，可以給用戶提供2個(gè)信息：通過(guò)了一致性測(cè)試的合約實(shí)現(xiàn)，具有合約所要求的各種能力；在具有代表性的合約實(shí)例中，被測(cè)試的合約代碼實(shí)現(xiàn)的外部特性與標(biāo)準(zhǔn)合約文本的要求一致.

圖2 形式化方法應(yīng)用框架

綜上，我們提出智能合約的形式化方法框架如圖2所示.一個(gè)合約的生成包括：首先，用戶提出需求，根據(jù)用戶需求制定合約文本；然后對(duì)合約文本進(jìn)行形式化描述，并選擇合適的建模語(yǔ)言和建模工具對(duì)形式化規(guī)格說(shuō)明文檔進(jìn)行建模和性質(zhì)驗(yàn)證，其中，模型驗(yàn)證包括理論證明和模型檢測(cè)，在模型檢測(cè)中，我們通常使用模型轉(zhuǎn)換來(lái)驗(yàn)證更多的性質(zhì)；最后是一致性測(cè)試.為了證明合約代碼與合約文本在性質(zhì)和執(zhí)行力是保持一致的，因此，需要對(duì)合約文本和合約代碼進(jìn)行一致性測(cè)試.這就是將形式化方法應(yīng)用于智能合約完整生命周期的框架.

圖3是將形式化方法應(yīng)用于智能合約整個(gè)生命周期的流程.當(dāng)需要新的合約時(shí)，使用非正式化規(guī)范來(lái)設(shè)計(jì)合約，然后使用形式化規(guī)范來(lái)描述合約以驗(yàn)證合約.模型檢驗(yàn)工具可以用來(lái)檢查合約，或使用演繹驗(yàn)證方法來(lái)證明合約.其次，可以通過(guò)模型工具，將模型自動(dòng)化生成合約代碼.最后，一致性測(cè)試確保文本和程序代碼的一致性.

圖3 智能合約的形式化流程

將形式化方法應(yīng)用于智能合約，使得合約的生成和執(zhí)行有了規(guī)范性約束，保證了合約的可信性，使人們可以信任智能合約的生產(chǎn)過(guò)程和執(zhí)行效力.合約的形式化驗(yàn)證保證了合約的正確屬性，自動(dòng)化代碼生成提高了合約的生成效率，合約的一致性測(cè)試保證了合約代碼與合約文本的一致性.

3 智能合約的形式化驗(yàn)證方法

對(duì)智能合約的形式化驗(yàn)證包括形式化描述、形式化驗(yàn)證、自動(dòng)代碼生成和一致性測(cè)試.本文中，我們重點(diǎn)探討智能合約的形式化描述和形式化驗(yàn)證方法.

形式化方法的另一個(gè)重要研究?jī)?nèi)容是形式化驗(yàn)證.形式化驗(yàn)證與形式化規(guī)約之間具有緊密的聯(lián)系，形式化驗(yàn)證就是驗(yàn)證已有的程序(系統(tǒng))P是否滿足其規(guī)約(φ，ψ)的要求(即P(φ，ψ))，它也是形式化方法所要解決的核心問(wèn)題[15].

傳統(tǒng)的驗(yàn)證方法包括模擬和測(cè)試，它們都是通過(guò)實(shí)驗(yàn)的方法對(duì)系統(tǒng)進(jìn)行查錯(cuò).模擬和測(cè)試分別在系統(tǒng)抽象模型和實(shí)際系統(tǒng)上進(jìn)行，一般的方法是在系統(tǒng)的某點(diǎn)給予輸入，觀察在另一點(diǎn)的輸出，這些方法花費(fèi)很大，而且由于實(shí)驗(yàn)所能涵蓋的系統(tǒng)行為有限，很難找出所有潛在的錯(cuò)誤.基于此，早期的形式驗(yàn)證主要研究如何使用數(shù)學(xué)方法，嚴(yán)格證明一個(gè)程序的正確性(即程序驗(yàn)證).

Von Neumann[16](馮.諾伊曼)早在1948年發(fā)表的論文“Planing and Coding Problems for an Electronic Computer Instrument”中就提到了程序正確性證明；Floyd[17]在1967年發(fā)表論文“Assigning Meanings to Programs”中提出了驗(yàn)證流程圖程序正確性的歸納斷言方法，這是程序驗(yàn)證方面的開(kāi)創(chuàng)性工作；1969年，Hoare[18]在“An axiomatic Basis for Computer Programming”一文對(duì)Floyd歸納斷言法形式化，首次提出程序驗(yàn)證的公理系統(tǒng)，稱為Hoare邏輯公理化方法，1970年以來(lái)還出現(xiàn)能輔助用戶正確編制程序的實(shí)用的半自動(dòng)程序驗(yàn)證系統(tǒng).1976年，S.Owicki，D.Gries提出并發(fā)程序的驗(yàn)證方法；1977年，A.Pnueli提出反映系統(tǒng)驗(yàn)證的時(shí)序邏輯方法；1981年，E.M.Clarke，E.A.Emerson提出有窮狀態(tài)并發(fā)系統(tǒng)的模型檢測(cè)方法；80年代后期主要研究解決模型檢測(cè)“狀態(tài)爆炸問(wèn)題”；90年代起主要研究實(shí)時(shí)與混成系統(tǒng)的形式驗(yàn)證問(wèn)題.

目前常見(jiàn)的形式化驗(yàn)證方法主要可分為2類(lèi)：演繹驗(yàn)證和模型檢測(cè).其中，早期(20世紀(jì)60—70年代)的形式化技術(shù)主要采用演繹法證明順序和并發(fā)程序正確性，而近期(20世紀(jì)80—90年代)則多采用模型檢測(cè)方法驗(yàn)證實(shí)時(shí)和混成系統(tǒng).

1) 演繹驗(yàn)證.演繹驗(yàn)證是早期采用的主要驗(yàn)證技術(shù)，它基于定理證明的基本思想，采用邏輯公式描述系統(tǒng)及其性質(zhì)，通過(guò)一些公理或推理規(guī)則來(lái)證明系統(tǒng)具有某些性質(zhì).

演繹驗(yàn)證的優(yōu)點(diǎn)是可以使用歸納的方法來(lái)處理無(wú)限狀態(tài)的問(wèn)題，并且證明的中間步驟使用戶對(duì)系統(tǒng)和被證明性質(zhì)有更多的了解.缺點(diǎn)是現(xiàn)有的方法不能做到完全自動(dòng)化，還需與用戶交互，要求用戶能提供驗(yàn)證中創(chuàng)造性最強(qiáng)部分的工作.因而演繹證明方法的效率較低，很難用于大系統(tǒng)的驗(yàn)證.

目前主要演繹驗(yàn)證工具有：基于Manna-Pnueli證明系統(tǒng)的STeP(stanford theorem prover)、TLV、機(jī)器定理證明器(ACL2，Coq，HOL，Isabelle，Larch，Nuprl，PVS，TPS)等[19].

2) 模型檢測(cè)(算法驗(yàn)證).模型檢測(cè)是對(duì)有窮狀態(tài)系統(tǒng)的一種形式化確認(rèn)方法，它基于狀態(tài)搜索的基本思想，是模擬和測(cè)試方法的自然延伸，搜索的可窮盡性有賴于為合約建立有窮狀態(tài)的模型，這為建模造成一定的難度，但能保證搜索過(guò)程終止.

模型檢測(cè)方法的基本思想是通過(guò)狀態(tài)空間搜索來(lái)確認(rèn)合約是否具有某些性質(zhì).即給定一個(gè)合約(程序)P和規(guī)約ψ，生成對(duì)應(yīng)的合約模型M，然后證明Mψ，即規(guī)約公式ψ在合約模型M中成立，這樣就證明了合約(程序)P滿足規(guī)約ψ.

模型檢測(cè)方法通常采用Dolev-Yao模型、模態(tài)邏輯、有限狀態(tài)機(jī)和進(jìn)程代數(shù)等理論作為合約分析的理論基礎(chǔ)，其基本思想是用狀態(tài)遷移系統(tǒng)S表示系統(tǒng)的行為，用模態(tài)時(shí)序邏輯公式F描述系統(tǒng)的性質(zhì).一般地，一個(gè)模型檢測(cè)方法主要由特定的形式模型、形式邏輯和相應(yīng)的模型檢測(cè)算法3個(gè)方面構(gòu)成，不同的模型檢測(cè)方法具有不同的應(yīng)用領(lǐng)域.

將模型檢測(cè)應(yīng)用于智能合約以解決合約的可信問(wèn)題，一般包括以下步驟：

1) 建模.通過(guò)選擇合適的建模語(yǔ)言和建模工具，使用模型檢測(cè)工具能夠接受的形式語(yǔ)言來(lái)描述合約.

2) 描述.闡明所要驗(yàn)證的合約性質(zhì)，包括合約的狀態(tài)可達(dá)性、死鎖、活鎖、有界性等.

3) 驗(yàn)證.對(duì)合約的狀態(tài)空間進(jìn)行搜索，發(fā)現(xiàn)合約存在的問(wèn)題并及時(shí)修改，對(duì)合約進(jìn)行迭代驗(yàn)證.

目前形式化描述技術(shù)主要分為2種類(lèi)型：形式化描述模型和形式化描述語(yǔ)言.通過(guò)形式化描述模型，可以獲得抽象的合約模型.形式化描述語(yǔ)言總是基于一種或多種形式化描述模型.形式化描述技術(shù)已經(jīng)有幾十年的發(fā)展，目前有多種形式化描述模型和形式化描述語(yǔ)言，如圖4所示.形式化描述語(yǔ)言主要有3種標(biāo)準(zhǔn)：CCITT國(guó)際電報(bào)電話咨詢委員會(huì)(International Telephone and Telegraph Consultative Committee)組織制定的SDL，ISO組織制定的LOTOS和ESTELLE.

形式化描述方法分類(lèi)內(nèi)容形式化描述模型狀態(tài)變遷模型FSM,EFSM,Petri網(wǎng)模型進(jìn)程代數(shù)通信系統(tǒng)演算(CCS)通信順序進(jìn)程(CSP)其他時(shí)序邏輯(或時(shí)態(tài)邏輯)(TL)形式化描述語(yǔ)言CCITT組織SDLISO組織LOTOS,ESTELLE其他Promela語(yǔ)言:SPIN(著名模型檢測(cè)工具)的輸入語(yǔ)言

圖4 各種形式化描述技術(shù)

SPIN是美國(guó)貝爾實(shí)驗(yàn)室的形式化方法與驗(yàn)證小組開(kāi)發(fā)的模型檢測(cè)工具.它所關(guān)心的主要問(wèn)題是進(jìn)程之間的信息能否正確地交互，而不是進(jìn)程內(nèi)部的具體細(xì)節(jié).由于其良好的性能、完善的文檔、開(kāi)源及不斷的維護(hù)更新服務(wù)使得SPIN被廣泛應(yīng)用于工業(yè)界和學(xué)術(shù)界.它采用的描述語(yǔ)言為Promela[20].

模型檢測(cè)主要適用于有窮狀態(tài)系統(tǒng)，早期主要用于硬件和協(xié)議的驗(yàn)證.模型檢測(cè)的優(yōu)點(diǎn)是完全自動(dòng)化并且驗(yàn)證速度快，即便是只給出了部分描述的合約，通過(guò)搜索也可以提供關(guān)于已知部分正確性的有用信息.尤其重要的是，在性質(zhì)未被滿足時(shí)，搜索終止可以給出反例，這種信息常常反映出合約設(shè)計(jì)中的細(xì)微失誤，因而對(duì)于合約排錯(cuò)有極大的幫助.

形式化驗(yàn)證方法可以檢查智能合約的很多屬性，例如，合約的公平性、可達(dá)性、有界性、活鎖、死鎖、不可達(dá)以及無(wú)狀態(tài)二義性等.

4 智能合約的驗(yàn)證實(shí)例

在本節(jié)中，使用Promela建模語(yǔ)言和檢測(cè)工具SPIN來(lái)建立和驗(yàn)證智能購(gòu)物合約SSC(smart shopping contract)的模型.

SPIN[20]是一個(gè)通用的工具，以嚴(yán)格的和大多數(shù)自動(dòng)化的方式驗(yàn)證分布式軟件模型的正確性.它是從1980年開(kāi)始，由Gerard J. Holzmann和貝爾實(shí)驗(yàn)室計(jì)算科學(xué)研究中心的原始Unix組的研究人員編寫(xiě)而成.該軟件自1991年以來(lái)一直可用，并繼續(xù)遵循該領(lǐng)域的新發(fā)展而發(fā)展.SPIN是一種著名的分析驗(yàn)證并發(fā)系統(tǒng)邏輯一致性的工具，以其簡(jiǎn)潔明了和自動(dòng)化程度高而備受注目.SPIN已成功應(yīng)用在安全協(xié)議驗(yàn)證、控制系統(tǒng)驗(yàn)證、軟件驗(yàn)證及最優(yōu)化規(guī)劃等領(lǐng)域.

作為一種形式化自動(dòng)驗(yàn)證工具，SPIN的目的是提供：1)系統(tǒng)建模語(yǔ)言Promela(process meta language)，用于直觀、明確地描述系統(tǒng)Promela模型規(guī)約，而不考慮具體實(shí)現(xiàn)細(xì)節(jié)；2)功能強(qiáng)大而簡(jiǎn)明的描述系統(tǒng)應(yīng)滿足性質(zhì)(屬性要求)的邏輯表示法(LT)L；3)提供一套驗(yàn)證系統(tǒng)建模邏輯一致性及系統(tǒng)是否滿足所要驗(yàn)證性質(zhì)的方法.除模型檢測(cè)之外，SPIN還可以作為模擬器操作，遵循系統(tǒng)的一個(gè)可能的執(zhí)行路徑并且向用戶呈現(xiàn)所產(chǎn)生的執(zhí)行軌跡.

SSC應(yīng)在用戶訂單之后觸發(fā)，并且它具有2個(gè)參與者，即用戶和商店.

智能購(gòu)物合約的描述如下：當(dāng)用戶下訂單時(shí)需要將購(gòu)物所需的資金提交給智能購(gòu)物合約，智能購(gòu)物合約暫時(shí)持有資金.同時(shí)SSC啟動(dòng)2個(gè)子進(jìn)程:用戶進(jìn)程和商店進(jìn)程.用戶進(jìn)程：如果商家在7天內(nèi)沒(méi)有交貨，用戶將取消交易，SSC會(huì)將資金退還給用戶，用戶進(jìn)程定時(shí)、周期地檢測(cè)交貨狀態(tài)；商店進(jìn)程：商家收到訂單后，首先系統(tǒng)判斷訂單是否結(jié)束，如果訂單沒(méi)有超時(shí)，則商店發(fā)貨.SSC需要確保資金的安全性和交易過(guò)程中各個(gè)狀態(tài)的可達(dá)性.

SSC的Promela模型如圖5所示.

使用模型檢測(cè)工具SPIN檢測(cè)SSC模型，模型的模擬結(jié)果如圖6所示.

圖5 SSC的Promela模型

從圖6(a)的模型仿真結(jié)果可以看出，一旦超時(shí)(day= 8)，SSC將錢(qián)退還給用戶.

如圖6(b)結(jié)果所示，當(dāng)商店在第2天送貨時(shí)，SSC將錢(qián)轉(zhuǎn)給商店.實(shí)驗(yàn)結(jié)果與預(yù)期結(jié)果一致.

由于SSC是有限狀態(tài)模型，通過(guò)對(duì)SSC的建模和驗(yàn)證，SPIN可以隨機(jī)生成合約的所有狀態(tài)，實(shí)驗(yàn)結(jié)果與合約的預(yù)期結(jié)果一致.

5 結(jié) 論

本文針對(duì)智能合約存在的可信與安全問(wèn)題，將形式化方法應(yīng)用于智能合約的生命周期驗(yàn)證，從形式化描述和形式化驗(yàn)證方面進(jìn)行了詳細(xì)的闡述.一個(gè)好的模型檢測(cè)工具有助于檢查和驗(yàn)證智能合約的各項(xiàng)屬性.通過(guò)一個(gè)驗(yàn)證實(shí)例可以看出，智能合約可以在合約的不同階段獲得不同的狀態(tài)，當(dāng)智能合約驗(yàn)證時(shí)，SPIN可以隨機(jī)產(chǎn)生若干種不同的結(jié)果.形式化方法可以在智能合約的建立、驗(yàn)證和代碼生成中得到重要應(yīng)用，是智能合約可信和安全性的發(fā)展方向.因此，后續(xù)將會(huì)對(duì)合約的自動(dòng)化代碼生成和一致性測(cè)試作更深入的研究.

(a) 超時(shí)退款

(b) 交易完成圖6 模型模擬結(jié)果

[1]Decentralized autonomous organization:The DAO[EB/OL]. (2016-06-17)[2016-10-10]. https://en.wikipedia.org/wiki/Decentralized_autonomous_organization

[2]Castillo M. DAO Attack[EB/OL]. 2016[2016-10-10]. http://www.coindesk.com/the-dao-just-raised-50-million-but-what-is-it/

[3]Szabo N. Formalizing and securing relationships on public networks[J/OL]. First Monday, 1997, 2(9) [2016-10-10]. http://ojphi.org/ojs/index.php/fm/article/view/548

[4]Miller M S. The digital path: Smart contracts and the third world[EB/OL]. 2003[2016-10-10]. http://www.erights.org/talks/pisa/paper/index.html

[5]Ethereum: A next-generation smart contract and decentralized application platform[OL]. 2014[2016-10-10].https://github. com/ethereum/wiki/wiki/%5BEnglish%5D-White-Paper

[6]Ethereum[EB/OL]. 2014 [2016-10-10]. http://www.ethereum.org/

[7]Formal methods[EB/OL]. 2002[2016-10-10]. http://en.wikipedia.orgi/Formal_ methods

[8]Vidar S, Peter H, Kraemer F A. Model-driven engineering of reliable fault-tolerant systems—A state-of-the-art survey[J]. Advances in Computers, 2013, 91: 119-205

[9]Hyperledger: Blockchain technologies for business[EB/OL]. 2016 [2016-10-10]. https://www.hyperledger.org/[10]OpenTransactions: Smart contracts from open yransactions[EB/OL]. [2016-10-10]. http://opentransactions.org/wiki/index.php?title=Smart_contracts

[11]Kenneth M. Symmetry and model checking[J]. Formal Methods in System Design, 1996, 9(1/2): 105-131

[12]Baier, Christel, Katoen, et al. Principles of Model Checking[M]. Cambridge:MIT Press,2008

[13]朱江. 基于AADL架構(gòu)模型的代碼自動(dòng)生成技術(shù)研究與實(shí)現(xiàn)[D]. 北京: 北京航空航天大學(xué), 2011

[14]張穎蓓. LDP協(xié)議一致性測(cè)試研究與實(shí)現(xiàn)[D]. 長(zhǎng)沙: 國(guó)防科技大學(xué), 2003

[15]Schamann J M. Automated Theorem Proving in Software Engineering[M]. Berlin: Springer, 2001: 546-555

[16]Von Neumann J, Goldstine H H. Planning and coding of problems for an electronic computing instrument[OL]. Institute for Advanced Study, Princeton, New Jersey, 1948 [2016-10-10]. http://publications.ias.edu/sites/default/files/u:13_p:214____Planning_Coding_Problems_v2p3r.pdf

[17]Floyd R W. Assigning meanings to programs[M] //Program Verification.Berlin:Springer, 1967:19-32

[18]Hoare C A R. An axiomatic basis for computer programming[M] //Pioneers and Their Contributions to Software Engineering. Berlin: Springer, 1969: 576-580

[19]Clarke E M, Grumber J O, Peled D A. Model Checking[M]. Cambridge: MIT Press, 1999

[20]Prigent A, Cassez F, Dhaussy P, et al. Extending the translation from SDL to promela[C] //Proc of the 9th Int SPIN Workshop on Model Checking of Software. Berlin: Springer, 2002: 79-94

胡 凱

博士，教授，主要研究方向?yàn)榉植际接?jì)算、區(qū)塊鏈與數(shù)字社會(huì)技術(shù).

hukai@buaa.edu.cn

白曉敏

碩士研究生，主要研究方向?yàn)樾问交椒?、智能合約和區(qū)塊鏈技術(shù).

baixiaomin@buaa.edu.cn

高靈超

高級(jí)工程師，主要研究方向?yàn)橹悄茈娋W(wǎng)、大數(shù)據(jù)、企業(yè)云計(jì)算和區(qū)塊鏈技術(shù).

gaolingchao@sgitg.sgcc.com.cn

董愛(ài)強(qiáng)

碩士研究生，高級(jí)工程師，主要研究方向?yàn)閲?guó)網(wǎng)信息化、大數(shù)據(jù)多維度分析、云環(huán)境下軟建構(gòu)建平臺(tái)和區(qū)塊鏈技術(shù).

dongaiqiang@sgitg.sgcc.com.cn

Formal Verification Method of Smart Contract

Hu Kai1, Bai Xiaomin1, Gao Lingchao2, and Dong Aiqiang2

1(SchoolofComputerScienceandEngineering,BeihangUniversity,Beijing100191)2(BeijingChinaPowerPuhuaInformationTechnologyCo.Ltd,Beijing100192)

Smart contract is a code contract and algorithm contract and will become the basis of future agreements in digital society. Smart Contract utilizes protocols and user interfaces to facilitate all steps of the contracting process. This paper summarized the main technical characteristics of smart contract and existing problems such as trustworthiness and security and proposed that formal method is applied to the smart contract modeling, model checking and model verification to support the large-scale generation of smart contract. In this paper, a formal verification framework and verification method for smart contract in the whole life circle of smart contract has been proposed. The paper presented a smart shopping scene, in which Promela language is used for modeling a SSC(smart shopping contract) and SPIN is used to simulate and model checking to verify the effect of formal method on smart contract.

smart contract; formal method; modeling; verification; SPIN

2016-10-31

國(guó)家自然科學(xué)基金項(xiàng)目(91538202)

白曉敏(baixiaomin@buaa.edu.cn)

TP301