前言
Move語言是一種可編譯運行在實現了MoveVM的區塊鏈環境中的智能合約語言。其誕生之初，考慮到了諸多區塊鍊和智能合約的安全性問題，並參考了一些RUST語言的安全設計。作為新一代以安全為主要特點的智能合約語言，其安全性究竟如何？是否在語言層面或相關機制方面可以避開常見於EVM、WASM等合約虛擬機的安全威脅？其本身是否存在特有的安全性問題？
Numen Cyber Labs 在對基於MoveVM實現智能合約的兩條公鏈——APTOS和SUI的研究過程中, 發現了一些虛擬機層面較為底層的漏洞(https://mp.weixin.qq.com/s/IY8nj73J1oyOJ-oomDcOPg和https://mp.weixin.qq.com/s/gNGtQVVPTE2tYlshRfDhmg）並得到了官方的確認和修復。
而本篇文章將從語言特性、運行機制和驗證工具三個層面嘗試解答有關Move語言的安全性問題。
1、Move語言的安全特性
編寫正確的代碼是困難的，即使經過多次測試，我們也無法保證自己編寫的代碼不出漏洞。在與不受信任的代碼交互時，編寫能夠保持關鍵安全屬性的代碼則更加困難。有許多技術可以強制執行一些運行時的安全性：如沙箱、進程隔離、對象鎖等編程模式；或者，可以在編譯時指定靜態的安全性，如強制靜態類型或斷言檢查。
有時，我們也可以藉助語義分析與靜態分析工具，以確保其代碼和安全規則相一致，即確保即使在代碼鏈接到不受信任的代碼並與之交互時，在一些可證明的邏輯規約上也會保持不變。
看上去這些都是很好的方案，能夠避免運行時的開銷，並且提前發現安全問題。然而不幸的是，編程語言能夠通過使用這些方法獲得安全性極其有限，我們將其歸因於兩個原因。首先，他們通常具有無法使用靜態分析工具的語言的特性，例如動態分派、共享可變性和反射等非線性邏輯，違反了安全不變量規則，從而給黑客們提供了廣泛的攻擊面。所以，大多數編程語言不能輕易地使用與安全相關的靜態工具或表達性強的規約化語言（specification language）進行擴展。儘管這兩種擴展都是至關重要的，可被預先定義的。
與許多現有的編程語言不同，Move語言被設計為既支持編寫與不受信任的代碼安全交互的程序，又支持靜態驗證。 Move語言具備這樣的安全特性，是因為捨棄了所有的基於靈活性考慮的非線性邏輯，不支持動態分派，也不支持遞歸的外部調用，而是使用了泛型、全局存儲、資源等概念來實現一些具有替代性的編程模式。例如，Move省略的動態調度和遞歸調用特性，這些特性在其他智能合約語言中導致了代價高昂的重入漏洞。
為了更加了解Move語言的特性，我們看以下的示例程序：
Move中一個幣資產的實現
a)模塊（Module）:每個Move模塊由一系列結構類型和過程定義組成。模塊可以導入類型定義(例如，在第2行use 0x1::signer)並調用在其他模塊中聲明的過程。模塊的完全限定名以存儲模塊代碼的16字節帳戶地址開始(在這裡，我們編寫一個帳戶地址，如0x1，作為16字節十六進制地址的簡寫，用前導0填充)。帳戶地址充當一個命名空間，用於區分具有相同名稱的模塊;例如，0x1::TestCoin和0x2::TestCoin是不同的模塊，具有自己的類型和過程。
b) 結構體（Structs）:模塊中定義了兩個結構體Coin和Info。一個Coin代表分配給模塊用戶的代幣，而Info記錄了該代幣總共存在多少。由聲明上的has key語法可知，這兩個結構體都被定義為了資源類型（具備key或store Abilities的結構體），表示這兩個結構體都可以存儲在持久全局鍵/值存儲中。
c)過程（function）:代碼定義了一個初始化、一個安全過程和一個不安全過程。創建任何Coin之前必須調用initialize過程，它將單例Info值的total_supply初始化為零。在這裡，signer是一個特殊的類型，它表示一個由Move之外的邏輯驗證的用戶。斷言簽名者的地址等於ADMIN確保這個過程只能由指定的管理員帳戶調用。過程mint允許管理員創建所需數量的新代幣(第25行);這是在硬幣總數更新之後(第23行)。像初始化一樣，這個過程有訪問控制，以確保它只能由管理員帳戶調用(第20和21行)。 value_mut過程接受一個對Coin的可變引用作為輸入，並返回一個指向Coin值字段的可變引用。
可以看到，合約結構上和其他的智能合約語言沒有太大差別，但我們需要對資源類型以及全局存儲(Persistent Global Store)的概念進行更詳細的解釋，這是Move語言中對存儲和資源安全的關鍵機制。
全局存儲允許Move程序存儲持久數據(例如，Coin餘額)，這些數據只能由擁有它的模塊以編程方式讀/寫，但也存儲在公共賬本中，可以由在其他模塊中運行代碼的用戶查看。
全局存儲中的每個鍵都由完全限定的類型名稱(例如，0x1::TestCoin::Coin)和存儲該類型值的帳戶地址(帳戶地址存儲模塊代碼和結構數據)組成。雖然全局存儲在所有模塊之間共享，但每個模塊都對其聲明的key（賬戶地址）具有獨占的讀/寫訪問權。也就是說聲明了資源類型(比如Coin)的模塊可以:
•通過move_to
•通過move_from
•通過borrow_global_mut
由於模塊“擁有”由其通過key控制的全局存儲條目，它可以對該存儲強制約束。例如，確保只有ADMIN帳戶地址可以持有類型為0x1::TestCoin::Info的結構體。它只通過定義一個過程(initialize)來實現這一點，該過程在Info類型上使用move_to，並強制執行在ADMIN地址上調用move_to的前置條件(第13行)。這些約束不同於靜態不變量，因為它們需要運行時檢查。在這種情況下，由於參數account是在運行時提供的，程序員不能靜態地強制它始終是ADMIN的，因此需要在第13行進行不變量檢查。
以下就是兩個保證該模塊代碼安全的兩個靜態檢查特性機制：不變量規約和字節碼驗證器
a)不變量檢查（規約檢查）:模塊的第10行，表示靜態檢查的不變量——系統中所有Coin對象的值字段之和必須等於存儲在ADMIN地址的Info對象的total_value字段。所謂不變量，是形式化驗證中的一個術語，表示了一種狀態的守恆性，也可以稱為不變式或不變性。我們希望守恆屬性適用於模塊的所有可能的客戶端(包括惡意的客戶端):任何違反都會破壞Coin的完整性。因此，不變式不只是影響單個對象，而是影響它們的集合(即所有的Coin對象)。該處其實就是我們下一節要介紹的move prover中可用於形式化檢查的specification language。
b)字節碼驗證器:安全類型和線性化是字節碼驗證器的主要驗證範圍: 如本例，儘管其他模塊不能訪問由0x1::TestCoin::Coin 控制的全局存儲單元，但它們可以在自己的過程和結構聲明中使用這種類型。例如，另一個模塊可以公開一個支付過程，該過程接受0x1::TestCoin::Coin作為輸入。
乍一看，允許Coin等敏感值流出創建它們的模塊可能看起來很危險——惡意客戶端模塊會創建假冒硬幣，人為增加其擁有的硬幣的價值，或複制/銷毀現有硬幣。幸運的是，Move有一個字節碼驗證器(一個在字節碼級別強制執行的類型系統)，它允許模塊所有者防止這些不希望出現的結果。只有聲明了結構類型Coin的模塊才可以:
•創建一個Coin類型的值(例如，第25行);
•“解包”一個Coin類型的值到它的組件字段中(在本例中為value);
•通過rust風格的可變或不可變borrow(例如&mut Coin)獲得對Coin字段的引用。
這允許模塊作者在模塊中聲明的結構的創建值和字段值。驗證器還強制結構默認為線性。以確保線性地防止在聲明結構的模塊之外複製和銷毀(例如，通過覆蓋存儲結構的變量或允許它超出作用域)。同時，驗證器還會對一些類型的常見內存問題（如溢出）進行強制檢查。
檢測過程主要有三類：
1）結構體合法檢查：保證字節碼的完整性, 檢測錯誤非法的引用，重複的資源實體以及非法的類型簽名等
2）過程邏輯的語義檢測：包括參數類型錯誤，循環索引，空索引以及重複定義變量等。
3）鏈接時錯誤，非法調用內部過程，或者鏈接一個聲明和定義不匹配的流程。
驗證器會首先創建一個CFG（Control-flow Graph，控制流圖），因為沒有非線性邏輯，這個控制流圖可以清晰的描述程序塊間的調用關係，而無需考慮遞歸深度的問題。
隨後，驗證器會檢測棧裡面被調用者的訪問範圍，保證合約的被調用者不能訪問到調用者的棧空間。例如一個過程被執行的時候，調用者首先在CallStackFrame裡面初始化局部變量，然後將局部變量放入到棧裡面，假設當前棧的高度是n，那麼有效的bytecode必須滿足不變量：當調用過程結束的時候，棧的高度依然還是n。驗證器主要是通過分析每個指令塊的指令對棧的可能影響，保證不操作高度高於n的棧空間。這裡有一個例外就是，一個以return結尾的指令塊，他退出的時候高度必須是n+m，其中m是過程返回值的個數。
同時為了檢查類型，每一個Value 棧都維護了一個對應的Type 棧，執行的時候Type棧也跟這指令執行進行pop和push。
接下來是資源檢查和引用檢查。資源主要檢查資源的不可雙花、不可銷毀、必有歸屬（返回值必須被接受）等約束。而引用檢查結合了動態和靜態分析。靜態分析利用類似rust類型系統的borrow checking機制，保證：1. 所有引用必須指向一個已經被分配的存儲上，防止空指針；2. 所有的引用都有安全的讀寫權限。
而borrow_global調用的時候會動態的對全局變量的引用進行了計數，解釋器會對每個發布了的資源進行判斷，如果被borrow或者move了，再次引用就會報錯。
最後是鏈接檢查，需要對鏈接的對象和聲明是否匹配，過程的訪問控制等做再次的檢查。
可見，通過不變量檢查和字節碼驗證器兩種機制，雙重保障了代碼在編譯時的安全性。接下來我們通過分析move的運行機制，來看看MoveVM如何保證運行時的安全性。
2、Move的運行機制
首先，Move程序運行在虛擬機中，並且在運行時不能訪問系統內存。這使得Move可以在不信任的環境中安全地運行，並且不會被破壞或濫用。
其次，Move程序是在堆棧上執行的，形式上，之前提到的全局存儲被分為兩部分:內存（堆）和全局變量（棧）。內存是一個一階存儲，因此它的單元不能用來存儲指向內存單元的指針。全局變量被用來存儲指向內存單元的指針，但是它們的索引方式與內存不同。為了訪問全局變量，代碼提供了一個地址和一個綁定到該地址的類型。這種劃分簡化了操作，使得move語言在語義上更容易形式化。
而Move的字節碼指令在一個棧式的解釋器進行執行，棧式虛擬機的好處是易於實現和控制，對硬件環境的要求較少，非常適合區塊鏈場景。同時相對寄存器式的解釋器, 棧式解釋器在不同的變量之間進行copy和move更容易控制和檢測。
在Move語言中，任何被定義為資源的值都只能被破壞性地移動(使以前保存該值的存儲位置無效)，但只有某些值(例如，整數)可以被複製。
Move程序運行在堆棧上的時候，其狀態為⟨C, M, G, S⟩的四元組，由:調用棧（C），內存（M），全局變量（G）和操作數（S）組成。堆棧還維護一個函數表(模塊本身)來解析包含函數體的指令。
調用棧包含了一個過程執行的所有上下文信息以及指令編號（指令會被唯一編碼，減少代碼體積）。當在一個過程中執行Call指令調用其他的過程的時候，會創建一個新的調用棧對象，然後將對應的調用參數存儲到內存和全局變量上面，最後解釋器開始以此執行新的合約的指令。執行過程遇到分支指令的時候，會在本過程內部發生一個靜態跳轉，所謂靜態跳轉實際上是指跳轉的offset是事先已經確定好的，不會像evm一樣動態跳轉。這也就是之前提到的不支持動態分派的特性。也就是說模塊內的過程依賴是無環的，加上模塊本身的沒有動態指派，這樣就加強了執行期間的函數調用的不可變性：一個procedure在執行過程的call frame必然是相鄰的，從而避免了重入的可能性。最後調用return結束調用，同時返回值放在棧頂。
通過研究MoveVM的代碼，我們可以清晰的看到，MoveVM將數據的存儲和調用堆棧（過程邏輯）的存儲是分開的，這點是和EVM最大的不同的地方，例如，在EVM中，要實現一個ERC20的Token，需要在一個合約中寫好邏輯和對每個用戶的狀態進行記錄，而在MoveVM中，用戶狀態（賬戶地址下的資源）是獨立存儲的，程序調用必須符合權限和關於資源的強制性規則，雖然犧牲了一定的靈活性，但是在安全性和執行效率（有助於實現並發執行）上獲得了很大的提升。
3、Move Prover
最後，我們來了解下Move提供的能夠進行輔助自動化審計的工具Move prover。
Move Prover是一種基於推理的形式化驗證工具。它使用形式化語言來描述程序的行為，並使用推理算法來驗證程序是否符合預期，可以幫助開發人員確保智能合約的正確性，從而減少交易風險。簡單來說，形式化驗證就是用數學方法去證明我們的系統是無Bug 的。
目前主流的自動軟件驗證算法是基於可滿足性模理論求解器（SMT solver, satisfiability module theories solver）的。雖然這名字看起來有點唬人，但其實SMT solver 就是一個公式求解器。上層的軟件驗證算法將其驗證目標拆分為一些公式，交由SMT solver 求解，再根據求出的結果進一步分析，最終報告驗證目標成立，或者是發現了一個反例。
一種基本的驗證算法是演繹驗證（deductive verification），也有不少其他的驗證算法，比如有界模型檢測、k 歸納法、謂詞抽象和路徑抽像等
Move Prover就是使用了演繹驗證算法來驗證程序是否符合預期。這意味著，Move Prover可以根據已知的信息推斷出程序的行為，並確保其與預期的行為相匹配。這有助於確保程序的正確性，並減少了人工手動測試的工作量。
Move Prover的總體架構如下圖所示：
首先，Move Prover 接收一個Move源文件作為輸入，該文件中需要設置程序輸入規範（specification）。之後Move Parser 會在源碼中把規範提取出來。 Move 編譯器將源文件編譯為字節碼，和規範系統(specification)共同轉化為驗證者對像模型(Prover Object Model)。
這個模型會被翻譯成一種名為Boogie的中間語言。這段Boogie 代碼會被傳入Boogie 驗證系統，該系統對輸入進行“驗證條件生成”(verification condition generation)。該驗證條件會被傳入一個名為Z3 的求解器中，這是微軟研發的一種可滿足性理論（SMT）求解器。
VC 被傳進Z3 程序後，該驗證器會檢查SMT公式（程序代碼是否滿足specification規範）是否是不可滿足的。如果是這樣，這意味著規範是成立的。否則，將生成一個滿足條件的模型，並將其轉換回Boogie格式，以便發布診斷報告。然後將診斷報告還原為與標準編譯器錯誤類似的源碼級錯誤。
為了描述規範系統，move使用Move Specification Language，其是Move語言的子集，它引入了對靜態描述有關程序正確性的行為的支持，而不影響生產。同時可以獨立為專門的規約化文件，從而讓業務代碼和形式化驗證代碼分開。
網上已經有很多其他的關於Move Specification Language的教程，感興趣的可以自行學習，建議合約程序員們多加了解，以提高自己代碼的安全性。同時，由於Move Specification Language可以不侵入代碼的單獨編寫，對於安全性要求更高的項目來說，可以將該規約代碼交由安全經驗更加豐富的第三方安全公司來撰寫，在審計代碼的同時，可以給出更嚴格的形式化驗證報告。
總的來說，Move Prover是一種非常有用的工具，可以幫助開發人員確保智能合約的正確性。它使用形式化語言來描述程序的行為，並使用推理算法來驗證程序是否符合預期。這有助於減少交易風險，並使開發人員能夠更自信地將智能合約部署到生產環境中。
4、總結
Move語言的設計在安全性的考慮上非常出色，在語言特性、虛擬機執行和安全工具層面，都給出了非常全面的考慮。語言特性上犧牲了部分靈活性，強制類型檢查和線性邏輯，方便在編譯檢查、形式化驗證時更加的自動化和具備安全可驗證性，而MoveVM在設計上將狀態與邏輯分開，更加貼合區塊鏈上資產安全管理的需求。
綜上，在語言層面，常見於EVM的重入、溢出、Call/DelegateCall注入等漏洞可以有效避免，但是鑑權、代碼邏輯、大整數結構溢出（最新的move語言版本已經支持u256，如使用官方u256類型不會產生溢出漏洞）等問題並不能依賴語言層面的特性去避免，而Move Prover並不能在整體的大意疏忽時產生作用。
雖然Move語言在安全層面已經為程序員考慮了很多，但沒有完全安全的語言，也沒有完全安全的程序。我們仍然建議，Move智能合約的開發者使用第三方安全公司審計服務，並且將specification部分代碼的編寫和驗證交由第三方安全公司來完成。
5、Numen現已支持Move合約審計及項目安全評估服務
Numen Cyber Labs可以為Move語言的開發者提供以下服務：
a、合約審計，包括溢出、隨機數、DDos、鑑權、業務邏輯、價格操縱、套利限制、代碼規範、市場公平性等審計項
b、形式化驗證，基於move prover提供Specification Language編寫及形式化驗證服務。
c、安全測試，使用Fuzzer和模擬交易腳本的安全性測試服務。
d、合約監控，對合約相關的transaction進行意圖分析及安全響應。
歡迎Move生態的開發者聯繫我們進行交流和諮詢，郵箱contact@numencyber.com 。更多信息，歡迎關注我們微信公眾號@Numen Cyber Labs，或通過下方鏈接關注，閱讀。
Move語言安全性解析-智能合約語言的game changer
