智能合约的形式化验证方法研究综述

doi:10.12263/DZXB.20200723

电子学报 ›› 2021, Vol. 49 ›› Issue (4): 792-804.DOI: 10.12263/DZXB.20200723

智能合约的形式化验证方法研究综述

朱健, 胡凯, 张伯钧

北京航空航天大学软件开发环境国家重点实验室, 北京 100191

收稿日期:2020-07-16 修回日期:2020-10-07 出版日期:2021-04-25
- 通讯作者:
- 张伯钧
- 作者简介:
- 朱健男,1997年生于安徽铜陵.现为北京航空航天大学硕士研究生.主要研究方向为区块链技术和形式化验证技术.E-mail:zhujian@buaa.edu.cn;胡凯男,1963年生于湖南长沙,现为北京航空航天大学计算机学院教授、博士,主要研究方向和关注领域:分布式计算、区块链与数字社会技术.Email:hukai@buaa.edu.cn
- 基金资助:
- 国家重点研发项目 (No.2018YFB1402702）; 国家自然科学基金 (No.61672074，No.61672075）; 教育部中国移动基金 (No.MCM20180104）; 软件开发重点实验室基金 (No.SKLSDE-2020ZX-21）

Review on Formal Verification of Smart Contract

ZHU Jian, HU Kai, ZHANG Bo-jun

State Key Laboratory of Software Development Environment, Beijing University of Aeronautics and Astronautics, Beijing 100191, China

Received:2020-07-16 Revised:2020-10-07 Online:2021-04-25 Published:2021-04-25
- Corresponding author:
- ZHANG Bo-jun
- Supported by:
- National Key Research and Development Program (No.2018YFB1402702); National Natural Science Foundation of China (No.61672074, No.61672075); Joint Fund of Ministry of Education of China and China Mobile (No.MCM20180104); Foundation of Key Laboratory of Software Development (No.SKLSDE-2020ZX-21)

摘要/Abstract

摘要： 形式化方法是在安全关键软件系统中被广泛采用而有效的基于数学的验证方法，而智能合约属于安全关键代码，采用形式化方法验证智能合约已经成为热点研究领域.本文对自2015年以来的47篇典型相关论文进行了研究分析，对技术进行了详细的分类研究和对比分析；对形式化验证智能合约的过程中使用的形式化方法、语言、工具和框架进行综述.研究表明，其中定理证明技术和符号执行技术适用范围最广，可验证性质最多，很多底层框架均有所涉及，而运行时验证技术属于轻量级的新验证技术，仍处于探索阶段.由此我们列出了一些关键问题如智能合约的自动化验证问题，转换一致性问题，形式化工具的信任问题和形式化验证的评判标准问题.本文还展望了未来形式化方法与智能合约结合的研究方向，对领域研究有一定的推动作用.

关键词: 形式化验证, 智能合约, 区块链, 隐私保护, 信息安全, 可信交易

Abstract: Formal methods are widely used in safety-critical software systems and have effective mathematical-based verification methods, while smart contracts belong to safety-critical codes. Using formal methods to verify smart contracts has become a popular research topic. This paper has conducted researches and analysis on 47 typical related papers since 2015 and carried out detailed classification research and comparative analysis on technology, as well as the formal methods, languages, tools and frameworks used in the formal verification of smart contracts overview. Research shows that theorem proving technique and symbolic execution technique have the widest scope of application, can verify the most properties and are involved in many basic frameworks. And the runtime verification is a new lightweight verification technology, still in the exploratory stage. From this, we have listed some key issues such as automatic verification of smart contracts, conversion consistency, trust in formal tools, and evaluation criteria for formal verification. This paper also looks forward for the future research direction on the combination of formal methods and smart contracts. For attracting more valuable ideas and promote the research in the field.

Key words: formal verification, smart contract, blockchain, privacy protection, information security, trusted transaction

中图分类号:

TP301

朱健, 胡凯, 张伯钧. 智能合约的形式化验证方法研究综述[J]. 电子学报, 2021, 49(4): 792-804.

ZHU Jian, HU Kai, ZHANG Bo-jun . Review on Formal Verification of Smart Contract[J]. Acta Electronica Sinica, 2021, 49(4): 792-804.

参考文献

[1] Nikolic I,et al.Finding the Greedy,Prodigal,and Suicidal Contracts at Scale[EB/OL].https://arxiv.org/abs/1802.06038,2018-05-14/2020-08-20.
[2] Amritarj Singh,Reza M Parizi,Zhang Qi,et al.Blockchain smart contracts formalization:approaches and challenges to address vulnerabilities[J].Computers & Security,2020,(88):1-10.
[3] Liu J,Liu Z.A survey on security verification of blockchain smart contracts[J].IEEE Access,2019,(7):77894-77904.
[4] 王璞巍,杨航天,孟佶,等.面向合同的智能合约的形式化定义及参考实现[J].软件学报,2019,30(9):2608-2619. Wang P W,Yang H T,Meng J,et al.Formal definition for classical smart contracts and reference implementation[J].Journal of Software,2019,30(9):2608-2619.(in Chinese)
[5] Leroy X.A formally verified compiler back-end[J].Journal of Automated Reasoning,2009,43(4):363-446.
[6] Bhargavan K,Delignat-Lavaud A,et al.Formal verification of smart contracts:short paper[A].The 2016 ACM Workshop on Programming Languages and Analysis for Security[C].USA:ACM,2016.91-96.
[7] Fan Zhang,Ethan Cecchetti,Kyle Croman,Ari Juels,Elaine Shi.Town Crier:an authenticated data feed for sma rt contracts[A].The 2016 ACM SIGSAC Conference on Computer and Communications Security[C].USA:ACM,2016.270-282.
[8] Nielsen B J,Spitters B.Smart Contract Interactions in Coq[EB/OL].https://arxiv.org/abs/1911.04732,2019-12-2/2020-8-20.
[9] Zhu J,Hu K,Filali M,et al.Formal Verification of Solidity Vontracts in Event-B[EB/OL].https://arxiv.org/abs/2005.01261,2020-5-4/2020-8-20.
[10] 胡凯,白晓敏,等.智能合约的形式化验证方法[J].信息安全研究,2016,2(12):1080-1089. Hu K,Bai X M,et al.Formal verification method of smart contract[J].Journal of Information Security Research,2016,2(12):1080-1089.(in Chinese)
[11] Grishchenko I,Maffei M,Schneidewind C.A semantic fr-amework for the security analysis of ethereum smart contracts[A].International Conference on Principles of Security and Trust[C].Germany:Springer,2018.243-269.
[12] Sun T,Yu W.A formal verification framework for security issues of blockchain smart contracts[J].Electronics,2020,9(2):254-255.
[13] Hirai Y.Defining the ethereum virtual machine for interactive theorem provers[A].International Conference on Financial Cryptography and Data Security[C].Germany:Springer,2017.520-535.
[14] Mulligan D P,Owens S,Gray K E,et al.Lem:Reusable engineering of real-world semantics[J].ACM SIGPLAN Notices,2014,49(9):175-188.
[15] Hildenbrandt E,et al.KEVM:A complete formal semantics of the ethereum virtual machine[A].2018 IEEE 31st Computer Security Foundations Symposium[C].USA:IEEE,2018.204-217.
[16] Sidney A,Myriam B,Maksym Bo,Mark Staples.Towards verifying ethereum smart contract bytecode in Isabelle/HOL[A].The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs[C].USA:ACM,2018.66-77.
[17] Daejun P,Zhang Y,Manasvi S,et al.A formal verification tool for ethereum VM bytecode[A].The 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering[C].USA:ACM,2018.912-915.
[18] Idelberger F,Governatori G,Riveret R,et al.Evaluation of logic-based smart contracts for blockchain systems[A].International Symposium on Rules and Rule Markup Languages for the Semantic Web[C].Germany:Springer,2016.167-183.
[19] Sergey I,Hobor A.A concurrent perspective on smart contracts[A].International Conference on Financial Cryptography and Data Security[C].Germany:Springer,2017.478-493.
[20] Sánchez D C.Raziel:Private and Verifiable Smart Contracts on Blockchains[OL].https://arxiv.org/abs/1807.09484,2018-7-25/2020-8-20.
[21] Schwartz E J,Avgerinos T,Brumley D.All you ever wanted to know about dynamic taint analysis and forward symbolic execution[A].2010 IEEE Symposium on Security and Privacy[C].USA:IEEE,2010.317-331.
[22] Luu L,Chu D H,Olickel H,et al.Making smart contracts smarter[A].The 2016 ACM SIGSAC Conference on Computer and Communications Security[C].USA:ACM,2016.254-269.
[23] Plotkin G D.A structural approach to operational semantics[J].Journal of Logic and Algebraic Programming,2004,60(61):121-134.
[24] Hierons R M,BogdanovK,Bowen J P,et al.Using formal specifications to support testing[J].ACM Computing Surveys,2009,41(2):1-76.
[25] Mueller B.Smashing ethereum smart contracts for fun and real profit[A].HITB SECCONF[C].USA:Hacker Noon,2018.1-10.
[26] Tsankov P,Dan A,Drachsler-Cohen D,et al.Securify:Practical security analysis of smart contracts[A].The 2018 ACM SIGSAC Conference on Computer and Communications Security[C].USA:ACM,2018.67-82.
[27] Nikolić I,Kolluri A,Sergey I,et al.Finding the greedy,prodigal,and suicidal contracts at scale[A].The 34th Annual Computer Security Applications Conference[C].USA:ACM,2018.653-663.
[28] Permenev A,Dimitrov D,Tsankov P,et al.Verx:safety verification of smart contracts[A].IEEE Symposium on Security and Privacy[C].USA:IEEE,2020.18-20.
[29] Wichmann B A,Canning A A,Clutterbuck D L,et al.Industrial perspective on static analysis[J].Software Engineering Journal,1995,10(2):69-75.
[30] Le T C,Xu L,Chen L,et al.Proving conditional termination for smart contracts[A].The 2nd ACM Workshop on Blockchains,Cryptocurrencies,and Contracts[C].USA:ACM,2018.57-59.
[31] Zhou E,Hua S,Pi B,et al.Security assurance for smart contract[A].International Conference on New Technologies,Mobility and Security[C].USA:IEEE,2018.1-5.
[32] Bang T,Nguyen H H,Nguyen D,et al.Verification of ethereum smart contracts:a model checking approach[J].International Journal of Machine Learning and Computing,2020,10(4):588-593.
[33] Z Yang,H Lei,W Qian.A hybrid formal verification system in Coq for ensuring the reliability and security of ethereum-based service smart contracts[J].IEEE Access,2020,(8):21411-21436.
[34] Hoare C A R.An axiomatic basis for computer programming[J].Communications of the ACM,1969,12(10):576-580.
[35] Christel B,Joost-Pieter K.Principles of Model Checking[M].MIT Press,2008.
[36] Clarke EM.The birth of model checking[A].Proc of the 25 Years of Model Checking[C].Germany:Springer,2008.1-26.
[37] Z Nehaï,P Piriou,F Daumas.Model-checking of smart contracts[A].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)[C].USA:IEEE,2018.980-987.
[38] T Abdellatif,K Brousmiche.Formal verification of smart contracts based on users and blockchain behaviors models[A].2018 9th IFIP International Conference on New Technologies,Mobility and Security[C].USA:IEEE,2018.1-5.
[39] Sistla A P,Gyuris V,Emerson E A.SMC:a symmetry-based model checker for verification of safety and liveness properties[J].ACM Transactions on Software Engineering and Methodology,2000,9(2):133-166.
[40] Bai X,Cheng Z,Duan Z,Hu K.Formal modeling and verification of smart contracts[A].2018 7th International Conference on Software and Computer Applications[C].USA:ACM,2018.322-326.
[41] Kalra S,Goel S,Dhawan M,Sharma S.ZEUS:analyzing safety of smart contracts[A].NDSS[C].USA:ISOC,2018.1-8.
[42] Antonino P,Roscoe A W.Formalizing and Verifying Smart Contracts with Solidifier:A Bounded Model Checker for Solidity[OL].https://arxiv.org/abs/2002.02710,2020-2-7/2020-8-20.
[43] Akash L,Shaz Q,Shuvendu K L.A solver for reachability modulo theories[A].International Conference on Computer Aided Verification[C].Germany:Springer,2012.427-443.
[44] Bigi G,Bracciali A,Meacci G,Tuosto E.Validation of decentralised smart contracts through game theory and formal methods[J].Programming Languages with Applications to Biology and Security,2015,9465:142-161.
[45] Alqahtani S,He X,Gamble R,et al.Formal verification of functional requirements for smart contract compositions in supply chain management systems[A].Hawaii International Conference on System Sciences[C].USA:University of Hawaii,2020.1-10.
[46] Scoca V,Uriarte R B,Nicola R D.Smart contract negotiation in cloud computing[A].2017 IEEE 10th International Conference on Cloud Computing[C].USA:IEEE,2017.592-599.
[47] Bernardi T,Dor N,Fedotov A,et al.WIP:Finding Bugs Automatically in Smart Contracts with Parameterized Invariants[EB/OL].https://www.certora.com/pubs/sbc2020.pdf,2020-9-5/2020-10-5.
[48] Biryukov A,Khovratovich D,Tikhomirov S.Findel:Secure derivative contracts forethereum[A].International Conference on Financial Cryptography and Data Security[C].Germany:Springer,2017.453-467.
[49] He X,Qin B,Zhu Y,et al.SPESC:A specification language for smart contracts[A].2018 IEEE 42nd Annual Computer Software and Applications Conference[C].USA:IEEE,2018.132-137.
[50] Yang Z,Lei H.Lolisa:Formal Syntax and Semantics for A Subset of the Solidity Programming Language[EB/OL].https://arxiv.org/abs/1803.09885,2018-5-27/2020-8-20.
[51] Park D,Zhang Y,Rosu G.End-to-end formal verification of ethereum 2.0 deposit smart contract[A].Computer Aided Verification[C].Germany:Springer,2020.151-164.
[52] Kosba A,Miller A,Shi E,Wen Z,Papamanthou C.Hawk:the blockchain model of cryptography and privacy-preserving smart contracts[A].2016 IEEE Symposium on Security and Privacy[C].USA:IEEE,2016.839-858.
[53] Canetti R.Universally composable security:a new paradigm for cryptographic protocols[A].Proceedings of 42nd IEEE Symposium on Foundations of Computer Science[C].USA:IEEE,2001.136-145.
[54] Goldwasser S,Micali S,Rackoff C.The knowledge complexity of interactive proof-systems[A].The 17th Annual ACM Symposium on Theory of Computing[C].USA:ACM,1985.291-304.
[55] Kim H,Laskowski M.A perspective on blockchain smart contracts:reducing uncertainty and complexity in value exchange[A].The 26th International Conference on Computer Communication and Networks[C].USA:IEEE,2017.1-6.
[56] Breidenbach L,Daian P,Tramèr F,Juels A.Enter the hydra:towards principled bug bounties and exploit-resistant smart contracts[A].The 27th USENIX Conference on Security Symposium[C].USA:ACM,2018.1335-1352.
[57] Chen L,Avizienis A.N-version programming:a fault-tolerance approach to reliability of software operation[A].The 25th International Symposium on Fault-Tolerant Computing[C].USA:IEEE,1995.113-120.
[58] Beillahi S M,Ciocarlie G,et al.Behavioral simulation for smart contracts[A].The 41st ACM SIGPLAN Conference on Programming Language Design and Implementation[C].USA:ACM,2020.470-486.
[59] Serge,I,Amrit K,Aquinas H.Scilla:A Smart Contract Intermediate-Level Language[EB/OL].https://arxiv.org/abs/1801.00687,2018-1-2/2020-8-20.
[60] Xu W,Glenn A F.Building Executable Secure Design Models for Smart Contracts with Formal Methods[OL].https://arxiv.org/abs/1912.04051,2019-12-9/2020-8-20.
[61] Mavridou A,Laszka A.Designing secure ethereum smart contracts:a finite state machine-based approach[A].International Conference on Financial Cryptography and Data Security[C].Germany:Springer,2018.523-540.
[62] Wang Y,Lahiri S K,Chen S,et al.Formal verification of workflow policies for smart contracts in Azure blockchain[A].Working Conference on Verified Software:Theories,Tools,and Experiments[C].Germany:Springer,2019.87-106.
[63] Petri C A.Communication with Automata[M].USA:Rome Laboratory,1966.
[64] Kurt J.Colored Petri Nets:Basic Concepts,Analysis Methods and Practical Use[M].USA:ACM,2010.
[65] Liu Z,Liu J.Formal verification of blockchain smart contract based on colored Petri net models[A].The 43rd Annual Computer Software and Applications Conference[C].USA:IEEE,2019.555-560.
[66] Wang D,Huang X,Ma X.Formal analysis of smart contract based on colored Petri nets[J].IEEE Intelligent Systems.2020,35(3):19-30.
[67] Bartocci E,Falcone Y.Lectures on Runtime Verification[M].Germany:Springer,2018.
[68] J Ellul,G J Pace.Runtime verification of ethereum smart contracts[A].2018 14th European Dependable Computing Conference[C].USA:IEEE,2018.158-163.
[69] Ao L,Jemin A C,Fan L.Securing smart contract with runtime validation[A].The 41st ACM SIGPLAN Conference on Programming Language Design and Implementation[C].USA:ACM,2020.438-453.

智能合约的形式化验证方法研究综述

Review on Formal Verification of Smart Contract

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	郭庆, 田有亮, 万良. 基于代理重加密的区块链数据受控共享方案[J]. 电子学报, 2023, 51(2): 477-488.
[2]	唐飞, 冯卓, 黄永洪. 基于区块链的公平可验证数据持有方案[J]. 电子学报, 2023, 51(2): 406-415.
[3]	张少波, 原刘杰, 毛新军, 朱更明. 基于本地差分隐私的K-modes聚类数据隐私保护方法[J]. 电子学报, 2022, 50(9): 2181-2188.
[4]	丁毅, 沈薇, 李海生, 钟琼慧, 田明宇, 李洁. 面向CNN的区块链可信隐私服务计算模型[J]. 电子学报, 2022, 50(6): 1399-1409.
[5]	佘维, 霍丽娟, 刘炜, 张志鸿, 宋轩, 田钊. 一种可隐藏敏感文档和发送者身份的区块链隐蔽通信模型[J]. 电子学报, 2022, 50(4): 1002-1013.
[6]	杨坤伟, 杨波, 周彦伟. 群智网络中基于区块链的有序聚合签名认证方案[J]. 电子学报, 2022, 50(2): 358-365.
[7]	郑锐, 汪秋云, 林卓庞, 靖蓉琦, 姜政伟, 傅建明, 汪姝玮. 一种基于威胁情报层次特征集成的挖矿恶意软件检测方法[J]. 电子学报, 2022, 50(11): 2707-2715.
[8]	袁水莲, 皮德常, 胥萌. 基于差分隐私的轨迹隐私保护方法[J]. 电子学报, 2021, 49(7): 1266-1273.
[9]	包象琳, 熊焰, 黄文超, 陈凯杰, 汪万森, 孟昭逸, 徐晓峰, 方贤进. 基于SmartVerif的比特币底层协议算力盗取漏洞发现[J]. 电子学报, 2021, 49(12): 2390-2398.
[10]	秦超霞, 郭兵, 沈艳, 苏红, 张珍, 周驰岷. 区块链的安全风险评估模型[J]. 电子学报, 2021, 49(1): 117-124.
[11]	郑孝遥, 罗永龙, 汪祥舜, 孙丽萍, 陈付龙, 胡桂银, 汪小寒. 基于位置服务的分布式差分隐私推荐方法研究[J]. 电子学报, 2021, 49(1): 99-110.
[12]	陈露, 相峰, 孙知信. 基于属性密码体制的区块链安全技术研究进展[J]. 电子学报, 2021, 49(1): 192-200.
[13]	陈传明, 林文诗, 俞庆英, 罗永龙. 一种基于单点收益的轨迹隐私保护方法[J]. 电子学报, 2020, 48(1): 143-152.
[14]	王继军, 李国祥, 夏国恩, 孙泽锐. 图像插值空间完全可逆可分离密文域信息隐藏算法[J]. 电子学报, 2020, 48(1): 92-100.
[15]	孙君, 熊关. SCMA mMTC系统中基于联盟区块链的无线电资源交易的信用支付[J]. 电子学报, 2019, 47(8): 1677-1684.