物联网应用中访问控制智能合约的形式化验证

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

（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］。……