排序方式： 共有2条查询结果，搜索用时 0 毫秒
1
1.
蓝牙、WiFi等网络技术的进步推动物联网（IoT）的发展,然而IoT在方便了人们生活的同时也存在严重的安全隐患。若无安全的访问控制,非法接入IoT的访问可能给用户带来各方面的损失。传统的访问控制方法需要一个可信任的中心节点,不适合节点分散的IoT环境。区块链及智能合约的出现为IoT应用的访问控制提供了更有效的解决方案,但用一般测试方法难以保证实现IoT应用的访问控制智能合约的正确性。针对这个问题,提出一种利用模型检测工具Verds对访问控制智能合约进行形式化验证从而保障合约正确性的方法。该方法利用状态迁移系统定义Solidity智能合约的语义,应用计算树逻辑（CTL）公式描述所要验证的性质,并对智能合约交互及用户行为进行建模,从而形成Verds的输入模型及所要验证性质,然后利用Verds验证待测性质的正确性。方法核心是Solidity合约子集到Verds输入模型的转换。对两个IoT资源访问控制智能合约的实验结果表明,该方法可以对访问控制合约的典型场景及期望性质进行验证,提升了智能合约的可靠性。 相似文献
2.
智能合约是一套以数字形式定义的承诺.通过智能合约可以大大减少协议制定的中间环节, 提高协议制定的效率.区块链技术为智能合约的执行提供了可信平台.随着区块链应用的拓广与深入, 智能合约的作用必然越来越突出, 智能合约的可靠性问题也将更加突显.以提高智能合约可靠性为目的的研究日益得到重视, 但尚未有人对智能合约的时间性质可能引起的可靠性问题进行过系统的研究.本文通过分析典型智能合约, 对智能合约时间约束的不同表现形式进行梳理, 提炼出相应的时间约束模式并对其进行形式化; 定义Solidity智能合约到时间自动机的转换规则并实现其到实时模型检测工具UPPAAL入口模型的自动转换; 再利用UPPAAL验证合约的时间相关性质.最后对两个实际合约进行实例研究, 结果表明本文所提炼模式的普遍性以及本文所提出形式化验证方案的可行性和有效性. 相似文献
1