一种比特币支付协议的形式化建模验证方法

王炯涵 黄文超 汪万森 熊 焰

(中国科学技术大学计算机科学与技术学院 合肥 230026)

比特币作为一种广受关注的数字货币体系,目前已经在全世界多个地区被广泛使用,目前日交易额规模为数十亿美元.比特币的高价值使得其成为黑客攻击的目标之一[1],因此比特币的安全分析逐渐成为人们所关注.比特币通过一系列的网络协议来运行,包括共识协议、支付协议、挖矿协议等,对这些协议的安全性分析已经有很多报道[2-8].但是在这些工作中针对比特币支付协议的分析还相当欠缺,尚未有一套针对支付过程的完整安全模型与可行的分析方法,使得大量在比特币网络中支付行为的安全性得不到保证.实现比特币支付协议的安全性分析面临3个主要问题:

第一,比特币支付协议作为一种非传统的网络协议,其相关规范比较模糊,许多执行标准并不清晰,仅在一些文档中作了简单说明,缺少一套用标准化的语法描述的完整模型供分析;

第二,现有的对比特币的安全分析方法大多基于手工的推理与分析,这种方法工作量大并且不易于拓展,需要一种更加简单易行的方法完成这一复杂的工作;

第三,针对这类体系尚未有一套标准的安全属性规范,仅有部分电子支付协议的安全属性可以参考.因此要实现针对支付协议的安全分析需要先提取具有代表性的支付流程与安全需求才能进行.

针对这些问题,本文从比特币社区规范出发,基于多重集合重写的建模语法建立了2个具有代表性的比特币支付协议的符号化模型,并从比特币的功能目标与分布式一致性的概念出发提出了对应的安全属性作为分析的基础.本文工作的贡献如下:

1) 为比特币支付协议建立了一套完整的符号化模型与安全属性;

2) 基于网络协议自动形式化验证工具Tamarin实现了对上述模型与属性的自动形式化验证,最终得到了对2个模型及相关安全属性的验证结果;

3) 基于验证结果发现了一种未被讨论过的比特币支付协议中的安全威胁,讨论了该问题可能产生的影响.

1 相关工作

目前针对比特币安全性问题的工作一部分主要集中在对比特币共识协议的安全性分析与对双花攻击的讨论上:Garay等人[2-3]为比特币共识协议提供了一种基于计算方法的形式化模型,并手工证明了比特币的共识安全;Eyal等人[4]为攻击者提出了一种最优的自私挖掘策略来分叉比特币区块链;Heilman等人[5]提出了比特币网络中的日蚀攻击并实际测算了比特币网络中网络分区与异步程度;而Saad等人[6]基于此进一步讨论了在比特币异步网络中存在的双花.还有一部分工作分析了比特币挖矿行为中可能的攻击:其中Gao等人[7]提出了一种算力调整与贿赂计算的新型挖矿攻击方法;包象琳等人[8]基于符号化的形式化验证分析了比特币的矿池协议,并发现了相应的漏洞.总体而言,现阶段针对比特币网络协议的分析尚未对比特币支付协议的安全性问题进行较为细致的讨论.

在对比特币支付过程的安全性分析方面,前人的工作主要集中在对比特币钱包程序的安全分析上,其中Das等人[9]的计算方法形式化分析了比特币确定性钱包的安全性,Dabrowski等人[10]分析了硬件钱包中在密钥管理上存在的问题,指出了硬件钱包在设计不当时也会带来严重的密钥泄露等问题.Hu等人[11]讨论了智能手机上的钱包程序面临的安全威胁,但是这些工作也都没有涉及对整个支付流程细致的分析.

2 比特币支付协议建模方法

2.1 协议过程确立

本文将关注重点放在比特币支付协议(1)比特币支付过程描述(https://developer.bitcoin.org/devguide/payment_processing.html)上.比特币支付协议规范了比特币的发送和接收方式、交易过程、比特币共识节点可以确认的合法交易格式以及比特币共识节点如何验证交易等一系列过程,是比特币作为数字货币使用的基础.支付过程的许多细节为了契合现实需求在不断演变中形成了一系列支付协议过程.其中比特币社区中有一系列比特币改进协议(2)比特币改进协议介绍(https://github.com/bitcoin/bips)(bitcoin improvement proposals, BIP),负责以各种方式改进比特币,这些协议用数字表明提案时间的先后.其中BIP70为比特币商家和支付方之间的支付过程提供了详细的规范.

本文实现了对比特币支付环境下的BIP70协议与一般交易流程的完整建模.BIP70协议是现行比特币社区中的个人用户与比特币商家进行交易的标准,具有重要的分析价值.BIP70其规定的交易过程为:首先比特币支付者将收到来自商家的支付链接或二维码,然后付款人使用其钱包软件与商家直接通信,钱包发送发票消息以确认商家的付款请求.验证信息后商家将返回一条确认消息.在接收到确认消息后,钱包确认支付,基于支付请求构建交易,并将交易发送给比特币商家.然后,商家检查交易并向付款人确认交易成功,同时将交易发送到比特币网络以纳入区块链.尽管已经有相关协议规范支付流程,但是在比特币社区中一些相对简单的交易模式仍然是被支持的,尤其是个人与个人之间的转账一般都是通过简单交易流程完成.基于经验与比特币平台早期的交易规范,我们总结出一般的交易流程为支付者在得到收款人的地址之后,会构造一个交易发送给比特币网络,然后在比特币网络收到该交易并验证上链后,收款方会访问比特币网络,观察给自己的交易是否存在,进而向收款人确认付款.2种交易过程主要区别在于给比特币网络发送交易的角色不同,BIP70协议是由商家发送与确认上链,一般的交易则由支付方发送交易,只需要收款方查看即可.

2.2 建模思路

在建模中,为了规避挖矿与共识传播等符号化模型难以表达的部分,模型中的比特币共识网络模型对实际的比特币共识网络进行了一定的抽象处理.具体地讲,模型中假设比特币网络内部处于较为理想的同步网络状态下,可以把整个比特币共识网络作为一个网络实体进行简化建模,这样的设置将会忽略共识分叉等问题,但是也可以使得研究分析重点能够集中到支付流程上来,这与工作的目标是一致的.在敌手模型上,信道部分本文工作中假设比特币交易者与比特币网络之间的信道是不安全的,并基于Dolev-Yao模型[17]赋予不安全的信道中的敌手以攻击能力.对于协议实体中的敌手,为了简化分析,本文工作中的假设协议实体都是诚实的,即都会按照符合协议规范的行为进行计算与通信.

2.3 符号化建模方法

2.3.1 消息格式建模

针对比特币交易协议中的诸多消息格式进行符号化建模问题,本文基于Tamarin对基本的密码学原语的支持,通过适当的抽象构建各个消息的核心部分.例如,比特币支付协议中的地址尽管在实际实现上是通过脚本方式构建,但是其逻辑内核仍然是一个公钥地址,因此本文就通过简单的公钥地址原语构建地址类型的消息.Tamarin会基于内置的或者用户自定义的模理论完成不同的对协议消息的运算[17].这样符号化的定义配合简单的模理论足以实现对比特币交易过程中针对核心消息的运算的描述.同时需要指出的是,Tamarin中支持基于别名的定义方式,这使得建立的符号模型易于修改与拓展,在需要额外表达新的协议结构时只需要修改别名的解释作拓展即可,不影响原有消息格式的表达.

2.3.2 协议逻辑建模

协议逻辑包括3个方面:协议角色的状态转移、信道上的消息的收发与对协议执行轨迹的逻辑约束.针对协议角色的状态转移,本文的建模方法是通过显式地建模每个角色在执行过程中的状态,将其作为多重集合中一个事实,通过一条多重集合重写规则应用时所产生的从前置状态l到后置状态r的转化,实现协议角色从一个状态到另一个状态的转化,从而完成协议角色的状态迁移的描述,并且可以用重写规则中的标记动作a来标记协议步骤的执行或者用于添加约束.针对信道上消息的收发,本文通过Tamarin内置的Out与In事实,分别代表协议角色在公共信道上的消息收发行为进行解决.同时Tamarin自身会在模型中添加基于Dolev-Yao敌手模型的模型规则[17].用于描述不安全信道上的敌手行为.

如图1所示,可通过如下规则完成BIP70协议中交易验证行为的描述:

图1 BIP70协议模型规则示例

图1代码示例中给出了BIP70协议中的一条具体的模型规则实例,该规则描述了比特币商家进行交易发送时的过程,其中let和in字段申明了模型中变量别名的具体含义;箭头前括号中谓词B_3为前置事实,表明了该模型规则使用时所需要的状态条件;箭头中2个谓词VerfiTrans_ture与Eq分别为动作标识谓词与约束谓词,分别用于后续安全属性的构建与执行约束的构建;箭头后括号中的谓词为后置事实,描述了将该规则对应行为发生后系统的状态与行为.

基于以上建模方法,本文完整的模型代码示例被展示在公开的代码仓库(4)https://gitee.com/wang-jionghan/bitcoin-payment-protocol-model.git中.

2.4 安全属性设置

对比特币支付过程的分析中目前还缺少一个明确的安全属性定义,在交易过程中一个核心的目标是所有参与方应该就交易的各方面内容达成一致,鉴于此本文提出一组基于一致性概念的安全属性.这里所有的参与方指在支付中的被支付者、支付者以及比特币共识网络三方,而在比特币交易系统中,一笔交易真正生效的凭据是被打包进入某个区块中,此时将一笔交易作为一次有效交易,故一致性的属性应该是针对有效交易而言,比特币网络、商家、支付者能够就其内容达成一致.

考虑到协议中商家与支付者之间的信道被设置为安全信道,那么双方就交易内容达成一致是不需要考察的,因此需要重点关注的是一笔被比特币共识网络所确认的有效交易的交易信息能否与商家和支付者达成一致.基于以上考量,阐述支付过程中的一致性属性如下:

1) 当一笔交易被比特币网络所确认上链时,商家与支付者应该最终能够确认这比交易,并且交易中的关键参数保持一致;

2) 当商家或者支付者确认一笔交易已经发生时,这笔交易必须已经被比特币网络所确认上链.

这些属性事实上对应了对比特币交易双方的财产保护,如果一笔交易已经被比特币网络所确认,但是支付者却认为自己发送出的交易是失效的,那么就对应了支付者的财产损失.同理,如果一笔交易没有被比特币网络所确认,但是商家却错误地认为自己接受了这比交易,则对应了商家的财产损失.这样的属性设置参考了在电子支付协议中洛氏分类法中认证性研究与Jannik对金额一致性的定义[18-19].同时这样的属性描述可以通过一阶谓词逻辑的语言所表达,这与本文使用的验证工具的表达能力相吻合.

在构建了对比特币交易过程安全属性的自然表述之后,还需要基于自动化验证系统Tamarin输入的形式[17]完成该安全属性的符号化定义,具体的属性设置参考前述模型示例文件中的lemma部分.以BIP70协议中的属性1)为例,该属性可以被形式化为图2所示:

图2 安全属性示例

3 验证结果与安全威胁分析

3.1 验证结果

在完成协议运行规则建立后,在执行时Tamarin工具将分析规则的执行轨迹,以验证模型安全属性,模型规则执行后,对应结果状态事实将被Tamarin添加到当前状态集合中,前置状态事实则被移除,从而完成对程序状态转移的刻画.验证中Tamarin采用反证法的思路,通过对待验证属性的反命题进行约束求解,如果求解器可以求解得到一条不满足属性的模型运行轨迹,则说明待验证属性不成立,若证明得到这样的运行轨迹不存在,则等价证明了待验证属性成立[17].使用自动化形式验证工具Tamarin对上述模型进行推理验证,最终结果如表1所示:

表1 比特币支付协议的验证结果

对2个不同协议的验证最终得到一致的结果.在一致性属性1)的验证中,验证工具报告了违反安全属性的攻击执行路径,本文在3.2节详细分析这些攻击.对于一致性属性2),2个模型都得到成功验证.这一安全属性得到保证的原因是由于限制了敌手计算能力,因此其无法伪造交易在链上被确认的证据,这样的设置与结论总体上也符合区块链网络的实际情况.

3.2 攻击方式分析

在3.1节对比特币支付协议的符号化模型进行形式化验证的验证结果中发现BIP70协议与一般支付过程协议模型都不满足2.4节中所设置的属性1),基于观察推理证明脚本,发现一种对比特币支付过程进行攻击的全新方式,基于该攻击的执行路径可以将其命名为失败-重放攻击,正是这一攻击使得2.4节中所设置的属性1)被破坏.

攻击发生在支付者或商家与比特币网络之间的不安全信道中,当支付者或商家将一笔交易发送给比特币网络时,该消息被敌手所阻断,并且敌手可以通过构造无效交易获得比特币网络对于无效交易的响应,并且伪装成比特币网络将这样的响应发送给交易双方,因此支付者或商家会得到一个交易失败的结果.但是敌手可以在后续将这个交易发送给比特币网络,而比特币网络会接收并且执行这笔原始的交易.这样支付者就会在不知情的状况下损失这笔交易对应的比特币.图3示出在BIP70协议中执行失败-重放攻击的模式,在一般支付过程中该攻击路径是类似的.

图3 失败-重放攻击执行路径

3.3 安全威胁与缓解方法

从上述的攻击模式可以看出,这类攻击实现的充分条件是敌手可以完全控制商家或支付者与比特币网络之间的信道,这等价于对相应的用户实行了日蚀攻击.在比特币网络中执行日蚀攻击可以基于长时间的地址污染与拒绝服务攻击来实现[4].另一方面,这一攻击实现的必要条件在于可以拦截到比特币网络中的针对某笔交易的特定流量,这种攻击在传统的网络流量劫持中尚未讨论,但是原有的网络流量劫持方法仍然可以以一定的概率实现这一目标[20].综上所述,这种新的攻击方式具有理论上的可行性,是一种对比特币支付协议的潜在威胁.该攻击在现实中可能造成的威胁包括使得支付者的财产造成损失,以及若支付者在不知情的情况下如果重复使用这次被攻击的交易中的UTXO,则有可能会被判定为使用双花攻击的不诚实支付者,进而遭到惩罚.

4 结 语

基于比特币社区一般性规范与其数字货币功能属性,本文提出并建立了比特币支付协议的符号模型与安全属性,介绍了针对比特币支付协议的详细的符号化建模方法.并且进一步使用自动形式化验证工具Tamarin验证了该模型与其对应的安全属性是否成立.基于验证结果发现了一个此前没有被讨论过的比特币支付过程中的安全威胁,分析了该问题成立的条件及可能的影响.本文的工作为对比特币支付过程的形式化建模与验证提供一种切实有效的方法,并且可以挖掘出一些可能的安全威胁,从而帮助构建更为安全有序的区块链生态.