📢 #Gate广场征文活动第二期# 正式啓動!
分享你對 $ERA 項目的獨特觀點,推廣ERA上線活動, 700 $ERA 等你來贏!
💰 獎勵:
一等獎(1名): 100枚 $ERA
二等獎(5名): 每人 60 枚 $ERA
三等獎(10名): 每人 30 枚 $ERA
👉 參與方式:
1.在 Gate廣場發布你對 ERA 項目的獨到見解貼文
2.在貼文中添加標籤: #Gate广场征文活动第二期# ,貼文字數不低於300字
3.將你的文章或觀點同步到X,加上標籤:Gate Square 和 ERA
4.徵文內容涵蓋但不限於以下創作方向:
ERA 項目亮點:作爲區塊鏈基礎設施公司,ERA 擁有哪些核心優勢?
ERA 代幣經濟模型:如何保障代幣的長期價值及生態可持續發展?
參與並推廣 Gate x Caldera (ERA) 生態周活動。點擊查看活動詳情:https://www.gate.com/announcements/article/46169。
歡迎圍繞上述主題,或從其他獨特視角提出您的見解與建議。
⚠️ 活動要求:
原創內容,至少 300 字, 重復或抄襲內容將被淘汰。
不得使用 #Gate广场征文活动第二期# 和 #ERA# 以外的任何標籤。
每篇文章必須獲得 至少3個互動,否則無法獲得獎勵
鼓勵圖文並茂、深度分析,觀點獨到。
⏰ 活動時間:2025年7月20日 17
詳解對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模塊。
來源:
Bank模塊
Cosmos SDK中的bank模塊主管所有與代幣管理相關的功能,比如原生代幣的轉移。發送代幣需要滿足諸多限制和條件,比如賬戶要有充足的可用代幣,而不包括那些已質押、鎖定或正在解綁的代幣。在staking和auth等模塊的支持下,bank模塊管理代幣發送的全過程。儘管bank模塊需要依賴於其他幾個模塊,但由於它們不在本次形式化驗證的範圍內,所以我們對其功能作了一些假設,以簡化流程。
SDK的bank模塊由若干子模塊構成,其中包括keeper和types,它們是定義模塊行為和數據類型的核心組件。我們將重點關注keeper子模塊,因為它涵蓋了模塊的主要功能和特性。
keeper子模塊有兩個關鍵組成部分:view和send。 view keeper負責管理賬戶和余額,而send keeper則負責更改賬戶餘額,如轉賬和質押已鎖定或未鎖定的代幣。 bank模塊的流程如下圖所示,箭頭表示從組件到功能或Keeper的方向。
來源:
驗證方法
如前文所述,本次驗證的範圍僅限於bank模塊。驗證開始前,我們首先對bank模塊內的數據類型製定其形式化規範。例如,bank模塊中有一個代幣數據結構,其包含string類型的面額和big.Int類型的金額,在源代碼中定義如下:
這個結構很簡單,我們採用Coq(我們的建模和形式化驗證語言)作如下定義:
基於這個定義,我們首先證明關於coin基本操作的一些性質,以為bank模塊的功能完整性打下基礎,因為其需要經常修改和操作coin類型。例如:
該引理證明了一個基本的不變性:兩個coin相減不會改變其面額,也不會導致餘額為負。
與前述例子類似,對每次狀態轉換的底層組件都在Coq中進行了建模,這些組件包括KV Store、GasMeter、Error Handling和Context。
數據類型的詳細規範及其驗證請見:
對keeper建模
在完成基礎組件的建模後,我們可以對bank模塊的核心keeper進行建模,以描述模塊的功能。 bank keeper有兩個接口,一個用於代幣數據的只讀訪問,另一個用於代幣的轉移和供應維護。
View keeper負責處理賬戶餘額的只讀訪問,內含四個用於計算賬戶餘額的函數:
GetBalance:通過地址查詢特定面額的賬戶餘額。它考慮兩種情況:空字節序列和非空字節序列。形式化驗證確保GetBalance函數在這兩種情況下都能產生正確的結果。
LockedCoins:返回某地址所對應賬戶的所有不可消費代幣。由於時間限制,我們對一些來自auth模塊的實現做了假設。
GetAllBalances:返回指定地址下的所有賬戶餘額。
GetAccountsBalances:從存儲中返回所有賬戶餘額,並以字段BAddress和BCoins作為記錄。
Send管理器負責處理代幣轉賬和供應。在轉賬過程中,它會保持代幣的供應量,因此不會有新的代幣被鑄造。
SetBalance:通過地址為賬戶設置代幣餘額。此函數考慮兩種情況:設置為零的餘額和設置為非零的餘額。在這兩種情況下,SetBalance的正確性都得到了證明。
subUnlockedCoin:從某地址中扣除指定金額(代幣)。遞歸函數subUnlockedCoins對一組代幣執行同樣的操作。這些函數的相關屬性被視作公理假設。
addCoin:為某地址增加指定金額(代幣)。遞歸函數addCoins對一組代幣執行相同的操作。這些函數的相關屬性被視作公理假設。
SendCoins:從一個賬戶地址向另一個賬戶地址發送金額,使兩個地址的金都得到更新。如果接收方不存在,將為其新建賬戶。
利用以上核心組件的模型,我們可以開始進行驗證了。
驗證過程
我們的驗證是通過形式化描述這些函數的不變性質、並在輔助證明系統中進行證明來完成的,主要關注點是“View Keeper”和“Send Keeper”的核心功能。
例如,規範和引理setBalance_ok證明了BaseSendKeeper模塊的setBalance函數的正確性,具體證明了以下性質:
當send.setBalance返回“Ok”狀態時,存在一個newMultiStore,此時更新後的環境uctx是通過更新newMultiStore,從原來的舊環境ctx衍生而來。
被設置的餘額是有效代幣(它具有系統中代幣所需的屬性)。
setBalance_prop的關係保持,確保函數以符合預期的方式在newMultiStore中進行餘額更新,並生成更新後的環境uctx。
4.餘額設置完成後,使用賬戶地址addr和麵額balance.(Denom)在更新後的環境uctx上調用view.GetBalance,將會返回send.setBalance所設置的相同餘額。
這些性質在Coq規範語言中的描述如下:
關於其他性質的Coq代碼,訪問:
未來的工作
本次驗證的基礎建立在若干假設和公理之上,我們可以對其進行更深入的核實,以擴大驗證的範圍。未來工作的重點包括以下領域:
1.假設的驗證:目前的驗證於依賴於一系列的假設作為證明的基礎。未來可以對這些假設進行驗證,以確保它們準確地反映系統的預期行為和性質。
2.Auth模塊的驗證:該模塊負責管理賬戶數據以及簽名機制,是Cosmos SDK的核心組件。在未來可以對其進行全面的形式化驗證,保證模塊實現及與其他模塊的交互準確無誤。
3.關於委託、鑄幣和銷幣的更多定理:拓展驗證範圍,引入更多關於委託、鑄幣和銷幣的定理,將有助於更全面地了解系統的運行機制。這些定理可以與auth模塊的驗證相結合,以確保系統的整體一致性和正確性。
4.拓展整個Cosmos SDK基礎架構:現階段的驗證工作主要集中在bank模塊及其相關組件。在未來可以將形式化驗證的過程擴展到整個Cosmos SDK基礎架構,從而增強平台的整體準確性、安全性和穩定性,為開發者和用戶提供一個更穩固、更可靠的環境。
5.與其他模塊進行整合:由於Cosmos SDK包括各種相互連接的模塊,探究它們之間的交互和依賴關係是十分有益的。這需要驗證模塊之間交互的正確性,並確保某個模塊的任何更改都不會對其他模塊產生不利影響。
6.激勵機制的建模與驗證:Cosmos SDK也整合瞭如staking和獎勵分發等激勵機制。未來的研究會對這些機制進行建模和驗證,以確保其正確性,並與預期的經濟激勵保持一致。
本文展示了對Cosmos SDKbank模塊進行先進形式化驗證的首個成功案例,為區塊鏈生態系統的安全性和可靠性基礎做了有效的工作。未來的工作將在這一成果的基礎上進行擴展,通過驗證假設、驗證其他模塊,並涵蓋整個Cosmos SDK基礎架構,最終為開發者和用戶構建一個更加堅實可信的平台。