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

Formal verification of smart contract for access control in IoT applications

作　　者：包玉龙 朱雪阳[1,2] 张文辉 孙鹏飞[1,2] 赵颖琪 BAO Yulong;ZHU Xueyang;ZHANG Wenhui;SUN Pengfei;ZHAO Yingqi(State Key Laboratory of Computer Science(Institute of Software,Chinese Academy of Sciences),Beijing 100190,China;University of Chinese Academy of Sciences,Beijing 100049,China)

机构地区：[1]计算机科学国家重点实验室(中国科学院软件研究所),北京100190 [2]中国科学院大学,北京100049

出　　处：《计算机应用》2021年第4期930-938,共9页journal of Computer Applications

基　　金：国家自然科学基金资助项目(62072443)。

摘　　要：蓝牙、WiFi等网络技术的进步推动物联网(IoT)的发展,然而IoT在方便了人们生活的同时也存在严重的个可信任的中心节点,不适合节点分散的IoT环境。区块链及智能合约的出现为IoT应用的访问控制提供了更有效的解决方案,但用一般测试方法难以保证实现IoT应用的访问控制智能合约的正确性。针对这个问题,提出一种利用模型检测工具Verds对访问控制智能合约进行形式化验证从而保障合约正确性的方法。该方法利用状态迁移系统定义从而形成Verds的输入模型及所要验证性质,然后利用Verds验证待测性质的正确性。方法核心是Solidity合约子集到Verds输入模型的转换。对两个IoT资源访问控制智能合约的实验结果表明,该方法可以对访问控制合约的典型场景及期望性质进行验证,提升了智能合约的可靠性。The advancement of network technologies such as bluetooth and WiFi has promoted the development of the Internet of Things(IoT).IoT facilitates people’s lives,but there are also serious security issues in it.Without secure access control,illegal access of IoT may bring losses to users in many aspects.Traditional access control methods usually rely on a trusted central node,which is not suitable for an IoT environment with nodes distributed.The blockchain technology and smart contracts provide a more effective solution for access control in IoT applications.However,it is difficult to ensure the correctness of smart contracts used for access control in IoT applications by using general test methods.To solve this problem,a method was proposed to formally verify the correctness of smart contracts for access control by using model checking tool Verds.In the method,the state transition system was used to define the semantics of the Solidity smart contract,the Computation Tree Logic(CTL)formula was used to describe the properties to be verified,and the smart contract interaction and user behavior were modelled to form the input model of Verds and the properties to be verified.And then Verds was used to verify whether the properties to be verified are correct.The core of this method is the translation from a subset of Solidity to the input model of Verds.Experimental results on two smart contracts for access control of IoT source show that the proposed method can be used to verify some typical scenarios and expected properties of access control contracts,thereby improving the reliability of smart contracts.

关 键 词：物联网 访问控制 智能合约 形式化验证 模型检测 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]