全球首個 Move 智能合約安全審計報告發布

MoveBit
2022-10-13 11:48:26
收藏
Move 語言的願景是幫助開發人員安全、輕鬆、快速地構建區塊鏈應用程序的框架,Move 是為區塊鏈而生的智能合約編程語言。

作者:MoveBit

10月11日,專注 Move 生態的安全公司 MoveBit (莫比安全)團隊發布了全球首個 Move 智能合約安全審計報告------《Starcoin Framework Audit Report》。

這份審計報告是全球 Move 生態上的首個智能合約安全審計報告,並最早總結了基於 Move 構建 DApp 應用的安全經驗,標誌著 Move 生態安全體系建設的開始。

Move 語言介紹

Move 語言最早是為 Meta 的 Diem 區塊鏈項目而開發的,現在Move 語言由開源社區維護。Move 語言的願景是幫助開發人員安全、輕鬆、快速地構建區塊鏈應用程序的框架,Move 是為區塊鏈而生的智能合約編程語言。

根據 MystenLabs 的 Move 語言的文檔介紹,目前有 4 條公鏈已經使用 Move 語言,分別是 Aptos、Sui、Starcoin、0L Network。目前 Starcoin 和 0L Network 已經上線主網,而 Aptos、Sui 還處在測試網階段。

Starcoin 是一個2021年6月主網上線的以 PoW 為核心共識機制的 Move 區塊鏈,使用增強的工作證明共識和 Move 語言。它通過分層和靈活的互操作性來優化 DeFi、NFT、遊戲等不同生態系統的構建。

Starcoin Framework是 Starcoin 鏈上的通用 Move庫, 包括了賬戶、NFT、Token 等通用標準,是生態建設的重要基礎設施。Starcoin Framework 的安全性是 Starcoin 上開發各種 Move項目應用安全的基礎。

Move智能合約的重要概念

Move Prover: Move 中內置用於智能合約的形式化驗證工具叫做 Move Prover,通過這個工具,你能夠斷言所寫智能合約的特性和規範,為智能合約運行提供額外安全保障。它的基本思想是通過形式驗證領域的自動定理證明求解器來驗證程序是否符合某種規範(specification)。

Move Specification: Move 自己定義了一套規範語言,它通過前提條件、後置條件、不變式等來描述程序怎麼樣才算正確運行。Move Specification 可以直接在程序中插入,或者單獨寫成一個 Move Specification文件。Move Specification 常被縮寫成Move Spec。

Move Framework:Move 語言的關鍵設計是能夠將特定於區塊鏈的框架邏輯與 Move 語言的通用功能分離。Move Framework 是鏈的創世狀態中的內置的一組 Move 模塊。 這些模塊通常實現諸如賬戶、Token等關鍵組件,一般是用於實現特定區塊鏈的通用框架邏輯,是DApp 開發的基礎。

構建Move DApp應用的安全經驗

在過去的幾周中,專注於Move安全生態的安全公司 MoveBit 與 Starcoin 團隊進行了深入交流合作,對Starcoin Framework 的每個細節進行了審計。

MoveBit 深入研究了 Starcoin Framework 的代碼結構,作為最早上線的 Move Framework,其中 Account、Token、STC、Config、DAO、NFT、Oracle、Genesis 和 Block等代碼功能全面,覆蓋了大部分開發者的通用場景需求。基於此,MoveBit 最早總結了基於 Move 構建 DApp應用的安全經驗,對以下14類風險進行了分析。

  • Transaction-ordering dependence
  • Timestamp dependence
  • Integer overflow/underflow
  • Number of rounding errors
  • Denial of service / logical oversights
  • Access control
  • Centralization of power
  • logic contradicting the specification
  • Code clones, functionality duplication
  • Gas usage
  • Arbitrary token minting
  • Unchecked CALL Return Values
  • The flow of capability
  • Witness Type

MoveBit 的發現

Starcoin Framework 作為 Starcoin 的 Move 標準庫,包含 69 個 Move 源文件和 70 多個模塊。在此審計工作之前,我們提前閱讀了 Starcoin SIP 和其他開發資源。我們首先回顧了框架架構,然後主要進行了人工代碼審查、測試和使用 Move Prover 的形式化驗證。

我們一直與 Starcoin 團隊保持密切聯繫,在v11版本中一共發現了21個 Issue (其中Major 1個,Medium 4個,Minor 16個),已匯總成審計報告並對外公開。在與 Starcoin 團隊的會議期間,我們對所有問題進行了廣泛討論。一些問題已經在後續迭代中得到修復,其他問題講很快得到解決。除了原生函數和一些包含無法推理的特殊元素的函數(例如,運行時類型信息、位運算符)外,我們為大多數函數和文件添加了形式化驗證代碼 Move Specification。所有的形式化驗證代碼都會作為 PR 提交到代碼倉庫,最終由 Starcoin 團隊在以後的升級和修訂中合併。

審計報告鏈接:[++https://www.movebit.xyz/file/Starcoin-Framework-Audit-Report.pdf++]

這份審計報告是 全球Move 生態的第一個智能合約安全審計報告,標誌著 Move 生態安全體系建設的開始。MoveBit 將與 Move 社區同行,專注為 Move 生態的安全保駕護航。

關於Starcoin

Starcoin, 主網已在2021年5月上線,是 Move 生態第一個無許可公鏈,基於最成熟的去中心化共識增強版 PoW 以及智能合約語言 Move 提供來自原力的安全,通過分層的靈活互操作性,為參與 Web.3.0 生態搭建的人們提供價值賦能的數字資產服務的分佈式金融網絡。

關於MoveBit

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

鏈捕手ChainCatcher提醒,請廣大讀者理性看待區塊鏈,切實提高風險意識,警惕各類虛擬代幣發行與炒作,站內所有內容僅係市場信息或相關方觀點,不構成任何形式投資建議。如發現站內內容含敏感信息,可點擊“舉報”,我們會及時處理。
ChainCatcher 與創新者共建Web3世界