作者 /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/
