隨著即將到來的2 0版重大更新(代號(hào)為Serenity)，以太坊正在過渡到分片的權(quán)益證明(PoS)共識(shí)機(jī)制。它帶來了更好的能效，安全性和可擴(kuò)展性。以
隨著即將到來的2.0版重大更新(代號(hào)為Serenity)，以太坊正在過渡到分片的權(quán)益證明(PoS)共識(shí)機(jī)制。它帶來了更好的能效，安全性和可擴(kuò)展性。以太坊2.0的特定PoS協(xié)議稱為信標(biāo)鏈。
我們很高興地報(bào)告Runtime Verification與以太坊基金會(huì)之間正在進(jìn)行的合作中的第一個(gè)里程碑，以構(gòu)建一個(gè)用于建模和驗(yàn)證信標(biāo)鏈的正式框架。在K框架下完成了信標(biāo)鏈的可執(zhí)行形式化模型K規(guī)范和描述這項(xiàng)工作的技術(shù)報(bào)告都可以在線獲得。
那么什么是信標(biāo)鏈?K中的模型是如何開發(fā)的?為什么這一發(fā)展很重要?
Nutshell中的信標(biāo)鏈
信標(biāo)鏈?zhǔn)羌磳⒌絹淼囊蕴?.0的PoS協(xié)議層。協(xié)議主要負(fù)責(zé)在參與協(xié)議的網(wǎng)絡(luò)中所有節(jié)點(diǎn)之間就系統(tǒng)狀態(tài)達(dá)成共識(shí)。
參與節(jié)點(diǎn)(在協(xié)議中稱為驗(yàn)證者)主要根據(jù)節(jié)點(diǎn)的當(dāng)前狀態(tài)，通過提議新的信標(biāo)區(qū)塊或?qū)ΜF(xiàn)有的信標(biāo)區(qū)塊進(jìn)行投票來為系統(tǒng)的分布式操作做出貢獻(xiàn)。信標(biāo)區(qū)塊主要封裝了發(fā)布到網(wǎng)絡(luò)的一組投票。該協(xié)議管理如何選擇驗(yàn)證者來提議和投票給區(qū)塊，以確保每個(gè)驗(yàn)證者都有公平的貢獻(xiàn)機(jī)會(huì)。
投票給一個(gè)信標(biāo)區(qū)塊叫做證明。證明是共識(shí)機(jī)制的基本組成部分。通過信標(biāo)區(qū)塊的證明：
· 驗(yàn)證者證明該區(qū)塊是有效的，并且應(yīng)將其附加到鏈中;
· 如果鏈分叉成多個(gè)分支(根據(jù)分叉選擇規(guī)則)，則驗(yàn)證者通過標(biāo)識(shí)區(qū)塊應(yīng)附加到的位置來投票給“規(guī)范的塊鏈”;
· 驗(yàn)證者有助于確定區(qū)塊的確定性，這一過程告訴我們何時(shí)可以將信標(biāo)區(qū)塊視為最終的，因此不應(yīng)還原(根據(jù)Casper FFG);
· 如果該區(qū)塊不屬于主鏈，則驗(yàn)證者將對(duì)該區(qū)塊的分片投票。直觀上，分片是鏈接到信標(biāo)鏈的獨(dú)立鏈，可以通過系統(tǒng)中的驗(yàn)證者子集與狀態(tài)中的其他分片并行處理，從而顯著提高了系統(tǒng)一次處理更多交易的能力，從而提高了它的可擴(kuò)展性(請(qǐng)參閱sharding和crosslinks)。
最后，遵循協(xié)議并做出明智決策的驗(yàn)證者將獲得以太坊獎(jiǎng)勵(lì)，以紅利形式分配，以鼓勵(lì)適當(dāng)?shù)男袨?。另一方面，偏離協(xié)議或行為不正常的驗(yàn)證者可能會(huì)因拒絕或在某些情況下因削減其抵押的以太幣而受到處罰。這種獎(jiǎng)勵(lì)懲罰系統(tǒng)有助于使惡意用戶在經(jīng)濟(jì)上不可行，無法在該系統(tǒng)上發(fā)起成功的攻擊(請(qǐng)參閱《 Serenity設(shè)計(jì)原理》注釋)。
信標(biāo)鏈當(dāng)前由以太坊基金會(huì)開發(fā)的Python“以太坊2.0階段0 –信標(biāo)鏈”的參考實(shí)現(xiàn)定義。
定義協(xié)議操作的實(shí)現(xiàn)的主要組件是信標(biāo)鏈狀態(tài)轉(zhuǎn)換函數(shù)state_transition。該函數(shù)實(shí)現(xiàn)的相關(guān)部分的摘錄如下所示：
處理從創(chuàng)始狀態(tài)(已處理的創(chuàng)始信標(biāo)區(qū)塊的狀態(tài))開始。給定要處理的下一個(gè)信標(biāo)區(qū)塊，并假定該區(qū)塊有效，信標(biāo)鏈狀態(tài)轉(zhuǎn)換功能將給定的信標(biāo)鏈狀態(tài)(前狀態(tài))轉(zhuǎn)換為新狀態(tài)(后狀態(tài))。此后狀態(tài)反映了以下結(jié)果：
· 考慮(可能)丟失的區(qū)塊; (process_slots);
· 處理區(qū)塊的內(nèi)容(process_block)。
在K中建模信標(biāo)鏈
我們?cè)谶@項(xiàng)工作中的目標(biāo)是建立一個(gè)信標(biāo)鏈的形式模型，該模型盡可能與“以太坊2.0階段0規(guī)范”給出的參考實(shí)現(xiàn)相對(duì)應(yīng)，從而實(shí)現(xiàn)以下功能：
· 模擬或設(shè)置信標(biāo)鏈狀態(tài)轉(zhuǎn)換函數(shù)的執(zhí)行。
· 從信標(biāo)鏈測(cè)試套件運(yùn)行現(xiàn)有測(cè)試。
· 分析現(xiàn)有測(cè)試套件的代碼覆蓋率，并通過新測(cè)試進(jìn)行改進(jìn)。
K是實(shí)現(xiàn)此目標(biāo)的非常合適的框架，因?yàn)樗軌蜷_發(fā)信標(biāo)鏈的形式模型，其特征是：
1. 可通過K工具中的模式重寫來執(zhí)行，因此可以直接從規(guī)范中獲取信標(biāo)鏈狀態(tài)轉(zhuǎn)換函數(shù)的解釋器(無需任何額外費(fèi)用)。
2. 具體而言，其規(guī)范直接對(duì)應(yīng)于系統(tǒng)的Python實(shí)現(xiàn)(對(duì)某些特定的抽象進(jìn)行?；绾灻?yàn)證)。
K模型也為更復(fù)雜的驗(yàn)證任務(wù)(例如可達(dá)性分析和演繹驗(yàn)證)奠定了基礎(chǔ)，但這是正在進(jìn)行的工作和將來的工作的一部分，將在其他地方進(jìn)行介紹。
該項(xiàng)目的github存儲(chǔ)庫(kù)中提供了k中模型的完整規(guī)范，以及一份更詳細(xì)地描述這項(xiàng)工作的技術(shù)報(bào)告。https://github.com/runtimeverification/beacon-chain-spec
信標(biāo)鏈?zhǔn)侨绾斡胟建模的?
通常信標(biāo)鏈在K中建模為狀態(tài)轉(zhuǎn)換系統(tǒng)，其狀態(tài)為信標(biāo)鏈狀態(tài)，其轉(zhuǎn)換由主信標(biāo)鏈狀態(tài)轉(zhuǎn)換函數(shù)定義。
在K中，信標(biāo)鏈狀態(tài)被指定為由(可能嵌套的)單元組成的配置，其中每個(gè)單元代表定義協(xié)議所需的配置的語義元素。 例如下面的摘錄顯示了
信標(biāo)鏈狀態(tài)轉(zhuǎn)換功能由K中的運(yùn)算符指定，該函數(shù)將由當(dāng)前信標(biāo)鏈配置建模的信標(biāo)鏈前狀態(tài)轉(zhuǎn)換為由結(jié)果K配置建模的信標(biāo)鏈后狀態(tài)。 運(yùn)算符聲明如下：
如上所述，涉及兩個(gè)主要的連續(xù)步驟：process_slots和process_block。命令在k中的排序自然指定為使用運(yùn)算符~>，將計(jì)算疊加在一個(gè)連續(xù)項(xiàng)上。例如使用以下k規(guī)則定義狀態(tài)轉(zhuǎn)換函數(shù)：
只有當(dāng)process_slots成功終止時(shí)，才會(huì)進(jìn)行由process_block定義的下一次計(jì)算，該計(jì)算將捕獲預(yù)期的語義。
在開發(fā)轉(zhuǎn)換函數(shù)的語義規(guī)范時(shí)，我們面臨的挑戰(zhàn)之一是python語義豐富的表達(dá)式和大多數(shù)命令式編程風(fēng)格與k語言定義的構(gòu)造和聲明式規(guī)范風(fēng)格之間的不匹配。在這一發(fā)展過程中，我們已經(jīng)確定了一些模式以及如何在k中優(yōu)雅地指定它們，例如如上所述的用于排序的堆疊計(jì)算結(jié)構(gòu)。
其他模式更復(fù)雜，不匹配更明顯，例如列表理解表達(dá)式，它們?cè)贐eacon鏈的引用實(shí)現(xiàn)中被大量使用。在這些情況下，這種編碼通常相當(dāng)冗長(zhǎng)，但如果不用k定義中間語言結(jié)構(gòu)，就無法避免。然而，其優(yōu)點(diǎn)是，這種編碼容易實(shí)現(xiàn)更詳細(xì)的覆蓋率分析。
驗(yàn)證模型
以太坊基金會(huì)為信標(biāo)鏈提供了豐富的測(cè)試套件。 除了用作Python實(shí)現(xiàn)的調(diào)試工具之外，第三方生產(chǎn)客戶開發(fā)人員還使用測(cè)試套件來確保與參考實(shí)現(xiàn)一致。 該測(cè)試套件包含3,000多種不同的單元測(cè)試。
在給定的開發(fā)K模型抽象級(jí)別，可以在模型中直接執(zhí)行信標(biāo)鏈的標(biāo)準(zhǔn)測(cè)試套件中的測(cè)試，而無需任何工具。這證明是非常有價(jià)值的，因?yàn)樗峁┝艘环N機(jī)制來驗(yàn)證模型，并確保模型符合參考實(shí)現(xiàn)，就像驗(yàn)證其他生產(chǎn)實(shí)現(xiàn)一樣,按照項(xiàng)目資源庫(kù)中的說明，所有測(cè)試都可以自動(dòng)運(yùn)行。
擴(kuò)展測(cè)試覆蓋范圍
標(biāo)準(zhǔn)信標(biāo)鏈測(cè)試套件的設(shè)計(jì)使代碼覆蓋率最大化，可以使用Python的可用代碼覆蓋率分析工具。 但是Python的覆蓋范圍通常比較粗略。它不會(huì)區(qū)分執(zhí)行語義豐富的Python構(gòu)造(例如列表理解表達(dá)式)的各個(gè)分支。
K提供了不同的基于規(guī)則的覆蓋率分析工具。它檢測(cè)執(zhí)行中是否應(yīng)用了規(guī)則(如果適用，則應(yīng)用了多少次)。 使用這種基于K的工具進(jìn)行語義覆蓋已經(jīng)證明在其他語言(例如JavaScript)的環(huán)境中很有用，我們?cè)谒袨g覽器中都發(fā)現(xiàn)了新的錯(cuò)誤(這些結(jié)果在PLDI’15論文中進(jìn)行了描述)。
因此該計(jì)劃是評(píng)價(jià)標(biāo)準(zhǔn)的Python代碼覆蓋率如何確保語義覆蓋面，看是否基于規(guī)則的覆蓋分析可能暴露不是由標(biāo)準(zhǔn)的Python代碼覆蓋工具檢測(cè)到任何未覆蓋的功能。 確實(shí)分析顯示測(cè)試未涵蓋或未充分涵蓋的執(zhí)行路徑，而Python覆蓋率未檢測(cè)到這些執(zhí)行路徑 這些檢測(cè)中的大多數(shù)都屬于復(fù)雜行為的規(guī)范，例如列表理解表達(dá)式和復(fù)雜循環(huán)中通常遇到的行為。
以下是K覆蓋率工具生成的覆蓋率分析報(bào)告的快照，顯示了未在測(cè)試套件的任何測(cè)試中應(yīng)用的規(guī)則。
繼續(xù)向前
信標(biāo)鏈的可執(zhí)行k模型是實(shí)現(xiàn)正式驗(yàn)證信標(biāo)鏈的基本安全性和活性特性及其參考實(shí)現(xiàn)這一最終目標(biāo)的第一步，但也是至關(guān)重要的一步。事實(shí)上，如果沒有一個(gè)可信的、形式化的系統(tǒng)模型來驗(yàn)證，形式化驗(yàn)證的問題是沒有意義的。除了能夠執(zhí)行狀態(tài)轉(zhuǎn)換函數(shù)、運(yùn)行測(cè)試和分析測(cè)試覆蓋率之外，本文提出的k形式化模型還可以用來描述和驗(yàn)證在這種低抽象級(jí)別上可表示的低級(jí)別不變量。
但是信標(biāo)鏈?zhǔn)且粋€(gè)非常復(fù)雜的協(xié)議。在這種較低的抽象級(jí)別上直接驗(yàn)證高級(jí)屬性(如安全性和活動(dòng)性)通常是不可行的。相反，通常使用抽象細(xì)化技術(shù)。因此我們的計(jì)劃如下：
· 建立此具體模型的抽象，該模型保留協(xié)議的核心共識(shí)機(jī)制;
· 在抽象模型上證明所需的屬性;
· 表明這些屬性保留在具體模型中;（鏈三豐）
關(guān)鍵詞： K模型 共識(shí)機(jī)制 信標(biāo)鏈
