智能合約的形式化驗證方法

胡 凱 白曉敏 高靈超 董愛強

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

智能合約的形式化驗證方法

胡 凱1白曉敏1高靈超2董愛強2

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

(hukai@buaa.edu.cn)

智能合約是一種代碼合約和算法合同，將成為未來數字社會的基礎技術，它利用協議和用戶接口，完成合約過程的所有步驟.總結了智能合約主要技術特點和現存的可信、安全等問題，提出將形式化方法應用于智能合約的建模、模型檢測和模型驗證過程，以支持規模化智能合約的生成.研究提出了一個應用于智能合約生命周期的形式化驗證框架和驗證方法，針對一個智能購物場景，采用Promela建模語言對智能購物合約進行建模，用SPIN進行了模型檢測，驗證了形式化方法對智能合約的作用.

智能合約；形式化方法；建模；驗證；SPIN模型檢測工具

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

“智能合約”(smart contract)[3]這個術語至少可以追溯到1995年,是由密碼學家尼克薩博首次提出的.智能合約是能夠自動執行合約條款的計算機程序，他創造性地提出“智能合約就是執行合約條款的可計算交易協議”.

尼克薩博指出計算機代碼可以代替機械設備，進行更復雜的數字財產交易，未來的某一天，這些程序甚至可能取代處理某些特定金融交易的律師和銀行，“智能財產可以將智能合約內置到物理實體的方式，被創造出來”.比如，房屋出租商將發現智能合約這種用途很有吸引力，一所房屋的門鎖，能由被連接到物聯網上的智能合約打開,所有門鎖都是連接互聯網的.當你為租房進行了一筆交易時，存儲在智能手機中的鑰匙可以為你打開房屋,并進行自動資金轉移.雖然智能合約仍然處于初始階段，但是其潛力顯而易見，因為它把人與法律協議以及網絡之間復雜的關系程序化了.

智能合約有許多非形式化的定義，尼克薩博給出了一個簡短的概念，即“智能合約通過使用協議和用戶接口來促進合約的執行”；Miller[4]認為智能合約就是用程序代碼編寫的合約，它的條款由程序來執行；Ethereum的智能合約就是基于區塊鏈的可直接控制數字資產的程序[5].

總的來說，一個智能合約是一套以數字形式定義的承諾，包括合約參與方可以在上面執行這些承諾的協議.它是能夠自動執行合約條款的計算機程序，被部署在分享的、復制的賬本上，它可以維持自己的狀態，控制自己的資產和對接收到的外界信息或者資產進行回應.承諾指的是合約參與方同意的權利與義務，這些承諾定義了合約的本質和目的.數字形式意味著合約不得不寫入計算機可讀的代碼中.只要參與方達成協議，智能合約建立的權利和義務，是由一臺計算機或者計算機網絡執行完成的.協議是技術實現，在此基礎上，合約承諾被實現，或者合約承諾實現被記錄下來.

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

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

形式化方法[7]是描述系統性質的基于數學的技術，用于計算機軟件的規范、開發和驗證.將形式化方法用于軟件設計，是期望能夠像其他工程學科一樣，使用適當的數學分析以提高設計的可靠性和魯棒性.其中，形式化方法中很重要的一步就是形式化驗證，形式化驗證可以以更正式的方式產生程序.例如，可以進行從規范到程序的屬性或細化的證明.

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

將形式化方法應用于智能合約整個生命周期的流程包括合約設計、自然語言描述、形式化描述、模型驗證、自動代碼生成和一致性測試.本文重點探討形式化描述和形式化驗證可以更好地生成和執行智能合約.其中，形式化描述可以克服自然語言描述的缺點，例如二義性.形式化驗證可以檢查合約中是否存在邏輯錯誤，可以做可達性分析、不變性分析、等價性分析等.

1 智能合約的性質

目前，智能合約處在逐漸的發展中.2015年3月20日，以太坊基金會發布了Ethereum項目，它是一個開源數字貨幣和區塊鏈平臺，為開發者提供在區塊鏈上搭建和發布智能合約的平臺，可用來擔保和交易任何事物.2015年，Linux基金會發起一個推進區塊鏈數字技術和交易驗證的開源項目hyperledger[9]，這是一個區塊鏈和智能合約結合的開源平臺，允許任何人發行個人貨幣，通過權限控制保證了用戶的隱私和交易的安全性.目前有很多機構和學者都是基于以上2個原型系統對智能合約作更深入的研究.

研究智能合約通過協議與用戶界面來促進合約過程的所有步驟，我們提出了一個良好的智能合約，它具備以下6個基本特征：一致性、可定制性、可觀察性、可驗證性、自強制性和接入控制.

1) 一致性.智能合約應與現有法律一致，必須經過具有專業法律知識的專業人士制定審核，不與現有法律沖突，具有法律效應.

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

3) 可觀察性.合約方能夠通過用戶界面去觀察關于合約的所有狀態，包括合約本身及合約執行過程的記錄等.

4) 可驗證性.合約方執行合約的過程是可驗證的.

5) 自強制性.對于違反合約行為的制裁必須是強制性的，這需要把資產變得數字化可控，并且由密碼協議保證其安全.

6) 接入控制.就是指具有相關合約利益的人才能接觸相應的合約信息，即與合約相關的知識、控制、執行都應該作為資產保護起來，只有發生爭執時，才把內容提供給第三方檢驗.

智能合約作為計算法律學的一種新技術，有一個很重要的特性是當條件滿足時可以自動執行相應動作.但這一特性在其他應用領域已經有類似的技術.例如，20世紀80年代的基于知識系統都有這一特性.一個是基于規則的系統，當滿足某個條件時，相應的規則就會被觸發.如果有多個規則同時被觸發，會有相應的解決機制協調這些規則的執行.一個是黑板架構系統，在這個系統中，有多個代理同時監控，當某個條件滿足時，相應的代理會激活自身的規則并執行.

在Open-Transactions[10]中這樣描述智能合約：一個智能合約涉及多個當事人，一旦被激活就能自主運行，它有可執行的代碼；只有被選定的功能可以被激活執行；可操縱那些被明確聲明的合法資產；可暫時存儲資金；合約的狀態值被不斷地更新、記錄.

下面給出一個互聯網智能購物合約的例子.基本合約包括商品訂貨、分銷和售后服務.組合的合約用于連接客戶和商家.

基礎合約:

合約1. 貨物訂購與分配.

合約方：客戶和商家.

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. 售后服務合約.

合約方：客戶和商家.

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

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

1) 如何編制合約雙方認可的模板框架，誰來編程實現合約代碼，并保證代碼的正確性及獲得雙方認可.

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

3) 合約的定制問題. 如何制定好的智能合約模板，根據不同場景定制不同合約，組合多個合約形成復合合約.

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

5) 智能合約執行過程中的可控性和可調度性，要確保執行過程中的可信性和安全性.

下面本文提出采用形式化方法來研究解決這些問題.

2 形式化方法的引入

為解決智能合約上述所提到的問題，本文引入形式化方法，將形式化方法應用于智能合約生成和執行的整個生命周期.

形式化方法[11]是指用數學方法描述和推理基于計算機的系統，直觀地說，就是規范語言+形式推理，在技術上通過精確的數學手段和強大的分析工具得到支持，其表現形式通常有邏輯、離散數學、狀態機等.規范語言包括語法、語義以及滿足關系等，可以分為4類：抽象模型規范法、代數規范法、狀態遷移規范法和公理規范法.

形式化方法主要包括形式規約和形式化驗證.形式規約使用具有精確語法和語義的形式語言刻畫系統的行為和性質，是設計系統的約束和驗證系統是否正確的依據；形式化驗證則是在形式規約的基礎上，建立系統行為及其性質的關系，從而驗證系統是否滿足期望的關鍵性質，主要包括模型檢測和定理證明.

模型檢測[11]是一種重要的自動驗證和分析技術，通過顯式狀態搜索或隱式不動點計算來驗證有窮狀態系統是否滿足預期的性質.模型檢測方法目前已經涵蓋了并發系統模型檢測、實時系統模型檢測、混成系統模型檢測以及概率模型檢測等多個方面.

模型檢測[12]詳細探討了模型中的相關屬性.這不僅對于有限模型是可以實現的，而且對于一些無限模型也是可以實現的，其中無限狀態集合可以通過使用抽象或利用對稱性的優點來表示.通常包括：探索模型中的所有的狀態和轉換，通過使用智能的和領域特定的抽象技術在單個操作中考慮整個狀態組，并減少計算時間.

基于有限狀態機的模型檢驗可以全自動驗證，它可以檢測模型的不同狀態.定理證明需要在一些關鍵路徑進行手動控制，它可以證明程序的正確性.等價驗證主要是驗證設計的一致性，也就是說，設計是否滿足需要，或者程序和合約是否相同.

定理證明技術將系統行為和性質都用邏輯方法來刻畫，基于公理和推理規則組成的形式系統，證明系統是否滿足期望的關鍵性質.而使用定理證明器來輔助證明，相當于將手工證明變成一系列能夠在計算機上自動進行的符號演算，能夠對證明過程進行正確性檢查，從而提高證明的可信度.常用的定理證明器主要有Coq，PVS，Isabelle等.

圖1 智能合約的MDE流程圖

作為形式化方法的工程實踐，模型驅動工程(MDE)旨在提高程序規范中的抽象級別，并增加程序開發的自動化.MDE[8]的思想是使用不同抽象級別的模型用于開發系統，從而提高程序規范中的抽象級別.通過使用可執行模型轉換來增加程序開發中的自動化.較高級別的模型被轉換為較低級別的模型，直到該模型可以使用代碼生成或模型解釋來執行.MDE可以支持智能合約的整個生命周期，從建模、驗證、代碼生成到一致性測試，應用于智能合約的形式化方法流程如圖1所示.

在模型驅動框架下，由于體系結構模型包含的系統特征和信息較多，一般不直接對體系結構模型進行驗證和分析，而主要采用模型轉換的方式，即將體系結構模型(或子集)轉換到另一個形式模型，或者直接轉換到模型檢測工具或定理證明器，目的是為了重用這些已有的驗證和分析能力.

基于模型的代碼自動生成[13]概念源于模型驅動架構 (model driven architecture, MDA).模型到代碼的生成和模型到模型的轉換都是MDA模型轉換的子集.MDA能夠盡早對系統進行分析與驗證，并將驗證后符合需求的模型生成代碼，不僅有助于保證系統的質量屬性，同時能夠促進應用開發的標準化和工業化，并有效控制開發時間與成本.

一致性測試[14]指的是被測系統與標準的一致性，它是一種黑盒測試.通過一致性測試，可以給用戶提供2個信息：通過了一致性測試的合約實現，具有合約所要求的各種能力；在具有代表性的合約實例中，被測試的合約代碼實現的外部特性與標準合約文本的要求一致.

圖2 形式化方法應用框架

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

圖3是將形式化方法應用于智能合約整個生命周期的流程.當需要新的合約時，使用非正式化規范來設計合約，然后使用形式化規范來描述合約以驗證合約.模型檢驗工具可以用來檢查合約，或使用演繹驗證方法來證明合約.其次，可以通過模型工具，將模型自動化生成合約代碼.最后，一致性測試確保文本和程序代碼的一致性.

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

將形式化方法應用于智能合約，使得合約的生成和執行有了規范性約束，保證了合約的可信性，使人們可以信任智能合約的生產過程和執行效力.合約的形式化驗證保證了合約的正確屬性，自動化代碼生成提高了合約的生成效率，合約的一致性測試保證了合約代碼與合約文本的一致性.

3 智能合約的形式化驗證方法

對智能合約的形式化驗證包括形式化描述、形式化驗證、自動代碼生成和一致性測試.本文中，我們重點探討智能合約的形式化描述和形式化驗證方法.

形式化方法的另一個重要研究內容是形式化驗證.形式化驗證與形式化規約之間具有緊密的聯系，形式化驗證就是驗證已有的程序(系統)P是否滿足其規約(φ，ψ)的要求(即P(φ，ψ))，它也是形式化方法所要解決的核心問題[15].

傳統的驗證方法包括模擬和測試，它們都是通過實驗的方法對系統進行查錯.模擬和測試分別在系統抽象模型和實際系統上進行，一般的方法是在系統的某點給予輸入，觀察在另一點的輸出，這些方法花費很大，而且由于實驗所能涵蓋的系統行為有限，很難找出所有潛在的錯誤.基于此，早期的形式驗證主要研究如何使用數學方法，嚴格證明一個程序的正確性(即程序驗證).

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

目前常見的形式化驗證方法主要可分為2類：演繹驗證和模型檢測.其中，早期(20世紀60—70年代)的形式化技術主要采用演繹法證明順序和并發程序正確性，而近期(20世紀80—90年代)則多采用模型檢測方法驗證實時和混成系統.

1) 演繹驗證.演繹驗證是早期采用的主要驗證技術，它基于定理證明的基本思想，采用邏輯公式描述系統及其性質，通過一些公理或推理規則來證明系統具有某些性質.

演繹驗證的優點是可以使用歸納的方法來處理無限狀態的問題，并且證明的中間步驟使用戶對系統和被證明性質有更多的了解.缺點是現有的方法不能做到完全自動化，還需與用戶交互，要求用戶能提供驗證中創造性最強部分的工作.因而演繹證明方法的效率較低，很難用于大系統的驗證.

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

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

模型檢測方法的基本思想是通過狀態空間搜索來確認合約是否具有某些性質.即給定一個合約(程序)P和規約ψ，生成對應的合約模型M，然后證明Mψ，即規約公式ψ在合約模型M中成立，這樣就證明了合約(程序)P滿足規約ψ.

模型檢測方法通常采用Dolev-Yao模型、模態邏輯、有限狀態機和進程代數等理論作為合約分析的理論基礎，其基本思想是用狀態遷移系統S表示系統的行為，用模態時序邏輯公式F描述系統的性質.一般地，一個模型檢測方法主要由特定的形式模型、形式邏輯和相應的模型檢測算法3個方面構成，不同的模型檢測方法具有不同的應用領域.

將模型檢測應用于智能合約以解決合約的可信問題，一般包括以下步驟：

1) 建模.通過選擇合適的建模語言和建模工具，使用模型檢測工具能夠接受的形式語言來描述合約.

2) 描述.闡明所要驗證的合約性質，包括合約的狀態可達性、死鎖、活鎖、有界性等.

3) 驗證.對合約的狀態空間進行搜索，發現合約存在的問題并及時修改，對合約進行迭代驗證.

目前形式化描述技術主要分為2種類型：形式化描述模型和形式化描述語言.通過形式化描述模型，可以獲得抽象的合約模型.形式化描述語言總是基于一種或多種形式化描述模型.形式化描述技術已經有幾十年的發展，目前有多種形式化描述模型和形式化描述語言，如圖4所示.形式化描述語言主要有3種標準：CCITT國際電報電話咨詢委員會(International Telephone and Telegraph Consultative Committee)組織制定的SDL，ISO組織制定的LOTOS和ESTELLE.

形式化描述方法分類內容形式化描述模型狀態變遷模型FSM,EFSM,Petri網模型進程代數通信系統演算(CCS)通信順序進程(CSP)其他時序邏輯(或時態邏輯)(TL)形式化描述語言CCITT組織SDLISO組織LOTOS,ESTELLE其他Promela語言:SPIN(著名模型檢測工具)的輸入語言

圖4 各種形式化描述技術

SPIN是美國貝爾實驗室的形式化方法與驗證小組開發的模型檢測工具.它所關心的主要問題是進程之間的信息能否正確地交互，而不是進程內部的具體細節.由于其良好的性能、完善的文檔、開源及不斷的維護更新服務使得SPIN被廣泛應用于工業界和學術界.它采用的描述語言為Promela[20].

模型檢測主要適用于有窮狀態系統，早期主要用于硬件和協議的驗證.模型檢測的優點是完全自動化并且驗證速度快，即便是只給出了部分描述的合約，通過搜索也可以提供關于已知部分正確性的有用信息.尤其重要的是，在性質未被滿足時，搜索終止可以給出反例，這種信息常常反映出合約設計中的細微失誤，因而對于合約排錯有極大的幫助.

形式化驗證方法可以檢查智能合約的很多屬性，例如，合約的公平性、可達性、有界性、活鎖、死鎖、不可達以及無狀態二義性等.

4 智能合約的驗證實例

在本節中，使用Promela建模語言和檢測工具SPIN來建立和驗證智能購物合約SSC(smart shopping contract)的模型.

SPIN[20]是一個通用的工具，以嚴格的和大多數自動化的方式驗證分布式軟件模型的正確性.它是從1980年開始，由Gerard J. Holzmann和貝爾實驗室計算科學研究中心的原始Unix組的研究人員編寫而成.該軟件自1991年以來一直可用，并繼續遵循該領域的新發展而發展.SPIN是一種著名的分析驗證并發系統邏輯一致性的工具，以其簡潔明了和自動化程度高而備受注目.SPIN已成功應用在安全協議驗證、控制系統驗證、軟件驗證及最優化規劃等領域.

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

SSC應在用戶訂單之后觸發，并且它具有2個參與者，即用戶和商店.

智能購物合約的描述如下：當用戶下訂單時需要將購物所需的資金提交給智能購物合約，智能購物合約暫時持有資金.同時SSC啟動2個子進程:用戶進程和商店進程.用戶進程：如果商家在7天內沒有交貨，用戶將取消交易，SSC會將資金退還給用戶，用戶進程定時、周期地檢測交貨狀態；商店進程：商家收到訂單后，首先系統判斷訂單是否結束，如果訂單沒有超時，則商店發貨.SSC需要確保資金的安全性和交易過程中各個狀態的可達性.

SSC的Promela模型如圖5所示.

使用模型檢測工具SPIN檢測SSC模型，模型的模擬結果如圖6所示.

圖5 SSC的Promela模型

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

如圖6(b)結果所示，當商店在第2天送貨時，SSC將錢轉給商店.實驗結果與預期結果一致.

由于SSC是有限狀態模型，通過對SSC的建模和驗證，SPIN可以隨機生成合約的所有狀態，實驗結果與合約的預期結果一致.

5 結 論

本文針對智能合約存在的可信與安全問題，將形式化方法應用于智能合約的生命周期驗證，從形式化描述和形式化驗證方面進行了詳細的闡述.一個好的模型檢測工具有助于檢查和驗證智能合約的各項屬性.通過一個驗證實例可以看出，智能合約可以在合約的不同階段獲得不同的狀態，當智能合約驗證時，SPIN可以隨機產生若干種不同的結果.形式化方法可以在智能合約的建立、驗證和代碼生成中得到重要應用，是智能合約可信和安全性的發展方向.因此，后續將會對合約的自動化代碼生成和一致性測試作更深入的研究.

(a) 超時退款

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

[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架構模型的代碼自動生成技術研究與實現[D]. 北京: 北京航空航天大學, 2011

[14]張穎蓓. LDP協議一致性測試研究與實現[D]. 長沙: 國防科技大學, 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

胡 凱

博士，教授，主要研究方向為分布式計算、區塊鏈與數字社會技術.

hukai@buaa.edu.cn

白曉敏

碩士研究生，主要研究方向為形式化方法、智能合約和區塊鏈技術.

baixiaomin@buaa.edu.cn

高靈超

高級工程師，主要研究方向為智能電網、大數據、企業云計算和區塊鏈技術.

gaolingchao@sgitg.sgcc.com.cn

董愛強

碩士研究生，高級工程師，主要研究方向為國網信息化、大數據多維度分析、云環境下軟建構建平臺和區塊鏈技術.

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

國家自然科學基金項目(91538202)

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

TP301