MoveBit 對Aptos Framework開展形式化驗證

MoveBit ｜2022-12-26 15:10

MoveBit（莫比安全）作為專注於服務Move生態的安全公司，近期和Aptos 合作開展了Aptos Framework 的形式化驗證工作。

MoveBit（莫比安全）作為專注於服務Move生態的安全公司，近期和Aptos 合作開展了Aptos Framework 的形式化驗證工作。 Aptos 是一個頂級公鏈，其願景是將Web3 帶入主流，並獲得頂級資本的投資，而其底層基礎代碼庫Aptos Framework 是Aptos 公鏈上的通用Move 庫，包括了賬戶、NFT、Token 等通用標準，是生態建設的重要基礎設施。

Aptos Framework 的安全性是Aptos 上開發各種Move 項目應用安全的基礎。在此形式化驗證工作之前，MoveBit 團隊全面了解分析了Aptos Framework 的開發資源和框架架構，並和Aptos Team 合作開啟了基於Move Prover 的形式化驗證。

以下是MoveBit 團隊對Aptos Framework 形式化驗證後的代碼提交示例：

添加了模塊帳戶和幣的規範。詳細鏈接：https://github.com/aptos-labs/aptos-core/pull/5237
添加了模塊和aptos_account 和state_storage 的規範。詳細鏈接：https://github.com/aptos-labs/aptos-core/pull/5478
更新了consensus_config 的規範，添加了transaction_fee 和transaction_validation 的規範。更新了重新配置和權益以及storage_gas 的規範。詳細鏈接：https://github.com/aptos-labs/aptos-core/pull/5549
添加了Aggregator & AggregatorFactory & OptionalAggregator & StakingConfig & Version & Event & Guid & Timestamp 規範。詳細鏈接：https://github.com/aptos-labs/aptos-core/pull/5653
添加了模塊gas_schedule & aptos_coin & chain_id & chain_status 的規範。詳細鏈接：https://github.com/aptos-labs/aptos-core/pull/5771

什麼是Move Prover 形式化驗證?

形式化驗證是一種使用嚴格的數學方法來描述行為和推理計算機系統的正確性的技術。現在已經廣泛應用在芯片驗證、航空航天、操作系統、編譯器等對正確性要求高的領域。

部署在區塊鏈上的智能合約操作著各種數字資產，它們的安全性也十分關鍵。 Move Prover就是為盡可能防止Move 語言編寫的智能合約中的錯誤而設計。用戶可以使用Move 規範語言指定智能合約的功能屬性，然後使用Move Prover 靜態地檢查它們。

簡單地說，Move 文件中可以分兩種：

一部分是程序代碼，這是我們多數人最熟悉的部分。它用Move 程序語言寫成。我們用它定義數據類型、函數。

另一部分是形式規範。它是可選的，用Move 規範語言寫成。我們用它說明程序代碼應該滿足怎樣的性質，比如描述函數的行為和全局的屬性。

MoveBit 主要根據代碼邏輯進行形式規範驗證，寫完規範後調用Move Prover，Move Prover會按照寫好的規範去驗證Aptos Framework 的Move 程序有沒有滿足這些要求，幫助Aptos 的開發人員在開發階段儘早發現潛在的問題，並讓其用戶可以盡快將已經驗證過的程序運用到產品當中。

本文將對此形式化驗證過程中的關鍵步驟進行展示：

withdraw() 是aptos-framework coin模塊下的一個函數,該函數作用是從簽名賬戶中提取指定數量的代幣，並將代幣返回。 MoveBit為aptos提供了形式化驗證代碼。
我們驗證了`withdraw`函數的功能性質及中止條件.
`balance`是`account`賬戶下(某種)代幣的餘額,`amount`為要取出的代幣餘額,我們可以看到,該函數有三種中止(abort)的情況:
1.該賬戶下不存在`CoinType`類型的代幣。
2.該賬戶下餘額不足
3.該賬戶被凍結
我們預期執行完該函數後,`account`賬戶下的餘額應該為`balance - amount`,且返回一個金額為`amount`的代幣。如果沒有達到我們的預期,那麼prover會提示我們條件沒有滿足。
deposit 函數作用是將代幣餘額存入接收者的賬戶。
該函數有兩種中止的情況:
1.接收者的賬戶被凍結
2.接收者的賬戶下不存在CoinStore<CoinType>資源
我們預期執行完該函數後接收者賬戶的餘額等於接受前的餘額加上轉入的金額。且返回一個金額為amount的代幣。

構建Aptos生態安全

Aptos 極其重視生態安全的建設，MoveBit 作為專注於Move 生態安全的安全審計公司，除了對Aptos Framework 展開形式化驗證，與Aptos 協作了MoveVM 的安全審計，並且與Apots 生態上的MoveDID, Token Pocket, Starswap ，OminBTC，Pontem 等項目達成了合作，MoveBit 將會持續為Aptos 生態安全保駕護航

關於MoveBit

MoveBit(莫比安全)團隊是一家服務於Move生態的安全公司，其願景是讓Move生態成為最安全的Web3生態系統。 MoveBit團隊由學術界安全大牛和企業界安全領軍人物組成，具有10年的安全經驗，在NDSS 、 CCS等頂級國際安全學術會議上發表安全研究成果。團隊是Move生態最早期的貢獻者，與Move開發者共同製定安全Move應用的標準。 MoveBit已經陸續與全球多家知名交易所、公鏈項目合作，為合作夥伴提供安全審計服務。