基于SmartVerif的比特币底层协议算力盗取漏洞发现

doi:10.12263/DZXB.20201194

电子学报 ›› 2021, Vol. 49 ›› Issue (12): 2390-2398.DOI: 10.12263/DZXB.20201194

基于SmartVerif的比特币底层协议算力盗取漏洞发现

包象琳¹^,², 熊焰², 黄文超², 陈凯杰², 汪万森², 孟昭逸², 徐晓峰¹, 方贤进³

^1.安徽工程大学计算机与信息学院, 安徽芜湖 241000
^2.中国科学技术大学计算机科学与技术学院，安徽合肥 230026
^3.安徽理工大学计算机科学与工程学院，安徽淮南 232001

收稿日期:2020-10-26 修回日期:2021-04-19 出版日期:2021-12-25
- 作者简介:
- 包象琳　女，1994年12月生于安徽芜湖，安徽工程大学计算机与信息学院教师.研究方向包括：区块链，形式化方法，网络与信息安全等.E-mail：baoxianglin@ahpu.edu.cn
  熊焰　男，1960年8月生于安徽合肥，中国科学技术大学计算机科学与技术学院教授、博士生导师.研究方向包括：计算机网络与信息安全，移动计算与移动网络，分布式处理等.E-mail：yxiong@ustc.edu.cn
  黄文超（通讯作者）男，1982年6月生于湖北宜昌，中国科学技术大学计算机科学与技术学院副教授.研究方向包括：信息安全，人工智能，移动计算，网络与系统安全自动化验证技术，Android系统安全等.E-mail：hangwc@ustc.edu.cn
  陈凯杰　男，1997年6月出生于安徽合肥，中国科技大学计算机科学与技术学院在读硕士研究生.研究方向包括：区块链，形式化方法.E-mail：ckjkevin@mail.ustc.edu.cn
  汪万森　男，1995年9月生于安徽合肥，中国科学技术大学计算机科学与技术学院在读博士生.研究方向包括：协议形式化验证，区块链.E-mail：wangws@mail.ustc.edu.cn
  孟昭逸　男，1992年5月生于安徽合肥，中国科学技术大学计算机科学与技术学院博士后研究员.研究方向包括：安卓安全，软件形式化验证等.E-mail：mzy516@ustc.edu.cn
  徐晓峰　男，1992年12月生于安徽芜湖，安徽工程大学计算机与信息学院讲师.研究方向包括：零样本学习，深度学习，机器学习，信息安全等.E-mail：xuxiaofeng@ahpu.edu.cn
  方贤进　男，1970年11月生于安徽舒城，安徽理工大学计算机科学与工程学院教授、博士生导师.研究方向包括：信息安全，数据挖掘等.E-mail：xjfang@aust.edu.cn
- 基金资助:
- 国家自然科学基金 (61972369); 国家重点研发计划 (2018YFB2100300); 安徽工程大学校级科研项目 (XJKY2020122); 安徽工程大学引进人才科研启动基金项目 (2020YQQ062)

Detection of the Computational Power Stealing Attack in Bitcoin Protocols Based on SmartVerif

BAO Xiang-lin¹^,², XIONG Yan², HUANG Wen-chao², CHEN Kai-jie², WANG Wan-sen², MENG Zhao-yi², XU Xiao-feng¹, FANG Xian-jin³

^1.School of Computer and Information, Anhui Polytechnic University, Wuhu, Anhui 241000, China
^2.School of Computer Science and Technology, University of Science and Technology of China, Hefei, Anhui 230026, China
^3.College of Computer Science and Engineering, Anhui University of Science and Technology, Huainan, Anhui 232001, China

Received:2020-10-26 Revised:2021-04-19 Online:2021-12-25 Published:2021-12-25
- Supported by:
- National Natural Science Foundation of China (61972369); National Key Research and Development Program of China (2018YFB2100300); Research Program of Anhui Polytechnic University (XJKY2020122); Research Fund for Talent Introduction of Anhui Engineering University (2020YQQ062)

摘要/Abstract

摘要：

比特币引入了一种新的P2P(Peer to Peer)交易方法，并依靠其底层协议实现去中心化交易.然而，由于目前缺乏对比特币各底层协议的细粒度形式化分析和系统建模，比特币安全性并未被保证.本文通过设计多维度的比特币安全模型引理和细粒度的比特币模型规则，系统地抽象了多协议组合运行考虑下的比特币协议实体交互，完成了对比特币的形式化符号建模与自动化安全分析.与以前的工作相比，本文更细粒度地建模了比特币协议实体及其相关操作，并全面设计了满足比特币各实体需求的安全属性.此外，本文利用自动化形式化验证系统SmartVerif实现了无需额外手工推导证明的形式化验证实验，通过将本文所建模的符号模型规则与引理作为SmartVerif的输入，发现了比特币底层协议算力盗取攻击.

关键词: 比特币, 区块链, 协议安全, 符号模型, 形式化分析

Abstract:

Bitcoin introduces a new P2P(Peer to Peer) trading method to the public and relies on its protocols to achieve decentralization. However, due to the lack of fine-grained formal analysis and systematic modeling of bitcoin, the security of bitcoin protocols is not guaranteed. We provide a comprehensive symbolic analysis of bitcoin protocols. Our work develops bitcoin model rules and model lemmas with the abstraction of in-protocol interactions and inter-protocols interactions. We refine the modeling of bitcoin protocol entities and their related protocol operations compared to the previous work, along with the comprehensive design of the security lemmas that bitcoin protocols should guarantee. The symbolic model rules and lemmas developed in our work are inputted into the automatic formal verification system SmartVerif. We find the computational power stealing attack and no additional manual work is needed for the model verification with the help of the SmartVerif.

Key words: bitcoin, blockchain, protocol security, symbolic model, formal analysis

中图分类号:

TP309

包象琳, 熊焰, 黄文超, 等. 基于SmartVerif的比特币底层协议算力盗取漏洞发现[J]. 电子学报, 2021, 49(12): 2390-2398.

Xiang-lin BAO, Yan XIONG, Wen-chao HUANG, et al. Detection of the Computational Power Stealing Attack in Bitcoin Protocols Based on SmartVerif[J]. Acta Electronica Sinica, 2021, 49(12): 2390-2398.

图/表 5

参考文献 19

1	NakamotoS. Bitcoin: A peer-to-peer electronic cash system[EB/OL]. ，2020-2-13.
2	TschorschF, ScheuermannB. Bitcoin and beyond: A technical survey on decentralized digital currencies[J]. IEEE Communications Surveys & Tutorials, 2016, 18(3): 2084 - 2123.
3	秦超霞, 郭兵, 沈艳, 等. 区块链的安全风险评估模型[J]. 电子学报, 2021, 49(1): 117 - 124.
	QinC X, GuoB, ShenY, et al. Security risk assessment model of blockchain[J]. Acta Electronica Sinica, 2021, 49(1): 117 - 124.(in Chinese)
4	陈露, 相峰, 孙知信. 基于属性密码体制的区块链安全技术研究进展[J]. 电子学报, 2021, 49(1): 192 - 200.
	ChenL, XiangF, SunZ X. A survey of blockchain security technologies based on attribute-based cryptography[J]. Acta Electronica Sinica, 2021, 49(1): 192 - 200.(in Chinese)
5	ContiM, Sandeep KumarE, LalC, et al. A survey on security and privacy issues of bitcoin[J]. IEEE Communications Surveys & Tutorials, 2018, 20(4): 3416 - 3452.
6	BastiaanM. Preventing the 51%-attack: a stochastic analysis of two phase proof of work in bitcoin[EB/OL]., 2020-2-14.
7	MillerA, LaViola JrJ J. Anonymous byzantine consensus from moderately-hard puzzles: A model for bitcoin[EB/OL]. , 2020-2-13.
8	EyalI, SirerE G. Majority is not enough: Bitcoin mining is vulnerable[A]. International Conference on Financial Cryptography and Data Security[C]. Berlin, Heidelberg: Springer, 2014. 436 - 454.
9	BlanchetB. Security protocol verification: Symbolic and computational models[A]. International Conference on Principles of Security and Trust[C]. Tallinn, Estonia:Springer, 2012. 3 - 29.
10	GarayJ, KiayiasA, LeonardosN. The bitcoin backbone protocol: Analysis and applications[A]. Annual International Conference on the Theory and Applications of Cryptographic Techniques[C]. Sofia, Bulgaria: Springer, 2015. 281 - 310.
11	GarayJ, KiayiasA, LeonardosN. The bitcoin backbone protocol with chains of variable difficulty[A]. Annual International Cryptology Conference[C]. Cham: Springer,2017. 291 - 323.
12	KiayiasA, PanagiotakosG. Speed-security tradeoffs in blockchain protocols[EB/OL]. ,2016.
13	DasP, FaustS, LossJ. A formal treatment of deterministic wallets[A]. Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security[C]. London, United Kingdom: ACM, 2019. 651 - 668.
14	CremersC, HorvatM, HoylandJ, et al. A comprehensive symbolic analysis of TLS 1.3[A]. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security[C]. Dallas, Texas, USA:ACM,2017. 1773 - 1788.
15	BasinD, DreierJ, HirschiL, et al. A formal analysis of 5G authentication[A].Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security[A]. Toronto, Canada: ACM, 2018. 1383 - 1396.
16	XiongY, SuC, HuangW, et al. Smartverif: Push the limit of automation capability of verifying security protocols by dynamic strategies[A]. 29th {USENIX} Security Symposium ({USENIX} Security 20) [C]. USA：{USENIX} Association, 2020.253 - 270.
17	LoweG. A hierarchy of authentication specifications[A]. Proceedings 10th Computer Security Foundations Workshop[C]. Rockport, MA, USA: IEEE, 1997. 31 - 43.
18	üstersR K, TruderungT, VogtA. Accountability: definition and relation-ship to verifiability [A]. Proceedings of the 17th ACM conference on Computer and Communications Security[C]. Chicago, Illinois, USA: ACM, 2010. 526 - 535.
19	DreierJ, KassemA, LafourcadeP. Formal analysis of e-cash protocols[A]. 2015 12th International Joint Conference on e-Business and Telecommunications (ICETE)(Volum:04)[C]. Colmar, France: IEEE, 2015. 65 - 75.

	可认证性	隐私性	可问责性	金额一致性
PP	PM：√	×	√	√
CP	NF： -	-	-	×
SP	WF：×	-	×	-
IP	PN： -	-	√	-
PP&CP	PM：× NF： -	×	-	×
CP&SP	NF： - WF：×	-	×	×
PP&IP	PM：√ PN： -	×	×	-

	可认证性	隐私性	可问责性	金额一致性
PP	PM：√	×	√	√
CP	NF： -	-	-	×
SP	WF：×	-	×	-
IP	PN： -	-	√	-
PP&CP	PM：× NF： -	×	-	×
CP&SP	NF： - WF：×	-	×	×
PP&IP	PM：√ PN： -	×	×	-

[1]	郭庆, 田有亮, 万良. 基于代理重加密的区块链数据受控共享方案[J]. 电子学报, 2023, 51(2): 477-488.
[2]	唐飞, 冯卓, 黄永洪. 基于区块链的公平可验证数据持有方案[J]. 电子学报, 2023, 51(2): 406-415.
[3]	佘维, 霍丽娟, 刘炜, 张志鸿, 宋轩, 田钊. 一种可隐藏敏感文档和发送者身份的区块链隐蔽通信模型[J]. 电子学报, 2022, 50(4): 1002-1013.
[4]	杨坤伟, 杨波, 周彦伟. 群智网络中基于区块链的有序聚合签名认证方案[J]. 电子学报, 2022, 50(2): 358-365.
[5]	郑锐, 汪秋云, 林卓庞, 靖蓉琦, 姜政伟, 傅建明, 汪姝玮. 一种基于威胁情报层次特征集成的挖矿恶意软件检测方法[J]. 电子学报, 2022, 50(11): 2707-2715.
[6]	朱健, 胡凯, 张伯钧. 智能合约的形式化验证方法研究综述[J]. 电子学报, 2021, 49(4): 792-804.
[7]	秦超霞, 郭兵, 沈艳, 苏红, 张珍, 周驰岷. 区块链的安全风险评估模型[J]. 电子学报, 2021, 49(1): 117-124.
[8]	陈露, 相峰, 孙知信. 基于属性密码体制的区块链安全技术研究进展[J]. 电子学报, 2021, 49(1): 192-200.
[9]	孙君, 熊关. SCMA mMTC系统中基于联盟区块链的无线电资源交易的信用支付[J]. 电子学报, 2019, 47(8): 1677-1684.
[10]	马晓婷, 马文平, 刘小雪. 基于区块链技术的跨域认证方案[J]. 电子学报, 2018, 46(11): 2571-2579.
[11]	陈祖希, 徐中伟, 霍伟伟, 喻钢. 基于Craig插值的线性混成系统符号化模型检测[J]. 电子学报, 2014, 42(7): 1338-1346.
[12]	韩志耕;罗军舟. 多方不可否认协议时限性分析与改进[J]. 电子学报, 2009, 37(2): 377-381.
[13]	谢鸿波;吴远成;刘一静;周明天. 一种安全协议的组合分析模型研究[J]. 电子学报, 2008, 36(11): 2262-2267.
[14]	陶志红, Hans Kleine Büning, 张世琨, 王立福. Dining Cryptographer安全协议及工程分析[J]. 电子学报, 2005, 33(2): 262-265.
[15]	范红, 冯登国. 一个非否认协议ZG的形式化分析[J]. 电子学报, 2005, 33(1): 171-173.

基于SmartVerif的比特币底层协议算力盗取漏洞发现

Detection of the Computational Power Stealing Attack in Bitcoin Protocols Based on SmartVerif

RichHTML

PDF

可视化

摘要/Abstract

引用本文

使用本文

图/表 5

参考文献 19

相关文章 15

编辑推荐

Metrics