Formal verification of smart contract for access control in IoT applications

doi:10.11772/j.issn.1001-9081.2020111732

Abstract

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:

TP301

BAO Yulong, ZHU Xueyang, ZHANG Wenhui, SUN Pengfei, ZHAO Yingqi. Formal verification of smart contract for access control in IoT applications[J]. Journal of Computer Applications, 2021, 41(4): 930-938.

包玉龙, 朱雪阳, 张文辉, 孙鹏飞, 赵颖琪. 物联网应用中访问控制智能合约的形式化验证[J]. 计算机应用, 2021, 41(4): 930-938.

References

[1] YAQOOB I,AHMED E,HASHEM I A T,et al. Internet of things architecture:recent advances,taxonomy,requirements,and open challenges[J]. IEEE Wireless Communications,2017,24(3):10-16.
[2] PALATTELLA M R,DOHLER M,GRIECO A,et al. Internet of things in the 5G era:enablers,architecture,and business models[J]. IEEE Journal on Selected Areas in Communications,2016,34(3):510-527.
[3] AL-FUQAHA A,GUIZANI M,MOHAMMADI M,et al. Internet of things:a survey on enabling technologies, protocols, and applications[J]. IEEE Communications Surveys and Tutorials, 2015,17(4):2347-2376.
[4] XU L D,HE W,LI S. Internet of things in industries:a survey[J]. IEEE Transactions on Industrial Informatics,2014,10(4):2233-2243.
[5] BERTINO E,ISLAM N. Botnets and internet of things security[J]. Computer,2017,50(2):76-79.
[6] D' ORAZIO C J,CHOO K K R,YANG L T. Data exfiltration from internet of things devices:iOS devices as case studies[J]. IEEE Internet of Things Journal,2017,4(2):524-535.
[7] OUADDAH A,MOUSANNIF H,ABOU ELKALAM A,et al. Access control in the internet of things:big challenges and new opportunities[J]. Computer Networks,2017,112:237-262.
[8] SICARI S,RIZZARDI A,GRIECO L A,et al. Security,privacy and trust in internet of things:the road ahead[J]. Computer Networks,2015,76:146-164.
[9] SINGH J, PASQUIER T, BACON J, et al. Twenty security considerations for cloud-supported internet of things[J]. IEEE Internet of Things Journal,2016,3(3):269-284.
[10] SANDHU R S,COYNE E J,FEINSTEIN H L,et al. Role-based access control models[J]. Computer,1996,29(2):38-47.
[11] HU V C,KUHN D R,FERRAIOLO D F,et al. Attribute-based access control[J]. Computer,2015,48(2):85-88.
[12] SANDHU R S,SAMARATI P. Access control:principle and practice[J]. IEEE Communications Magazine,1994,32(9):40-48.
[13] HUSSEIN D,BERTIN E,FREY V. A community-driven access control approach in distributed IoT environments[J]. IEEE Communications Magazine,2017,55(3):146-153.
[14] 沈鑫, 裴庆祺, 刘雪峰. 区块链技术综述[J]. 网络与信息安全学报,2016,2(11):11-20.(SHEN X,PEI Q Q,LIU X F. Survey of block chain[J]. Chinese Journal of Network and Information Security,2016,2(11):11-20.)
[15] 贺海武, 延安, 陈泽华. 基于区块链的智能合约技术与应用综述[J]. 计算机研究与发展,2018,55(11):2452. (HE H W, YAN A,CHEN Z H. Survey of smart contract technology and application based on blockchain[J]. Journal of Computer Research and Development,2018,55(11):2452-2466.)
[16] 袁勇, 王飞跃. 区块链技术发展现状与展望[J]. 自动化学报, 2016,42(4):481-494.(YUAN Y,WANG F Y. Blockchain:the state of the art and future trends[J]. Acta Automatica Sinica, 2016,42(4):481-494.)
[17] LUU L,CHU D H,OLICKEL H,et al. Making smart contracts smarter[C]//Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. New York:ACM,2016:254-269.
[18] FINLEY K. A $50 million hack just showed that the DAO was all too human[EB/OL].[2020-05-01]. https://www.wired.com/2016/06/50-million-hack-just-showed-dao-human/.
[19] NEWMAN L H. Security news this week:$280 M worth of Ethereum is trapped thanks to a dumb bug[EB/OL].[2020-05-05]. https://www.wired.com/story/280m-worth-of-ethereum-istrapped-for-a-pretty-dumb-reason/.
[20] ATZEI N,BARTOLETTI M,CIMOLI T. A survey of attacks on Ethereum Smart Contracts (SoK)[C]//Proceedings of the 6th International Conference on Principles of Security and Trust. Cham:Springer,2017:164-186.
[21] DELMOLINO K,ARNETT M,KOSBA A,et al. Step by step towards creating a safe smart contract:lessons and insights from a cryptocurrency lab[C]//Proceedings of the 2016 International Conference on Financial Cryptography and Data Security. Cham:Springer,2016:79-94.
[22] BIGI G, BRACCIALI A, MEACCI G, et al. Validation of decentralised smart contracts through game theory and formal methods[C]//Programming Languages with Applications to Biology and Security, 9465. Cham:Springer,2015:142-161.
[23] BHARGAVAN K,DELIGNAT-LAVAUD A,FOURNET C,et al. Formal verification of smart contracts:Short paper[C]//Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security. New York:ACM,2016:91-96.
[24] ABDELLATIF T, BROUSMICHE K-L. Formal verification of smart contracts based on users and blockchain behaviors models[C]//Proceedings of the 2018 IFIP International Conference on New Technologies,Mobility and Security. Piscataway:IEEE, 2018:1-5.
[25] NEHAI Z,PIRIOU P-Y,DAUMAS F. Model-checking of smart contracts[C]//Proceedings of the 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications(GreenCom) and IEEE Cyber, Physical and Social Computing(CPSCom)and IEEE Smart Data (SmartData). Piscataway:IEEE,2018:980-987.
[26] ALQAHTANI S,HE X,GAMBLE R,et al. Formal verification of functional requirements for smart contract compositions in supply chain management systems[EB/OL].[2020-05-10]. https://scholarspace.manoa.hawaii.edu/handle/10125/64392..
[27] EMERSON E A,HALPERN J Y."Sometimes"and"not never" revisited:on branching versus linear time temporal logic[J]. Journal of the ACM,1986,33(1):151-178.
[28] CLARKE E M,WING J M. Formal methods:state of the art and future directions[J]. ACM Computing Surveys,1996,28(4):626-643.
[29] ZHANG W. Verds[EB/OL].[2020-05-04]. http://lcs.ios.ac.cn/~zwh/verds/index.html.
[30] ZHANG Y,KASAHARA S,SHEN Y,et al. Smart contract-based access control for the internet of things[J]. IEEE Internet of Things Journal,2019,6(2):1594-1605.
[31] AL BREIKI H,AL QASSEM L,SALAH K,et al. Decentralized access control for IoT data using blockchain and trusted oracles[C]//Proceedings of the 2019 IEEE International Conference on Industrial Internet. Piscataway:IEEE,2019:248-257.
[32] HU H,AHN G. Enabling verification and conformance testing for access control model[C]//Proceedings of the 13th ACM Symposium on Access Control Models and Technologies. New York:ACM,2008:195-204.
[33] HU V C, KUHN D R, XIE T, et al. Model checking for verification of mandatory access control models and properties[J]. International Journal of Software Engineering and Knowledge Engineering,2011,21(1):103-127.
[34] MAVRIDOU A,LASZKA A,STACHTIARI E,et al. VeriSolid:correct-by-design smart contracts for Ethereum[C]//Proceedings of the 2019 International Conference on Financial Cryptography and Data Security,LNCS 11598. Cham:Springer,Cham,2019:446-465.
[35] NAKAMOTO S. Bitcoin:a peer-to-peer electronic cash system[EB/OL].[2020-05-05]. https://bitcoin.org/bitcoin.pdf.
[36] Ethereum. Solidity v0.7. 1[EB/OL].[2020-05-05]. https://solidity.readthedocs.io/en/v0.7.1/.
[37] SERGEY I, HOBOR A. A concurrent perspective on smart contracts[C]//Proceedings of the 2017 International Conference on Financial Cryptography and Data Security, LNCS 10323. Cham:Springer,2017:478-493.
[38] BURCH J R,CLARKE E M,MCMILLAN K L,et al. Symbolic model checking:1020 states and beyond[J]. Information and Computation,1992,98(2):142-170.
[39] ZHANG W. Bounded semantics[J]. Theoretical Computer Science,2015,564:1-29.
[40] ZHANG W. QBF encoding of temporal properties and QBF-based verification[C]//Proceedings of the 2014 International Joint Conference on Automated Reasoning, LNCS 8562. Cham:Springer,2014:224-239.
[41] PELED D A. Software reliability methods[J]. Texts in Computer Science,2001,106(1):1-30.
[42] ZENG N, ZHANG W. An executable semantics of SystemC transaction level models and its applications with VERDS[C]//Proceedings of the 19th International Conference on Engineering of Complex Computer Systems. Piscataway:IEEE,2014:198-201.
[43] ZENG N, ZHANG W. A symbolic partial order method for verifying SystemC[C]//Proceedings of the 21st Asia-Pacific Software Engineering Conference. Piscataway:IEEE, 2014:271-278.
[44] ZHANG W. VERDS modeling language[EB/OL].[2020-05-05]. http://lcs.ios.ac.cn/~zwh/verds/verds_pdf/verds1.42vml.pdf.