计算机应用

作者：包玉龙, 朱雪阳, 张文辉, 孙鹏飞, 赵颖琪

单位：1. 计算机科学国家重点实验室(中国科学院软件研究所), 北京 100190;2. 中国科学院大学, 北京 100049

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

基金：国家自然科学基金资助项目（62072443）。

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

来源：2021年第4期

《计算机应用》期刊编辑部

查看计算机应用杂志2021年第4期