一種比特幣支付協議的形式化建模驗證方法

王炯涵 黃文超 汪萬森 熊 焰

(中國科學技術大學計算機科學與技術學院 合肥 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驗證了該模型與其對應的安全屬性是否成立.基于驗證結果發現了一個此前沒有被討論過的比特幣支付過程中的安全威脅,分析了該問題成立的條件及可能的影響.本文的工作為對比特幣支付過程的形式化建模與驗證提供一種切實有效的方法,并且可以挖掘出一些可能的安全威脅,從而幫助構建更為安全有序的區塊鏈生態.