包玉龍，朱雪陽*，張文輝，孫鵬飛，趙穎琪

（1.計(jì)算機(jī)科學(xué)國家重點(diǎn)實(shí)驗(yàn)室（中國科學(xué)院軟件研究所），北京 100190；2.中國科學(xué)院大學(xué)，北京 100049）

0 引言

隨著藍(lán)牙、WiFi、網(wǎng)絡(luò)等飛速發(fā)展，越來越多設(shè)備，如傳感器和執(zhí)行器，已連接到網(wǎng)絡(luò)，形成了物聯(lián)網(wǎng)（Internet of Things，IoT）［1-2］。物理對(duì)象無處不在的互聯(lián)顯著加速了數(shù)據(jù)收集、聚合和共享，使得IoT 成為智能醫(yī)療、智能交通、家庭自動(dòng)化等［3-4］應(yīng)用的最基本架構(gòu)之一。但是，這樣的互聯(lián)也可能會(huì)給IoT 系統(tǒng)帶來嚴(yán)重的安全問題［5-6］。若系統(tǒng)無安全的訪問控制，通過入侵系統(tǒng)，未經(jīng)授權(quán)的實(shí)體（攻擊者）只需簡單部署自己的資源，就可以非法訪問現(xiàn)有的物聯(lián)網(wǎng)中的設(shè)備，給用戶帶來損失。因此，物聯(lián)網(wǎng)的訪問控制問題得到學(xué)術(shù)界和工業(yè)界的廣泛關(guān)注［7-9］。

傳統(tǒng)的物聯(lián)網(wǎng)訪問控制方案主要建立在訪問控制模型上，包括基于角色的訪問控制（Role-Based Access Control，RBAC）模型［10］、基于屬性的訪問控制（Attribute-Based Access Control，ABAC）模型［11］、基于能力的訪問控制（Capability-Based Access Control，CapBAC）模型［12］。但是在以上方案中，驗(yàn)證對(duì)象的訪問權(quán)限通常是由中心節(jié)點(diǎn)進(jìn)行的，一旦中心節(jié)點(diǎn)出現(xiàn)故障或者漏洞，整個(gè)訪問控制系統(tǒng)就會(huì)出現(xiàn)問題。為了避免中心節(jié)點(diǎn)故障導(dǎo)致系統(tǒng)出現(xiàn)問題，最近有學(xué)者基于CapBAC 提出了分布式CapBAC 模型［13］，其中訪問權(quán)限驗(yàn)證是由請求的IoT 對(duì)象本身而不是中心節(jié)點(diǎn)執(zhí)行的。但是，物聯(lián)網(wǎng)對(duì)象通常功能較弱，很容易受到入侵者的破壞，因此不能完全信任它們作為訪問權(quán)限驗(yàn)證實(shí)體，所以，分布式CapBAC 模型仍無法很好解決不可信賴的IoT環(huán)境中的訪問控制問題。

區(qū)塊鏈及智能合約的出現(xiàn)給研究人員帶來了解決分布式網(wǎng)絡(luò)中不信任問題的新思路［14-16］。區(qū)塊鏈具有高度透明、去中心化、去信任、不可篡改、匿名等特征。智能合約（Smart Contract，SC）是執(zhí)行合約條款的計(jì)算機(jī)交易協(xié)議，部署在區(qū)塊鏈上的智能合約可以按照預(yù)寫入的邏輯在區(qū)塊鏈上執(zhí)行，同時(shí)由區(qū)塊鏈平臺(tái)、分布式網(wǎng)絡(luò)中的各個(gè)節(jié)點(diǎn)及共識(shí)協(xié)議來保證合約執(zhí)行的正確性。

區(qū)塊鏈平臺(tái)的可信賴性能夠保證正確執(zhí)行智能合約，但無法保證合約代碼的正確性。實(shí)際上，在實(shí)踐中部署的大量合約都存在軟件漏洞，這些漏洞通常是由合約編寫者對(duì)基本執(zhí)行語義和智能合約的實(shí)際語義所做的假設(shè)之間的語義差距引入的。最近有學(xué)者對(duì)部署在以太坊公共區(qū)塊鏈上的19 336個(gè)合約進(jìn)行的自動(dòng)化分析發(fā)現(xiàn)，有8 333個(gè)合約至少有一個(gè)潛在的安全問題［17］。盡管并非所有這些問題都導(dǎo)致安全漏洞，但其中許多漏洞都可以被用來竊取例如加密貨幣等數(shù)字資產(chǎn)。智能合約的漏洞導(dǎo)致過嚴(yán)重安全事件。例如，“權(quán)力下放的自治組織（Decentralized Autonomous Organization，DAO）攻擊”導(dǎo)致價(jià)值5 000 萬美元的加密貨幣被盜［18］；2017 年多簽名奇偶校驗(yàn)錢包庫的黑客攻擊，導(dǎo)致約2.8 億美元的電子貨幣損失［19］。由于區(qū)塊鏈的不可篡改性，為了讓智能合約提供正確和安全的功能，在部署前對(duì)智能合約進(jìn)行驗(yàn)證是至關(guān)重要的。

為了解決智能合約本身的安全問題，已有學(xué)者探索了多種方法，例如靜態(tài)分析［20-21］或使用形式驗(yàn)證技術(shù)和博弈論［22-26］進(jìn)行模型檢測。這些方法都側(cè)重于研究基于單個(gè)智能合約構(gòu)建的系統(tǒng)的正確性，未考慮用戶對(duì)合約的調(diào)用次序，并且很少關(guān)注基于合約交互及在一定次序調(diào)用下的系統(tǒng)的正確性。對(duì)于IoT 的訪問控制系統(tǒng)而言，這樣的研究尤其重要，在此類系統(tǒng)中，按一定次序調(diào)用合約且不同物理設(shè)備間的智能合約能夠進(jìn)行交互，可以實(shí)現(xiàn)不同的業(yè)務(wù)目標(biāo)。

本文提出了一種對(duì)智能合約和區(qū)塊鏈執(zhí)行協(xié)議以及用戶調(diào)用次序行為進(jìn)行形式化建模的新方法。本文利用狀態(tài)遷移系統(tǒng)作為形式化建模語言，用計(jì)算樹邏輯（Computation Tree Logic，CTL）［27］描述其期望的性質(zhì)，并使用模型檢測［28］工具Verds［29］進(jìn)行驗(yàn)證。最后基于一個(gè)資源訪問控制智能合約實(shí)例［30］來介紹本文方法，并用另外一個(gè)實(shí)例［31］來展示本文方法的適用性。

本文主要工作如下：

1）提出了一種對(duì)智能合約、區(qū)塊鏈執(zhí)行協(xié)議以及用戶調(diào)用次序行為進(jìn)行形式建模的新方法；

2）基于上述形式建模，實(shí)現(xiàn)Solidity 到模型檢測工具Verds輸入語言的轉(zhuǎn)換，并利用Verds對(duì)期望的性質(zhì)進(jìn)行驗(yàn)證；

3）對(duì)兩個(gè)實(shí)際案例進(jìn)行實(shí)例研究，并對(duì)比兩個(gè)案例的驗(yàn)證結(jié)果。

1 相關(guān)工作

在訪問控制驗(yàn)證方面，Hu 等［32］針對(duì)RBAC 模型和模型相應(yīng)的策略進(jìn)行安全性質(zhì)驗(yàn)證，將RCL2000 語言表示的RBAC模型轉(zhuǎn)化為Alloy語言表示，利用Alloy及其自帶的Analyzer對(duì)模型進(jìn)行分析驗(yàn)證，驗(yàn)證內(nèi)容包括模型中函數(shù)功能驗(yàn)證以及約束驗(yàn)證（Constraint Verification），驗(yàn)證的對(duì)象包括模型本身以及模型部署后的代碼。在驗(yàn)證過程中通過反例生成相應(yīng)的測試用例，后續(xù)提供給模型進(jìn)行測試。Hu等［33］又使用相同的方法驗(yàn)證了強(qiáng)制訪問控制（Mandatory Access Control）的通用性質(zhì)。

在智能合約驗(yàn)證方面，Nehai等［25］提出了一種基于智能合約的以太坊應(yīng)用的驗(yàn)證方法。該方法分為三層：1）代表智能合約行為的內(nèi)核層；2）對(duì)智能合約邏輯建模的應(yīng)用層；3）對(duì)以太坊執(zhí)行框架建模的環(huán)境層。一組建模規(guī)則用于將智能合約的Solidity 代碼轉(zhuǎn)換為模型檢查語言。然后，用CTL 形式化用英語編寫的系統(tǒng)要求和性質(zhì)，并將其應(yīng)用于生成的檢測模型。研究人員通過能源市場領(lǐng)域的案例研究說明了該方法的適用性。

Mavridou 等［34］開發(fā)了VeriSolid 框架，該框架驗(yàn)證合約模型及相關(guān)性質(zhì)準(zhǔn)確性，從而設(shè)計(jì)正確的Solidity 智能合約。VeriSolid 可以用作智能合約開發(fā)人員的工具，以有限狀態(tài)機(jī)（Finite State Machine，F(xiàn)SM）的抽象形式手動(dòng)指定其需求。VeriSolid 使用行為交互優(yōu)先級(jí)（Behavior Interaction Priority，BIP）工具從給定的FSM中提取合約的行為模型。使用CTL指定系統(tǒng)要求。模型檢測工具（NuSMV）用于驗(yàn)證BIP 行為模型和指定的CTL 性質(zhì)的正確性。在驗(yàn)證了系統(tǒng)設(shè)計(jì)之后，VeriSolid 為該系統(tǒng)生成了Solidity 代碼，可以直接在以太坊平臺(tái)中進(jìn)行部署。

Bhargavan 等［23］介紹了一種通過將Solidity 和以太坊虛擬機(jī)（Ethereum Vitual Machine，EVM）字節(jié)碼合約轉(zhuǎn)為功能編程語言F*描述模型來檢測以太坊智能合約代碼中的缺陷的新穎框架。Abdellatif 等［24］提出的方法利用模型檢測語言對(duì)智能合約、區(qū)塊鏈執(zhí)行環(huán)境和用戶行為進(jìn)行建模。然后，使用現(xiàn)成的統(tǒng)計(jì)模型檢測工具檢查生成的模型，從而分析智能合約的設(shè)計(jì)漏洞。他們通過對(duì)簡單的名稱注冊智能合約案例的研究證明了該方法的適用性。Alqahtani 等［26］提出的方法基于BIP對(duì)智能合約的交互進(jìn)行建模，然后使用模型檢測工具對(duì)BIP模型進(jìn)行轉(zhuǎn)換驗(yàn)證。他們通過對(duì)供應(yīng)鏈管理智能合約案例的研究證明了該方法的適用性。

與傳統(tǒng)的訪問控制驗(yàn)證相比，本文方法不局限于特定的訪問控制模型；與現(xiàn)有的智能合約驗(yàn)證方法相比較，本文方法能夠模擬不同合約之間的交互，且能對(duì)用戶的調(diào)用順序進(jìn)行模擬。

2 準(zhǔn)備知識(shí)

2.1 智能合約與訪問控制

自從中本聰2009 年提出了比特幣的概念［35］，區(qū)塊鏈的概念逐漸進(jìn)入各個(gè)研究領(lǐng)域的視野。作為一個(gè)維護(hù)公共賬本的分布式協(xié)議，區(qū)塊鏈具有高度透明、去中心化、去信任、不可篡改、匿名等特征。早期的區(qū)塊鏈平臺(tái)如比特幣，僅關(guān)注于加密貨幣和支付系統(tǒng)。以太坊是一種開源的公共區(qū)塊鏈平臺(tái)，和比特幣平臺(tái)相比，它進(jìn)一步支持了智能合約，實(shí)現(xiàn)了一種稱為Solidity［36］的圖靈完備的智能合約語言。它提供了去中心化的以太坊虛擬機(jī)（Ethereum Vitual Machine，EVM），以通過其獨(dú)特的加密貨幣以太幣處理點(diǎn)對(duì)點(diǎn)合約。

以太坊區(qū)塊鏈的智能合約一般來說是一組函數(shù)，用戶通過調(diào)用合約函數(shù)將交易發(fā)送到以太坊網(wǎng)絡(luò)，以便：1）創(chuàng)建新合約；2）調(diào)用合約功能；3）將以太幣轉(zhuǎn)讓給合約或其他用戶。所有交易均記錄在每個(gè)參與共識(shí)的節(jié)點(diǎn)上，區(qū)塊鏈上的交易順序決定了每個(gè)合約的狀態(tài)以及每個(gè)用戶的余額。

智能合約類似并發(fā)對(duì)象［37］，和通常程序不同的是，它的并發(fā)不是停留在內(nèi)存中，而是存在整個(gè)區(qū)塊鏈上。而和傳統(tǒng)的并發(fā)不同的是，由于交易的計(jì)算模型，智能合約的方法執(zhí)行是原子的。也就是說，對(duì)合約的單次調(diào)用（或?qū)Ρ舜苏{(diào)用的一系列合約的調(diào)用鏈）按順序執(zhí)行（無中斷），在成功更新區(qū)塊鏈后終止或中止并回滾到調(diào)用之前的狀態(tài)；合約之間的相互調(diào)用也可以被認(rèn)為是單線程，即當(dāng)A 合約調(diào)用B 合約時(shí)，A 合約會(huì)暫停執(zhí)行，B 合約返回時(shí)B 合約會(huì)暫停執(zhí)行，A 合約重新恢復(fù)運(yùn)行。盡管智能合約的方法執(zhí)行是原子的，但是包含在區(qū)塊內(nèi)的交易順序無法確定，而交易的結(jié)果很大程度上取決于其他交易的順序。由此導(dǎo)致的不確定性可以看作一種特殊的并發(fā)。

一個(gè)簡單Solidity 合約SimpleBank 如下所示，包含了以太坊智能合約的最典型屬性。

一個(gè)合約可以包含狀態(tài)變量，狀態(tài)變量會(huì)持久化存儲(chǔ)在區(qū)塊鏈中，SimpleBank 合約中的狀態(tài)變量包括balances，它是一個(gè)address 類型到256 位整型的映射。Solidity 支持的更多值類型包括布爾型、有符號(hào)和無符號(hào)整型、地址類型、數(shù)組類型、枚舉類型和結(jié)構(gòu)體類型等。一旦合約被部署后，一個(gè)地址就會(huì)賦值到SimpleBank 的實(shí)例，由于該合約沒有提供構(gòu)造函數(shù)，所以其狀態(tài)變量會(huì)被賦值為默認(rèn)值。合約定義了可以對(duì)其狀態(tài)進(jìn)行操作的相關(guān)函數(shù)，函數(shù)可以將數(shù)據(jù)作為參數(shù)接收、執(zhí)行計(jì)算、操作狀態(tài)變量及與其他賬戶進(jìn)行交互。除了聲明的參數(shù)外，函數(shù)還接收一個(gè)包含事物詳細(xì)信息的msg 結(jié)構(gòu)。該示例合約代碼中定義了兩個(gè)函數(shù)deposit（）和withdraw（）。其中deposit（）函數(shù)被標(biāo)記為public 和payable，這意味著任何人都可以調(diào)用deposit（）函數(shù)，并且允許該函數(shù)在調(diào)用中接收以太幣，該函數(shù)從msg.value 中讀取接收到的以太幣數(shù)量，并將其加到調(diào)用者對(duì)應(yīng)地址的balances 中，調(diào)用者的地址可以從msg.sender 中讀取。withdraw（）函數(shù)允許調(diào)用者取出存在合約中的以太幣。該函數(shù)首先使用require 語句去檢查調(diào)用者的存款是否充足，若require 條件失敗，則該事件會(huì)失敗并且不會(huì)生效；否則，調(diào)用者會(huì)通過call 方法取回自己存款的一部分，如果call方法失敗，整個(gè)交易將回滾。

以下通過一個(gè)資源訪問控制智能合約案例［30］來介紹IoT系統(tǒng)所期望的訪問控制。該合約實(shí)現(xiàn)了IoT 中資源（數(shù)據(jù)、服務(wù)、存儲(chǔ)、計(jì)算等資源）的訪問控制。下面展示了該實(shí)例中的兩個(gè)智能合約：

1）錯(cuò)誤行為處罰合約——JC（Judge Contract）合約。在JC中含有錯(cuò)誤行為懲罰的主要函數(shù)。JC 函數(shù)主要變量及函數(shù)解釋：

2）訪問控制合約——ACC（Access Control Contract）合約。在ACC 合約中含有訪問控制的主要函數(shù)，包括添加訪問策略、修改訪問策略、修改配置策略、配置信息及申請?jiān)L問合約。ACC合約主要變量及函數(shù)解釋：

通過上面兩個(gè)合約偽代碼可以看出，訪問控制包括兩部分：訪問權(quán)限檢查及訪問權(quán)限修改更新。綜合來看，訪問控制合約應(yīng)當(dāng)滿足以下三個(gè)基本性質(zhì)：

1）無訪問權(quán)限的用戶無法訪問；

2）有訪問權(quán)限的用戶能夠訪問；

3）特定用戶（如管理員、合約創(chuàng)建者、資源擁有者等）才能修改（增、刪、改）訪問策略，一般用戶無法修改。

2.2 模型檢測工具Verds

模型檢測是一種形式化技術(shù)，早期用于硬件及協(xié)議的相關(guān)性質(zhì)驗(yàn)證，現(xiàn)在可被用于分析具有較大可達(dá)狀態(tài)空間的軟件系統(tǒng)規(guī)范。模型檢測的基本思想是用狀態(tài)遷移系統(tǒng)（S）表示并發(fā)系統(tǒng)的行為，用模態(tài)/時(shí)序式（F）描述系統(tǒng)的性質(zhì)。這樣，就可以把系統(tǒng)是否具有所期望的性質(zhì)問題轉(zhuǎn)化為S 是否是F 的模型問題。對(duì)于有窮狀態(tài)系統(tǒng)，這個(gè)問題是算法可判定的。與其他驗(yàn)證方法相比，模型檢測有兩個(gè)顯著的特點(diǎn)：一是可以自動(dòng)進(jìn)行，無須人工干預(yù)；二是在系統(tǒng)不滿足所要求的性質(zhì)時(shí)，可以生成反例。這兩個(gè)特點(diǎn)對(duì)模型檢測在實(shí)際應(yīng)用中的成功起了至為重要的作用。

Verds［29］是一款模型檢測工具，它的實(shí)現(xiàn)包含兩種技術(shù)，分別為傳統(tǒng)的符號(hào)模型檢查［38］和有界正確性檢查［39-40］。后者可以看作是有界模型檢查的擴(kuò)展，是對(duì)傳統(tǒng)符號(hào)模型檢查的補(bǔ)充。該工具的形式模型是衛(wèi)式狀態(tài)遷移系統(tǒng)（guarded command Transition System，TS）［41］，性質(zhì)用CTL 表示。Verds已在多方面得到應(yīng)用，如對(duì)C 程序的驗(yàn)證，對(duì)SystemC 設(shè)計(jì)的驗(yàn)證以及對(duì)多代理系統(tǒng)的驗(yàn)證［42-43］。

CTL 語法及語義：設(shè)AP為命題符號(hào)集合，p為AP集合中的一個(gè)命題，則在AP上的CTL公式集合Φ定義如下：

其中：Φ為CTL 公式；Ψ為輔助路徑公式。CTL 公式的事態(tài)操作符由路徑算子和時(shí)態(tài)算子組成。其中路徑算子有兩種：AΨ表示對(duì)所有的路徑都應(yīng)成立，EΨ表示至少存在一條及以上的路徑使得成立。時(shí)態(tài)算子由X、F、G、U組成，本文中用到的時(shí)態(tài)算子有F、G、U三種，其中：FΦ為在當(dāng)前路徑下Φ最終會(huì)在某個(gè)狀態(tài)為真；GΦ為對(duì)當(dāng)前路徑下所有狀態(tài)中Φ都應(yīng)被滿足；Φ1∪Φ2為當(dāng)前路徑下，Φ1會(huì)一直滿足，直到Φ2滿足。

Verds 的輸入語言稱為VML 語言［44］。一個(gè)Verds 驗(yàn)證模型（Verds Verification Model，VVM）包含全局變量定義、進(jìn)程定義、進(jìn)程實(shí)例化及性質(zhì)描述四個(gè)部分。下面用VML 語言描述了一個(gè)簡單的VVM：

在該模型中，定義了一個(gè)進(jìn)程p0mod（i）（關(guān)鍵字MODULE 引出，第11）～15）行，其中第12）行定義了進(jìn)程內(nèi)部的局部變量，第13）行定義了局部變量的初始值，第14）～15）行描述了進(jìn)程內(nèi)狀態(tài)的遷移。在PROC 關(guān)鍵字下（第5）～6）行）實(shí)例化了兩個(gè)進(jìn)程，其中：p0 進(jìn)程將i賦值成0，p1 進(jìn)程將i賦值成1。除此之外，有一個(gè)兩個(gè)進(jìn)程共享的變量z（第2）行定義，第3）行初始化）和期望系統(tǒng)保持的三個(gè)性質(zhì)（第8）～10）行定義）。實(shí)例化的兩個(gè)進(jìn)程的遷移系統(tǒng)如圖1所示。

圖1 example1狀態(tài)遷移系統(tǒng)Fig.1 State transition system for example1

對(duì)于Verds 工具的形式化模型衛(wèi)式狀態(tài)遷移系統(tǒng)TS，由一個(gè)多元組(S，s0，Act，G，→)來表示，其中：

1）S表示TS中所有狀態(tài)，是所有變量取值的集合；

2）s0表示初始狀態(tài)；

3）Act表示動(dòng)作的集合；

4）G表示衛(wèi)式條件及Guard的集合；

5）→?S×Act×S為遷移關(guān)系。

同樣，對(duì)于當(dāng)前狀態(tài)s下的某個(gè)變量i（i=0，1，2，3)的值，可以由s.i表示，到下一個(gè)狀態(tài)的Guard 和動(dòng)作可以由s.guard和s.act來表示。對(duì)于圖1中的狀態(tài)遷移系統(tǒng)TS(p0)，其S為變量(x，z)取值的集合，初始狀態(tài)為(x，z)=(0，0)，從狀態(tài)(x，z)=(0，0)到狀態(tài)(x，y)=(1，1)的遷移衛(wèi)式條件為(x，z)=(0，0)，其動(dòng)作為(x，z)：=(x+1，1-0)。對(duì)于示例example1，一個(gè)完整的VVM 是由TS(p0) 和TS(p1) 并發(fā)組成，若將MODULEp0mod（i）實(shí)例化四個(gè)進(jìn)程，那么整個(gè)模型就是TS(p0)、TS(p1)、TS(p2)及TS(p3)的并發(fā)。

3 基本框架

本文工作的總體框架如圖2所示。通過將Solidity編寫的智能合約、進(jìn)程的實(shí)例及需要驗(yàn)證的性質(zhì)轉(zhuǎn)換成VVM，然后使用Verds 模型檢測工具可以驗(yàn)證性質(zhì)是否為真。在本文方法中，Solidity 編寫的智能合約文件作為輸入文件，然后在步驟一中，使用狀態(tài)遷移模型對(duì)合約中的所有函數(shù)進(jìn)行形式化定義；接著在步驟二中，針對(duì)用戶的不同調(diào)用場景，對(duì)進(jìn)程進(jìn)行實(shí)例化；然后，步驟三針對(duì)不同調(diào)用場景，使用CTL 語言對(duì)期望系統(tǒng)保持的性質(zhì)進(jìn)行形式化描述，再將前三個(gè)步驟得到的結(jié)果形成VVM，最后使用Verds 工具進(jìn)行驗(yàn)證，若步驟三中定義性質(zhì)不滿足，Verds將生成一個(gè)反例文件。

圖2 整體框架Fig.2 Overall framework

4 訪問控制權(quán)限驗(yàn)證

為了介紹本文方法，使用2.1 節(jié)中的資源訪問控制智能合約作為案例，闡述第3章中整體框架的三個(gè)步驟。

4.1 智能合約建模

使用一個(gè)雙元組(Q，F(xiàn))表示智能合約，其中：Q表示合約中的全局變量的集合；F表示合約中的函數(shù)集合。將智能合約的建模分成兩部分：第一部分為合約函數(shù)形式化，第二部分為函數(shù)外部調(diào)用接口描述。在第一部分中，對(duì)于F集合中的每一個(gè)函數(shù)f，將其映射為一個(gè)TS，本文使用一個(gè)二元組(P，R)來表示f中的帶標(biāo)號(hào)的程序語句集合，其中：P表示函數(shù)中程序語句的標(biāo)號(hào)，其值域?yàn)? 到函數(shù)中的程序語句總數(shù)；R表示函數(shù)中的所有語句的集合，包含簡單賦值語句、條件語句、循環(huán)語句、異常語句、返回語句。同時(shí)，本文使用R(p)來表示標(biāo)號(hào)為p的語句。

同時(shí)，為了使得TS的遷移順序同Solidity合約函數(shù)的執(zhí)行順序一致，在每個(gè)函數(shù)的TS中添加了變量pc，其值等同于函數(shù)中當(dāng)前執(zhí)行程序語句的標(biāo)號(hào)，所以每個(gè)函數(shù)的TS的狀態(tài)為所有變量及pc值的集合。其映射函數(shù)ts=funcMap(f)算法如下所示。

算法1 funcMap。

使用算法ts=funcMap(f)把上文中的policyUpdate（）函數(shù)轉(zhuǎn)換成圖3所示的狀態(tài)遷移系統(tǒng)。例如第4）行的條件語句轉(zhuǎn)變?yōu)楫?dāng)條件為真時(shí)pc=3向pc=4遷移的狀態(tài)，當(dāng)條件為假時(shí)pc=3向pc=6遷移的狀態(tài)。

在第二部分，將合約中的所有函數(shù)描述成一個(gè)函數(shù)外部調(diào)用接口圖。當(dāng)合約被部署到區(qū)塊鏈上后，合約處于idle 狀態(tài)。合約處于idle 狀態(tài)的含義是指合約被部署到鏈上并已經(jīng)執(zhí)行完畢構(gòu)造函數(shù)，并且當(dāng)合約處于該狀態(tài)時(shí)用戶可以調(diào)用除構(gòu)造函數(shù)外的其他函數(shù)，待函數(shù)執(zhí)行完畢后合約重新進(jìn)入idle狀態(tài)。

圖3 policyUpdate函數(shù)的狀態(tài)遷移模型Fig.3 State transition system for policyUpdate function

根據(jù)以上規(guī)則，可以將資源訪問控制智能合約案例描述成如圖4所示的函數(shù)外部調(diào)用接口圖。

圖4 ACC合約函數(shù)外部調(diào)用接口圖Fig.4 Function external call interface diagram for ACC contract

ACC合約有6個(gè)狀態(tài)：

1）idle：ACC 合約被部署到區(qū)塊鏈上，構(gòu)造函數(shù)已執(zhí)行完畢；

2）添加訪問策略：ACC 合約擁有者調(diào)用policyAdd（）函數(shù)，添加新的訪問策略，執(zhí)行完之后返回idle狀態(tài)；

3）更新訪問權(quán)限：調(diào)用policyUpdate（）函數(shù)，更新訪問權(quán)限，執(zhí)行完之后返回idle狀態(tài)；

4）更新最小訪問時(shí)間間隔：調(diào)用minIntervalUpdate（），更新最小時(shí)間間隔，執(zhí)行完之后返回idle狀態(tài)；

5）更新訪問閾值：調(diào)用thresholdUpdate（），更新訪問閾值，執(zhí)行完之后返回idle狀態(tài)；

6）訪問申請：用戶調(diào)用accessControl（）方法，申請以特定方式訪問資源，獲得返回結(jié)果，之后返回idle狀態(tài)。

由于調(diào)用合約函數(shù)產(chǎn)生的交易在以太坊虛擬機(jī)上是以類似單線程的方式執(zhí)行，本文使用一個(gè)全局布爾型變量process_control 來模擬，該變量初始值為False，當(dāng)構(gòu)造函數(shù)執(zhí)行完畢后，它被賦值為True，除構(gòu)造函數(shù)外其余所有實(shí)例化進(jìn)程在未執(zhí)行前均在等待該變量值為True，一旦該變量值為True，等待的所有進(jìn)程將有一個(gè)進(jìn)程獲取到執(zhí)行權(quán)限，開始執(zhí)行且同時(shí)將該變量的值設(shè)置為False，待執(zhí)行完畢后將該變量的值設(shè)置為True。

而區(qū)塊鏈上合約互相調(diào)用的執(zhí)行模型也可以被認(rèn)為是順序執(zhí)行，當(dāng)調(diào)用者處于執(zhí)行狀態(tài)時(shí)，被調(diào)用者處于休眠狀態(tài)，當(dāng)被調(diào)用處于執(zhí)行狀態(tài)時(shí)，調(diào)用者處于休眠狀態(tài)。每次交互時(shí)，用VVM 中兩個(gè)全局布爾變量來模擬此過程，即call_start、call_end。當(dāng)合約A 調(diào)用者調(diào)用函數(shù)f1 并運(yùn)行至調(diào)用函數(shù)f2時(shí)，令call_start=True，此時(shí)f1 暫停執(zhí)行，函數(shù)f2 在此之前一直處于等待狀態(tài)，并在檢測到call_start=True 時(shí)才開始執(zhí)行，當(dāng)f2執(zhí)行完畢時(shí)，令call_end=True，此時(shí)f1恢復(fù)執(zhí)行。

4.2 場景定義

由于模型檢測為一個(gè)閉系統(tǒng)，所以在VVM 中，需要對(duì)已定義好的模塊進(jìn)行實(shí)例化來模擬用戶對(duì)合約函數(shù)的調(diào)用。而模型檢測中所有實(shí)例化的模塊均為并發(fā)執(zhí)行，但在現(xiàn)實(shí)世界中，用戶一般按照自己的邏輯去調(diào)用合約中的函數(shù)，同時(shí)由于區(qū)塊鏈的特性，用戶可以查看鏈上數(shù)據(jù)，所以用戶可以等待鏈上特定事件發(fā)生后或者特定狀態(tài)后再去調(diào)用合約中的函數(shù)，而且在模擬用戶調(diào)用順序的同時(shí)，也需要模擬在多個(gè)用戶調(diào)用之間存在的并發(fā)行為。

在資源訪問控制智能合約案例中，用戶可以在合約擁有者部署合約并且添加完訪問策略之后進(jìn)行訪問，也可以在合約擁有者調(diào)用policyUpdate（）去更新訪問策略時(shí)去進(jìn)行訪問。如圖5 所示，擁有者可以先部署合約，然后合約擁有者調(diào)用三次policyAdd（）函數(shù)添加訪問控制策略，然后在這三次調(diào)用執(zhí)行完畢后，用戶調(diào)用policyUpdate（）函數(shù)并且與此同時(shí)用戶調(diào)用accessControl（）函數(shù)。函數(shù)Constructor（p1，p2）的含義是將合約變量owner 設(shè)置為p1，object 設(shè)置為p1，subject 設(shè)置為p2；函數(shù)policyAdd（p1，p2，p3，p4，p5，p6）的含義是讓地址為subject 的用戶對(duì)p2 號(hào)資源在p5 時(shí)間內(nèi)最多有p4 權(quán)限訪問p6次，p1 為該函數(shù)的調(diào)用者；函數(shù)policyUpdate（p1，p2，p3，p4）的含義為將subject 地址的用戶對(duì)p2 號(hào)資源p3 號(hào)操作的權(quán)限更新為p4，p1 為該函數(shù)的調(diào)用者；函數(shù)accessControl（p1，p2，p3，p4）的含義為p1號(hào)地址在p4時(shí)間點(diǎn)對(duì)p2號(hào)資源進(jìn)行p3操作。

在VVM 中，若不加以控制，則所有實(shí)例化的進(jìn)程均為并發(fā)執(zhí)行，所以，本文使用全局變量order、level［i］及進(jìn)程processordercontrol（）來控制進(jìn)程的執(zhí)行順序。其中：order表示執(zhí)行序號(hào)，值的范圍為0 到4 且初始值為0；level［i］為當(dāng)前執(zhí)行序號(hào)下有多少進(jìn)程已經(jīng)開始執(zhí)行且初始值為0；進(jìn)程processordercontrol（）的作用是待當(dāng)前執(zhí)行序號(hào)下所有進(jìn)程執(zhí)行完后，將執(zhí)行序號(hào)更改為下一個(gè)執(zhí)行序號(hào)。如在圖5 所示的調(diào)用順序場景中，accessControl（）進(jìn)程的執(zhí)行序號(hào)為3，且accessControl（）等待order=3 時(shí)才可開始執(zhí)行，如當(dāng)三個(gè)policyAdd（）均執(zhí)行完時(shí)level［2］=3。

圖5 ACC合約調(diào)用順序定義Fig.5 Call order definition of ACC contract

4.3 性質(zhì)形式化

本文方法將整個(gè)合約中的所有函數(shù)均建模成一個(gè)個(gè)VVM 中的模塊，同時(shí)對(duì)應(yīng)具體場景進(jìn)行實(shí)例化及執(zhí)行順序定義；最后，根據(jù)不同的場景，使用CTL 描述期望系統(tǒng)保持的性質(zhì)。對(duì)于權(quán)限訪問控制應(yīng)用，應(yīng)準(zhǔn)許所有符合規(guī)則特定約束的訪問請求，而所有未遵循的訪問請求都應(yīng)被拒絕。

在資源訪問控制智能合約案例做進(jìn)程描述時(shí)，使用function（msg_ender，parameters）來表示用戶msg_sender 發(fā)起交易，調(diào)用函數(shù)function（），即代表VVM 中function 模塊實(shí)例化，函數(shù)本身實(shí)現(xiàn)參數(shù)列表為parameters，同時(shí)使用UML活動(dòng)圖來描述用戶的調(diào)用順序。

圖6 模擬了用戶在具有訪問權(quán)限且無違規(guī)行為的情況下能夠正常獲取訪問權(quán)限的場景，函數(shù)實(shí)例化及調(diào)用順序如圖6 所示，在該場景中實(shí)例化了三個(gè)進(jìn)程及其對(duì)應(yīng)的執(zhí)行順序：第一個(gè)執(zhí)行的是進(jìn)程p0：constructor（1，2），作用為將合約的owner 設(shè)置為1，subject 設(shè)置為2；第二個(gè)執(zhí)行的是進(jìn)程p1：policyAdd（1，1，1，1，2，2），作用為1號(hào)地址調(diào)用該函數(shù)，將2號(hào)地址設(shè)置可以在2 個(gè)時(shí)間間隔內(nèi)對(duì)1 號(hào)資源執(zhí)行2 次讀操作（讀操作用1 表示）；第三個(gè)執(zhí)行的進(jìn)程為p3：accessControl（2，1，1，2），作用為2 號(hào)地址請求在時(shí)間2 時(shí)對(duì)1 號(hào)資源進(jìn)行讀操作。

圖6 場景1 Fig.6 Scenario 1

在該案例性質(zhì)形式化時(shí)，errcode表示最終獲取訪問權(quán)限的結(jié)果：errcode=0 表示正常訪問，訪問成功；errcode=1 表示尚處于懲罰期間，訪問失敗；errcode=2 表示沒有訪問權(quán)限，訪問失??；errcode=3表示最小時(shí)間間隔內(nèi)訪問次數(shù)超過閾值，訪問失??；errcode=4 表示沒有訪問權(quán)限且最小時(shí)間間隔內(nèi)訪問次數(shù)超過閾值，訪問失敗；errcode=5表示訪問的非當(dāng)前IoT設(shè)備，訪問失敗。則該場景性質(zhì)描述：AG（?。╬3.pc=33）|（errcode=0）），即accessControl（）進(jìn)程執(zhí)行完成后，最終該場景驗(yàn)證結(jié)果為可以正常獲得訪問權(quán)限即errcode=0（對(duì)應(yīng)基本性質(zhì)1）。

5 案例研究

本文方法使用Python 語言及Solidity 語言的solidity_parser 工具，實(shí)現(xiàn)了Solidity 語言子集到VVM 的轉(zhuǎn)換，并用兩個(gè)案例進(jìn)行了驗(yàn)證。

5.1 案例一：資源訪問控制智能合約

本文對(duì)2.1 節(jié)中的資源訪問控制智能合約進(jìn)行了驗(yàn)證，該合約實(shí)現(xiàn)了區(qū)塊鏈上用戶對(duì)IoT 中資源（數(shù)據(jù)、服務(wù)、存儲(chǔ)、計(jì)算等資源）的訪問控制，可以決定用戶在請求訪問IoT 中的資源時(shí)是否能夠獲取到所申請的資源，同時(shí)也可根據(jù)懲罰策略對(duì)用戶的錯(cuò)誤行為進(jìn)行懲罰。除4.3 節(jié)的場景外，本文還對(duì)另外的四種場景進(jìn)行了實(shí)例化及對(duì)相應(yīng)的性質(zhì)進(jìn)行了形式化定義并驗(yàn)證。

1）用戶在最小訪問時(shí)間間隔內(nèi)訪問次數(shù)超過設(shè)置的閾值后會(huì)收到懲罰。

用戶實(shí)例化及調(diào)用順序描述如圖7所示。

圖7 場景2Fig.7 Scenario 2

性質(zhì)描述：AG（?。╬5.pc=33）|（p5.errcode=3））。

場景及性質(zhì)解釋：首先，在1 號(hào)地址調(diào)用Constructor（）合約部署成功后，將合約owner及subject分別設(shè)置為地址1和地址2；然后，1 號(hào)地址添加訪問策略，使得地址為2 的用戶在2個(gè)時(shí)間單位內(nèi)最多對(duì)1 號(hào)資源執(zhí)行2 次讀操作（用1 來表示）；接著，當(dāng)?shù)刂窞? 的用戶在時(shí)間2 時(shí)對(duì)1 號(hào)資源執(zhí)行2 次讀操作（p3和p4），時(shí)間3時(shí)做同樣的操作（p5）會(huì)被懲罰，即待進(jìn)程p5執(zhí)行完畢后p5.errcode=3。

2）用戶在合約擁有者修改其權(quán)限為不可訪問后用戶不可再訪問（對(duì)應(yīng)基本性質(zhì)2）。

用戶調(diào)用順序描述如圖8所示。

圖8 場景3Fig.8 Scenario 3

性質(zhì)描述：AG（?。╬3.pc=33）|（p3.errcode=2））。

場景及性質(zhì)解釋：首先，在1 號(hào)地址調(diào)用Constructor（）合約部署成功后，將合約owner及subject分別設(shè)置為地址1和地址2；然后，1 號(hào)地址添加訪問策略，使得地址為2 的用戶在2個(gè)時(shí)間單位內(nèi)最多對(duì)1 號(hào)資源執(zhí)行2 次讀操作；接著，1 號(hào)地址用戶調(diào)用policyUpdate 函數(shù)修改地址為2 的用戶的權(quán)限為對(duì)1 號(hào)地址不能執(zhí)行讀操作；最后，2 號(hào)地址用戶在時(shí)間點(diǎn)4申請對(duì)1 號(hào)資源執(zhí)行讀操作時(shí)并不能獲得訪問權(quán)限，即待進(jìn)程p3執(zhí)行完畢后p3.errcode=2。

3）用戶在合約擁有者修改其訪問權(quán)限時(shí)進(jìn)行訪問，不能獲取到訪問權(quán)限。

用戶調(diào)用順序描述如圖9所示。

圖9 場景4Fig.9 Scenario 4

性質(zhì)描述：AG（?。╬2.pc=33&p3.pc=7）|（p2.errcode=2））。

場景及性質(zhì)解釋：首先，在1 號(hào)地址調(diào)用Constructor（）合約部署成功后，將合約owner及subject分別設(shè)置為地址1和地址2；然后，1 號(hào)地址添加訪問策略，使得地址為2 的用戶在2個(gè)時(shí)間單位內(nèi)最多對(duì)1 號(hào)資源執(zhí)行2 次讀操作；接著，1 號(hào)地址用戶調(diào)用policyUpdate 函數(shù)修改地址為2 的用戶的權(quán)限為對(duì)1號(hào)地址不能執(zhí)行讀操作，與此同時(shí)2號(hào)地址用戶在時(shí)間點(diǎn)4申請對(duì)1號(hào)資源執(zhí)行讀操作時(shí)并不能獲得訪問權(quán)限，即待進(jìn)程p2及p3執(zhí)行完畢后p2.errcode=2。

4）非合約擁有者不能修改自身的訪問的權(quán)限（對(duì)應(yīng)基本性質(zhì)3）。

用戶調(diào)用順序描述如圖10所示。

圖10 場景5Fig.10 Scenario 5

性質(zhì)描述：AG（?。╬3.pc=33）|（p3.errcode=2））。

場景及性質(zhì)解釋：首先，在1 號(hào)地址調(diào)用Constructor（）合約部署成功后，將合約owner及subject分別設(shè)置為地址1和地址2；然后，1 號(hào)地址添加訪問策略，使得地址為2 的用戶不能對(duì)1 號(hào)資源執(zhí)行讀操作；接著，2 號(hào)地址用戶調(diào)用policyUpdate函數(shù)修改地址為2的用戶的權(quán)限為對(duì)1號(hào)地址能執(zhí)行讀操作；最后，2 號(hào)地址用戶在時(shí)間點(diǎn)4 申請對(duì)1 號(hào)資源執(zhí)行讀操作時(shí)并不能獲得訪問權(quán)限，即待進(jìn)程p2 及p3 執(zhí)行完畢后p2.errcode=2。

5.2 案例二：帶可信Oracle的訪問控制智能合約

本文同樣對(duì)文獻(xiàn)［31］中的案例進(jìn)行了驗(yàn)證，該案例引入帶信譽(yù)的Oracle 來控制用戶訪問權(quán)限，使用AccessControl 來決定用戶是否有權(quán)限來獲取到所申請的資源，若能夠獲取則向Oracle 發(fā)起調(diào)用獲得數(shù)據(jù)庫中的數(shù)據(jù)。而該案例中與權(quán)限驗(yàn)證相關(guān)的函數(shù)均在AccessControl 合約中，本文將AccessControl 合約之外的部分作了省略。在AccessControl 合約中有7 個(gè)函數(shù)，7 個(gè)函數(shù)的功能分別為構(gòu)造函數(shù)、添加管理者、添加設(shè)備、添加用戶與設(shè)備的映射、刪除管理者、刪除用戶、進(jìn)行訪問。

本文對(duì)AccessControl合約驗(yàn)證了如下四個(gè)場景：

1）用戶在具有對(duì)設(shè)備的訪問權(quán)限時(shí)，可以正常訪問（對(duì)應(yīng)基本性質(zhì)1）；

2）用戶在具有對(duì)設(shè)備的訪問權(quán)限時(shí)，管理者發(fā)起調(diào)用刪除用戶函數(shù)交易后，用戶無法訪問設(shè)備（對(duì)應(yīng)基本性質(zhì)2）；

3）用戶在具有對(duì)設(shè)備的訪問權(quán)限時(shí)，管理者發(fā)起調(diào)用刪除用戶函數(shù)交易時(shí)，用戶發(fā)起調(diào)用訪問函數(shù)交易，用戶一定能夠訪問；

4）用戶可以修改自身的訪問權(quán)限（對(duì)應(yīng)基本性質(zhì)3）。

5.3 驗(yàn)證結(jié)果及分析

本文的所有實(shí)驗(yàn)均在一臺(tái)運(yùn)行Ubuntu18.04.3 系統(tǒng)Intel Xeon E5-2690的服務(wù)器完成，其CPU主頻為2.90 GHz，內(nèi)存為384 GB。

對(duì)于案例一，其場景1、2、3 的驗(yàn)證結(jié)果均為True，場景4及場景5不滿足，并各自提供了一個(gè)反例。從場景4反例中可以得出，當(dāng)調(diào)用p2：accessControl（2，1，1，2）和調(diào)用p3：policyUpdate（1，1，1，0）并發(fā)時(shí)，最終交易的執(zhí)行順序是不確定的，當(dāng)p2：accessControl（2，1，1，2）先于p3：policyUpdate（1，1，1，0）執(zhí)行時(shí)，用戶在這一次調(diào)用能夠獲取到訪問權(quán)限。對(duì)于場景5，分析其反例可以得出，2 號(hào)地址能夠調(diào)用policyUpdate（）函數(shù)修改其合約權(quán)限，造成非法訪問。

對(duì)于案例二，場景1、場景2 及場景4 驗(yàn)證結(jié)果為True，場景3的驗(yàn)證結(jié)果為False，由其反例可以得出，當(dāng)管理者調(diào)用刪除用戶函數(shù)與用戶進(jìn)行訪問申請并發(fā)時(shí)，用戶訪問申請可能先執(zhí)行，最終可以訪問。

本文將案例一和案例二中相同的四個(gè)場景作了對(duì)比，結(jié)果如表1所示。

表1 案例一與案例二相同場景對(duì)比Tab.1 Comparison between case one and case two under same scenarios

從表1 可看出，案例一和案例二均能在合理時(shí)間內(nèi)結(jié)束，同時(shí)，由于對(duì)于合約的驗(yàn)證需要在合約部署之前進(jìn)行，所以對(duì)實(shí)際運(yùn)行并不產(chǎn)生影響。對(duì)于更新權(quán)限與進(jìn)入交易并發(fā)，不能進(jìn)入場景，當(dāng)用戶發(fā)起交易請求訪問同時(shí)，管理者調(diào)用刪除用戶的函數(shù)或調(diào)用修改其權(quán)限的函數(shù)發(fā)起交易，最終用戶可能會(huì)獲取到訪問權(quán)限，即當(dāng)用戶訪問的交易先于管理者刪除用戶的交易執(zhí)行時(shí)，用戶可以獲取到訪問權(quán)限，但管理者刪除用戶的交易先于用戶訪問的交易時(shí)，用戶無法獲取到訪問權(quán)限。對(duì)于場景4，案例二的驗(yàn)證結(jié)果為True，相對(duì)于案例一，案例二的修改權(quán)限相關(guān)的函數(shù)均加了修飾器onlyAdmin，只有管理者身份的地址才能調(diào)用修改權(quán)限相關(guān)的函數(shù)，而案例一中的合約函數(shù)沒有相關(guān)修飾器，所有的地址用戶均能修改權(quán)限。

6 結(jié)語

本文針對(duì)IoT 中訪問控制的正確性問題，提出了一種基于形式化驗(yàn)證的解決方案。該方法對(duì)Solidity 編寫的訪問控制智能合約進(jìn)行形式建模，用共享變量實(shí)現(xiàn)合約之間的交互，并使用CTL 描述系統(tǒng)所期望的性質(zhì)。本文實(shí)現(xiàn)了這一方法，將Solidity 合約轉(zhuǎn)換為模型檢測工具Verds 的輸入文件；再利用Verds 進(jìn)行驗(yàn)證；且對(duì)兩個(gè)IoT 的訪問控制合約進(jìn)行了進(jìn)行實(shí)例研究及實(shí)驗(yàn)。實(shí)驗(yàn)結(jié)果表明，本文方法可以對(duì)訪問控制合約的典型場景進(jìn)行及期望性質(zhì)進(jìn)行驗(yàn)證，進(jìn)而提升合約的可靠性。在將來的工作中，我們計(jì)劃將方法擴(kuò)展到通用的智能合約功能正確性驗(yàn)證上，而不僅限制于IoT 的權(quán)限控制類合約。