除了 Staking,形式化驗證也是 Tezos 的技術亮點。

原文標題:《用 Python 進行 DeFi 應用的開發——不同的區塊鏈項目是如何解決安全問題的?
撰文:Justin Cai
本文由 LongHash 向鏈聞授權轉載

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

用 Python 也能開發 DeFi?簡析 Tezos 安全技術亮點

形式化驗證方法和 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 ),在安全領域擁有很好的口碑。常見過程式語言編寫的代碼,一般必須重新用函數式語言標記方能進行形式化驗證。

用 Python 也能開發 DeFi?簡析 Tezos 安全技術亮點

我們看到,在以上項目中,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 的主要區別是,

靜態類型

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

原子計算

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

明確的調用失敗

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

嚴格的語義

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

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

SmartPy 開發工具包

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

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

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

用 Python 也能開發 DeFi?簡析 Tezos 安全技術亮點

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

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

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

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

用 Python 也能開發 DeFi?簡析 Tezos 安全技術亮點
LongHash,用數據讀懂區塊鏈。
LongHash 立足於海量數據,透視區塊鏈行業,將繁雜的數據通過可視化圖表的方式呈現,從客觀的立場深入淺出地解讀數據背後的故事,幫助用戶加深對區塊鏈行業的瞭解,併爲用戶的投資提供及時、可靠的支持。

來源鏈接:www.longhash.com