除了Libra之外,你也該好好認識能有效確保安全的「Move語言」
安比(SECBIT)實驗室/作者:郭宇/張詠晴編譯
2019-06-20 17:45

 

Facebook 發起的加密貨幣項目 Libra 6月18日正式公開亮相。Libra 同步發布了多語言官網和白皮書,定位為面向數十億人的全球貨幣和金融服務基礎設施。Libra 還發布了多個技術白皮書,詳細介紹了其新開發的編程語言 Move 和共識協議 LibraBFT。Libra 原始碼已在 GitHub 開源,測試網路也已上線。目前設計為許可鏈(聯盟鏈),其聲稱當前非許可鏈(公鏈)不存在成熟的解決方案能夠支撐數十億人的使用需求,並表明將在發布五年內開始轉向非許可鏈的過渡工作。

 

Libra 的一系列發布中,新的編程語言 Move 尤為吸人眼球。第一時間看了 Move 的白皮書,嗯,這也許才是未來智慧合約語言該有的樣子。

 

First-class Resources 理念

 

First-class Resources 這個詞相當的學術,中文翻譯過來叫資源是一等公民,這究竟什麼意思呢?

 

所謂的編程語言的一等公民,就是編程語言在編程的時候,首要考慮的被編程對象。

 

那麼資源,Resources又是什麼呢? 這也是一個很學術的名字。Resources是和Value相對應的概念。Value 是可以隨意拷貝的,而 Resources 只能被消耗,不能被拷貝。Resources就像可樂,你喝了一瓶就少了一瓶,而Value,就好比寫在本子上的英文單詞,每天早上都可以念一遍,念完他不會消失,如果你記住了,那就在腦子裡拷貝了一份。不僅你可以念,我也可以念,你可以背,我也可以背。

 

傳統的編程語言,包括以太坊智慧合約語言中,對於數位資產的記帳是採用的 Value 方式,這會導致一個問題:記帳是有可能記錯的。事實上記錯帳的智慧合約相當得多,比如:張三向李四轉帳,李四的帳戶多了10塊錢,但是張三的帳戶餘額卻沒改。過去兩年裡的各種記帳漏洞甚至一度搞得大家已經對智慧合約的未來喪失了信心。

 

Move 合約採用了一種吸收了傳統理論「線性邏輯」的類型,叫做資源類型。數位資產可以用「資源類型」來定義,這樣一來,數位資產就像資源一樣,滿足線性邏輯中的一些特性:

 

  1. 數位資產不能被複製
  2. 數位資產不能憑空消失

 

First-class Resources 的真正含義是數位資產是一等公民,這句話可以引申出,Move 是為操作數位資產而生的智慧合約語言。從技術角度講,數位資產可以作為合約的變量,數位資產可以儲存,可以賦值,可以作為函數/過程的參數,也可以作為函數/過程的返回值。而 Move 的靜態類型系統使得智慧合約代碼能夠在編譯期,也就是部署前就可以透過編譯器檢查出絕大多數的資源使用錯誤。保證智慧合約不再像以前那樣的脆弱不堪。

 

摘用白皮書摘要中的一句話:

 

First-class resources are a very general concept that programmers can use not only to implement safe digital assets but also to write correct business logic for wrapping assets and enforcing access control policies.作為一等公民的資源是一種非常普遍的概念,工程師不僅可以用它實現安全的數位資產,同時也可以編寫正確的業務邏輯,實現正確的訪問控制策略。 

 

合約安全性設計

 

Move 合約在設計時,充分考慮了安全性。首先 Move 完全不支持動態指派(Dynamic Dispatch)。好,我這裡解釋下什麼是 Dynamic Dispatch,通俗地說,這是一種非常靈活的語言機制。在程式裡面是可以寫很多的函數,或者過程,或者子程式。然後一個主程式可以來調用這些函數/過程/子程式,來分別完成不同的功能。如果程式在運行之前,我們就能知道它到底都調用了哪個函數,或者以某種順序調用很多函數,那麼這些函數調用是「靜態」的,如果在運行之前,我們不清楚某一步的函數調用究竟是調用了哪一個函數,直到程式運行的時候,透過觀察,我們才能知道的話,那麼這個函數調用被稱為是「動態」的。「動態」顯然要比「靜態」靈活的多。

 

但是靈活也意味著更容易出問題。現代很多編程語言都或多或少支持動態指派,也就是從語言層面直接支持,比如面向對象語言中的「繼承」導致的「動態綁定」。動態特性是不利於程式的推理,更不利於形式化驗證(Formal verification),也更容易出安全問題。在以太坊智慧合約設計中就存在許多「動態特性」,比如支持函數指針做參數、合約做參數、delegatecall等等。而在 Move 語言中,完全不支持任何形式的「動態指派」或者「動態特性」,所有的合約執行路徑都能在編譯的時候確定,然後可以進行非常充分的分析、驗證。

 

Move 合約在運行前都會經過一個字節碼驗證器(Bytecode verifier)進行校驗,這個驗證器可以檢查出各種類型錯誤。同時字節碼在解釋執行的時候,仍然是帶著類型,一邊運行,一邊檢查。

 

Move 語言對合約可修改變量進行了非常嚴格的限制,並且從 Rust 語言那邊偷學了一些設計理念。保證任何時刻只能由一個指針對可修改變量進行修改,這樣不會造成混亂。以太坊 Solidity 裡面,可以定義很多的指針指向同一個變量,如果代碼邏輯沒考慮清楚,就會很容易出問題。

 

與以太坊EVM平台相比,Move 模塊系統不支持循環遞歸依賴,完美解決合約重入漏洞(Re-entrancy)。

 

本文為巴比特資訊授權刊登,原文標題為「Move語言:我眼中的 Libra 最大亮點