引介：形式化驗證Gasper共識機制的終局性
編者按：本文來自以太坊愛好者（ID：ethfans）編者按：本文來自
以太坊愛好者（ID：ethfans）
以太坊愛好者（ID：ethfans）
以太坊愛好者（ID：ethfans）
Gasper
以太坊愛好者（ID：ethfans）
一級標題
以太坊愛好者（ID：ethfans）
一級標題
二級標題
我們很高興宣布，Runtime Verification 和以太坊基金會長久合作中的另一大里程碑圓滿成功：我們開發了一套形式框架來模擬和驗證信標鏈協議，並成功形式化地證明了Gasper 終局性的正確性（correctness）；並且，我們還使用這些結果證明了信標鏈的Gasper 抽象實現同樣具備這些屬性。模型和證明腳本都可以在此處找到。
一級標題
二級標題
信標鏈協議是一套新的權益證明協議，是以太坊未來的重大升級“以太坊2.0” 的核心。在信標鏈協議中，參與的節點（或者叫“驗證者”）都在系統中存有保證金（stake，形式為ETH）。驗證者通過向網絡提交“見證消息（attestation）” 來證實區塊的有效性並為其多種屬性投票。信標鏈協議本身包含了多種工具，以幫助驗證者們對區塊鏈的最新狀態達成共識。
二級標題
當且僅當條件滿足：（1）來源檢查點B0 已得到合理化；（2）大多數人（即至少2/3 的驗證者）同樣投票給B0-B1 來源-目標對；則目標檢查點B1就經由來源檢查點B0 得到了合理化。
正文
如果驗證者嘗試偏離協議要求、提交自相矛盾的投票，則該驗證者會被懲罰：其保證金會被扣除一大部分。 Gasper 定義了兩個條件（也稱罰沒條件）來定義何謂自相矛盾的投票：
二級標題
正文
環繞投票（Surround-voting）：驗證者發布的一個投票所關聯的兩個檢查點恰好在自己所發布的另一個投票的兩個檢查點高度範圍內。
二級標題
正文
發起雙重投票的驗證者被認為違反了第一罰沒條件；而發起環繞投票的驗證者則違反了第二罰沒條件。不論是哪種情況，違反規則的驗證者都會被扣除大量保證金。
二級標題
正確性（Correctness Properties）
與其它拜占庭容錯型（Byzantine Fault Tolerance，BFT）協議相同，Gasper 協議的一個關鍵底層假設是絕大多數驗證者（超過2/3，以保證金數量定義）是誠實的、會遵循協議的要求。在此假設下，Gasper 有兩大基本屬性：
可追責的安全性（Accountable Safety）：不會有兩個屬於不同分叉的區塊都被終局化，除非有至少1/3 的驗證者（以保證金數量計）被罰沒；
似然活性（Plausible Liveness）：無論區塊鏈過往發生了什麼事，區塊的終局化進程永遠不會陷入僵局。
可罰沒下限（Slashable bound）：只要能夠使用協議外條件來控制驗證者的激活和退出參數條件，就能證明（在打破安全性時）可被罰沒的保證金數量有一個下限。
動態驗證者集合（也即信標鏈協議所實現的）引入了另一個有挑戰性的問題：系統不再那麼能夠可靠地懲罰惡意驗證者，因為他們可能會在作惡之後、保證金被實際罰沒之前離開網絡。而可罰沒下限屬性使得調整活躍驗證者集合的可變幅度、維持最低水平的可追責性成為可能。
Gasper 旨在為終局性提供一個數學化的、精確的、可用來形式化地證明其正確性的描述；這種正確性也是證明信標鏈協議安全性的關鍵。以太坊平台正日漸被用作大型金融交易系統的股價，更突出了安全性保證的前所未有的重要性。
二級標題
與以太坊基金會通力合作，我們已經使用Coq 證明助手，形式化了Gasper 在動態驗證者集合一般條件下的終局性機制。我們在這一條件下指出並證明了Gasper 的所有三種關鍵屬性：可追責的安全性、似然活性以及可罰沒下限；所有證明都使用了同一個Coq 模型。
這裡我們僅對這一成就給出概要的說明。完整的細節可見：
二級標題
該項目的Github 代碼庫
建模及驗證方法
這一模型有三個主要的結構化模塊：
正文
區塊樹。我們用區塊哈希的有限型來模擬一個區塊Hash:finType，另外，用genesis 代表創世區塊。我們使用符號h1 <~ h2 這樣的符號來表示區塊父子關係（ h1 就是h2 的父輩），以此模擬檢查點區塊樹。
正文
二級標題
接下來我們使用h1 <~* h2 來定義祖先關係，h1 就是h2 的祖先，而h2 就是h1 的後代（h1 和h2 可以是同一個區塊）。至於祖先關係的屬性，比如祖先的祖先也是祖先，與父子關係的屬性類同。
正文
正文
正文
正文
該命題指出兩個相互矛盾的區塊b1 和b2 都被終局化了（因為b1 和b2 都不是對方的祖先區塊）。這兩個區塊可以是在任意合理化高度的時候被任意長的鏈終局化的。
正文
這些定義和結果組中被用來指出和證明可追責的安全性、似然活性以及可罰沒下限三種定理。為清楚起見，我們還用下式重新定義了可追責安全性定理的表述：
一級標題
正文
