State-of-the-art survey of smart contract verification based on formal methods
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 use...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
POSTS&TELECOM PRESS Co., LTD
2022-08-01
|
| Series: | 网络与信息安全学报 |
| Subjects: | |
| Online Access: | http://www.cjnis.com.cn/thesisDetails#10.11959/j.issn.2096-109x.2022041 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1841529743404433408 |
|---|---|
| author | Wenbo ZHANG Simin CHEN Lifei WEI Wei SONG Dongmei HUANG |
| author_facet | Wenbo ZHANG Simin CHEN Lifei WEI Wei SONG Dongmei HUANG |
| author_sort | Wenbo ZHANG |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-d037ea612520499e8686b8de1cfdbfae |
| institution | Kabale University |
| issn | 2096-109X |
| language | English |
| publishDate | 2022-08-01 |
| publisher | POSTS&TELECOM PRESS Co., LTD |
| record_format | Article |
| series | 网络与信息安全学报 |
| spelling | doaj-art-d037ea612520499e8686b8de1cfdbfae2025-01-15T03:15:53ZengPOSTS&TELECOM PRESS Co., LTD网络与信息安全学报2096-109X2022-08-018122859573081State-of-the-art survey of smart contract verification based on formal methodsWenbo ZHANGSimin CHENLifei WEIWei SONGDongmei HUANGSmart 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.http://www.cjnis.com.cn/thesisDetails#10.11959/j.issn.2096-109x.2022041smart contractformal methodsblockchainEthereumprogram verification |
| spellingShingle | Wenbo ZHANG Simin CHEN Lifei WEI Wei SONG Dongmei HUANG State-of-the-art survey of smart contract verification based on formal methods 网络与信息安全学报 smart contract formal methods blockchain Ethereum program verification |
| title | State-of-the-art survey of smart contract verification based on formal methods |
| title_full | State-of-the-art survey of smart contract verification based on formal methods |
| title_fullStr | State-of-the-art survey of smart contract verification based on formal methods |
| title_full_unstemmed | State-of-the-art survey of smart contract verification based on formal methods |
| title_short | State-of-the-art survey of smart contract verification based on formal methods |
| title_sort | state of the art survey of smart contract verification based on formal methods |
| topic | smart contract formal methods blockchain Ethereum program verification |
| url | http://www.cjnis.com.cn/thesisDetails#10.11959/j.issn.2096-109x.2022041 |
| work_keys_str_mv | AT wenbozhang stateoftheartsurveyofsmartcontractverificationbasedonformalmethods AT siminchen stateoftheartsurveyofsmartcontractverificationbasedonformalmethods AT lifeiwei stateoftheartsurveyofsmartcontractverificationbasedonformalmethods AT weisong stateoftheartsurveyofsmartcontractverificationbasedonformalmethods AT dongmeihuang stateoftheartsurveyofsmartcontractverificationbasedonformalmethods |