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

• 学术论文 • 上一篇    下一篇

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

包象琳1,2, 熊焰2, 黄文超2, 陈凯杰2, 汪万森2, 孟昭逸2, 徐晓峰1, 方贤进3   

  1. 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-lin1,2, XIONG Yan2, HUANG Wen-chao2, CHEN Kai-jie2, WANG Wan-sen2, MENG Zhao-yi2, XU Xiao-feng1, FANG Xian-jin3   

  1. 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)

摘要:

比特币引入了一种新的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

中图分类号: