Facebook的Diem團隊夢碎 但成果留存：談談Move的編程魅力（下）

昨天，我們發布了【Facebook的Diem團隊夢碎，但成果留存：談談Move的編程魅力（上）】，向大家介紹了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編寫的智能合約的形式化驗證工具）進行的技術深入研究。

鄭重聲明：本文版權歸原作者所有，轉載文章僅為傳播信息之目的，不構成任何投資建議，如有侵權行為，請第一時間聯絡我們修改或刪除，多謝。