/ 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基礎架構，最終為開發者和用戶構建一個更加堅實可信的平台。
