號稱 Libra 最大創新的 Move 與 Solidity、DeepSEA 到底有何區別？

前言

6 月 18 日，Facebook 發布 Libra 項目白皮書，旨在建立一個簡單的全球性貨幣且為數十億人賦能的金融基礎設施。

Facebook Libra 在全球被普遍關注，金融監管者、從業者和學者紛紛從不同角度進行解讀。還有很多人從哲學、政治學或是經濟學等角度分析 Libra。正如一千個人眼中有一千個哈姆雷特，一千個人心中也有一千種貨幣觀點。

我們作為一個技術驅動的公司，更關注這次 Libra 發布的智能合約語言 Move，這個被很多人都譽為 Libra 最大的創新，Move 和以太坊的 Solidity、以及可驗證智能合約的 DeepSEA 語言到底有哪些區別呢？

眾所周知，基於以太坊的編程語言 Solidity是目前區塊鏈領域中最常用的開發語言之一。

即使 Solidity 在安全性方面存在一定的缺陷，並在近幾年發生了不少類似合約溢出的安全事件，並導致用戶大量損失。但由於其良好的適應性和可擴展性，已被廣大開發者和社區用戶所積極採用。

而這次 Libra 攜 Move 強勢歸來，便是主打的安全牌。基於 Rust 和 100%靜態類型驗證的全新思路，從底層內存和智能合約編程的代碼層面，來提高了安全性，以期避免發生在以太坊的安全事件。這也是這次 Libra 發布後，不少人都認為，Move 語言才是 Libra 最大的創新。

但可能我們不太了解的是，由美國區塊鏈安全公司 CertiK、耶魯大學實驗室和哥倫比亞大學實驗室共同研發的編程語言 DeepSEA 的研發也將於近期開發完成。

該語言利用植入其編程語言本身的形式化驗證技術，自動創建數學原理來證明源代碼的安全性，並獲得了以太坊基金會、IBM Blockchain和量子鏈基金會的科研獎金。DeepSEA 語言在主打安全性的同時，也在尋求兼容除 EVM 之外的更多虛擬機，實現信息和資產的跨鏈共享。

今天來自 CertiK 的安全專家團隊對 Move、Solidity、DeepSEA 進行了分析比較，解釋這三種編程語言之間的差異，並詳細說明其中的優缺點和複雜性。

Solidity 

以太坊成功地在應用場景中引入了智能合約的概念：

當比特幣將儲存在區塊鏈上的數據類型進行編碼時，以太坊的用戶就可以上傳任意一個程序來定製該系統。與比特幣相比，以太坊最大的不同點是：它可以支持更加強大的腳本語言，允許開發者在上面開發任意應用，實現任意智能合約，就是基於這個圖靈完備編程語言——Solidity 用以執行這些智能合約。

在 Solidity 上發行一個應用程序其實十分的簡單，它可以讓用戶創建一個自己的 Token（也可稱為「代幣」），用戶可以自行持有或者將其轉移至任何以太坊的賬戶上，也就是我們常說的發幣程序。

簡而言之，實現這個功能的方法只需要上傳一個儲存表格的程序，表中需要顯示每個用戶持有多少代幣，並列出一些功能即可。

比如將一個賬戶上的代幣轉移至另一賬戶上的代碼如下：

但是，在實際運行過程中，Solidity 的使用並沒有我們想像的那麼順利。比如經常出現的整數溢出漏洞會導致 Token 無限增發、重入風險會導致智能合約遭受到類似DAO 攻擊的嚴重損失等。

2018年4月，就有黑客利用以太坊 ERC-20 智能合約中整數溢出漏洞攻擊 BEC（美鏈的代幣「美蜜」）智能合約，成功向兩個地址轉出了天量級別的 BEC 代幣，導致市場上大量增發的 BEC 被拋售。此事使得當日 BEC 的價值幾乎歸零，64 億人民幣瞬間蒸發。

另一個 Solidity 可能存在的錯誤是在編譯器中仍存在一些漏洞，這些漏洞可能會導致智能合約存在巨大的安全風險。通常程序員只查看程序的源代碼，如果編譯器有一個bug導致它打出的位元組是錯誤的，這樣的錯誤非常難以防範，即便經過了完善的人工測試和靜態分析也仍然不可避免。

整體而言：Solidity 是一個功能強大並且非常靈活的編程語言——但是仍舊存在安全風險。Solidity 不提供任何證明代碼（或者以太坊虛擬機中的編解碼）安全性的功能。因此由第三方提供智能合約代碼審計、或者第三方的形式化驗證是證明代碼正確的最有效的方式。目前基於以太坊的智能合約應用廣泛，Solidity 的安全性是值得我們重視的。

Move 

Libra 的智能合約編程語言 Move，通過 Rust 語言固有的安全機制和 Move 語言 100%的靜態類型驗證等措施來達到提高安全的能力。但是經過 CertiK 的安全專家團隊研究發現，與 Solidity 相比，Move 擁有以下三個重要的不同之處：

首先，Move 通過省略某些特徵——動態調度和一般指針——來限制語言的表達，而對語言靈活性的大規模限制可能會引發重入錯誤。Move的設計者表示，這些限制會讓編寫 Move 的形式化驗證工具更加簡單，但是目前這些工具並不存在，Facebook 團隊表示已經充分認識到形式化驗證的優勢和重要性。

一個人口味最好雜一點，耳音要好一些，能多聽懂幾種方言。口味單調一點，耳音差一點，也不要緊，最要緊的是對生活的興趣要廣一點。

「我們將創建一種邏輯規範語言和自動形式化驗證工具，利用 Move 的驗證友好設計(參見第 3.4 節)。

驗證工具鏈將有檢查特定程序功能正確性的屬性，這些屬性超出了 Move 位元組碼驗證器執行的安全保證(參見 5.2 節)。」

                                                                                                                        ——Facebook 團 隊

其次，Move 支持「資源類型」（受線性類型系統啟發）。模塊可以定義特定類型的數據為「資源」，這意味著模塊外部的任何代碼都不能查看該類型值的內容：它們只能在變數之間移動並傳遞給函數，這雖然能夠幫助 Move的開發人員確保資源得到保存，但它們還不足以確保功能的正確性——Move 設計者也同意這一點，並認為最終他們將需要使用形式化驗證。

第三, 關於執行的問題：Move 的編譯器會生成類型化的位元組碼，同時，有一個可以檢查輸出類型是否正確的「位元組碼驗證器」。需要說明的是，這種「驗證器」與形式化驗證無關，它僅是對輸出類型進行一次完整性的檢查。當然，仍然可能會存在它創建類型正確但內容錯誤的編譯器 bug。

綜上而言，Libra 的 Move 語言額外添加了一層規範，可以避免很多 Solidity 的漏洞，然而這些安全性和正確性的保障仍舊是單獨存在的壁壘加持。

DeepSEA 

DeepSEA是一個將安全性放在首位的函數式編程語言，使用形式化驗證對源代碼進行安全保護。允許用戶在高抽象的層面上對代碼進行推理，實現無縫驗證代碼安全性的過程。

DeepSEA 編譯器能夠為每個程序自動輸出兩個重要信息：

1. 一個可執行的位元組碼。

2. 一個可以載入到 Coq 中的程序模型。

作為Coq的本機編程語言。由於Coq是一個完全通用的定理證明環境，因此可以與任何類型的人工編寫規範相關聯，除了安全性之外，也具備靈活性和兼容性。

圖為將 DeepSEA 語言寫到 EVM 編譯器中的例子：

與 Solidity 相比，DeepSEA 語言與 Move 類似，在程序模型上會有所限制。目前來看，在第一個版本中還未引用，所以開發團隊將會用與Move 使用相同的「樹狀結構儲存」結構（每個位置都可以在單個路徑下訪問），它具有與 Move 談及的相同的「驗證友好設計」。

DeepSEA系統的另一個主要優勢是其編譯器本身是由Coq編寫的，並已證明其正確性。這意味著它在基礎上就與其他的系統不同。我們可以確保高級語言的語義將會保留在位元組碼中。這與僅檢查輸出類型是否正確的 Move 不同，DeepSEA 檢查輸出的內容是否正確（它可以滿足 Coq 模型可證明的所有屬性）。

DeepSEA 的設計理念是為了提供一個高於其他語言能夠提供的保護層。在區塊鏈世界中，系統具有去中心化、可自我執行、永久、開源等特性，這讓哪怕是最微小的錯誤都有可能導致巨大且嚴重的問題。作為一個新時代的編程語言，DeepSEA 的開發團隊運用過去的經驗和知識，致力於為創造一個更加安全和可信賴的區塊鏈生態鋪路。

雖然 Move 語言比標準編程稍稍先進一些，提供了「驗證友好」的設計。但它仍舊需要創造額外的工具，這與繼承了形式化驗證語言本身的 DeepSEA 不同，DeepSEA 語言允許開發者在一個互動式輔助證明工具（Coq）的環境下開發自己的智能合約。

未來

綜上所述，我們發現在智能合約編程語言這個底層技術支撐中，不同的安全實現方式，將會給我們的應用帶來不同的安全保障。Solidity的動態靈活、應用廣泛卻安全性不夠；Move語言的安全性提升但是還沒有做到全方位的安全保障機制；DeepSEA 的安全機制相對領先，但是還沒有在足夠多的應用上使用。

隨著區塊鏈生態環境的不斷成熟，新的編程語言開始浮現，和過去幾年間所發生的安全問題相抗衡。Solidity 作為先行者，擁有了巨大的採用度和公眾熟悉度等優勢，Move 和 DeepSEA 等新語言也緊隨其後，取其精華，去其糟粕，學習其一路走來的經驗，避免歷史上的錯誤重演。

隨著這三個語言的先後問世，智能合約開發者擁有了更大程度的選擇自由的同時，在安全的前提下，未來的區塊鏈世界將會變得更加豐富多彩。這值得每一個人拭目以待。