作者/ LongHash Justin Cai

來源/ LongHash

Tezos（特所思）作為著名的PoS 公鏈，其亮點並不僅僅只是Staking，Tezos 的形式化驗證特徵同樣也是其主要技術亮點之一。形式化驗證能讓DeFi 的安全性方面如虎添翼，讓用戶對資金的智能合約安全更加有信心。

形式化驗證方法和DeFi 安全

DeFi 的爆發式增長吸引了不少開發者，著名的DeFi 協議如Compound、Uniswap、Syntheix 累計收穫了上億美元的資金。但是，DeFi 存在一個重大漏洞：安全性。

這個漏洞的代價是昂貴的，它給一些區塊鏈項目（比如以太坊）的網絡效應帶來了負面的影響。過去幾個月被攻擊的DeFi 項目就包括Curve.fi、Lendf.Me、PegNet 等，其損失從數十萬美元到數千萬美元不等。 tBTC 在上線幾天后通過自查及時發現了bug 並凍結了存幣，避免了一場災難。

而對於注重安全性的DeFi 開發者來說，Tezos 的形式化驗證方案能夠在加強安全性的同時賦能DeFi 應用。

在傳統互聯網應用中，如果服務器被黑客攻擊，只需要對服務器端用戶數據進行回滾就可以挽回用戶損失。因此，重視用戶體驗的傳統互聯網應用可以以犧牲安全性換取速度和功能上的快速迭代。然而在DeFi 應用中，由於區塊鏈的不可篡改性，智能合約一旦上線並出現安全隱患，對用戶造成的損失是巨大且不可挽回的。

因此，DeFi 應用開發的過程需要用大量的測試和昂貴的審計以獲取足夠的安全性，而反過來會犧牲迭代的速度，影響了產品的易用性。並且，因為安全審計的價格昂貴，很多開發者並沒有能力發起DeFi 應用。

區塊鏈開發人員目前仍然是稀缺的，導致人工審計的成本非常高昂。因此越來越多地使用機器輔助驗證是目前的趨勢，而機器輔助審計中的形式化驗證方法更是確保安全性的不二法寶。

形式化驗證指的是用數學中的形式化方法對算法的性質進行證明或證偽，方法有兩種：

一種是模型檢驗，即把系統所有可能的狀態列出並進行一一檢驗，此種方法全自動化但只適合小型系統；

另一種是演繹驗證，首先把系統代碼標記成抽像數學模型，然後對定理進行證明，此種方法適合大型系統，但是首先需要人工將系統的運作方法轉換成驗證系統可以理解的語言。

形式化驗證方法在很長一段時間裡，由於其成本較高昂，主要應用於學術、國防軍工、航空航天等領域，在商業領域應用較少。由於傳統互聯網應用與區塊鏈應用的運行環境有著本質的不同，其開發流程也應當相應地進行調整，其中最關鍵點在於安全驗證環節的投入比例。

函數式語言在公鏈領域的應用

許多區塊鏈項目為了保證安全性，在底層架構、虛擬機或智能合約的語言方面，選擇了函數式語言，如Ocaml、Haskell、Erlang 等。函數式語言由於其嚴格的變量類型定義和編譯檢驗，以及擁有較好的形式化驗證工具鏈（比如CoQ ），在安全領域擁有很好的口碑。常見過程式語言編寫的代碼，一般必須重新用函數式語言標記方能進行形式化驗證。

我們看到，在以上項目中，Tezos 支持的智能合約高級語言的種類最豐富，不僅包括Pascal, Ocaml, Haskell 等多種函數式語言，也包括了Python 這一應用普遍的語言。而Cardano、Aeternity 都需要開發者學習一門新的函數式語言，使得開發門檻變得較高。

Michelson 語言的安全特性

在智能合約語言的設計上，Tezos 採用了一種取長補短的創新方案。 Tezos 的智能合約底層採用基於Ocaml 的Michelson 語言，而開發者實際接觸的是Python 等高級語言，並不需要了解Michelson 語言本身。如此以來，可以結合Michelson 語言更好的安全性與可審計性，與Python 等高級語言的易於編程性。

Michelson 在架構上對標的是以太坊EVM ，與EVM 相比其相似之處有

1）是一種stack 語言

2）使用鏈上存儲

3）採用gas 費用模型

4）圖靈完備

Michelson 與EVM 的主要區別是，

1）靜態類型

所有進入Michelson 智能合約的數據，都需要明確定義其類型。避免了跟類型不匹配有關的程序bug ，如浮點溢出、除以0 等。

2）原子計算

一個Michelson 智能合約必須完成執行後才能調用其它智能合約。這一點避免了以太坊上經常發生的re-entrancy 攻擊 (如著名的DAO 攻擊）。

3）明確的調用失敗

執行期發生的失敗只有三種，明確失敗（用FAILWITH 語句處理）、gas 耗盡、數量溢出。這一點避免了以太坊上常出現的隱含模代數、錯誤指令、stack 溢出等類型的常見執行期攻擊。

4）嚴格的語義

大小寫、空格、短行都有嚴格規範的要求，讓代碼審計變得更方便。

可以看到Michelson 相比EVM 在安全上有諸多的改進，可以更好地抵禦以太坊上經常出現的攻擊類型。

SmartPy 開發工具包

Tezos 上的Dapp 開發者並不需要掌握Michelson 語言。這是因為開發者可以使用基於Python 的SmartPy SDK ，並將Python 代碼寫的智能合約編譯成Michelson 語言。因此Dapp 開發者只需要會Python 就可以輕鬆上手。

SmartPy是一個Python 庫，而SmartPy.io 讓用戶能夠在一個瀏覽器中執行Python 腳本。 Smartpy 的官方網站提供了一個在線編輯器(https://smartpy.io/demo/)，Dapp 開發者可以直接用Python 編寫代碼並編譯成Michelson 智能合約，然後部署到Tezos 主網上。其使用界面設計相比以太坊的Remix 在線編輯器更簡潔明了，非常容易上手。 Smartpy 還自帶了一些現成的開發模版，方便開發者參考學習。

SmartPy.io 的界面如下。屏幕左側區域是代碼編寫區，開發者可以輕鬆地使用Python 來寫入並編輯合約的代碼。 Smartpy 不需要像Remix 一樣分兩步編譯和執行，按一下代碼區上方的執行按鈕就一步搞定，非常方便。執行結果立馬就可以在屏幕右側顯示出來，包括合約調用的入口、存儲狀態、編譯的Michelson 代碼等。

除了在線編輯器，SmartPy 還有一個命令行版本SmartPyBasic ，讓開發者在本地環境也可以編譯運行SmartPy 代碼。

部署的智能合約可以用SmartPy Contract Explorer 進行查看，合約的當前狀態和歷史操作都一覽無餘。

目前SmartPy 已經支持Python 常見的許多功能，如本地變量，變量類型判斷，Lambda 函數等。少數不支持的功能如array，可以用map 來代替。這也就意味著學習SmartPy 不需要投入很多的時間和精力，開發者可以專注於實現更好的功能。

以下是一些關於SmartPy 入門的訓練課程：

Cryptoverse Wars: https://cryptocodeschool.in/tezos/overview/

Blockmatics SmartPy Developer course: https://cryptocodeschool.in/tezos/overview/

最大化的投資收益就是在投資品種基本面未改變下，一路長期持有。