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

（1.計算機科學(xué)國家重點實驗室（中國科學(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］。物理對象無處不在的互聯(lián)顯著加速了數(shù)據(jù)收集、聚合和共享，使得IoT 成為智能醫(yī)療、智能交通、家庭自動化等［3-4］應(yīng)用的最基本架構(gòu)之一。但是，這樣的互聯(lián)也可能會給IoT 系統(tǒng)帶來嚴(yán)重的安全問題［5-6］。若系統(tǒng)無安全的訪問控制，通過入侵系統(tǒng)，未經(jīng)授權(quán)的實體（攻擊者）只需簡單部署自己的資源，就可以非法訪問現(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］。但是在以上方案中，驗證對象的訪問權(quán)限通常是由中心節(jié)點進行的，一旦中心節(jié)點出現(xiàn)故障或者漏洞，整個訪問控制系統(tǒng)就會出現(xiàn)問題。為了避免中心節(jié)點故障導(dǎo)致系統(tǒng)出現(xiàn)問題，最近有學(xué)者基于CapBAC 提出了分布式CapBAC 模型［13］，其中訪問權(quán)限驗證是由請求的IoT 對象本身而不是中心節(jié)點執(zhí)行的。但是，物聯(lián)網(wǎng)對象通常功能較弱，很容易受到入侵者的破壞，因此不能完全信任它們作為訪問權(quán)限驗證實體，所以，分布式CapBAC 模型仍無法很好解決不可信賴的IoT環(huán)境中的訪問控制問題。

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

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

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

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

本文主要工作如下：

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

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

3）對兩個實際案例進行實例研究，并對比兩個案例的驗證結(jié)果。

1 相關(guān)工作

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

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

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

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

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

2 準(zhǔn)備知識

2.1 智能合約與訪問控制

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

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

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

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

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

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

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

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

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

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

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

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

2.2 模型檢測工具Verds

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

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

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

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

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

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

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

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

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

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

3）Act表示動作的集合；

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

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

同樣，對于當(dāng)前狀態(tài)s下的某個變量i（i=0，1，2，3)的值，可以由s.i表示，到下一個狀態(tài)的Guard 和動作可以由s.guard和s.act來表示。對于圖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)，其動作為(x，z)：=(x+1，1-0)。對于示例example1，一個完整的VVM 是由TS(p0) 和TS(p1) 并發(fā)組成，若將MODULEp0mod（i）實例化四個進程，那么整個模型就是TS(p0)、TS(p1)、TS(p2)及TS(p3)的并發(fā)。

3 基本框架

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

圖2 整體框架Fig.2 Overall framework

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

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

4.1 智能合約建模

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

同時，為了使得TS的遷移順序同Solidity合約函數(shù)的執(zhí)行順序一致，在每個函數(shù)的TS中添加了變量pc，其值等同于函數(shù)中當(dāng)前執(zhí)行程序語句的標(biāo)號，所以每個函數(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)條件為真時pc=3向pc=4遷移的狀態(tài)，當(dāng)條件為假時pc=3向pc=6遷移的狀態(tài)。

在第二部分，將合約中的所有函數(shù)描述成一個函數(shù)外部調(diào)用接口圖。當(dāng)合約被部署到區(qū)塊鏈上后，合約處于idle 狀態(tài)。合約處于idle 狀態(tài)的含義是指合約被部署到鏈上并已經(jīng)執(zhí)行完畢構(gòu)造函數(shù)，并且當(dāng)合約處于該狀態(tài)時用戶可以調(diào)用除構(gòu)造函數(shù)外的其他函數(shù)，待函數(shù)執(zhí)行完畢后合約重新進入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個狀態(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）更新最小訪問時間間隔：調(diào)用minIntervalUpdate（），更新最小時間間隔，執(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)生的交易在以太坊虛擬機上是以類似單線程的方式執(zhí)行，本文使用一個全局布爾型變量process_control 來模擬，該變量初始值為False，當(dāng)構(gòu)造函數(shù)執(zhí)行完畢后，它被賦值為True，除構(gòu)造函數(shù)外其余所有實例化進程在未執(zhí)行前均在等待該變量值為True，一旦該變量值為True，等待的所有進程將有一個進程獲取到執(zhí)行權(quán)限，開始執(zhí)行且同時將該變量的值設(shè)置為False，待執(zhí)行完畢后將該變量的值設(shè)置為True。

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

4.2 場景定義

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

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

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

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

4.3 性質(zhì)形式化

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

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

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

圖6 場景1 Fig.6 Scenario 1

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

5 案例研究

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

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

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

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

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

圖7 場景2Fig.7 Scenario 2

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

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

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

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

圖8 場景3Fig.8 Scenario 3

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

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

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

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

圖9 場景4Fig.9 Scenario 4

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

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

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

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

圖10 場景5Fig.10 Scenario 5

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

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

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

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

本文對AccessControl合約驗證了如下四個場景：

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

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

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

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

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

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

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

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

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

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

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

6 結(jié)語

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