Journal of Computer Applications ›› 2021, Vol. 41 ›› Issue (4): 930-938.DOI: 10.11772/j.issn.1001-9081.2020111732

Special Issue: 2020 CCF中国区块链技术大会(CCF CBCC 2020)

• 2020 CCF China Blockchain Conference (CCF CBCC 2020) • Previous Articles     Next Articles

Formal verification of smart contract for access control in IoT applications

BAO Yulong1,2, ZHU Xueyang1,2, ZHANG Wenhui1,2, SUN Pengfei1,2, ZHAO Yingqi1,2   

  1. 1. State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;
    2. University of Chinese Academy of Sciences, Beijing 100049, China
  • Received:2020-11-09 Revised:2020-12-15 Online:2021-04-10 Published:2021-01-29
  • Supported by:
    This work is partially supported by the National Natural Science Foundation of China (62072443).


包玉龙1,2, 朱雪阳1,2, 张文辉1,2, 孙鹏飞1,2, 赵颖琪1,2   

  1. 1. 计算机科学国家重点实验室(中国科学院软件研究所), 北京 100190;
    2. 中国科学院大学, 北京 100049
  • 通讯作者: 朱雪阳
  • 作者简介:包玉龙(1995—),男,湖北随州人,硕士研究生,CCF会员,主要研究方向:形式化方法、模型检测;朱雪阳(1971—),女,福建莆田人,副研究员,博士,CCF会员,主要研究方向:嵌入式系统、模型检测;张文辉(1963—),男,福建福安人,研究员,博士,CCF会员,主要研究方向:逻辑与形式化方法;孙鹏飞(1997—),男,江苏泰州人,硕士研究生,CCF会员,主要研究方向:区块链、物联网、智能合约、边缘计算;赵颖琪(1994—),女,河北张家口人,硕士研究生,CCF会员,主要研究方向:并发程序验证。
  • 基金资助:

Abstract: 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.

Key words: Internet of Things (IoT), access control, smart contract, formal verification, model checking

摘要: 蓝牙、WiFi等网络技术的进步推动物联网(IoT)的发展,然而IoT在方便了人们生活的同时也存在严重的安全隐患。若无安全的访问控制,非法接入IoT的访问可能给用户带来各方面的损失。传统的访问控制方法需要一个可信任的中心节点,不适合节点分散的IoT环境。区块链及智能合约的出现为IoT应用的访问控制提供了更有效的解决方案,但用一般测试方法难以保证实现IoT应用的访问控制智能合约的正确性。针对这个问题,提出一种利用模型检测工具Verds对访问控制智能合约进行形式化验证从而保障合约正确性的方法。该方法利用状态迁移系统定义Solidity智能合约的语义,应用计算树逻辑(CTL)公式描述所要验证的性质,并对智能合约交互及用户行为进行建模,从而形成Verds的输入模型及所要验证性质,然后利用Verds验证待测性质的正确性。方法核心是Solidity合约子集到Verds输入模型的转换。对两个IoT资源访问控制智能合约的实验结果表明,该方法可以对访问控制合约的典型场景及期望性质进行验证,提升了智能合约的可靠性。

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

CLC Number: