电子学报 ›› 2021, Vol. 49 ›› Issue (4): 792-804.DOI: 10.12263/DZXB.20200723
朱健, 胡凯, 张伯钧
收稿日期:
2020-07-16
修回日期:
2020-10-07
出版日期:
2021-04-25
通讯作者:
作者简介:
基金资助:
ZHU Jian, HU Kai, ZHANG Bo-jun
Received:
2020-07-16
Revised:
2020-10-07
Online:
2021-04-25
Published:
2021-04-25
Corresponding author:
Supported by:
摘要: 形式化方法是在安全关键软件系统中被广泛采用而有效的基于数学的验证方法,而智能合约属于安全关键代码,采用形式化方法验证智能合约已经成为热点研究领域.本文对自2015年以来的47篇典型相关论文进行了研究分析,对技术进行了详细的分类研究和对比分析;对形式化验证智能合约的过程中使用的形式化方法、语言、工具和框架进行综述.研究表明,其中定理证明技术和符号执行技术适用范围最广,可验证性质最多,很多底层框架均有所涉及,而运行时验证技术属于轻量级的新验证技术,仍处于探索阶段.由此我们列出了一些关键问题如智能合约的自动化验证问题,转换一致性问题,形式化工具的信任问题和形式化验证的评判标准问题.本文还展望了未来形式化方法与智能合约结合的研究方向,对领域研究有一定的推动作用.
中图分类号:
朱健, 胡凯, 张伯钧. 智能合约的形式化验证方法研究综述[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. |
[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. |
阅读次数 | ||||||
全文 |
|
|||||
摘要 |
|
|||||