那些被一行代碼蒸發1個億的智能合約，形式化驗證了解一下？

「人物誌」為區塊鏈大本營（ID：blockchain_camp）著力打造的人物欄目，以「趣味而不失專業，可讀而不失深度」為宗旨，每期邀請區塊鏈領域的頂級專家和開發者就行業、投融資、開發、案例、項目實踐等展開探討。

作為以太坊生態的核心，智能合約這幾年發展迅速。最早的智能合約，可以追溯到1995年，由密碼學家尼克薩博首次提出。智能合約在多方參與、複雜交易的場景中有明顯優勢。

然而，近期隨著智能合約安全問題的頻繁出現，智能合約的劣勢也愈發明顯，包括智能合約如何對實體資產進行控制，從而保證其有效地執行合約；以及如何保證代碼完全反應合約方的意志而不出現漏洞等。這些問題所引起的漏洞，使DAO、Parity、BEC等著名項目的市值幾乎一夜歸零。

再加上智能合約一旦上傳即公開且不可更改，因此現在的區塊鏈項目，對於安全性的需求更加迫切。

針對這些安全問題，成都鏈安科技嘗試將原本應用于軍工領域的「形式化驗證」方法，應用於智能合約安全審計。形式化驗證（formal verification）是基於數學建模方法對系統進行描述，通過形式化驗證，開發者可以對程序的安全性事先進行審查，排除邏輯漏洞和安全漏洞，從而保證合約的安全。

關於形式化驗證的更多細節，近日，我們採訪了鏈安科技創始人/CEO楊霞，就形式化驗證的現狀、原理以及市場情況作了深入探討。

以下是與楊霞對話實錄。

偶然打開的區塊鏈新世界大門

區塊鏈大本營：我了解到你的主要身份是電子科技大學的教授，在從事區塊鏈之前有怎樣的人生經歷？

楊霞：我從本科到研究生到博士，一直都在電子科技大學，而且是一路保送過來的，有人說我這是「坐飛機」（笑），之後就順理成章的留校當老師了。2012年9月開始做形式化驗證；2013年，我在美國一所大學的國際級安全實驗室以訪問學者身份工作和學習了一年。

我為什麼要做形式化驗證呢？原因在於，我之前一直研究嵌入式操作系統的安全保障技術，別人就問我你怎麼證明你的系統是安全的？是不是得找一個方法來證明？於是我開始探索對系統安全性和功能進行證明的方法，於是發現了形式化驗證方法。其實形式化驗證本來是一個很冷門的領域，受眾範圍也沒那麼廣，所以基本都是在高校和研究所里在研究。我也將此技術應用於航天、航空、軍事等領域的安全關鍵軟體中。

區塊鏈大本營：作為教師，從教育工作到一個區塊鏈企業的創業者，是出於怎樣的契機？

楊霞：我接觸區塊鏈是2016年著名的DAO系統安全事件，其實那個時候真的沒有太在意。不過我有一個朋友在搞區塊鏈，他跟我說你搞形式化驗證，能不能去驗證一下智能合約的安全，比如針對Dao系統的安全事件。我覺得挺有趣的就去試了一下。那時候我們還沒有自動化的工具，只能靠人工進行代碼的形式化描述，然後去證明。最後發現，形式化驗證方法應用於智能合約安全審計效果不錯。

然後我又找來了一個IBM的捐款智能合約（當時的合約不多），也驗證了一下，發現了一個「Unchecked Send返回值」的漏洞。所以我們當時覺得，在區塊鏈領域，形式化驗證是大有作為的。在去年9月，萬向組織的第三屆全球區塊鏈峰會上，主辦方邀請我做了一個「智能合約形式化驗證」的主題演講，當時引起了大家的關注。

不過那個時候，我們還沒有做自動化的工具，要靠人工來做。但人也會犯錯，我就想如何提高自動化的能力，減少人工參與度，並且兼容更多區塊鏈平台。這就是VaaS平台建立的原因。

區塊鏈大本營：請簡單介紹一下VaaS這個平台。

楊霞：VaaS（Verification as a Services）作為第一個同時支持EOS和以太坊區塊鏈的高度自動化形式化驗證平台，具有驗證效率高、自動化程度高、人工參與度低、易於使用、支持多個合約開發語言等優點。

主要用於對智能合約進行安全審計，通過對這種「軍事級」的安全驗證，以提高區塊鏈生態系統的安全性，同時，達到有效控制漏洞風險的目的。VaaS平台的「一鍵式」形式化驗證工具，可精確定位到有風險的代碼位置和風險原因，有效的驗證智能合約或區塊鏈應用的常規安全漏洞、安全屬性和功能正確性，從而提高其安全等級。相關研究成果已申請軟體發明專利5項。

揭秘形式化驗證技術

區塊鏈大本營：形式化驗證跟傳統互聯網安全公司的做法有什麼不同？

楊霞：傳統的互聯網安全公司是「以攻促防」，而我們是直接從代碼自身安全形度出發，來防止不安全事件發生。舉個例子，就像一個是西醫，有病的時候給你治病，而一個是中醫，強調自身抵抗力的提升，自己身體更健康了，就很難生病了。

區塊鏈大本營：形式化驗證的原理到底是什麼？

楊霞：形式化驗證是一種基於數學和邏輯學的方法。具體來講，在智能合約部署之前，對其代碼和文檔進行形式化建模，然後通過數學的手段對代碼的安全性和功能正確性進行嚴格的證明，可有效檢測出智能合約是否存在安全漏洞和邏輯漏洞。該方法可以有效彌補傳統的靠人工經驗查找代碼邏輯漏洞的缺陷。形式化驗證技術的優勢在於，用傳統的測試等手段無法窮舉所有可能輸入，而我們用數學證明的角度，就能克服這一問題。

區塊鏈大本營：能舉個例子進一步說明一下嗎？

楊霞：通過對合約文檔和和代碼進行形式化的建模，通過數學推理和證明的方式驗證智能合約的功能正確性和安全屬性。可以發現代碼的邏輯漏洞和安全漏洞，彌補人工方式對邏輯漏洞查找的不足。

以近期頻發的溢出類安全漏洞屬性檢查為例，如檢查代碼

int8 c=a+b

是否存在溢出漏洞，下面展示對這行代碼的功能正確性和安全屬性的證明過程。

首先，我們對整數類型建模，定義形式化規則：

Int8.repr: Z -> int8

該規則通過截取純數學整數（取值範圍從無窮小到無窮大）的低8位數值得到一個8位長度的機器整數。然後寫加法運算的形式化規範，如下：

//

設置代碼執行的前提條件，保證a和b的類型是8位有符號機器整數;

//

加法運算的源碼程序；

{(int8.repr(a+b)) / ((Int8.repr (a+b)) = (a+b))} ; //

設置代碼正確執行的後置條件。

其中，(int8.repr(a+b))描述，

是為了證明代碼的功能正確性是否滿足，即需要證明源代碼是對a和b進行求和而不是求差或任何其他運算邏輯，並且將運算結果轉換為int8類型。此外，需要對是否溢出的安全屬性進行證明，因此添加後置條件：

((Int8.repr (a+b)) = (a+b))

因為一旦

a+b>int8.max_singed或

a+b都將導致

(Int8.repr (a+b)) ≠ (a+b)。

最後，根據前置條件證明代碼的執行是否滿足上述後置條件。如果產生一個不可證明結果，說明程序功能不正確，或者存在溢出安全漏洞。然後根據證明結果，對源程序進行分析修改，然後再重新證明，直到證明通過為止。我們採用這種數學的證明方式將代碼形式化描述為公式，並對其屬性進行同樣對其他邏輯漏洞和安全漏洞進行證明，基於此原理，我們實現了自動化的驗證工具，能夠方便、快速地驗證出代碼的功能正確性和安全屬性。

巨頭來抄怎麼辦？不怕！

區塊鏈大本營：形式化驗證平台的競爭門檻是什麼？如何防止被巨頭抄襲？

楊霞：一個是門檻比較高，其他人想進來的話可能也不是短期就能進來的，在形式化驗證領域，需要有多年的積累。

另外，我認為行業不排斥更多人進來啊，大家在裡面都找到各自的位置，市場不是一家就能做完的，誰做的更好，誰做的更快，誰就能佔據更多的會場份額。我們已經研製了高度自動化的區塊鏈形式化驗證平台，申請多項專利，也跟知名企業開展了合作，例如比原鏈、布比、火幣等。我們對自己的產品有信心，只有高度自動化的智能合約安全審計才能保障審計的準確性和效率。

區塊鏈大本營：在這一領域，目前有哪些公司跟你們有競爭關係，區別在哪？

楊霞：目前國內還沒有採用形式化驗證的方法進行智能合約安全審計的，我們是第一家，因為我們起步較早。

區塊鏈大本營：你認為從技術角度來看，形式化驗證在國內外的差異是否存在？

楊霞：技術上來講，差別不大。中國人的優勢是做事很拼，整個區塊鏈領域，我們的技術發展程度跟國外的差異都不大。而在安全方面，我們這樣的公司瞄準的比國外更早，積累也更多。比如我們率先做出了同時支持以太坊和EOS的自動化合約審計工具。

區塊鏈大本營：在研發這套系統的過程中，你們遇到的最大的技術挑戰是什麼？你們是如何應對的？

楊霞：對於我們來講，最麻煩的就是區塊鏈的驗證跟傳統的操作系統等軟體的形式化驗證不一樣，區塊鏈存在的問題是，多個區塊鏈平台，而且存在於多種智能合約開發語言，甚至有的區塊鏈平台，提供多種合約開發語言。這是最大的挑戰。

關於應對，只能是一個坑一個坑的去填。雖然我們也做了一個中間的框架層，能更快速的對各個平台的支持，但還是有一些技術的工作要一個個去完成。比如換一個平台之後，要去跟平台適配，為了把我們的工具移植到更多的平台，還是有很多工作要去做。

開發者，別讓小白錯誤毀了大生意

區塊鏈大本營：在你們接手的項目中，比較典型的安全漏洞有哪些？

楊霞：目前看來，還是小白級的錯誤居多。比如BEC的那個溢出漏洞。還有就是之前爆出來的以太坊平台資深的漏洞，比如短地址攻擊，以及拒絕服務攻擊等。這些漏洞通過形式化驗證都能找出來。

區塊鏈大本營：既然平台都那麼不安全，我們該怎樣看待這些問題？

楊霞：安全是多方面的，智能合約就不說了，80%都有安全問題；還有DApp層面的，比如前段時間爆出的BiYong漏洞，用明文傳送用戶信息。剩下一個就是平台自身的安全漏洞了。

就像Windows系統一樣，用的人越多，爆出的漏洞越多，被補上的就越多，但其實背後意味著這個平台逐步變得更安全。就像以太坊，大家每天都在罵不安全，但大家都還在用。

區塊鏈大本營：下一步你們有哪些打算？

楊霞：下一步我們會建立技術社區，讓所有開發者共同來建立一個安全的區塊鏈生態，把它做得更好。同時，我們將支持更多的區塊鏈平台，解決更多的區塊鏈安全問題，為行業提供更多的安全服務。

區塊鏈大本營：最後一個問題，請以創業者的身份，對那些想要入門區塊鏈的人說幾句心裡話。

楊霞：其實我最想說的就是，大家要踏踏實實地靜下心來做點實事，戒驕戒躁。可能這感覺有點像老師在說教（笑）。區塊鏈是很有意思的一個技術，我將會堅定的把這條路走下去，因為我相信堅持做下去的人會取得最終的勝利！

了解更多區塊鏈技術及應用內容

敬請關註：

喜歡這篇文章嗎？立刻分享出去讓更多人知道吧！