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

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

Abstract

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

CLC Number:

TP393

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.

Figures/Tables 13

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

References 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.

Metrics

Recommended 0

No Suggested Reading articles found!

函数可见性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中间语言	全自动

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

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

RichHTML

PDF下载

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 13

References 106

Related Articles 15

Metrics

Recommended 0

[1]	Zhao CAI, Tao JING, Shuang REN. Survey on Ethereum phishing detection technology [J]. Chinese Journal of Network and Information Security, 2023, 9(2): 21-32.
[2]	Heli WANG, Qiao YAN. Selfish mining detection scheme based on the characters of transactions [J]. Chinese Journal of Network and Information Security, 2023, 9(2): 104-114.
[3]	Beiyuan YU, Shanyao REN, Jianwei LIU. Overview of blockchain assets theft attacks and defense technology [J]. Chinese Journal of Network and Information Security, 2023, 9(1): 1-17.
[4]	Fei TANG, Ning GAN, Xianggui YANG, Jinyang WANG. Anti malicious KGC certificateless signature scheme based on blockchain and domestic cryptographic SM9 [J]. Chinese Journal of Network and Information Security, 2022, 8(6): 9-19.
[5]	Dan LIN, Kaixin LIN, Jiajing WU, Zibin ZHENG. Bytecode-based approach for Ethereum smart contract classification [J]. Chinese Journal of Network and Information Security, 2022, 8(5): 111-120.
[6]	Liquan CHEN, Xiao LI, Zheyi YANG, Sijie QIAN. Blockchain-based high transparent PKI authentication protocol [J]. Chinese Journal of Network and Information Security, 2022, 8(4): 1-11.
[7]	Feng LIU, Jie YANG, Jiayin QI. Survey on blockchain privacy protection techniques in cryptography [J]. Chinese Journal of Network and Information Security, 2022, 8(4): 29-44.
[8]	Xiaoling SONG, Yong LIU, Jingnan DONG, Yongfei HUANG. Application and prospect of blockchain in Metaverse [J]. Chinese Journal of Network and Information Security, 2022, 8(4): 45-65.
[9]	Lin JIN, Youliang TIAN. Multi-authority attribute hidden for electronic medical record sharing scheme based on blockchain [J]. Chinese Journal of Network and Information Security, 2022, 8(4): 66-76.
[10]	Pengkun JIANG, Wenyin ZHANG, Jiuru WANG, Shanyun HUANG, Wanshui SONG. Blockchain covert communication scheme based on the cover of normal transactions [J]. Chinese Journal of Network and Information Security, 2022, 8(4): 77-86.
[11]	Jianlin NIU, Zhiyu REN, Xuehui DU. Cross-domain authentication scheme based on consortium blockchain [J]. Chinese Journal of Network and Information Security, 2022, 8(3): 123-133.
[12]	Baoqin ZHAI, Jian WANG, Lei HAN, Jiqiang LIU, Jiahao HE, Tianhao LIU. Hierarchical proxy consensus optimization for IoV based on blockchain and trust value [J]. Chinese Journal of Network and Information Security, 2022, 8(3): 142-153.
[13]	Zhen GAO, Dongbin ZHANG, Xiao TIAN. Defense scheme for the world state based attack in Ethereum [J]. Chinese Journal of Network and Information Security, 2022, 8(2): 64-72.
[14]	Jiaren YU, Youliang TIAN, Hui LIN. Design of miner type identification mechanism based on reputation management model [J]. Chinese Journal of Network and Information Security, 2022, 8(1): 128-138.
[15]	Zhensheng GAO, Lifeng CAO, Xuehui DU. Research progress of access control based on blockchain [J]. Chinese Journal of Network and Information Security, 2021, 7(6): 68-87.