Move語言的安全性解析

前言

Move是一種可編譯運行在實現MoveVM的區塊鏈環境中的智能合約語言。它在設計之初就考慮了區塊鏈和智能合約的諸多安全性問題,並借鑑了RUST語言的一些安全設計理念。作爲新一代以安全爲主要特點的智能合約語言,Move的安全性究竟如何?它是否能在語言層面或相關機制上規避EVM、WASM等合約虛擬機常見的安全威脅?Move本身是否存在特有的安全性問題?

本文將從語言特性、運行機制和驗證工具三個層面來探討Move語言的安全性問題。

1. Move語言的安全特性

編寫無漏洞的代碼是困難的,即使經過多次測試也無法完全保證。與不可信代碼交互時,編寫能保持關鍵安全屬性的代碼則更具挑戰性。有多種技術可以在運行時強制執行安全性,如沙箱、進程隔離、對象鎖等編程模式;也可以在編譯時指定靜態安全性,如強制靜態類型或斷言檢查。

有時也可借助語義分析和靜態分析工具,確保代碼符合安全規則,即使與不可信代碼交互時也能保持某些可證明的邏輯規約。這些方法看似不錯,可以避免運行時開銷並提前發現安全問題。然而,編程語言通過這些方法獲得的安全性極其有限,主要有兩個原因:首先,它們通常具有難以用靜態分析工具分析的語言特性,如動態分派、共享可變性和反射等非線性邏輯,這些特性違反了安全不變量規則,爲攻擊者提供了廣泛的攻擊面。其次,大多數編程語言難以擴展成支持安全相關的靜態工具或表達性強的規約化語言,盡管這兩種擴展都很重要。

Move語言的設計既支持與不可信代碼安全交互,又支持靜態驗證。它具備這些安全特性,是因爲舍棄了所有基於靈活性考慮的非線性邏輯,不支持動態分派,也不支持遞歸外部調用,而是使用泛型、全局存儲、資源等概念來實現一些替代性的編程模式。例如,Move省略了動態調度和遞歸調用特性,這些特性在其他智能合約語言中導致了代價高昂的重入漏洞。

Move語言的主要安全特性包括:

• 模塊化:每個Move模塊由一系列結構類型和過程定義組成。模塊可以導入其他模塊中聲明的類型定義和調用過程。

• 結構體:可以定義資源類型的結構體,用於表示可存儲在全局鍵/值存儲中的數據。

• 過程:定義了初始化、安全和不安全過程。過程可以有訪問控制限制。

• 全局存儲:允許存儲持久數據,只能由擁有它的模塊以編程方式讀寫。

• 不變量檢查:可以定義靜態檢查的不變量,確保系統中資源的完整性。

• 字節碼驗證器:在字節碼級別強制執行類型系統,防止資源被不當創建、解包或引用。

這些特性使Move能夠在編譯時和運行時都提供強大的安全保障。

2. Move的運行機制

Move程序運行在虛擬機中,無法直接訪問系統內存,這確保了它可以在不信任的環境中安全運行。

Move採用棧式執行模型。全局存儲分爲內存(堆)和全局變量(棧)兩部分。內存是一階存儲,不能存儲指向內存單元的指針。全局變量用於存儲指向內存單元的指針,通過地址和類型進行訪問。

Move使用棧式解釋器執行字節碼指令,這種方式易於實現和控制,對硬件要求低,適合區塊鏈場景。相比寄存器式解釋器,棧式解釋器更容易控制和檢測變量間的復制和移動。

Move程序運行時的狀態是一個四元組⟨C, M, G, S⟩,包括調用棧(C)、內存(M)、全局變量(G)和操作數棧(S)。調用棧包含過程執行的上下文信息和指令編號。執行Call指令時會創建新的調用棧對象,存儲參數並執行新合約的指令。遇到分支指令時在過程內部進行靜態跳轉。

MoveVM將數據存儲和調用堆棧分開,這是它與EVM的主要區別。在Move中,用戶狀態(帳戶地址下的資源)是獨立存儲的,程序調用必須符合權限和資源規則。這種設計犧牲了一定靈活性,但提高了安全性和執行效率。

3. Move Prover

Move Prover是一個基於推理的形式化驗證工具,可以幫助開發人員確保智能合約的正確性,減少交易風險。它使用形式化語言描述程序行爲,並通過推理算法驗證程序是否符合預期。

Move Prover使用演繹驗證算法,根據已知信息推斷程序行爲,確保其與預期匹配。這有助於確保程序正確性,減少人工測試工作量。

Move Prover的工作流程如下:

1. 接收Move源文件作爲輸入,其中包含程序規範
2. 解析器提取規範,編譯器將源碼編譯爲字節碼
3. 生成驗證者對象模型
4. 將模型翻譯爲Boogie中間語言
5. Boogie驗證系統生成驗證條件
6. 將驗證條件傳入Z3求解器檢查
7. 生成診斷報告並轉換爲源碼級錯誤

Move提供了Move Specification Language來描述規範,它是Move語言的一個子集,支持靜態描述程序正確性行爲。規範可以獨立於業務代碼編寫。

Move Prover是一個強大的工具,可以幫助開發人員確保智能合約的正確性,減少交易風險。它使用形式化方法驗證程序是否符合預期,提高了開發人員部署智能合約的信心。

總結

Move語言在安全性方面進行了全面的考慮,從語言特性、虛擬機執行到安全工具都提供了強大的保障。它犧牲了一定的靈活性,強制類型檢查和線性邏輯,有利於編譯檢查和形式化驗證的自動化。MoveVM的設計將狀態與邏輯分開,更符合區塊鏈資產安全管理的需求。

Move語言可以有效避免EVM中常見的重入、溢出、Call/DelegateCall注入等漏洞。但鑑權、代碼邏輯、大整數結構溢出等問題仍需開發者額外注意。Move Prover雖然強大,但不能完全避免整體設計上的疏忽。

盡管Move在安全性上做了很多考慮,但沒有完全安全的語言和程序。建議Move智能合約開發者仍然使用第三方安全公司的審計服務,並將規範部分的編寫和驗證交由專業安全團隊完成。