技術的突破是推動區塊鏈行業前進的引擎,幣安中國區塊鏈研究院與鏈聞 ChainNews 同爲密切關注區塊鏈與密碼學等領域技術發展前沿的組織,故而聯合推出「他山之石」專欄,向中文世界讀者介紹全球範圍最值得關注的區塊鏈技術進展,以及在金融等產業最新的應用分析與動態,以期爲中國的區塊鏈行業「攻玉」提供借鑑和思考。

本文解釋瞭如何用 TLA+證明 force-move 協議爲狀態通道提供了擔保,以確保你能提款。

原文標題:《【他山之石】使用 TLA+分析狀態通道
撰文:Tom Close,Magmo 團隊負責人。本文基於 Andrew Stewart 的工作成果,在此感謝 Mike Kerzhner 和 George Knee 提出寶貴的意見和建議。

本文已取得作者授權,並由鏈聞和幣安中國區塊鏈研究院獲得中文地區翻譯首發權

目前我們在本系列的文章已經做了諸多與狀態通道(state channel)相關的專題,其中一篇介紹了狀態通道的底層擔保機制:即在鏈是活動的且不存在監管的情況下,參與方能夠在有限的時間內提款。我們引入了狀體通道退出遊戲(exit game)的一個玩具模型,並證明了該模型能夠提供擔保機制。

爲了支持實際的應用,我們需要透過此玩具模型,轉向更先進的狀態通道系統,如此底層擔保機制便能發揮作用嗎?在本文中,我們闡述瞭如何使用 TLA+驗證工具來測試我們的協議,以及如何修復該工具檢測到的問題。

什麼是 TLA+及使用 TLA+的原因

自發布 force-move 白皮書後,我們便一直在探尋證明該協議正確性的方法。由於狀態通道涉及多個在鏈上和鏈外進行交互的參與方,所以很難照顧到所有的可能性。不過,我們肯定,這個協議沒有問題。但是,我們經常會擔心一些新出現的極端情況,直到確定沒有問題,我們的疑慮才能打消。我們希望能找到一種方法,避免將來出現無法處理的情況,從而消除人們對該協議是否健全的擔憂。

我們到底要證明什麼?在此前關於通道融資的文章中,開頭中提到了擔保機制:即在鏈是活動的且不存在監管的情況下,參與方能夠在有限的時間內提款。我們想證明,我們的狀態通道系統也具備這樣的特性。特別是,我們想證明,藉助通道中交換的狀態,無論其他參與方採取了什麼行動,Alice 總是能在鏈上找到通向最終結果的一條路徑。而且,這樣的結果應該是「最新的」,因爲其圈數(turn number)應至少與 Alice 當前的通道狀態一樣大。

出於其他的一些原因,我們首先研究了智能合約的形式驗證,很快我們就意識到形式驗證無法實現我們需要的擔保程度。智能合約的形式驗證能說明協議的實現沒有問題,但是無法證明協議本身具備我們期望的性質。例如,如果你提交了一次 force-move,並簽署上正確的狀態,形式驗證能證明註冊了一次質詢(challenge),但是用戶如果想要在有限的時間內退出,無論其如何操作,形式驗證無法證明用戶所調用的一系列 force-move 操作。

在此背景下,Andrew 發現並意識到也許 TLA+正是我們所需要的。

TLA+是一種形式化規範語言,用於搭建算法或系統模型的工具,然後以編程方式驗證此模型是否具備特定的屬性。1999 年,Leslie Lamport 發佈了這個工具,用來編寫證明 Byzantine Paxos 正確性的形式證明。近期,AWS 的工程團隊將其應用在了工業中,用於發現並修復 DynamoDB 中的併發性問題。

由於 TLA+的功能,有人將其描述成可充分測試的僞代碼。正是這一點使其符合我們的需要。我們意識到,可以基於裁決人(adjudicator)以及在通道中與之交互的參與方,搭建一個模型。藉助此模型及 TLA+,我們可以找出所有可允許操作的潛在序列,找出在哪些場景下,Alice 無法在指定的時段內提款。而且,如果我們能按照「對於長度爲 n 的所有可能的操作序列,Alice 能在 m 步之內取出其資金,且 m<n」,通過窮舉搜索證明一個聲明,那麼我們就知道 Alice 總是能在 m 步之內提款,從而也就證明了協議的安全性。

收穫的見解

本節總結了 TLA+在從初版到最新版的連續三版協議下的應用情況。在該狀態庫中可找到模型的代碼以及關於結果重建的說明。

在深入此模型之前,我們希望先呈現以下內容,因爲據我們猜測,會有很多人對這些內容感興趣。如果想了解全部的細節,建議先閱讀最後的「模型」章節。

第一次嘗試

我們首先嚐試了 force-move 白皮書中定義的協議版本,這一版協議對 gas 進行了優化。此協議與《上手狀態通道退出遊戲》(Playing the State Channel Exit)一文中的玩具模型非常相似,區別在於,在此版本下,可以從質詢中「恢復」並繼續進行鏈下交互,而不必在發起首次質詢後就結束。爲了防止質詢進入無限循環,裁決人需要跟蹤其觀察的最新受支持狀態的輪號,並且只能允許可使此數值增大的質詢。與裁決人進行交互的方法可總結如下:

他山之石 | 如何用 TLA+工具分析狀態通道?

這有一種發起質詢的方法:forceMove(m,s*,p) 操作要求受支持狀態 s*需要帶有輪號 m,並且該操作必須由通道參與方 p 發起。假設 m 大於鏈上的輪號,則通道轉換成質詢狀態 Chal(m,s,p)。

這裏有三種響應 force-move 的方式。分別是:respond、refute 和 altRespond:

respond:是響應質詢的「預期」方式

  • 響應人提供下一狀態,然後在鏈下繼續進行交互。
  • 鏈上的輪號計數器會計數,因爲響應狀態擴展了受支持的質詢狀態,故之後會再創建一個受支持的狀態。

refute:是響應狀態質詢的一種方式

  • 響應人提供由質詢人簽名的下一狀態。
  • 這麼做可以代表質詢人證明可證明的不良行爲,所以,此時有機會在協議中構建 slashing
  • 這種方式也非常高效,因爲我們不需要檢查任何狀態轉換
  • 由於參與方只能看到一個狀態,也就不需要告訴他們最新的受支持狀態,所以鏈上的輪號計數器不會計數

altRespond:當參與方用相同的輪號簽名了多個狀態時,需要用到這種方式來說明情況

  • 響應者提供一個會使輪號計數器+1 的新受支持狀態。由於下一個受支持狀態是可見的,所以鏈上的輪號計數器也會計數。
  • 這就是響應人在說:「你已經質詢了狀態 s,但你之前給我發了一個狀態 s',所以我想從 s' 那裏開始」

在任何情況下,由於性能優化的影響,必須提供質詢狀態 s 的一個副本,因爲在優化版中,鏈上只儲存了 s 的哈希值。接下來你會看到,這個看似微不足道的變化會對協議的健全性產生相當大的影響。

TLA+裁定

我們編寫了這個模型的代碼,接着在 TLA+中跑了一遍。TLA+並不喜歡這個模型,並且發現了以下失敗場景:

  1. 從 Open(n) 狀態開始
    2.Alice 調用了 forceMove(n,s, Alice)
    3.Eve 利用 forceMove(n,s
    , Eve) 進行超前交易(front-run),將裁決人至於 Chal(n, s, Eve) 狀態下。
    4.Alice 的 force-move 從第 2 步開始失敗。
    5.Eve 調用 refute(n+k,s,s'),其中 k 大於 1,這樣的話就輪到了 Eve,並且 s' 可以是任何輪號爲 n+k 的有效狀態。通道返回至 Open(n) 狀態。
  2. 轉到第 1 步。

TLA+發現了一個無限循環,這個循環使 Eve 可以將資金無限期地鎖定在通道中!當然,Eve 必須付款,但是,每次交易失敗時,Alice 也在損失資金。而且損失率非常偏向 Eve:對應 Alice 的一筆交易,Eve 只需提交兩筆交易(再加上一筆保險費,確保她每次都能超前交易)。無論如何,協議中都存在嚴重的漏洞。(實際上,我們事前已經對這個問題有所留意,但是我們沒有想到 TLA+所發現的攻擊方式會這麼容易實現。)

不過,修復辦法可不容易找到。造成這種循環的原因是 refute 不會使鏈上的輪號計數器計數,因爲參與方不一定會看到新的受支持狀態。驗證鏈上的交易是確定存在新的受支持狀態的唯一方法,但是 refute 的意義就在於取消可查驗的不良質詢,從而不耗費 gas 去運行鏈上的轉換函數(transition function)。

我們想出的一種辦法是在鏈上保存一份在當前的輪號計數器下已經成功調用了 force-move 的參與方名單,從而確保輪號計數器每次+1 時,參與方只能調用一次 force-move。由於對通道中參與方的數量沒有限制,我們認爲這樣做太複雜了,同時浪費 gas。
最終,我們決定完全刪除 refute 操作,以精簡該協議。去掉對狀態質詢響應的優化也不是什麼大問題,因此在此情況下,我們仍然可以選擇引入 slashing,同時退還響應人的 gas 費用,這樣似乎是一種更能激勵正確行爲的方式。

第二次嘗試

在刪除 refute 後,我們保留了以下操作:

他山之石 | 如何用 TLA+工具分析狀態通道?

TLA+裁定

我們在 TLA+中跑了一遍這個新模型。

這次的結果變好了:Alice 總是能使通道向前走。但是,其中仍存在造成損失的機會,Eve 可以拖延 Alice 一會兒,而具體拖多久則與當前的輪號成比例:

  1. 從 Open(0) 狀態開始
    2.Alice 調用 forceMove(n, s, Alice)
    3.Eve 利用 forceMove(0, s0, Eve) 進行超前交易(front-run),裁決人轉換至 Chal(0, s0, Eve)。
    4.Alice 的 force-move 失敗。
  2. 然後,Eve 調用 respond(1, s0, s1),將通道轉換至 Open (1)。(如果 Eve 想要將 Alice 的損失最大化,那麼她可以等到快超時再調用這個函數,因爲她知道 Alice 可能不再持有此狀態了)。
    6.Alice 調用 forceMove(n, s, Alice)
    7.Eve 利用 forceMove(1, s1, Eve) 進行超前交易
    8.……諸如此類

看來這裏出現的問題至少與第 4 步存在一定的關聯:forceMove 函數之所以失敗,是因爲在交易提交後,鏈的狀態已經變化了。我們意識到,forceMove 應當覆蓋之前的質詢,並且使操作儘可能適用於更多的鏈狀態似乎是不錯的設計原則。

第三次嘗試

在第三次嘗試時,我們重寫了 forceMove,使其能適用於質詢狀態,並且不再需要提供鏈上質詢狀態。在實現這一點的同時保證 gas 效率是個挺有趣的挑戰,因爲需要將大量的信息壓縮至現有的 bytes32 通道存儲區中。

此外,我們還考慮了另外的移動操作,也意識到了一些問題。首先,不應該將 altRespond 限制成僅使輪號+1,由於已經提供了完整的受支持狀態,所以,無論增加了多少,都應使輪號計數器增至該狀態的輪號。其次,這種情況不能僅發生在質詢狀態下,例如,當你需要長時間下線時,爲了先發制人地提前排除大多數質詢,根據開放狀態(open state)增加輪號計數器也是非常實用的。

綜上,altRespond 像是更基本的操作,因此我們決定將其重命名爲 checkpoint (檢查點)。然後,我們開始把 respond 視作更高效的 checkpoint 版本,用一個後續狀態,優化了對 force-move 的響應。
我們最終得到了以下一系列操作:

他山之石 | 如何用 TLA+工具分析狀態通道?

TLA+裁定

成功!TLA+沒發現任何問題,所以通過窮舉搜索,我們知道此協議是可靠的。

不僅如此,假如 Alice 提交了 forceMove(n,s,Alice),Alice 僅需一筆交易就能使通道向前走(或結束)。此交易失敗的唯一可能是鏈上輪號計數器的次數 >n,在此情況下,通道已經前進了,並且 Alice 完成了交易。如果交易成功,則裁決人處於 Chal(n,s,Alice) 狀態下,接下來的唯一可能是鏈上的輪號計數器計數或超時,從而結束通道。因此,僅提交一項交易,Alice 就實現了其目的。

這樣可以保證條理有序,因爲我們能嚴格限制 Alice 需要提交多少次交易才能退出通道:在最壞的情況下,Alice 需要調用 k 個事務,其中 k 是參與方的數量。第一個參與方 k-1 首先使通道向前走,直到輪到 Alice 爲止,如上所述,最後一個用來 force-move 她自己,完成後,她便不再響應。

協議建模

在本節中,我們將更詳細介紹如何設置 TLA+規範以上述內容。如果對本節不感興趣,可以放心地跳過。

在深入研究我們的 TLA+建模決策之前,值得花一點時間來回顧我們的狀態通道協議有哪些關鍵特性:force-move 協議圍繞輪流制構建。在通道中交換的每個狀態都有一個輪號,通過輪號可以確定哪個參與方在當時有權使通道向前走。例如,在有兩個參與方的通道中,如果第一個參與方負責所有的偶數輪號,第二個參與方負責所有的奇數輪號。那麼,一個狀態必須由當時輪到的那個人簽名,才能成爲有效狀態轉換的一部分。

另外,引入受支持狀態的概念也非常有用。在有 k 個參與方的通道中,受支持狀態 s*是 k 個狀態之間有效轉換的序列,其最終狀態爲 s:s1->...-> sk = s (這是根據代碼簡化而來,可以達到我們當前的說明意圖)。由於輪流屬性,受支持狀態總會包含各個參與方的簽名。受支持狀態類似於輪流制的完全簽名狀態,即表示所有參與方均參與了將通道推進至該狀態。

下一步是檢查我們要證明的內容,看看是否可以減少問題,以簡化輸入 TLA+的模型。

我們想證明,Alice 有一種策略,這種策略使她可以無視其他參與方所採取的操作,始終能在有限時間內得出鏈上最終敲定的最新結果。我們實際證明的是以下主張成立:

通道進度聲明:如果 Alice 看到最新受支持狀態的輪號是 n,那麼她可以(a)獲得一個輪號 > n 的受支持狀態,或者(b)確保通道結束時狀態的輪號 >= n。
爲什麼這就夠了?假設在輪號是 n + m 時會再次輪到 Alice。如果 Alice 不用這個輪號簽名任何狀態,那麼沒有受支持的狀態會帶有此輪號或更高的輪號。因此,通過應用 m 次通道進度聲明,唯一可能的結果是該通道最終結束時狀態的輪號 >= n。

我們還需要指定該聲明成立的條件。我們的模型捕捉了以下場景:

  • Alice 是狀態通道中一名誠實的參與方,持有受支持的狀態,狀態的輪號是 n。
  • Alice 的目標是(a)獲得一個輪號大於 n 的受支持狀態,或(b)在輪號大於等於 n 的狀態下關閉通道
  • Alice 只儲存了最後一輪的狀態,因此只能訪問最新受支持的狀態。(這很重要,因爲這意味着對於誠實的參與方而言,存儲需求會根據開放通道(open channel)的數量而非狀態總數來擴展。)
  • Alice 總是能在質詢期內將交易打包,但是無法進行超前交易,也無法阻止別人進行超前交易。
  • 僅在(a)輪到她的時候,Alice 才能給狀態簽名,並且(b)表示從她所持有的受支持狀態開始的有效轉換。
  • Eve 是她的對手,控制着通道中其他的參與方。
  • Eve 儲存了在通道中交易的所有歷史狀態。
  • Eve 願意給過去或未來的任何狀態簽名,但不表示從她所持有的受支持狀態開始的有效轉換。她無法簽名的狀態是那些輪到 Alice 簽名的狀態,其輪號 > n,因爲這些狀態只有 Alice 可以簽名,但她還沒簽。
  • Eve 可以任意地在 Alice 之前進行超前交易,但無法阻止 Alice 的交易在質詢期內被打包。

他山之石 | 如何用 TLA+工具分析狀態通道?

他山之石 | 如何用 TLA+工具分析狀態通道?

如何用 TLA+給此場景建模?如果你夠勇敢,可以去代碼中自己找,也可以看我們在這裏的總結概括。

首先要了解的是,TLA+規範涉及到了多個過程,這些過程創建了修改共享狀態的操作。在模擬系統時,TLA+會搜索通過插入過程操作創建的所有潛在序列,在達到共享狀態上的某些條件時,則會停止各個序列。

在我們的案例中,Alice 和 Eva 是獨立的過程,裁決人構成共享狀態的一部分。爲了捕獲到超前交易行爲,我們需要引入一個額外的過程和狀態——交易處理器(transaction processor)和交易池(transaction pool)。當 Eve 流程直接修改裁決人狀態時,Alice 只能將交易放入交易池中,然後交易池會把此交易交給裁決人。

他山之石 | 如何用 TLA+工具分析狀態通道?

他山之石 | 如何用 TLA+工具分析狀態通道?

TLA+的概念是「公平過程」(fair process),即其行動不會受到無限阻礙的過程。這正是我們建模「Eve 可以任意地在 Alice 之前進行超前交易,但 Alice 最終會得到一筆交易」的行爲所需要的工具。我們沒有明確地對超時本身進行建模,因爲我們知道,只要 Alice 或 Eve 持有能避免超時的狀態,她們一定會避免超時。因此,發生超時的情況恰好是無法採取其他行動的情況,而 TLA +會自動阻止這種情況的發生。

就成功標準而言,有必要把聲明從「Alice 可在有限的時間內成功」改成「Alice 可在 N 步內成功」,其中 N 由我們決定。在這樣的修改後,我們可以確保 TLA+是在有限的、可管理的狀態空間內進行搜索。

另外,我們還選出了一對參與方來進行模擬。具體地說,我們證明了「在任何由 2 個參與方組成的通道內,Alice 可以在 5 步內實現其目標」。當然,儘管還不足以證明所有通道的聲明,但是,確實爲由少量參與方組成的通道提供了堅實的保障,這正是我們在實際應用中所關心的。我們也越來越相信,這種方法適用於任意數量的參與方,即便有額外的參與方,也不會有任何變化——在設置模型時,我們就有這種感覺。

總結

在本文中,我們解釋瞭如何用 TLA+證明 force-move 協議爲狀態通道提供了擔保,以確保你能提款。

下週,隨着 Web3Torrent 項目的發佈,我們將從理論轉向實踐。Web3Torrent 改善了 Webtorrent 的點對點文件共享,在狀態通道上構建了點對點微支付。我們希望它能證明當今狀態通道的可能性,啓發更多人在其機制設計中使用微支付 / 狀態通道。敬請期待!

來源鏈接:blog.statechannels.org