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

doi:10.11959/j.issn.2096-109x.2022041

网络与信息安全学报 ›› 2022, Vol. 8 ›› Issue (4): 12-28.doi: 10.11959/j.issn.2096-109x.2022041

• 专栏：区块链系统、智能合约与应用安全 • 上一篇下一篇

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

张文博¹^,², 陈思敏¹, 魏立斐¹, 宋巍¹, 黄冬梅³

¹ 上海海洋大学信息学院，上海 201306
² 上海市高可信计算重点实验室，上海 200062
³ 上海电力大学，上海 201306

修回日期:2022-07-04 出版日期:2022-08-15 发布日期:2022-08-01
作者简介:张文博（1992− ），男，河南洛阳人，博士，上海海洋大学讲师，主要研究方向为形式化验证、理论计算机科学
陈思敏（1998− ），女，安徽合肥人，上海海洋大学硕士生，主要研究方向为形式化验证、区块链
魏立斐（1982− ），男，浙江绍兴人，博士，上海海洋大学副教授，主要研究方向为密码学与云计算安全
宋巍（1977− ），女，山西大同人，博士，上海海洋大学教授、博士生导师，主要研究方向为计算机视觉、海洋大数据分析、软件工程等
黄冬梅（1964− ），女，河南郑州人，上海电力大学教授、博士生导师，主要研究方向为大数据分析、机器学习及智能服务
基金资助:
国家自然科学基金(61872142);上海市青年科技英才扬帆计划(21YF1417000);上海市高可信计算重点实验室开放课题;上海市自然科学基金面上项目(18ZR1417300);上海市科委部分地方高校能力建设项目(20050501900);上海海洋大学青年教师科研启动项目

State-of-the-art survey of smart contract verification based on formal methods

Wenbo ZHANG¹^,², Simin CHEN¹, Lifei WEI¹, Wei SONG¹, Dongmei HUANG³

¹ College of Information Technology, Shanghai Ocean University, Shanghai 201306, China
² Shanghai Key Laboratory of Trustworthy Computing, Shanghai 200062, China
³ Shanghai University of Electric Power, Shanghai 201306, China

Revised:2022-07-04 Online:2022-08-15 Published:2022-08-01
Supported by:
The National Natural Science Foundation of China(61872142);Shanghai Sailing Program(21YF1417000);The Open Project of Shanghai Key Laboratory of Trustworthy Computing;Shanghai Natural Science Foundation(18ZR1417300);The Program for the Capacity Development of Shanghai Local Colleges(20050501900);Startup Foundation for Young Teachers of Shanghai Ocean University

摘要/Abstract

摘要：

智能合约是区块链技术应用的一个重要场景，智能合约技术实现了区块链的可编程化，提高了其扩展性，有广阔的应用前景。然而，一系列关于智能合约的安全事件造成了大量经济损失，削弱了人们的信心，安全性问题已经成为制约智能合约进一步发展的关键问题。如果合约设计和代码实现的过程中存在缺陷，可能会造成严重后果。而智能合约发布后无法修改，因此，在智能合约发布前对其正确性做出验证尤为重要。近年来，国内外学者在智能合约的验证领域取得了大量成果，但对这些研究成果的系统分析和总结相对较少。对以太坊的交易过程、gas 机制、存储结构、编写语言做了简要介绍，在此基础上调查归纳了智能合约中常见的8种漏洞类型，解释了漏洞产生的原因，回顾了一些真实发生的安全事件并给出了漏洞示例代码；根据不同的技术手段，如符号执行、模型检测、定理证明等，对智能合约的形式化验证工作做分类介绍，分析了各种方法的优劣，并选取了3个开源的自动化验证工具Mythril、Slither和Oyente，从运行效率、检测漏洞类型以及准确率等方面作出实验评估和对比；研究了目前已有的相关综述文章，总结了这些研究的区别与优势；概述了智能合约的漏洞检测技术中仍存在的关键问题，对智能合约验证工作的现状进行了分析和展望，提出了未来能够进一步研究的方向。

关键词: 智能合约, 形式化方法, 区块链, 以太坊, 程序验证

Abstract:

Smart contract represents an essential application scenario of blockchain technology.Smart contract technology improves programmability and scalability of blockchain, and has broad development prospects.However, a series of security incidents caused a great number of economic losses and weakened users’ confidence in the Ethereum platform.The security of smart contract has become a critical problem that restricts the further development of smart contract.Defects in smart contract code may cause serious consequences and cannot be modified once deployed, it is especially important to verify the correctness of smart contract in advance.In recent years, researchers have obtained many achievements in verification of smart contract, but there is a lack of systematic summary of these research results.Therefore, some basic principles of Ethereum were introduced, including the transaction, gas mechanism, storage and programming language.Eight common types of vulnerabilities in smart contract were summarized and their causes were explained.Some real security events were reviewed and some examples of vulnerability codes were presented.Then, the research work on automatic verification of smart contract based on symbolic execution, model checking and theorem proving was classified and summarized.Three open-source automated tools were selected, including Mythril, Slither and Oyente.And experiments were implemented to evaluate and compare the three tools from the aspects of efficiency, accuracy and the types of vulnerability can be detected.Furthermore, related review articles were surveyed, and the advantages of this paper compared with these works were summarized.The critical problems in the vulnerability detection technology of smart contract were also summarized and the direction of future research was proposed at last.

Key words: smart contract, formal methods, blockchain, Ethereum, program verification

中图分类号:

TP393

张文博, 陈思敏, 魏立斐, 宋巍, 黄冬梅. 基于形式化方法的智能合约验证研究综述[J]. 网络与信息安全学报, 2022, 8(4): 12-28.

Wenbo ZHANG, Simin CHEN, Lifei WEI, Wei SONG, Dongmei HUANG. State-of-the-art survey of smart contract verification based on formal methods[J]. Chinese Journal of Network and Information Security, 2022, 8(4): 12-28.

图/表 13

图1

图2

图3

图4

图5

表1

图6

图7

图8

图9

表2

表3

对smartbugs数据集中合约的漏洞检测进行补充标记Table 3 Additional flagging of vulnerability detection for contracts in the smartbugs dataset"

Mythril新检测出的漏洞	合约名	Slither新检测出的漏洞	合约名
SWC-124 CWE-123	arbitrary_location_write_simple.sol	SWC-124CWE-123	arbitrary_location_write_simple.sol
任意存储位置的写入	mapping_write.sol	任意存储位置的写入
			arbitrary_location_write_simple.sol
	crypto_roulette.sol		blackjack.sol
SWC-116 CWE-829	parity_wallet_bug_2.sol	SWC-102CWE-937	crypto_roulette.sol
时间戳依赖攻击	roulette.sol	使用过时的编译器版本	dos_address.sol
	spank_chain_payment.sol		dos_number.sol
			dos_simple.sol
	unchecked_return_value.sol
	etherstore.sol
SWC-107 CWE-829	governmental_survey.sol	SWC-119CWE-710	arbitrary_location_write_simple.sol
重入漏洞	dos_address.sol	合约内容矛盾	blackjack.sol
	reentrancy_dao.sol		ether_lotto.sol
	spank_chain_payment.sol
			auction.sol
			blackjack.sol
			crypto_roulette.sol
			eth_tx_order_dependence_minimal.sol
SWC-120 CWE-330	etherpot_lotto.sol	SWC-107 CWE-829	etherpot_lotto.sol
基于链属性的弱随机性	lottery.sol	重入漏洞	list_dos.sol
	open_address_lottery.sol		lotto.sol
			lucky_doubler.sol
			modifier_reentrancy.sol
			odds_and_evens.sol
			wallet_02_refund_nosub.sol
SWC-104 CWE-252	king_of_the_ether_throne.sol	SWC-135 CWE-1164	BECToken.sol
未检查的调用返回值		无效代码	random_number_generator.sol
	multiowned_vulnerable.sol
	odds_and_evens.sol		blackjack.sol
	old_blockhash.sol		crypto_roulette.sol
SWC-105 CWE-284	open_address_lottery.sol	CWE-338	lucky_doubler.sol
无保护的以太币提款	modifier_reentrancy.sol	使用密码学上较弱的伪随机数	etherpot_lotto.sol
	reentrance.sol	发生器	open_address_lottery.sol
	roulette.sol		random_number_generator.sol
	simple_dao.sol		roulette.sol
	wallet_04_confused_sign.sol
			blackjack.sol
			crypto_roulette.sol
			FindThisHash.sol
SWC-106 CWE-284	parity_wallet_bug_2.sol	SWC-108 CWE-710	etherstore.sol
无保护的自毁指令	simple_suicide.sol	未声明状态变量可见性	guess_the_random_number.sol
			etheraffle.sol
			king_of_the_ether_throne.sol
			list_dos.sol
			send_loop.sol
			crypto_roulette.sol
			etherstore.sol
SWC-112 CWE-829	proxy.sol	SWC-116 CWE-829	guess_the_random_number.sol
委托调用非可信合约		时间戳依赖攻击	king_of_the_ether_throne.sol
			roulette.sol
			Timelock.sol
			etherpot_lotto.sol
SWC-110 CWE-670	spank_chain_payment.sol	SWC-104 CWE-252	list_dos.sol
触发assert断言		未检查的调用返回值	lotto.sol
			lucky_doubler.sol
			blackjack.sol
SWC-113 CWE-703	send_loop.sol	SWC-133 CWE-294	crypto_roulette.sol
失败调用引发的DoS攻击		变长参数导致的哈希冲突	dos_address.sol
			king_of_the_ether_throne.sol

表3

表4

参考文献 106

[1]	NAKAMOTO S . Bitcoin:a peer-to-peer electronic cash system[J]. Consulted, 2008: 1-49.
[2]	BUTERIN V . A next-generation smart contract and decentralized application platform[R]. White Paper, 2014.
[3]	SZABO N . Formalizing and securing relationships on public networks[J]. First Monday, 1997,2(9).
[4]	PETERS G W , PANAYI E . Understanding modern banking ledgers through blockchain technologies:future of transaction processing and smart contracts on the internet of moneybanking beyond banks and money[M]. Springer, 2016.
[5]	AZARIA A , EKBLAW A , VIEIRA T ,et al. MedRec:using blockchain for medical data access and permission management[C]// Proceedings of 2016 2nd International Conference on Open and Big Data (OBD). 2016: 25-30.
[6]	GRIGGS K N , OSSIPOVA O , KOHLIOS C P ,et al. Healthcare blockchain system using smart contracts for secure automated remote patient monitoring[J]. Journal of Medical Systems, 2018,42(7): 130.
[7]	CHRISTIDIS K , DEVETSIKIOTIS M . Blockchains and smart contracts for the Internet of Things[J]. IEEE Access, 2016,4: 2292-2303.
[8]	?LNES S , UBACHT J , JANSSEN M . Blockchain in government:benefits and implications of distributed ledger technology for information sharing[J]. Government Information Quarterly, 2017,34(3): 355-364.
[9]	MENGELKAMP E , NOTHEISEN B , BEER C ,et al. A blockchain-based smart grid:towards sustainable local energy markets[J]. Computer Science-Research and Development, 2018,33(1): 207-214.
[10]	ABEYRATNE S A . Blockchain ready manufacturing supply chain using distributed ledger[J]. International Journal of Research in Engineering and Technology, 2016,5(9): 1-10.
[11]	ATZEI N , BARTOLETTI M , CIMOLI T . A survey of attacks on ethereum smart contracts (SOK)[C]// International Conference on Principles of Security and Trust. 2017: 164-186.
[12]	The DAO smart contract[EB]. 2016.
[13]	An in-depth look at the parity multisig Bug[EB]. 2017.
[14]	The parity wallet vulnerability[EB]. 2017.
[15]	王戟, 詹乃军, 冯新宇 ,等. 形式化方法概貌[J]. 软件学报, 2019,30(1): 33-61.
	WANG J , ZHAN N J , FENG X Y ,et al. Overview of formal methods[J]. Journal of Software, 2019,30(1): 33-61.
[16]	BONNEAU J , CLARK J , GOLDFEDER S . On bitcoin as a public randomness source[J]. IACR Cryptology ePrint Archive, 2015:1015.
[17]	DANNEN C . Introducing Ethereum and solidity[M]. Berkeley: Apress, 2017.
[18]	ANDRYCHOWICZ M , DZIEMBOWSKI S . Distributed cryptography based on the proofs of work[J]. IACR Cryptology ePrint Archive, 2014:796.
[19]	WOOD G . Ethereum:a secure decentralised generalised transaction ledger[J]. Ethereum Project Yellow Paper, 2014,151: 1-32.
[20]	BUTERIN V . Dagger:a memory-hard to compute,memory-easy to verify scrypt alternative[R]. 2013.
[21]	BeautyChain Integer Overflow[EB]. 2018.
[22]	KingOfTheEtherThrone smart contract[EB].
[23]	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. 2016: 254-269.
[24]	KING J C . Symbolic execution and program testing[J]. Communications of the ACM, 1976,19(7): 385-394.
[25]	CLARKE E M , GRUMBERG O , PELED D . Model checking[M]. MIT Press, 1999.
[26]	BIBEL W . Automated theorem proving[M]. Wiesbaden: Vieweg+Teubner Verlag, 1987.
[27]	Microsoft Corporation . The Z3 theorem prover[EB].
[28]	MUELLER B , . Smashing Ethereum smart contracts for fun and real profit[C]// In 9th Annual HITB Security Conference (HITBSecConf). 2018.
[29]	NIKOLI? I , KOLLURI A , SERGEY I ,et al. Finding the greedy,prodigal,and suicidal contracts at scale[C]// Proceedings of the 34th Annual Computer Security Applications Conference. 2018: 653-663.
[30]	MOSSBERG M , MANZANO F , HENNENFENT E ,et al. Manticore:a user-friendly symbolic execution framework for binaries and smart contracts[C]// Proceedings of 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2019: 1186-1189.
[31]	KRUPP J , ROSSOW C . TEETHER:gnawing at Ethereum to automatically exploit smart contracts[C]// Proceedings of 27th USENIX Security Symposium. 2018: 1317-1333.
[32]	PERMENEV A , DIMITROV D , TSANKOV P ,et al. VerX:safety verification of smart contracts[C]// Proceedings of 2020 IEEE Symposium on Security and Privacy. 2020: 1661-1677.
[33]	TORRES C F , SCHüTTE J , STATE R . Osiris:hunting for integer bugs in Ethereum smart contracts[C]// Proceedings of the 34th Annual Computer Security Applications Conference. 2018: 664-676.
[34]	TORRES C F , STEICHEN M . The art of the scam:demystifying honeypots in Ethereum smart contracts[C]// Proceedings of the 28th USENIX Security Symposium. 2019: 1591-1607.
[35]	CHEN T , ZHANG Y F , LI Z H ,et al. TokenScope:automatically detecting inconsistent behaviors of cryptocurrency tokens in ethereum[C]// Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. 2019: 1503-1520.
[36]	TSANKOV P , DAN A , DRACHSLER-COHEN D ,et al. Securify:practical security analysis of smart contracts[C]// Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. 2018: 67-82.
[37]	ULLMAN J D . Principles of database and knowledge-base systems[J]. Computer Science, 1988.
[38]	JORDAN H , SCHOLZ B , SUBOTI? P , . Soufflé:on synthesis of program analyzers[C]// Computer Aided Verification. 2016: 422-430.
[39]	KALRA S , GOEL S , DHAWAN M ,et al. ZEUS:analyzing safety of smart contracts[C]// Proceedings 2018 Network and Distributed System Security Symposium. 2018: 1-12.
[40]	FEIST J , GRIECO G , GROCE A . Slither:a static analysis framework for smart contracts[C]// Proceedings of 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB). 2019: 8-15.
[41]	TIKHOMIROV S , VOSKRESENSKAYA E , IVANITSKIY I ,et al. SmartCheck:static analysis of ethereum smart contracts[C]// Proceedings of 2018 IEEE/ACM 1st International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB). 2018: 9-16.
[42]	SCHNEIDEWIND C , GRISHCHENKO I , SCHERER M ,et al. Ethor:practical and provably sound static analysis of Ethereum smart contracts[C]// Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security. 2020: 621-640.
[43]	GRECH N , KONG M , JURISEVIC A ,et al. MadMax:surviving out-of-gas conditions in Ethereum smart contracts[J]. Proceedings of the ACM on Programming Languages, 2018,2: 1-27.
[44]	HOLZMANN G J , CHECKER S M . The:primer and reference manual[J]. Septiembre del, 2003.
[45]	BENGTSSON J , LARSEN K , LARSSON F ,et al. UPPAAL—a tool suite for automatic verification of real-time systems[C]// International Hybrid Systems Workshop. 1995: 232-243.
[46]	CAVADA R , CIMATTI A , JOCHIM C A ,et al. Nusmv 2.4 user manual[J]. CMU and ITC-IRST, 2005.
[47]	NEHA? Z , PIRIOU P Y , DAUMAS F . Model-checking of smart contracts[C]// Proceedings of 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. 2018: 980-987.
[48]	ABDELLATIF T , BROUSMICHE K L . Formal verification of smart contracts based on users and blockchain behaviors models[C]// Proceedings of 2018 9th IFIP International Conference on New Technologies,Mobility and Security (NTMS). 2018: 1-5.
[49]	BAI X M , CHENG Z J , DUAN Z B ,et al. Formal modeling and verification of smart contracts[C]// Proceedings of the 2018 7th International Conference on Software and Computer Applications. 2018: 322-326.
[50]	ANDRYCHOWICZ M , DZIEMBOWSKI S , MALINOWSKI D ,et al. Modeling bitcoin contracts by timed automata[C]// International Conference on Formal Modeling and Analysis of Timed Systems. 2014: 7-22.
[51]	SERGEY I , HOBOR A . A concurrent perspective on smart contracts[C]// International Conference on Financial Cryptography and Data Security. 2017: 478-493.
[52]	BARTOLETTI M , ZUNINO R . BitML:a calculus for bitcoin smart contracts[C]// Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. 2018: 83-100.
[53]	LANEVE C , COEN C S , VESCHETTI A . On the prediction of smart contracts’ behaviors[M]// From Software Engineering to Formal Methods and Tools,and Back. 2019: 397-415.
[54]	QU M X , HUANG X , CHEN X ,et al. Formal verification of smart contracts from the perspective of concurrency[C]// International Conference on Smart Blockchain. Springer,Cham, 2018: 32-43.
[55]	ROSCOE A W . Understanding concurrent systems[M]. London: Springer London, 2010.
[56]	LI X Y , SU C , XIONG Y ,et al. Formal verification of BNB smart contract[C]// Proceedings of 2019 5th International Conference on Big Data Computing and Communications (BIGCOM). 2019: 74-78.
[57]	WANG D , HUANG X , MA X F . Formal analysis of smart contract based on colored petri nets[J]. IEEE Intelligent Systems, 2020,35(3): 19-30.
[58]	LIU Z T , LIU J . Formal verification of blockchain smart contract based on colored petri net models[C]// Proceedings of 2019 IEEE 43rd Annual Computer Software and Applications Conference. 2019: 555-560.
[59]	The coq proof assistant reference manual[EB].
[60]	NIPKOW T , WENZEL M , PAULSON L C . Isabelle/HOL[M]. Berlin,Heidelberg: Springer, 2002.
[61]	HIRAI Y , . Defining the Ethereum virtual machine for interactive theorem provers[C]// International Conference on Financial Cryptography and Data Security. 2017: 520-535.
[62]	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.
[63]	ANNENKOV D , NIELSEN J B , SPITTERS B . ConCert:a smart contract certification framework in Coq[C]// Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. 2020: 215-228.
[64]	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. 2016: 91-96.
[65]	AMANI S , BéGEL M , BORTIN M ,et al. Towards verifying Ethereum smart contract bytecode in Isabelle/HOL[C]// Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. 2018: 66-77.
[66]	YANG Z , LEI H . FEther:an extensible definitional interpreter for smart-contract verifications in coq[J]. IEEE Access, 2019,7: 37770-37791.
[67]	YANG Z , LEI H . Lolisa:formal syntax and semantics for a subset of the solidity programming language[J]. arXiv:1803.09885, 2008.
[68]	LI X M , SHI Z P , ZHANG Q Y ,et al. Towards verifying ethereum smart contracts at intermediate language level[M]// Formal Methods and Software Engineering. 2019: 121-137.
[69]	SERGEY I , KUMAR A , HOBOR A . Temporal properties of smart contracts[C]// International Symposium on Leveraging Applications of Formal Methods. 2018: 323-338.
[70]	SUN T Y , YU W S . A formal verification framework for security issues of blockchain smart contracts[J]. Electronics, 2020,9(2): 255.
[71]	SWAMY N , HRI?CU C , KELLER C ,et al. Dependent types and multi-monadic effects in F[C]// Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2016: 256-270.
[72]	GRISHCHENKO I , MAFFEI M , SCHNEIDEWIND C . A semantic framework for the security analysis of Ethereum smart contracts[C]// Principles of Security and Trust. 2018: 243-269.
[73]	STEF?NESCU A , PARK D , YUWEN S J ,et al. Semantics-based program verifiers for all languages[J]. ACM SIGPLAN Notices, 2016,51(10): 74-91.
[74]	HILDENBRANDT E , SAXENA M , RODRIGUES N ,et al. KEVM:a complete formal semantics of the Ethereum virtual machine[C]// Proceedings of 2018 IEEE 31st Computer Security Foundations Symposium. 2018: 204-217.
[75]	JIAO J , KAN S L , LIN S W ,et al. Semantic understanding of smart contracts:executable operational semantics of solidity[C]// Pro ceedings of 2020 IEEE Symposium on Security and Privacy. 2020: 1695-1712.
[76]	SERGEY I , KUMAR A , HOBOR A . Scilla:a smart contract intermediate-level language[J]. arXiv preprint arXiv:1801.00687, 2018.
[77]	REYNOLDS J C , . Definitional interpreters for higher-order programming languages[C]// Proceedings of the ACM Annual Conference. 1972: 717-740.
[78]	MAVRIDOU A , LASZKA A . Designing secure ethereum smart contracts:a finite state machine based approach[C]// Financial Cryptography and Data Security, 2018: 523-540.
[79]	MAVRIDOU A , LASZKA A . Tool demonstration:FSolidM for designing secure Ethereum smart contracts[C]// International Conference on Principles of Security and Trust. 2018: 270-277.
[80]	MAVRIDOU A , LASZKA A , STACHTIARI E ,et al. VeriSolid:Correct-by-design smart contracts for Ethereum[C]// International Conference on Financial Cryptography and Data Security. 2019: 446-465.
[81]	GROSSMAN S , ABRAHAM I , GOLAN-GUETA G , ,et al. Online detection of effectively callback free objects with applications to smart contracts[J]. Proceedings of the ACM on Programming Languages, 2018,2: 1-28.
[82]	XUE Y X , MA M L , LIN Y ,et al. Cross-contract static analysis for detecting practical reentrancy vulnerabilities in smart contracts[C]// Proceedings of 2020 35th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2020: 1029-1040.
[83]	BARTOLETTI M , ZUNINO R . Verifying liquidity of Bitcoin contracts[C]// 8th International Conference on Principles of Security and Trust,POST 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software. 2019: 222-247.
[84]	KOLLURI A , NIKOLIC I , SERGEY I ,et al. Exploiting the laws of order in smart contracts[C]// Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. 2019: 363-373.
[85]	JIANG B , LIU Y , CHAN W K . ContractFuzzer:fuzzing smart contracts for vulnerability detection[C]// Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering. 2018: 259-269.
[86]	NGUYEN T D , PHAM L H , SUN J ,et al. sFuzz:an efficient adaptive fuzzer for solidity smart contracts[C]// Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering. 2020: 778-788.
[87]	LI A , CHOI J A , LONG F . Securing smart contract with runtime validation[C]// Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 2020: 438-453.
[88]	BIGI G , BRACCIALI A , MEACCI G ,et al. Validation of decentralised smart contracts through game theory and formal methods[M]// Programming Languages with Applications to Biology and Security. Springer,Cham, 2015: 142-161.
[89]	田国华, 胡云瀚, 陈晓峰 . 区块链系统攻击与防御技术研究进展[J]. 软件学报, 2021,32(5): 1495-1525.
	TIAN G H , HU Y H , CHEN X F . Research progress on attack and defense techniques in block-chain system[J]. Journal of Software, 2021,32(5): 1495-1525.
[90]	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]// International conference on Financial Cryptography and Data Security. 2016: 79-94.
[91]	CHEN H S , PENDLETON M , NJILLA L ,et al. A survey on Ethereum systems security[J]. ACM Computing Surveys, 2021,53(3): 1-43.
[92]	DURIEUX T , FERREIRA J F , ABREU R ,et al. Empirical review of automated analysis tools on 47,587 Ethereum smart contracts[C]// Proceedings of 2020 IEEE/ACM 42nd International Conference on Software Engineering (ICSE). 2020: 530-541.
[93]	DI ANGELO M , SALZER G . A survey of tools for analyzing Ethereum smart contracts[C]// Proceedings of 2019 IEEE International Conference on Decentralized Applications and Infrastructures. 2019: 69-78.
[94]	IMERI A , AGOULMINE N , KHADRAOUI D . Smart Contract modeling and verification techniques:a survey[C]// Proceedings of the 8th International Workshop on ADVANCEs in ICT Infrastructures and Services (ADVANCE 2020). 2020: 1-8.
[95]	PARIZI R M , DEHGHANTANHA A . Smart contract programming languages on blockchains:An empirical evaluation of usability and security[C]// International Conference on Blockchain. 2018: 75-91.
[96]	GRISHCHENKO I , MAFFEI M , SCHNEIDEWIND C . Foundations and tools for the static analysis of Ethereum smart contracts[C]// International Conference on Computer Aided Verification. 2018: 51-78.
[97]	TOLMACH P , LI Y , LIN S W ,et al. A survey of smart contract formal specification and verification[J]. ACM Computing Surveys, 2021,54(7): 1-38.
[98]	钱鹏, 刘振广, 何钦铭 ,等. 智能合约安全漏洞检测技术研究综述[J]. 软件学报, 2022,33(8): 3059-3085.
	QIAN P , LIU Z G , HE Q M . Smart Contract vulnerability detection technique:a survey[J]. Journal of Software, 2022,33(8): 3059-3085.
[99]	章峰, 史博轩, 蒋文保 . 区块链关键技术及应用研究综述[J]. 网络与信息安全学报, 2018,4(4): 22-29.
	ZHANG F , SHI B X , JIANG W B . Review of key technology and its application of blockchain[J]. Chinese Journal of Network and Information Security, 2018,4(4): 22-29.
[100]	朱健, 胡凯, 张伯钧 . 智能合约的形式化验证方法研究综述[J]. 电子学报, 2021,49(4): 792-804.
	ZHU J , HU K , ZHANG B J . Review on formal verification of smart contract[J]. Acta Electronica Sinica, 2021,49(4): 792-804.
[101]	Ethereum Foundation. The serpent contract-oriented programming language[EB].
[102]	Lisp-Like language[EB].
[103]	CHEN T , LI X Q , LUO X P ,et al. Under-optimized smart contracts devour your money[C]// Proceedings of 2017 IEEE 24th International Conference on Software Analysis,Evolution and Reengineering. 2017: 442-446.
[104]	O'CONNOR R , . Simplicity:a new language for blockchains[C]// Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security. 2017: 107-120.
[105]	YAMASHITA K , NOMURA Y , ZHOU E C ,et al. Potential risks of hyperledger fabric smart contracts[C]// Proceedings of 2019 IEEE International Workshop on Blockchain Oriented Software Engineering. Piscataway, 2019: 1-10.
[106]	BECKERT B , HERDA M , KIRSTEN M ,et al. Formal specification and verification of Hyperledger Fabric chaincode[C]// 3rd Symposium on Distributed Ledger Technology (SDLT-2018) co-located with ICFEM. 2018: 44-48.

函数可见性public(默认)	本合约	子合约	外部合约
函数可见性public(默认)	√	√	√
private	√	×	×
internal	√	√	×
external	×	×	√
注：“√”表示可被调用，“×”表示不可被调用、访问或更改。

分析方法	检测工具	检测对象	自动化程度
	Oyente	EVM字节码+以太坊的全局状态	全自动
符号执行/静态分析	Zeus	Solidity源码→LLVM的中间语言	全自动
	Securify	EVM字节码→静态单一赋值形式	全自动
	Mythril	Solidity源码+EVM字节码	全自动
	SPIN	Solidity源码→PROMELA语言，LTL公式	半自动
模型检测	UPPAAL	带时间约束的Solidity源码	半自动
	NuSMV	Solidity源码建模	半自动
	F*	Solidity源码+EVM字节码	半自动
	Isabelle/HOL	EVM字节码→Lem语言	半自动
定理证明	Coq	Solidity源码建模	半自动
	F*	Solidity代码和EVM字节码	半自动
其他	Slither	Solidity源代码→SlithIR中间语言	全自动

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

State-of-the-art survey of smart contract verification based on formal methods

在线阅读

pdf下载

可视化

摘要/Abstract

引用本文

使用本文

图/表 13

参考文献 106

相关文章 15

Metrics

推荐阅读 0

工具	平均处理时间/s	实验样本（合约数）	准确率
Mythril	94	143	79.02%
Slither	5	143	81.12%
Oyente	36	69	15%

[1]	蔡召, 荆涛, 任爽. 以太坊钓鱼诈骗检测技术综述[J]. 网络与信息安全学报, 2023, 9(2): 21-32.
[2]	王贺立, 闫巧. 基于交易记录特征的自私挖矿检测方案[J]. 网络与信息安全学报, 2023, 9(2): 104-114.
[3]	余北缘, 任珊瑶, 刘建伟. 区块链资产窃取攻击与防御技术综述[J]. 网络与信息安全学报, 2023, 9(1): 1-17.
[4]	唐飞, 甘宁, 阳祥贵, 王金洋. 基于区块链与国密SM9的抗恶意KGC无证书签名方案[J]. 网络与信息安全学报, 2022, 8(6): 9-19.
[5]	林丹, 林凯欣, 吴嘉婧, 郑子彬. 基于字节码的以太坊智能合约分类方法[J]. 网络与信息安全学报, 2022, 8(5): 111-120.
[6]	陈立全, 李潇, 杨哲懿, 钱思杰. 基于区块链的高透明度PKI认证协议[J]. 网络与信息安全学报, 2022, 8(4): 1-11.
[7]	刘峰, 杨杰, 齐佳音. 区块链密码学隐私保护技术综述[J]. 网络与信息安全学报, 2022, 8(4): 29-44.
[8]	宋晓玲, 刘勇, 董景楠, 黄勇飞. 元宇宙中区块链的应用与展望[J]. 网络与信息安全学报, 2022, 8(4): 45-65.
[9]	金琳, 田有亮. 基于区块链的多权限属性隐藏电子病历共享方案[J]. 网络与信息安全学报, 2022, 8(4): 66-76.
[10]	姜鹏坤, 张问银, 王九如, 黄善云, 宋万水. 基于正常交易掩盖下的区块链隐蔽通信方案[J]. 网络与信息安全学报, 2022, 8(4): 77-86.
[11]	翟宝琴, 王健, 韩磊, 刘吉强, 何嘉豪, 刘天皓. 基于信任值的车联网分层共识优化协议[J]. 网络与信息安全学报, 2022, 8(3): 142-153.
[12]	高镇, 张东彬, 田潇. 基于以太坊状态数据库的攻击与防御方案[J]. 网络与信息安全学报, 2022, 8(2): 64-72.
[13]	余佳仁, 田有亮, 林晖. 基于信誉管理模型的矿工类型鉴别机制设计[J]. 网络与信息安全学报, 2022, 8(1): 128-138.
[14]	高振升, 曹利峰, 杜学绘. 基于区块链的访问控制技术研究进展[J]. 网络与信息安全学报, 2021, 7(6): 68-87.
[15]	杨冠群, 刘荫, 徐浩, 邢宏伟, 张建辉, 李恩堂. 基于区块链的电网可信分布式身份认证系统[J]. 网络与信息安全学报, 2021, 7(6): 88-98.