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

• 作者: 包玉龙 朱雪阳 张文辉 孙鹏飞 赵颖琪
• 来源期刊: 计算机应用
• 关键词: 物联网 访问控制 智能合约 形式化验证 模型检测
• 年，卷（期）: 2021,（4）
• 所属期刊栏目: 2020 CCF 中国区块链技术大会(CCF CBCC 2020)|2020 CCF China Blockchain Conference(CCF CBCC 2020)
• 页码范围: 930-938
• 页数: 9页
• 分类号: TP301
• 语种: 中文
• DOI: 10.11772/j.issn.1001-9081.2020111732

摘要

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