Move是一種相對發展時間較短的編程語言，但已經在許多Web3.0項目中得到了應用。
CertiK安全專家團隊最近審計了一個支持Move編寫智能合約的新型Layer 1區塊鏈。藉此機會，我們將為大家整體概述一下Move這一新型編程語言。
鑑於該內容較為專業，在這篇文章中，我們將討論Move及其兩個特性：可編程資源（有助於支持高交易率）和形式化驗證（有助於提高安全性）。
在這一過程中，本文也將展示Move的語法、類型系統和內存模型，並研究工程師在使用Move時可能犯的一些常見錯誤。除此之外，我們也將從技術角度審視Move形式化驗證的潛力及面臨的挑戰。
什麼是Move？
Move是一種用於編寫智能合約的特定領域編程語言。最近推出的幾個熱門項目均支持Move語言，包括Aptos、0L和Starcoin區塊鏈。另外還有Sui區塊鏈同樣支持Move語言並將其命名為Sui Move。
Move最初是作為Diem項目的一部分開發的，但這一屬於Meta（原Facebook）的基於區塊鏈的支付網絡現在已被解散。
在Diem發表的《為什麼要創建Move？ 》文檔中，其指出“為了成功支持像Diem支付網絡這樣的支付系統，我們需要一種可以對數字資產的所有權進行編碼，並為這些資產的轉移創建程序的編程語言。目前已經有數百種語言在使用，其中一些已經作為原生語言包含到區塊鏈的實現中。
Diem Networks本可以選擇一種通用語言，如WebAssembly或Java字節碼，或現有的區塊鏈語言，如EVM字節碼或比特幣script。理論上，我們的確應當選擇一種現有的語言，畢竟一種語言的社區、庫、工具都和語言設計一樣重要，而這些都需要多年的時間來建立。從這一角度上來說，應該謹慎創建一種新語言。但最終選擇創建Move是因為我們看到了一個機會——Move將可以幫助我們在幾個重要方面對現有替代方案進行逐步改進。 ”
Diem需要安全地支持大量的交易，因此其團隊決定以這些目標為基礎創建Move。
可編程資源
Move的關鍵特徵之一是它對可編程資源的使用。一個資源（Resource）直接代表著一條有價值的數據（例如一個用戶所持有的項目資產數量）。在Move中，每個持有項目資產的賬戶中通常都存儲著可以直接代表該資產的數據。這與Solidity中項目資產的表示形成了鮮明的對比，從賬戶到他們持有的項目資產數量的映射，Solidity通常是使用一張映射表在智能合約中進行記錄。
這種對可編程資源的利用有兩個主要優勢。首先，它形成了一個支持高交易率的智能合約編程模型。如果一項交易涉及兩個「僅相互交互」的賬戶，該交易可以與其他交易並行執行。類似於現實生活中，小明在便利店結賬付款並不影響小紅的結賬付款。 Aptos區塊鏈就是一個很好的例子，其使用軟件交易存儲器來並行運行交易，並檢測兩個同時進行的交易是否可能發生衝突。
可編程資源的第二個優勢是它們可以自動驗證程序是否存在某些類型的錯誤：例如，資源永遠不會被悄無聲息地刪除或複制——這是由Move編譯器完成的。但是仍然有可能在智能合約代碼中引入算術或邏輯錯誤，從而導致資源中出現不正確的值。
下圖來自GitHub（https://github.com/move-language/move）上的Move文檔，顯示了區塊鏈數據在Move中的組織方式。 Move將區塊鏈狀態稱為全局存儲。
每個區塊鏈地址代表一個賬戶，其中一些可能是外部擁有的。與以太坊不同的是，所有地址都可以存儲數據。在下圖中，BasicCoin持有者的賬戶中有數據表明他們所持有的BasicCoin數量（資源）。該圖顯示，地址0x42還擁有一個實現BasicCoin的代碼模塊。
當使用Move編寫智能合約時，最好的做法是將資源存儲在擁有該資源的賬戶中，而非包含該智能合約代碼的賬戶中。儘管有可能在Move智能合約中實現「Ethereum風格」的資源映射，但涉及此類合約的交易可能無法並行執行。
Move的安全功能
Move包含幾個可幫助開發者創建更安全智能合約的功能。其中就包括上文所提到的“編譯器會檢查資源的基本使用情況”這一功能。 Move語言原生就支持形式化驗證，並有意排除了那些容易導致形式化驗證困難的語言結構。
此外，Move還支持泛型。泛型編程（Generic Programming）允許通用代碼在不同類型中被重複使用。
這一點很重要，因為使代碼更安全的一種方法是重用那些已被專家精心編寫過的代碼，少編寫一些新代碼。就像許多Coin共享實現代碼——如Aptos Coin標準所示，通用編程允許該代碼在不同Coin之間共享。
Move類型系統和Rust
在處理有價值的數據時，追踪清楚是誰擁有這些數據，並限制對這些數據的操作（如復製或刪除）十分重要。
幸運的是，已經有一種開發完善的支持所有權特性的編程語言：Rust。 Move的開發者在類型和語法方面都受到了Rust思想的啟發。
此圖表顯示了Move的內置原始類型：
此圖表顯示了Move的結構類型，這些是由其他類型構建的類型：
當涉及到結構類型時，事情就變得有趣了，結構類型是Move中唯一的用戶定義類型，一個結構類型是一個存儲在字段中的值的集合：
在Move中，結構是一種“value”類型。結構類型的value在內存或存儲中是線性排列的，對一個結構的引用必須明確地構建。這與Solidity不同，在Solidity中，結構變量通常是對底層value的引用。下圖說明了這一點：
字段可以是除引用類型之外的任何類型，結構的實例是通過打包創建的（就像在Rust中那樣）。
Move為結構類型的value實現了一個類似於Rust的所有權系統，其中每個value都由包含它的變量或字段擁有。引用並不擁有它們所指向的任何value。
默認情況下，結構value只能被轉移到另一個所有者，它們不能被複製或刪除。當一個結構value被轉移到另一個所有者那裡時，它將無法被先前的所有者訪問。
在一個結構類型的value被創建後，同一時間只存在該value的一個可以使用的副本。以下代碼說明了這一點：
Move還有一個稱為abilities的類型特性，它可以控制一個給定類型的value可被允許進行哪些操作——這是受到了Rust的啟發。這四種能力分別是：
Copy：value可以被複製。不具備複製能力的結構在被使用後無法被訪問。
Drop：value可以被刪除。當一個value的所屬變量或字段超出範圍時，該value將被刪除。不具備刪除能力的結構則必須被使用，無法被丟棄。要么明確地銷毀它們，要么將它們“轉移”到其他地方。它們不能被無聲無息地刪除或丟棄。
Store：value可以存儲在全局存儲的其他結構中。
Key：該類型可用作「鍵」來對全局存儲進行訪問。
對於結構類型來說，abilities是在結構類型聲明中聲明的，如下圖所示：
以上內容主要介紹了Move是什麼，以及其一個關鍵特性：可編程資源。
接下來我們介紹Move的另一關鍵特性：形式化驗證，及該特性為Move所帶來的優勢和弊端。
深度資源
一個資源是一個只有key和store能力的結構體。在Move中，一個賬號每種類型的資源只能持有一個。資源不能被複製或丟棄，這使得資源適合直接代表價值的物品，例如coin。
賬戶與其資源之間的直接關聯，使得編寫某些「不好的」代碼也變得更加困難，例如導致價值意外損失的代碼。
但是，不正確的計算以及與資源有關的那些更微妙的邏輯錯誤還是有可能會出現。這就是為什麼我們強烈建議進行智能合約審計來增強安全保障。
區塊鏈上全局存儲的編程接口執行了一個限制——每個賬戶最多只能持有每個資源的一個副本。
一個程序可以使用以下操作在全局存儲中創建、讀取、更新和刪除資源：
為了避免資源的偽造及其他不當操作，Move執行嚴格的數據封裝（encapsulation of data）。 Move的代碼和類型聲明被分組為module。代碼作為module的一部分被部署到一個賬戶中。
當一個結構類型在一個模塊中被聲明時，只有在同一模塊中定義的函數可以訪問該結構類型的字段或創建該結構類型的value。 Move結構聲明被視為抽像數據類型，對其module以外的代碼隱藏其內部工作原理。 module中的函數默認為私有，只能在模塊內調用。它們可以被聲明為public，這使得它們可以被外部代碼訪問。 module可以有friend，也就是他們信任的其他module，並且可以聲明個別non-public方法以供friend訪問。
References
Reference是pointer的一種類型，包括對其使用方式的限制。使用pointer的語言中，一個常見問題是懸掛引用（dangling references）：指向已被重新用於其他目的或被取消分配的內存或存儲。
例如，如果你為一個向量的最後一個元素創建了一個reference，然後縮小了向量，則該reference現在就指向了無效的內存或存儲。懸掛引用和其他與不受限制的pointer相關的問題歷來是導致大多數軟件安全漏洞的原因。
Move處理reference的方式與Rust處理reference的方式類似。它包括類型檢查規則，以確保reference的生命週期不長於原始數據的生命週期。當代碼創建一個reference時，該reference並沒有取得數據的所有權。相反，代碼借用了讀取或寫入數據的能力。
在閱讀Move代碼時，名稱中帶有“borrow”一詞的操作就會產生reference。
Move語言的定義中並不包含對reference checking的完整描述（”borrow checker”，它確保borrow的reference不會存留太長時間）。
不過，今年有一份詳細的技術論文被發表（https://arxiv.org/abs/2205.05181），該定義中的兩個關鍵規則是：
① 不允許對reference的reference，而且reference不能存儲在結構中。這意味著，當一個函數被調用並帶有一個reference參數時，儘管它可以返回reference，但也不能將reference存儲在一個長期存在的數據結構中。一個函數調用並不會延長reference的生命週期。
② 對局部變量或局部變量字段的reference不能超過局部變量的作用域的終點。
類Rust語法
Move有一種類似於Rust的語法，在某些地方與C風格的語言有些不同。在此，我們總結了一些重要的語法規則，以便更輕鬆地瀏覽Move代碼。
使用let聲明變量：
類型註釋：type和initializer=e是可選的。當它們被省略時，Move使用類型推理來確定變量的類型。
下圖是一些變量聲明的例子：
Move有典型的表達式，用於算術、移位操作、函數調用、賦值等，用於流程控制的有if、while、for、break和continue等表達式。
函數是使用以下語法聲明的：
其中id是函數的名稱，parameter-list聲明參數，return-type是返回類型。還有一些必要的註釋，如acquires註釋。這些註釋列出了函數從全局存儲中訪問的資源，還有關於可見性的註解。如前所述，函數可以是公共的、私有的，或者可以被friend module訪問。
形式化驗證
智能合約安全和正確地運行至關重要，因為其往往持有巨額的資產。形式化驗證是確保一個程序（如智能合約）執行其預期操作的最佳技術之一。
在形式化驗證中，工程師編寫規範，並以數學方式表達代碼的預期行為。然後使用工具嘗試檢查代碼是否符合規範。
我們可以將這種檢查視為測試，但這其中有一個關鍵的區別：它不是檢查代碼在某些特定情況下的行為，而是檢查代碼在所有可能情況下的行為。
如果檢查通過，則說明該工具找不到代碼違反規範的用例。不過這並不意味著代碼100%不存在違反規範的情況，因為工具或編譯器的漏洞還是有可能導致錯誤的發生。但這依舊使得其比運行一組測試用例提供了更嚴格的規範保證。
對於一些代碼，特別是複雜的代碼，工具可能無法自動檢查代碼是否符合規範。因此工程師也許需要為一小部分的代碼添加具體化的規範，直到檢查器能夠成功運行為止。工程師甚至可能需要寫證明規則，然後該工具會根據數學原理檢查代碼是否符合這些證明規則。
因為確保智能合約的安全是至關重要的，一些智能合約編程語言會原生就提供對形式化驗證的支持。就像Solidity編譯器提供的SMTChecker工具，它假設requires子句始終為真，然後試圖證明assert子句永遠不會失敗。
Move也對形式化驗證技術進行了集成支持。它含有豐富的用於形式化驗證的規範語言，能夠規範比Solidity的requires和assert子句更複雜的屬性，並且有目的地刪除了會對形式化驗證造成問題的語言結構。 Move的開發環境中就包括一個名為“Move Prover”的檢查器。
CertiK由兩位常春藤盟校的計算機科學教授所創立。作為區塊鏈安全領域的先驅，CertiK運用的正是目前最先進的形式化驗證技術。創辦CertiK的兩位教授均是形式化驗證方面的專家，並創建了CertiKOS——世界上第一個也是唯一一個完全被驗證的並發式多核操作系統和管理程序。 CertiK致力於通過將形式化驗證技術應用於安全審計以確保智能合約的安全。
因此，CertiK安全專家自然而然地就注意到了Move這一集成了形式化驗證技術的編程語言。
下方是一個double函數及其規範的簡單示例。 double函數的功能是將一個64位無符號整數（unsigned integer）進行翻倍計算。由spec double給出的double 規範從數學上描述了預期的結果。
規範語言是Move的一個集成部分。規範被分離成spec block。 spec block指定了函數的前置條件（requirements）和後置條件（ensures）。
前置條件需要在函數被調用之前必須為真，以便該函數能夠正常運行。而後置條件則是指當函數返回時必須為真。
此外，spec block還指定了失敗條件（aborts_if）。規範語言支持大多數常規Move語法。它還支持用於指定程序行為的重要附加功能，包括forall、exists和implies。
下方是spec block的示例：
Move Prover將規範和程序語義轉換為了邏輯表達式。然後將它們傳遞給可滿足性模理論（SMT）求解器，例如Z3和CVC5，以證明或反駁。以下大幅簡化的圖表說明了這一點：
形式化驗證有其優勢也有弊端。
形式化驗證被認為是構建可靠程序的“黃金標準”，並被用於許多如NASA這樣的關鍵任務系統。編寫系統行為的形式化規範可以暴露出邏輯上的不一致或思維的不清晰。
然而即使是對於專家來說，將相對簡單的系統進行形式化規範也是困難且耗時的。
除此之外，在處理更複雜的程序或規範時，檢察員也會遇到阻礙，並且可能會需要極長的時間來將其解決。
在CertiK接下來發布的文章中，我們將更深入地探究Move形式化驗證的潛力和其所面臨的挑戰。
由於形式化驗證的複雜性，CertiK在此建議如有需求的用戶應當尋找一個在形式化驗證方向有所建樹的安全機構來進行合約審計或是協助對合約的形式化驗證。
寫在最後
我們希望這篇文章可為想要了解Move語言的讀者提供足夠的參考價值。
Move確實引入了新的方法來解決可擴展性問題以及提高安全性。然而，沒有一種語言可以100%保證安全，非可擴展的或不正確的代碼仍有機會干擾Move的內置功能。
如同Web3.0，兔子洞的存在是永遠數之不盡的。
如果你想了解關於Move技術特點的更多信息，那麼建議複製鏈接（https://move-language.github.io/move/introduction.html）至瀏覽器訪問這些值得參考的開發人員文檔，並持續關注我們對Move Prover（一個用Move編寫的智能合約的形式化驗證工具）進行的技術深入研究。
來源：星球日報
