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

张文博; 陈思敏; 魏立斐; 宋巍; 黄冬梅

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

您当前的位置：

首页 >

文章列表页 >

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

专栏：区块链系统、智能合约与应用安全 | 更新时间：2024-06-03

- 基于形式化方法的智能合约验证研究综述
- State-of-the-art survey of smart contract verification based on formal methods
- 网络与信息安全学报 2022年8卷第4期页码：12-28
- 作者机构：
  
  1. 上海海洋大学信息学院，上海 201306
  2. 上海市高可信计算重点实验室，上海 200062
  3. 上海电力大学，上海 201306
- 作者简介：
  
  [ "张文博（1992− ），男，河南洛阳人，博士，上海海洋大学讲师，主要研究方向为形式化验证、理论计算机科学" ]
  [ "陈思敏（1998− ），女，安徽合肥人，上海海洋大学硕士生，主要研究方向为形式化验证、区块链" ]
  [ "魏立斐（1982− ），男，浙江绍兴人，博士，上海海洋大学副教授，主要研究方向为密码学与云计算安全" ]
  [ "宋巍（1977− ），女，山西大同人，博士，上海海洋大学教授、博士生导师，主要研究方向为计算机视觉、海洋大数据分析、软件工程等" ]
  [ "黄冬梅（1964− ），女，河南郑州人，上海电力大学教授、博士生导师，主要研究方向为大数据分析、机器学习及智能服务" ]
- 基金信息：
  
  国家自然科学基金;The National Natural Science Foundation of China(61872142;62102243;61972241);上海市青年科技英才扬帆计划;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
- DOI：10.11959/j.issn.2096-109x.2022041
  中图分类号： TP393
- 网络首发：2022-08，
  
  纸质出版：2022-08-15
- 稿件说明：
移动端阅览
张文博, 陈思敏, 魏立斐, 等. 基于形式化方法的智能合约验证研究综述[J]. 网络与信息安全学报, 2022,8(4):12-28.

Wenbo ZHANG, Simin CHEN, Lifei WEI, et al. 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.
张文博, 陈思敏, 魏立斐, 等. 基于形式化方法的智能合约验证研究综述[J]. 网络与信息安全学报, 2022,8(4):12-28. DOI： 10.11959/j.issn.2096-109x.2022041.

Wenbo ZHANG, Simin CHEN, Lifei WEI, et al. 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. DOI： 10.11959/j.issn.2096-109x.2022041.

摘要

智能合约是区块链技术应用的一个重要场景，智能合约技术实现了区块链的可编程化，提高了其扩展性，有广阔的应用前景。然而，一系列关于智能合约的安全事件造成了大量经济损失，削弱了人们的信心，安全性问题已经成为制约智能合约进一步发展的关键问题。如果合约设计和代码实现的过程中存在缺陷，可能会造成严重后果。而智能合约发布后无法修改，因此，在智能合约发布前对其正确性做出验证尤为重要。近年来，国内外学者在智能合约的验证领域取得了大量成果，但对这些研究成果的系统分析和总结相对较少。对以太坊的交易过程、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

关键词

Keywords

references

NAKAMOTO S . Bitcoin:a peer-to-peer electronic cash system [J ] . Consulted , 2008 : 1 - 49 .

BUTERIN V . A next-generation smart contract and decentralized application platform [R ] . White Paper , 2014 .

SZABO N . Formalizing and securing relationships on public networks [J ] . First Monday , 1997 , 2 ( 9 ).

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 .

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 .

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 .

CHRISTIDIS K , DEVETSIKIOTIS M . Blockchains and smart contracts for the Internet of Things [J ] . IEEE Access , 2016 , 4 : 2292 - 2303 .

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

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 .

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 .

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 .

The DAO smart contract [EB ] . 2016 .

An in-depth look at the parity multisig Bug [EB ] . 2017 .

The parity wallet vulnerability [EB ] . 2017 .

王戟 , 詹乃军 , 冯新宇 , 等 . 形式化方法概貌 [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 .

BONNEAU J , CLARK J , GOLDFEDER S . On bitcoin as a public randomness source [J ] . IACR Cryptology ePrint Archive , 2015 :1015.

DANNEN C . Introducing Ethereum and solidity [M ] . Berkeley : Apress , 2017 .

ANDRYCHOWICZ M , DZIEMBOWSKI S . Distributed cryptography based on the proofs of work [J ] . IACR Cryptology ePrint Archive , 2014 :796.

WOOD G . Ethereum:a secure decentralised generalised transaction ledger [J ] . Ethereum Project Yellow Paper , 2014 , 151 : 1 - 32 .

BUTERIN V . Dagger:a memory-hard to compute,memory-easy to verify scrypt alternative [R ] . 2013 .

BeautyChain Integer Overflow [EB ] . 2018 .

KingOfTheEtherThrone smart contract [EB ] .

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 .

KING J C . Symbolic execution and program testing [J ] . Communications of the ACM , 1976 , 19 ( 7 ): 385 - 394 .

CLARKE E M , GRUMBERG O , PELED D . Model checking [M ] . MIT Press , 1999 .

BIBEL W . Automated theorem proving [M ] . Wiesbaden : Vieweg+Teubner Verlag , 1987 .

Microsoft Corporation . The Z3 theorem prover [EB ] .

MUELLER B , . Smashing Ethereum smart contracts for fun and real profit [C ] // In 9th Annual HITB Security Conference (HITBSecConf) . 2018 .

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 .

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 .

KRUPP J , ROSSOW C . TEETHER:gnawing at Ethereum to automatically exploit smart contracts [C ] // Proceedings of 27th USENIX Security Symposium . 2018 : 1317 - 1333 .

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 .

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 .

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 .

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 .

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 .

ULLMAN J D . Principles of database and knowledge-base systems [J ] . Computer Science , 1988 .

JORDAN H , SCHOLZ B , SUBOTIĆ P , . Soufflé:on synthesis of program analyzers [C ] // Computer Aided Verification . 2016 : 422 - 430 .

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 .

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 .

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 .

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 .

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 .

HOLZMANN G J , CHECKER S M . The:primer and reference manual [J ] . Septiembre del , 2003 .

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 .

CAVADA R , CIMATTI A , JOCHIM C A , et al . Nusmv 2.4 user manual [J ] . CMU and ITC-IRST , 2005 .

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 .

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 .

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 .

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 .

SERGEY I , HOBOR A . A concurrent perspective on smart contracts [C ] // International Conference on Financial Cryptography and Data Security . 2017 : 478 - 493 .

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 .

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 .

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 .

ROSCOE A W . Understanding concurrent systems [M ] . London : Springer London , 2010 .

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 .

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 .

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 .

The coq proof assistant reference manual [EB ] .

NIPKOW T , WENZEL M , PAULSON L C . Isabelle/HOL [M ] . Berlin,Heidelberg : Springer , 2002 .

HIRAI Y , . Defining the Ethereum virtual machine for interactive theorem provers [C ] // International Conference on Financial Cryptography and Data Security . 2017 : 520 - 535 .

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 .

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 .

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 .

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 .

YANG Z , LEI H . FEther:an extensible definitional interpreter for smart-contract verifications in coq [J ] . IEEE Access , 2019 , 7 : 37770 - 37791 .

YANG Z , LEI H . Lolisa:formal syntax and semantics for a subset of the solidity programming language [J ] . arXiv:1803.09885 , 2008 .

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 .

SERGEY I , KUMAR A , HOBOR A . Temporal properties of smart contracts [C ] // International Symposium on Leveraging Applications of Formal Methods . 2018 : 323 - 338 .

SUN T Y , YU W S . A formal verification framework for security issues of blockchain smart contracts [J ] . Electronics , 2020 , 9 ( 2 ): 255 .

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 .

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 .

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 .

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 .

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 .

SERGEY I , KUMAR A , HOBOR A . Scilla:a smart contract intermediate-level language [J ] . arXiv preprint arXiv:1801.00687 , 2018 .

REYNOLDS J C , . Definitional interpreters for higher-order programming languages [C ] // Proceedings of the ACM Annual Conference . 1972 : 717 - 740 .

MAVRIDOU A , LASZKA A . Designing secure ethereum smart contracts:a finite state machine based approach [C ] // Financial Cryptography and Data Security , 2018 : 523 - 540 .

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 .

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 .

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 .

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 .

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 .

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 .

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 .

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 .

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 .

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 .

田国华 , 胡云瀚 , 陈晓峰 . 区块链系统攻击与防御技术研究进展 [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 .

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 .

CHEN H S , PENDLETON M , NJILLA L , et al . A survey on Ethereum systems security [J ] . ACM Computing Surveys , 2021 , 53 ( 3 ): 1 - 43 .

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 .

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 .

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 .

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 .

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 .

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 .

钱鹏 , 刘振广 , 何钦铭 , 等 . 智能合约安全漏洞检测技术研究综述 [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 .

章峰 , 史博轩 , 蒋文保 . 区块链关键技术及应用研究综述 [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 .

朱健 , 胡凯 , 张伯钧 . 智能合约的形式化验证方法研究综述 [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 .

Ethereum Foundation . The serpent contract-oriented programming language [EB ] .

Lisp-Like language [EB ] .

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 .

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 .

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 .

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 .

浏览量

693

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于GR算法的区块链智能合约漏洞检测

以太坊钓鱼诈骗检测技术综述

基于字节码的以太坊智能合约分类方法

基于区块链的访问控制技术研究进展

基于智能合约的高对抗性僵尸网络研究