物聯網應用中訪問控制智能合約的形式化驗證

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

（1.計算機科學國家重點實驗室（中國科學院軟件研究所），北京 100190；2.中國科學院大學，北京 100049）

0 引言

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

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

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

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

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

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

本文主要工作如下：

1）提出了一種對智能合約、區塊鏈執行協議以及用戶調用次序行為進行形式建模的新方法；

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

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

1 相關工作

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

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

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

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

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

2 準備知識

2.1 智能合約與訪問控制

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

以太坊區塊鏈的智能合約一般來說是一組函數，用戶通過調用合約函數將交易發送到以太坊網絡，以便：1）創建新合約；2）調用合約功能；3）將以太幣轉讓給合約或其他用戶。所有交易均記錄在每個參與共識的節點上，區塊鏈上的交易順序決定了每個合約的狀態以及每個用戶的余額。

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

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

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

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

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

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

通過上面兩個合約偽代碼可以看出，訪問控制包括兩部分：訪問權限檢查及訪問權限修改更新。綜合來看，訪問控制合約應當滿足以下三個基本性質：

1）無訪問權限的用戶無法訪問；

2）有訪問權限的用戶能夠訪問；

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

2.2 模型檢測工具Verds

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

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

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

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

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

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

圖1 example1狀態遷移系統Fig.1 State transition system for example1

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

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

2）s0表示初始狀態；

3）Act表示動作的集合；

4）G表示衛式條件及Guard的集合；

5）→?S×Act×S為遷移關系。

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

3 基本框架

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

圖2 整體框架Fig.2 Overall framework

4 訪問控制權限驗證

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

4.1 智能合約建模

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

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

算法1 funcMap。

使用算法ts=funcMap(f)把上文中的policyUpdate（）函數轉換成圖3所示的狀態遷移系統。例如第4）行的條件語句轉變為當條件為真時pc=3向pc=4遷移的狀態，當條件為假時pc=3向pc=6遷移的狀態。

在第二部分，將合約中的所有函數描述成一個函數外部調用接口圖。當合約被部署到區塊鏈上后，合約處于idle 狀態。合約處于idle 狀態的含義是指合約被部署到鏈上并已經執行完畢構造函數，并且當合約處于該狀態時用戶可以調用除構造函數外的其他函數，待函數執行完畢后合約重新進入idle狀態。

圖3 policyUpdate函數的狀態遷移模型Fig.3 State transition system for policyUpdate function

根據以上規則，可以將資源訪問控制智能合約案例描述成如圖4所示的函數外部調用接口圖。

圖4 ACC合約函數外部調用接口圖Fig.4 Function external call interface diagram for ACC contract

ACC合約有6個狀態：

1）idle：ACC 合約被部署到區塊鏈上，構造函數已執行完畢；

2）添加訪問策略：ACC 合約擁有者調用policyAdd（）函數，添加新的訪問策略，執行完之后返回idle狀態；

3）更新訪問權限：調用policyUpdate（）函數，更新訪問權限，執行完之后返回idle狀態；

4）更新最小訪問時間間隔：調用minIntervalUpdate（），更新最小時間間隔，執行完之后返回idle狀態；

5）更新訪問閾值：調用thresholdUpdate（），更新訪問閾值，執行完之后返回idle狀態；

6）訪問申請：用戶調用accessControl（）方法，申請以特定方式訪問資源，獲得返回結果，之后返回idle狀態。

由于調用合約函數產生的交易在以太坊虛擬機上是以類似單線程的方式執行，本文使用一個全局布爾型變量process_control 來模擬，該變量初始值為False，當構造函數執行完畢后，它被賦值為True，除構造函數外其余所有實例化進程在未執行前均在等待該變量值為True，一旦該變量值為True，等待的所有進程將有一個進程獲取到執行權限，開始執行且同時將該變量的值設置為False，待執行完畢后將該變量的值設置為True。

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

4.2 場景定義

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

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

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

圖5 ACC合約調用順序定義Fig.5 Call order definition of ACC contract

4.3 性質形式化

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

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

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

圖6 場景1 Fig.6 Scenario 1

在該案例性質形式化時，errcode表示最終獲取訪問權限的結果：errcode=0 表示正常訪問，訪問成功；errcode=1 表示尚處于懲罰期間，訪問失敗；errcode=2 表示沒有訪問權限，訪問失敗；errcode=3表示最小時間間隔內訪問次數超過閾值，訪問失敗；errcode=4 表示沒有訪問權限且最小時間間隔內訪問次數超過閾值，訪問失敗；errcode=5表示訪問的非當前IoT設備，訪問失敗。則該場景性質描述：AG（！（p3.pc=33）|（errcode=0）），即accessControl（）進程執行完成后，最終該場景驗證結果為可以正常獲得訪問權限即errcode=0（對應基本性質1）。

5 案例研究

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

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

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

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

用戶實例化及調用順序描述如圖7所示。

圖7 場景2Fig.7 Scenario 2

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

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

2）用戶在合約擁有者修改其權限為不可訪問后用戶不可再訪問（對應基本性質2）。

用戶調用順序描述如圖8所示。

圖8 場景3Fig.8 Scenario 3

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

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

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

用戶調用順序描述如圖9所示。

圖9 場景4Fig.9 Scenario 4

性質描述：AG（！（p2.pc=33&p3.pc=7）|（p2.errcode=2））。

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

4）非合約擁有者不能修改自身的訪問的權限（對應基本性質3）。

用戶調用順序描述如圖10所示。

圖10 場景5Fig.10 Scenario 5

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

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

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

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

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

1）用戶在具有對設備的訪問權限時，可以正常訪問（對應基本性質1）；

2）用戶在具有對設備的訪問權限時，管理者發起調用刪除用戶函數交易后，用戶無法訪問設備（對應基本性質2）；

3）用戶在具有對設備的訪問權限時，管理者發起調用刪除用戶函數交易時，用戶發起調用訪問函數交易，用戶一定能夠訪問；

4）用戶可以修改自身的訪問權限（對應基本性質3）。

5.3 驗證結果及分析

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

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

對于案例二，場景1、場景2 及場景4 驗證結果為True，場景3的驗證結果為False，由其反例可以得出，當管理者調用刪除用戶函數與用戶進行訪問申請并發時，用戶訪問申請可能先執行，最終可以訪問。

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

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

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

6 結語

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