詳解對Cosmos SDK標準模塊的形式化驗證

/ Web3完整軟件棧先進形式化驗證/

CertiK最近發布了一份關於Cosmos SDK Bank模塊的先進形式化驗證報告,據我們所知,這是針對Cosmos SDK形式化驗證的首次成功嘗試。形式化驗證是一項運用數學邏輯來確保系統符合規範,使其在所有可能的輸入和條件下都如預期表現的技術。在本文中,我們將介紹形式化驗證Cosmos SDK Bank模塊的具體步驟,以及一些驗證結果。

Cosmos SDK是什麼?

Cosmos軟件開發工具包(簡稱SDK)是一個能讓開發人員構建自定義區塊鏈應用的框架。利用Cosmos SDK,開發者可以輕鬆啟動自己的Layer 1區塊鏈,不用操心從共識層到應用層的設計和實現。 Cosmos SDK提供了任何鏈都可直接導入和使用的標準核心模塊,如staking、auth、gov 和 mint模塊。

詳解對Cosmos SDK標準模塊的形式化驗證

來源: https://golden.com/wiki/Tendermint-4AP8KX8

Bank模塊

Cosmos SDK中的bank模塊主管所有與代幣管理相關的功能,比如原生代幣的轉移。發送代幣需要滿足諸多限制和條件,比如賬戶要有充足的可用代幣,而不包括那些已質押、鎖定或正在解綁的代幣。在staking和auth等模塊的支持下,bank模塊管理代幣發送的全過程。儘管bank模塊需要依賴於其他幾個模塊,但由於它們不在本次形式化驗證的範圍內,所以我們對其功能作了一些假設,以簡化流程。

SDK的bank模塊由若干子模塊構成,其中包括keeper和types,它們是定義模塊行為和數據類型的核心組件。我們將重點關注keeper子模塊,因為它涵蓋了模塊的主要功能和特性。

keeper子模塊有兩個關鍵組成部分:view和send。 view keeper負責管理賬戶和余額,而send keeper則負責更改賬戶餘額,如轉賬和質押已鎖定或未鎖定的代幣。 bank模塊的流程如下圖所示,箭頭表示從組件到功能或Keeper的方向。

詳解對Cosmos SDK標準模塊的形式化驗證

來源:https://docs.cosmos.network/v0.46/building-modules/msg-services.html

驗證方法

如前文所述,本次驗證的範圍僅限於bank模塊。驗證開始前,我們首先對bank模塊內的數據類型製定其形式化規範。例如,bank模塊中有一個代幣數據結構,其包含string類型的面額和big.Int類型的金額,在源代碼中定義如下:

詳解對Cosmos SDK標準模塊的形式化驗證

這個結構很簡單,我們採用Coq(我們的建模和形式化驗證語言)作如下定義:

詳解對Cosmos SDK標準模塊的形式化驗證

基於這個定義,我們首先證明關於coin基本操作的一些性質,以為bank模塊的功能完整性打下基礎,因為其需要經常修改和操作coin類型。例如:

詳解對Cosmos SDK標準模塊的形式化驗證

該引理證明了一個基本的不變性:兩個coin相減不會改變其面額,也不會導致餘額為負。

與前述例子類似,對每次狀態轉換的底層組件都在Coq中進行了建模,這些組件包括KV Store、GasMeter、Error Handling和Context。

數據類型的詳細規範及其驗證請見:https://github.com/CertiKProject/cosmos-sdk-fv/tree/master/coq_proofs/perennial/src/cosmos_sdk_proofs

對keeper建模

在完成基礎組件的建模後,我們可以對bank模塊的核心keeper進行建模,以描述模塊的功能。 bank keeper有兩個接口,一個用於代幣數據的只讀訪問,另一個用於代幣的轉移和供應維護。

View keeper負責處理賬戶餘額的只讀訪問,內含四個用於計算賬戶餘額的函數:

1. `GetBalance`:通過地址查詢特定面額的賬戶餘額。它考慮兩種情況:空字節序列和非空字節序列。形式化驗證確保`GetBalance`函數在這兩種情況下都能產生正確的結果。

2. `LockedCoins`:返回某地址所對應賬戶的所有不可消費代幣。由於時間限制,我們對一些來自auth模塊的實現做了假設。

3. `GetAllBalances`:返回指定地址下的所有賬戶餘額。

4. `GetAccountsBalances`:從存儲中返回所有賬戶餘額,並以字段`BAddress`和`BCoins`作為記錄。

詳解對Cosmos SDK標準模塊的形式化驗證

Send管理器負責處理代幣轉賬和供應。在轉賬過程中,它會保持代幣的供應量,因此不會有新的代幣被鑄造。

1. `SetBalance`:通過地址為賬戶設置代幣餘額。此函數考慮兩種情況:設置為零的餘額和設置為非零的餘額。在這兩種情況下,SetBalance的正確性都得到了證明。

2. `subUnlockedCoin`:從某地址中扣除指定金額(代幣)。遞歸函數`subUnlockedCoins`對一組代幣執行同樣的操作。這些函數的相關屬性被視作公理假設。

3. `addCoin`:為某地址增加指定金額(代幣)。遞歸函數`addCoins`對一組代幣執行相同的操作。這些函數的相關屬性被視作公理假設。

4. `SendCoins`:從一個賬戶地址向另一個賬戶地址發送金額,使兩個地址的金都得到更新。如果接收方不存在,將為其新建賬戶。

利用以上核心組件的模型,我們可以開始進行驗證了。

驗證過程

我們的驗證是通過形式化描述這些函數的不變性質、並在輔助證明系統中進行證明來完成的,主要關注點是“View Keeper”和“Send Keeper”的核心功能。

例如,規範和引理`setBalance_ok`證明了`BaseSendKeeper`模塊的`setBalance`函數的正確性,具體證明了以下性質:

1. 當`send.setBalance`返回“Ok”狀態時,存在一個`newMultiStore`,此時更新後的環境`uctx`是通過更新`newMultiStore`,從原來的舊環境`ctx`衍生而來。

2. 被設置的餘額是有效代幣(它具有系統中代幣所需的屬性)。

3. `setBalance_prop`的關係保持,確保函數以符合預期的方式在`newMultiStore`中進行餘額更新,並生成更新後的環境`uctx`。

4.餘額設置完成後,使用賬戶地址`addr`和麵額`balance.(Denom)`在更新後的環境`uctx`上調用`view.GetBalance`,將會返回`send.setBalance`所設置的相同餘額。

這些性質在Coq規範語言中的描述如下:

詳解對Cosmos SDK標準模塊的形式化驗證

關於其他性質的Coq代碼,訪問:https://skynet.certik.com/projects/cosmos。

未來的工作

本次驗證的基礎建立在若干假設和公理之上,我們可以對其進行更深入的核實,以擴大驗證的範圍。未來工作的重點包括以下領域:

1.假設的驗證:目前的驗證於依賴於一系列的假設作為證明的基礎。未來可以對這些假設進行驗證,以確保它們準確地反映系統的預期行為和性質。

2.Auth模塊的驗證:該模塊負責管理賬戶數據以及簽名機制,是Cosmos SDK的核心組件。在未來可以對其進行全面的形式化驗證,保證模塊實現及與其他模塊的交互準確無誤。

3.關於委託、鑄幣和銷幣的更多定理:拓展驗證範圍,引入更多關於委託、鑄幣和銷幣的定理,將有助於更全面地了解系統的運行機制。這些定理可以與auth模塊的驗證相結合,以確保系統的整體一致性和正確性。

4.拓展整個Cosmos SDK基礎架構:現階段的驗證工作主要集中在bank模塊及其相關組件。在未來可以將形式化驗證的過程擴展到整個Cosmos SDK基礎架構,從而增強平台的整體準確性、安全性和穩定性,為開發者和用戶提供一個更穩固、更可靠的環境。

5.與其他模塊進行整合:由於Cosmos SDK包括各種相互連接的模塊,探究它們之間的交互和依賴關係是十分有益的。這需要驗證模塊之間交互的正確性,並確保某個模塊的任何更改都不會對其他模塊產生不利影響。

6.激勵機制的建模與驗證:Cosmos SDK也整合瞭如staking和獎勵分發等激勵機制。未來的研究會對這些機制進行建模和驗證,以確保其正確性,並與預期的經濟激勵保持一致。

本文展示了對Cosmos SDKbank模塊進行先進形式化驗證的首個成功案例,為區塊鏈生態系統的安全性和可靠性基礎做了有效的工作。未來的工作將在這一成果的基礎上進行擴展,通過驗證假設、驗證其他模塊,並涵蓋整個Cosmos SDK基礎架構,最終為開發者和用戶構建一個更加堅實可信的平台。