Move語言安全性解析:智能合約語言的變革者

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

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

1. Move語言的安全特性

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

Move的主要安全特性包括:

1. 模塊(Module):每個Move模塊由一系列結構類型和過程定義組成。模塊可以導入類型定義並調用在其他模塊中聲明的過程。

2. 結構體(Structs):可以定義爲資源類型,表示可以存儲在持久全局鍵/值存儲中。

3. 過程(Function):定義了合約的業務邏輯。

4. 全局存儲:允許Move程序存儲持久數據,這些數據只能由擁有它的模塊以編程方式讀/寫。

5. 不變量檢查:可以定義靜態檢查的不變量,表示系統中資源的守恆性。

6. 字節碼驗證器:對字節碼進行安全類型和線性化驗證,強制執行資源的創建、銷毀和訪問規則。

通過這些特性,Move在編譯時就能保證較高的安全性。接下來我們分析Move的運行機制,看看MoveVM如何保證運行時的安全性。

2. Move的運行機制

Move程序運行在虛擬機中,在運行時不能訪問系統內存。這使得Move可以在不信任的環境中安全地運行,不會被破壞或濫用。

Move程序是在堆棧上執行的。全局存儲被分爲內存(堆)和全局變量(棧)兩部分。內存是一階存儲,不能存儲指向內存單元的指針。全局變量用於存儲指向內存單元的指針,但索引方式與內存不同。

Move的字節碼指令在棧式解釋器中執行。棧式虛擬機易於實現和控制,對硬件環境要求較低,適合區塊鏈場景。同時相對寄存器式解釋器,棧式解釋器在變量間進行copy和move更容易控制和檢測。

Move程序運行時狀態爲⟨C, M, G, S⟩四元組,由調用棧(C)、內存(M)、全局變量(G)和操作數(S)組成。堆棧還維護一個函數表來解析包含函數體的指令。

調用棧包含過程執行的所有上下文信息和指令編號。執行Call指令時創建新的調用棧對象,存儲調用參數,然後執行新合約指令。遇到分支指令時在過程內部進行靜態跳轉。這種設計避免了動態分派,加強了函數調用的不可變性,從而避免了重入的可能性。

MoveVM將數據存儲和調用堆棧(過程邏輯)的存儲分開,這是與EVM最大的不同。在MoveVM中,用戶狀態(帳戶地址下的資源)是獨立存儲的,程序調用必須符合權限和資源相關的強制規則。這種設計雖然犧牲了一定靈活性,但在安全性和執行效率上獲得了很大提升。

3. Move Prover

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

Move Prover使用演繹驗證算法來驗證程序是否符合預期。它可以根據已知信息推斷出程序的行爲,並確保其與預期行爲相匹配。這有助於確保程序的正確性,並減少了人工手動測試的工作量。

Move Prover的工作流程如下:

1. 接收Move源文件作爲輸入,該文件中需要設置程序輸入規範。
2. Move Parser從源碼中提取規範。
3. Move編譯器將源文件編譯爲字節碼,與規範系統共同轉化爲驗證者對象模型。
4. 該模型被翻譯成Boogie中間語言。
5. Boogie驗證系統對輸入進行"驗證條件生成"。
6. 驗證條件傳入Z3求解器進行檢查。
7. 如果規範成立,驗證通過;否則生成診斷報告。

爲描述規範系統,Move使用Move Specification Language,它是Move語言的子集,引入了對靜態描述程序正確性行爲的支持。Move Specification Language可以獨立爲專門的規約化文件,從而讓業務代碼和形式化驗證代碼分開。

Move Prover是一種非常有用的工具,可以幫助開發人員確保智能合約的正確性。它使用形式化語言描述程序行爲,並使用推理算法驗證程序是否符合預期。這有助於減少交易風險,讓開發人員更自信地將智能合約部署到生產環境中。

4. 總結

Move語言在安全性設計上非常出色,在語言特性、虛擬機執行和安全工具層面都給出了全面的考慮。語言特性上犧牲了部分靈活性,強制類型檢查和線性邏輯,方便在編譯檢查、形式化驗證時更加自動化和具備安全可驗證性。MoveVM設計將狀態與邏輯分開,更貼合區塊鏈上資產安全管理的需求。

在語言層面,Move可以有效避免EVM中常見的重入、溢出、Call/DelegateCall注入等漏洞。但鑑權、代碼邏輯、大整數結構溢出等問題仍需開發者額外注意。Move Prover雖然強大,但在整體大意疏忽時可能無法發揮作用。

盡管Move語言在安全層面爲程序員考慮了很多,但沒有完全安全的語言和程序。建議Move智能合約開發者使用第三方安全公司審計服務,並將specification部分代碼的編寫和驗證交由第三方安全公司完成,以進一步提高合約安全性。