Move語言安全性深度剖析：語言特性、運行機制和自動化審計

前言

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

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

1. Move語言的安全特性

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

有時也可借助語義分析與靜態分析工具,確保代碼符合安全規則,即使與不受信任的代碼交互時也能保持某些可證明的邏輯規約不變。

這些方案看似不錯,可以避免運行時開銷並提前發現安全問題。但遺憾的是,編程語言通過這些方法獲得的安全性極其有限,主要有兩個原因:首先,它們通常具有無法使用靜態分析工具的特性,如動態分派、共享可變性和反射等非線性邏輯,違反了安全不變量規則,給黑客提供了廣泛的攻擊面。其次,大多數編程語言難以使用與安全相關的靜態工具或表達性強的規約化語言進行擴展。盡管這兩種擴展都很重要,可以預先定義。

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

爲了更好地理解Move語言的特性,我們來看一個示例程序:

move module 0x1::TestCoin { use 0x1::signer;

const ADMIN: address = @0x1;

struct Coin has key, store {
    value: u64
}

struct Info has key {
    total_supply: u64
}

spec module {
    invariant forall addr: address where exists<coin>(addr):
        global<info>(ADMIN).total_supply >= global<coin>(addr).value;
}

public fun initialize(account: &signer) {
    assert!(signer::address_of(account) == ADMIN, 0);
    move_to(account, Info { total_supply: 0 })
}

public fun mint(account: &signer, amount: u64): Coin acquires Info {
    assert!(signer::address_of(account) == ADMIN, 0);
    
    let supply = borrow_global_mut<info>(ADMIN);
    supply.total_supply = supply.total_supply + amount;
    
    Coin { value: amount }
}

public fun value(coin: &Coin): u64 {
    coin.value
}

public fun value_mut(coin: &mut Coin): &mut u64 {
    &mut coin.value  
}

}

a) 模塊(Module):每個Move模塊由一系列結構類型和過程定義組成。模塊可以導入類型定義並調用其他模塊中聲明的過程。模塊的完全限定名以存儲模塊代碼的16字節帳戶地址開始。帳戶地址作爲命名空間,用於區分同名模塊。

b) 結構體(Structs):該模塊定義了兩個結構體Coin和Info。Coin代表分配給用戶的代幣,Info記錄代幣總量。兩個結構體都被定義爲資源類型,可存儲在持久全局鍵/值存儲中。

c) 過程(function):代碼定義了一個初始化、一個安全過程和一個不安全過程。創建Coin前必須調用initialize過程,將單例Info值的total_supply初始化爲零。signer是特殊類型,表示由Move外部邏輯驗證的用戶。斷言確保只有指定管理員帳戶可調用此過程。mint過程允許管理員創建新代幣,同樣有訪問控制。value_mut過程接受Coin的可變引用,返回指向value字段的可變引用。

合約結構上與其他智能合約語言相似,但資源類型和全局存儲是Move語言中存儲和資源安全的關鍵機制。

全局存儲允許Move程序存儲持久數據,這些數據只能由擁有它的模塊以編程方式讀寫,但存儲在公共帳本中,其他模塊的用戶可查看。全局存儲中的每個鍵由完全限定的類型名稱和存儲該類型值的帳戶地址組成。雖然全局存儲在所有模塊間共享,但每個模塊對其聲明的key具有獨佔的讀寫訪問權。

聲明資源類型的模塊可以: • 通過move_to指令將值發布到全局存儲 • 通過move_from指令從全局存儲中刪除值 • 通過borrow_global_mut指令獲取全局存儲中值的引用

模塊可對其控制的全局存儲強制約束。例如,確保只有ADMIN帳戶地址可持有Info類型結構體,通過定義initialize過程實現,該過程在Info類型上使用move_to,並強制執行在ADMIN地址上調用move_to的前置條件。

以下是兩個保證該模塊代碼安全的靜態檢查特性機制:不變量規約和字節碼驗證器

a) 不變量檢查(規約檢查):模塊第10行表示靜態檢查的不變量——系統中所有Coin對象的值字段之和必須等於存儲在ADMIN地址的Info對象的total_value字段。不變量是形式化驗證中的術語,表示狀態的守恆性。這種守恆屬性適用於模塊的所有可能客戶端。

b) 字節碼驗證器:安全類型和線性化是字節碼驗證器的主要驗證範圍。雖然其他模塊不能訪問由0x1::TestCoin::Coin控制的全局存儲單元,但它們可以在自己的過程和結構聲明中使用這種類型。

Move有字節碼驗證器(在字節碼級別強制執行的類型系統),允許模塊所有者防止不希望出現的結果。只有聲明結構類型Coin的模塊才可以: • 創建Coin類型的值 • "解包"Coin類型的值到其組件字段 • 通過rust風格的可變或不可變borrow獲得對Coin字段的引用

驗證器還強制結構默認爲線性,以確保在聲明結構的模塊之外線性地防止復制和銷毀。同時,驗證器還會對一些類型的常見內存問題進行強制檢查。

檢測過程主要有三類:

1. 結構體合法檢查:保證字節碼完整性,檢測錯誤非法引用、重復資源實體和非法類型籤名等
2. 過程邏輯的語義檢測:包括參數類型錯誤、循環索引、空索引和重復定義變量等
3. 連結時錯誤,非法調用內部過程,或連結聲明和定義不匹配的流程

驗證器首先創建CFG(控制流圖),然後檢測棧中被調用者的訪問範圍,保證合約被調用者不能訪問調用者的棧空間。同時爲檢查類型,每個Value棧都維護對應的Type棧。

接下來是資源檢查和引用檢查。資源主要檢查不可雙花、不可銷毀、必有歸屬等約束。引用檢查結合動態和靜態分析,使用類似rust類型系統的borrow checking機制。

最後是連結檢查,需要對連結對象和聲明是否匹配、過程的訪問控制等再次檢查。

2. Move的運行機制

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

其次,Move程序在堆棧上執行。全局存儲分爲內存(堆)和全局變量(棧)。內存是一階存儲,其單元不能存儲指向內存單元的指針。全局變量用於存儲指向內存單元的指針,但索引方式不同。訪問全局變量時,代碼提供地址和綁定到該地址的類型。這種劃分簡化了操作,使move語言語義更易形式化。

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

在Move中,定義爲資源的值只能被破壞性移動(使之前保存該值的存儲位置無效),但某些值(如整數)可以被復制。

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

調用棧包含過程執行的所有上下文信息和指令編號。執行Call指令時,創建新的調用棧對象,將調用參數存儲到內存和全局變量,然後解釋器執行新合約的指令。遇到分支指令時,在本過程內部發生靜態跳轉。模塊內過程依賴無環,加上模塊無動態指派,強化了執行期間函數調用的不可變性:procedure執行過程的call frame必然相鄰,避免了重入可能。調用return結束調用,返回值放在棧頂。

研究MoveVM代碼可見,MoveVM將數據存儲和調用堆棧(過程邏輯)存儲分開,這是與EVM最大的不同。在EVM中,實現ERC20 Token需在一個合約中寫好邏輯並記錄每個用戶狀態,而在MoveVM中,用戶狀態(帳戶地址下的資源)獨立存儲,程序調用必須符合權限和關於資源的強制性規則。這雖犧牲了一定靈活性,但在安全性和執行效率(有助於實現並發執行)上獲得很大提升。

3. Move Prover

最後,我們來了解Move提供的輔助自動化審計工具Move prover。

Move Prover是基於推理的形式化驗證工具。它使用形式化語言描述程序行爲,並用推理算法驗證程序是否符合預期,幫助開發人員確保智能合約正確性,減少交易風險。簡言之,形式化驗證就是用數學方法證明系統無Bug。

目前主流自動軟件驗證算法基於可滿足性模理論求解器(SMT solver)。SMT solver實際上是公式求解器。上層軟件驗證算法將驗證目標拆分爲公式,交由SMT solver求解,根據結果進一步分析,最終報告驗證目標成立或發現反例。

基本驗證算法是演繹驗證(deductive verification),還有其他驗證算法如有界模型檢測、k歸納法、謂詞抽象和路徑抽象等。

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

Move Prover總體架構如下:

首先,Move Prover接收含程序輸入規範(specification)的Move源文件。Move Parser從源碼中提取規範。Move編譯器將源文件編譯爲字節碼,與規範系統一起轉化爲驗證者對象模型(Prover Object Model)。

該模型被翻譯成Boogie中間語言。Boogie代碼傳入Boogie驗證系統,進行"驗證條件生成"。驗證條件傳入Z3求解器(微軟研發的SMT求解器)。

VC傳入Z3後,驗證器檢查SMT公式(程序代碼是否滿足specification規範)是否不可滿足。若是,表示規範成立。否則,生成滿足條件的模型,轉換回Boogie格式發布診斷報告。診斷報告還原爲類似標準編譯器錯誤的源碼級錯誤。

![Move安