包玉龙，朱雪阳*，张文辉，孙鹏飞，赵颖琪

（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 的权限控制类合约。