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

發表於 2023-09-09 13:40 作者： 區塊鏈情報速遞pro

在本文中，我們將介紹形式化驗證Cosmos SDK Bank模塊的具體步驟，以及一些驗證結果。

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

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

Cosmos SDK是什么？

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

來源: 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的方向。

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

驗證方法

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

這個結構很簡單，我們採用Coq（我們的建模和形式化驗證語言）作如下定義：

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

該引理證明了一個基本的不變性：兩個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`作爲記錄。

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規範語言中的描述如下：

關於其他性質的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基礎架構，最終爲开發者和用戶構建一個更加堅實可信的平台。

標題：詳解對Cosmos SDK標准模塊的形式化驗證

地址：https://www.coinsdeep.com/article/42421.html

鄭重聲明：本文版權歸原作者所有，轉載文章僅為傳播信息之目的，不構成任何投資建議，如有侵權行為，請第一時間聯絡我們修改或刪除，多謝。