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

作     者：包象琳 熊焰 黄文超 陈凯杰 汪万森 孟昭逸 徐晓峰 方贤进 BAO Xiang-lin;XIONG Yan;HUANG Wen-chao;CHEN Kai-jie;WANG Wan-sen;MENG Zhao-yi;XU Xiao-feng;FANG Xian-jin

作者机构：安徽工程大学计算机与信息学院安徽芜湖241000 中国科学技术大学计算机科学与技术学院安徽合肥230026 安徽理工大学计算机科学与工程学院安徽淮南232001 

基　　金：国家自然科学基金(No.61972369,No.61572453,No.61572454) 国家重点研发计划(No.2018YFB2100300) 安徽工程大学校级科研项目(No.XJKY2020122,No.XJKY2020119,No.XJKY2020120) 安徽工程大学引进人才科研启动基金项目(No.2020YQQ062) 

出 版 物：《电子学报》 (Acta Electronica Sinica)

年 卷 期：2021年第49卷第12期

页      码：2390-2398页

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

主 题 词：比特币 区块链 协议安全 符号模型 形式化分析 

学科分类：08[工学] 0839[0839] 081201[081201] 0812[工学-测绘类] 

核心收录：

D　O　I：10.12263/DZXB.20201194

馆 藏 号：203107097...