[1]王赫彬,郑长友,黄摇 松,等.以太坊智能合约安全形式化验证方法研究进展[J].计算机技术与发展,2021,31(09):104-111.[doi:10. 3969 / j. issn. 1673-629X. 2021. 09. 018]
　WANG He-bin,ZHENG Chang-you,HUANG Song,et al.Review:Secure Formal Verification Methods for Ethereum Smart Contracts[J].,2021,31(09):104-111.[doi:10. 3969 / j. issn. 1673-629X. 2021. 09. 018]
点击复制

以太坊智能合约安全形式化验证方法研究进展()
分享到：

《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]

卷:
31
期数:
2021年09期
页码:
104-111
栏目:
网络与安全
出版日期:
2021-09-10

文章信息/Info

Title:
Review:Secure Formal Verification Methods for Ethereum Smart Contracts
文章编号:
1673-629X(2021)09-0104-08
作者:
王赫彬1 ; 郑长友2 ; 黄摇 松2 ; 孙金磊1 ; 丁一先3
1. 中国人民解放军陆军工程大学 指挥控制工程学院,江苏 南京 210007;
2. 中国人民解放军陆军工程大学 全军军事训练软件测评中心,江苏 南京 210007;
3. 辽宁工程技术大学,辽宁 阜新 123000
Author(s):
WANG He-bin1 ; ZHENG Chang-you2 ; HUANG Song2 ; SUN Jin-lei1 ; DING Yi-xian3
1. School of Command and Control Engineering,Army Engineering University of PLA,Nanjing 210007,China;
2. Military Software Training and Evaluation Center,Army Engineering University of PLA,Nanjing 210007, China;
3. Liaoning Technical University,Fuxin 123000,?China
关键词:
以太坊; 智能合约; 形式化验证; 定理证明; 模型检测
Keywords:
Ethereum; smart contract; formal verification; theorem prove; model checking
分类号:
TP309;TP311
DOI:
10. 3969 / j. issn. 1673-629X. 2021. 09. 018
摘要:
以太坊智能合约是区块链技术的典型应用和实现。 由于智能合约一旦部署就难以修改,智能合约在上链之前的正确性显得至关重要。 虽然很多当前工作都对于智能合约漏洞的检测与预防进行了一系列研究,但是对于检查合约属性和范式的形式化验证方法还没有比较全面的总结。 首先介绍了智能合约基本的表示和编译方式、常用的编程语言、出现的漏洞类型和常见的形式化验证方法,并分析了形式化验证方法在智能合约方面的研究现状;然后,通过实验结果分析验证了两种现有的有界模型检测工具的检测好坏,对于某些具体的合约攻击,漏报率达到 30% 以上,现有形式化验证方法漏报率高、应用范围受限以及验证语言安全性未知等一系列缺陷亟待解决;最后,针对现有形式化验证方法存在的不足之处展望了未来的研究方向。
Abstract:
Ethereum smart contract is a typical application and implementation of block chain technology.? Since a? ?smart contract is difficult to be modified once it is deployed,thus it is important for coders to check smart contracts’ correctness before putting on the chains. Although there are many current researches of the vulnerability detection and prevention of smart contracts,no complete summary of the correctness and feasibility of concepts and properties of smart contracts,such as user interactions and specific technical concepts,are carried out. Firstly,basic representation and compilation,frequently-used programming languages, vulnerabilities of smart contracts and common formal verification methods were introduced. Secondly,the effectiveness of the two existing bounded model checking tools is checked and reproduced through the analysis of experiment results,false negative rate reaches 30% ,and it is urgent to correct weaknesses of the existing formal verification methods, such as high rate of false positives, limited applica-tion scopes, unknown security of the verification language and so on. Finally, the future research directions are prospected according to the limitations of these existing researches of formal verification methods.

相似文献/References:

[1]魏 艳,毛燕琴,沈苏彬.一种基于区块链的数据完整性验证解决方案[J].计算机技术与发展,2020,30(01):76.[doi:10. 3969 / j. issn. 1673-629X. 2020. 01. 014]
　WEI Yan,MAO Yan-qin,SHEN Su-bin.A Data Integrity Verification Solution Based on Blockchain[J].,2020,30(09):76.[doi:10. 3969 / j. issn. 1673-629X. 2020. 01. 014]
[2]汪 菲,沈苏彬.一种基于区块链的可信数据共享解决方案[J].计算机技术与发展,2020,30(09):115.[doi:10. 3969 / j. issn. 1673-629X. 2020. 09. 021]
　WANG Fei,SHEN Su-bin.A Solution for Decentralized Data Sharing Based on Blockchain[J].,2020,30(09):115.[doi:10. 3969 / j. issn. 1673-629X. 2020. 09. 021]
[3]朱诗生,李朝清,黄仁俊,等.基于区块链的医疗数据安全共享模型与机制[J].计算机技术与发展,2020,30(10):123.[doi:10. 3969 / j. issn. 1673-629X. 2020. 10. 023]
　ZHU Shi-sheng,LI Chao-qing,HUANG Ren-jun,et al.Secure Sharing Model and Mechanism of Medical Data Based on Block Chain[J].,2020,30(09):123.[doi:10. 3969 / j. issn. 1673-629X. 2020. 10. 023]
[4]文必龙,陈友良.基于区块链的企业数据共享模式研究[J].计算机技术与发展,2021,31(01):175.[doi:10. 3969 / j. issn. 1673-629X. 2021. 01. 031]
　WEN Bi-long,CHEN You-liang.Research on Enterprise Data Sharing Mode Based on Blockchain[J].,2021,31(09):175.[doi:10. 3969 / j. issn. 1673-629X. 2021. 01. 031]
[5]于爱荣,王 俊*,孙 海,等.基于区块链和智能合约的财务管理系统建设[J].计算机技术与发展,2021,31(04):164.[doi:10. 3969 / j. issn. 1673-629X. 2021. 04. 028]
　YU Ai-rong,WANG Jun*,SUN Hai,et al.Financial Management System Construction Based onBlockchain and Smart Contract[J].,2021,31(09):164.[doi:10. 3969 / j. issn. 1673-629X. 2021. 04. 028]
[6]李莎莎,姬永清,罗 盘,等.针对主从多链的区块链集成共识机制研究[J].计算机技术与发展,2021,31(08):82.[doi:10. 3969 / j. issn. 1673-629X. 2021. 08. 014]
　LI Sha-sha,JI Yong-qing,LUO Pan,et al.Research on Blockchain Integrated Consensus Mechanisms of Master and Slave Multi-chain[J].,2021,31(09):82.[doi:10. 3969 / j. issn. 1673-629X. 2021. 08. 014]
[7]陈传坤,谷立祥,颜廷贵.基于联盟链的指挥信息系统数据保护研究[J].计算机技术与发展,2021,31(10):105.[doi:10. 3969 / j. issn. 1673-629X. 2021. 10. 018]
　CHEN Chuan-kun,GU Li-xiang,YAN Ting-gui.Research on Data Protection of Command Information System Based on Consortium Blockchain[J].,2021,31(09):105.[doi:10. 3969 / j. issn. 1673-629X. 2021. 10. 018]
[8]左康达,孙知信.基于区块链技术的土建工程项目管理平台[J].计算机技术与发展,2021,31(12):187.[doi:10. 3969 / j. issn. 1673-629X. 2021. 12. 031]
　ZUO Kang-da,SUN Zhi-xin.A Civil Engineering Project Management Platform Based onBlockchain Technology[J].,2021,31(09):187.[doi:10. 3969 / j. issn. 1673-629X. 2021. 12. 031]
[9]郭子琪.基于区块链技术的粉丝贡献度系统设计[J].计算机技术与发展,2021,31(增刊):183.[doi:10. 3969 / j. issn. 1673-629X. 2021. S. 037]
　Olivia GUO.Design of Contribution System Based on Blockchain Technique[J].,2021,31(09):183.[doi:10. 3969 / j. issn. 1673-629X. 2021. S. 037]
[10]崔永杰,彭长根,丁红发,等.一种支持多用户的公平密文检索方案[J].计算机技术与发展,2022,32(10):100.[doi:10. 3969 / j. issn. 1673-629X. 2022. 10. 017]
　CUI Yong-jie,PENG Chang-gen,DING Hong-fa,et al.A Fair Searchable Encryption Scheme Supporting Multiple Users[J].,2022,32(09):100.[doi:10. 3969 / j. issn. 1673-629X. 2022. 10. 017]
[11]陈 曦,沈苏彬.一种基于区块链的存储资源可信分配方法[J].计算机技术与发展,2022,32(02):130.[doi:10. 3969 / j. issn. 1673-629X. 2022. 02. 021]
　CHEN Xi,SHEN Su-bin.A Storage Resource Allocation Method Based on Blockchain[J].,2022,32(09):130.[doi:10. 3969 / j. issn. 1673-629X. 2022. 02. 021]
[12]严国秀,沈苏彬.一种基于区块链的物联网标识管理方案[J].计算机技术与发展,2022,32(04):158.[doi:10. 3969 / j. issn. 1673-629X. 2022. 04. 027]
　YAN Guo-xiu,SHEN Su-bin.An Identity Management Solution of IoT Based on Blockchain[J].,2022,32(09):158.[doi:10. 3969 / j. issn. 1673-629X. 2022. 04. 027]
[13]毛典辉,梁秀霞,赵 爽,等.面向区块链平台的庞氏骗局模式检测方法[J].计算机技术与发展,2022,32(05):153.[doi:10. 3969 / j. issn. 1673-629X. 2022. 05. 026]
　MAO Dian-hui,LIANG Xiu-xia,ZHAO Shuang,et al.Ponzi Scheme Pattern Detection Method for Blockchain Platform[J].,2022,32(09):153.[doi:10. 3969 / j. issn. 1673-629X. 2022. 05. 026]
[14]李 铭,沈苏彬.一种基于区块链的自媒体版权管理方案[J].计算机技术与发展,2023,33(01):206.[doi:10. 3969 / j. issn. 1673-629X. 2023. 01. 031]
　LI Ming,SHEN Su-bin.A Solution for Self-media Copyright Management Based on Blockchain[J].,2023,33(09):206.[doi:10. 3969 / j. issn. 1673-629X. 2023. 01. 031]
[15]刘 江,沈苏彬.一种基于区块链的环境监测的可信管理[J].计算机技术与发展,2023,33(02):84.[doi:10. 3969 / j. issn. 1673-629X. 2023. 02. 013]
　LIU Jiang,SHEN Su-bin.A Trusted Management of Environmental Monitoring Based on Blockchain[J].,2023,33(09):84.[doi:10. 3969 / j. issn. 1673-629X. 2023. 02. 013]
[16]傅紫薇,沈子牛,陈云芳,等.以太坊智能合约的漏洞自动化修复技术研究[J].计算机技术与发展,2023,33(02):110.[doi:10. 3969 / j. issn. 1673-629X. 2023. 02. 017]
　FU Zi-wei,SHEN Zi-niu,CHEN Yun-fang,et al.Research on Automatic Vulnerability Repair Technology of Smart Contracts on Ethereum[J].,2023,33(09):110.[doi:10. 3969 / j. issn. 1673-629X. 2023. 02. 017]
[17]檀钟盛,陈春晖.基于区块链技术的疫情健康码方案[J].计算机技术与发展,2023,33(07):215.[doi:10. 3969 / j. issn. 1673-629X. 2023. 07. 032]
　TAN Zhong-sheng,CHEN Chun-hui.Epidemic Health Code Scheme Based on Blockchain Technology[J].,2023,33(09):215.[doi:10. 3969 / j. issn. 1673-629X. 2023. 07. 032]

更新日期/Last Update: 2021-09-10