歷時一年的EOS眾籌終於在本月初圓滿落下帷幕，而這一年40億美金的ICO也成就了目前為止加密貨幣歷史上的又一之最——耗時最久，金額最大。隨之而來的就是對EOS的潛力果真能與如此鉅額估值相匹配的質疑，大眾對這一史上最大ICO區塊鏈項目的期待越高，爭議也就越大。巨大的融資金融以及追捧，迅速將EOS推向了風口浪尖，支持者與反對者各執一詞，EOS主網上線喜憂參半。
成都鏈安科技創始人:楊霞教授
區塊鏈鉛筆：回顧區塊鏈發展歷程，這項技術容易遭黑客攻擊的領域都有哪些？哪個方面又會是黑客攻擊的最主要目標？從您專業的角度來看，造成一系列安全事件以及黑客攻擊的主要原因又在哪裡？
楊教授：區塊鏈技術容易遭受黑客攻擊的包括區塊鏈底層平臺、區塊鏈智能合約兩個方面。而智能合約由於代碼小，複雜度較低，攻擊較方便，因此黑客攻擊的最主要目標為智能合約。造成這些的攻擊的主要原因在於這些程序自身存在安全漏洞或者邏輯漏洞。
區塊鏈鉛筆：區塊鏈的安全問題一直是所有人的心腹之患，每一次安全事件的發生都會造成幣市恐慌從而引發瀑布。而對於行業來說，每一次安全問題的暴露無疑是給區塊鏈技術發展的當頭一棒，究竟區塊鏈的安全問題是與生俱來不可攻克，還是採取適當的舉措可以解決？又有什麼樣的方式修復這些安全隱患？
楊教授：區塊鏈作為一個新興技術，出現安全事件是可以理解的。任何軟件系統都不可避免的存在bug或者安全漏洞，也就是說這些安全問題不只是存在於區塊鏈平臺中。但是由於區塊鏈平臺一旦出現安全問題將會帶來巨大的財產損失，從而造成幣市恐慌。這些安全問題是可以採取適當措施進行解決的，比如對在智能合約部署之前，對其進行嚴格的安全審計，是可以有效提高智能合約程序的安全性，提前預防安全隱患。我們的VaaS智能合約安全審計平臺，採用了形式化驗證方法和技術，並且率先實現了自動化檢測合約安全漏洞的工具。
區塊鏈鉛筆：最初是如何想到使用形式化驗證的方法來檢測智能合約漏洞的？
楊教授：形式化驗證作為一種大家公認的提高安全關鍵軟件功能正確性和安全性的一種有效手段，並且在軍事、航空、航天等安全關鍵系統中得到了應用。區塊鏈作為一個有著大量數字貨幣交易的平臺，其所面臨的安全問題及其帶來的嚴重後果不亞於軍事等安全關鍵系統。因此，基於我原來在形式化驗證方面的研究成果和經驗，我萌生了將二者結合的想法。
區塊鏈鉛筆：形式化驗證方法如何對智能合約的漏洞起到預防作用？採用形式化驗證又會對智能合約的安全性帶來多大的改善？
楊教授：在智能合約部署之前，對其代碼和文檔進行形式化建模，然後通過數學的手段對代碼的安全性和功能正確性進行嚴格的證明，可有效檢測出智能合約是否存在安全漏洞和邏輯漏洞，防止被黑客攻擊。該方法可以有效彌補傳統的靠人工經驗查找代碼邏輯漏洞的缺陷。如果每個智能合約在部署之前，都進行完備的形式化驗證，可極大提高其安全性，防止被攻擊，保護用戶財產。
區塊鏈鉛筆：您在兩年前就開始了使用形式化驗證檢查以太坊智能合約漏洞的研究，如今我們也看到了VaaS平臺的誕生，那麼到目前為止通過該平臺已幫助發現多少智能合約漏洞？
楊教授：自2016年下半年開始，我嘗試用形式化驗證的方法提高智能合約安全性，並且研製了第一個高度自動化的智能合約安全審計平臺VaaS（同時支持EOS和以太坊平臺），能夠快速定位到出現安全漏洞的代碼位置，並生成安全審計報告。該方法可以有效的為智能合約提供安全審計，提高其安全性。我們藉助於VaaS平臺，對以太坊平臺的100多個智能合約進行了安全審計，發現了RMC,UET 等合約存在嚴重的溢出類安全漏洞和邏輯漏洞。通過VaaS智能合約安全審計平臺可以對智能合約進行整型溢出審計、可重入攻擊審計、異常可達狀態審計、多簽名錢包審計、執行順序依賴審計、時間戳依賴審計、Tx.origin漏洞審計、拒絕服務攻擊審計等10多種常規安全漏洞和bugs進行“一鍵式”自動化檢查。這種自動化的智能合約審計方式，提高了檢查效率和準確度，再以人工方式對智能合約代碼逐行復核，保證審計質量。
區塊鏈鉛筆：形式化驗證是指根據某個或某些形式規範或屬性，使用數學推理來驗證設計意圖（指標）在實現(RTL)中是否得以貫徹的一種方法，那麼VaaS平臺是如何實現對智能合約各種屬性的檢查與驗證的呢？可以舉例說明一下嗎？
楊教授：VaaS平臺使用了已經廣泛應用於航空、航天、軍事等安全關鍵領域的形式化驗證技術，通過對合約文檔和和代碼進行形式化的建模，通過數學推理和證明的方式驗證智能合約的功能正確性和安全屬性。可以有效的發現代碼的邏輯漏洞和安全漏洞，彌補人工方式對邏輯漏洞查找的不足。以近期頻發的溢出類安全漏洞屬性檢查為例展示如何通過形式化驗證的手段對該漏洞進行檢測的過程：
如檢查代碼 int8 c=a+b是否存在溢出漏洞，下面展示對這行代碼的功能正確性和安全屬性的證明過程;
我們首先對整數類型建模，定義形式化規則“Int8.repr: Z -> int8”，該規則通過截取純數學整數（取值範圍從無窮小到無窮大）的低8位數值得到一個8位長度的機器整數。然後寫加法運算的形式化規範，如下：
{a:int8,b:int8}
// 設置代碼執行的前提條件，保證a和b的類型是8位有符號機器整數;
{c = a + b;} // 加法運算的源碼程序；
{(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
最後，根據前置條件證明代碼的執行是否滿足上述後置條件。如果產生一個不可證明結果，說明程序功能不正確，或者存在溢出安全漏洞。然後根據證明結果，對源程序進行分析修改，然後再重新證明，直到證明通過為止。
我們採用這種數學的證明方式將代碼形式化描述為公式，並對其屬性進行同樣對其他邏輯漏洞和安全漏洞進行證明，基於此原理，我們實現了自動化的驗證工具，能夠方便，快速的驗證出代碼的功能正確性和安全屬性。
區塊鏈鉛筆：隨著EOS主網啟動在即，EOS智能合約是否會像以太坊智能合約那樣出現一系列安全事件？有沒有辦法防患於未然？對此，VaaS又做了哪些努力？
楊教授：安全是一個持續完善的過程，沒有絕對的安全，越是複雜的軟件系統，出現安全事件的概率越高，所以不能保證EOS智能合約不會出現類似以太坊智能合約所面臨的安全事件。為了避免安全事件的發生，最好的辦法就是提高軟件開發人員的安全意識，並對智能合約在部署之前進行全面的安全審計。VaaS平臺正是為此應運而生的，VaaS專注於智能合約的安全保障，並且為EOS智能合約量身打造了一套自動化的安全審計工具，可以“一鍵式”自動化檢查出EOS合約常見的安全漏洞，事先為智能合約做好安全保障。
區塊鏈鉛筆：作為一個致力於EOS社區安全的形式化驗證平臺，針對前幾天360發現的EOS安全漏洞，可以談談您的看法嗎？VaaS對EOS未來可能會出現安全漏洞是否預先設想過解決方案或預防措施呢？
楊教授：區塊鏈安全的細分領域有很多：系統平臺級安全、區塊鏈平臺安全、智能合約安全、DAPP安全等，360發現的是EOS平臺的安全漏洞，我們目前主要專注於智能合約安全，未來也會關注區塊鏈平臺的安全問題。VaaS平臺對EOS未來可能會出現的安全漏洞已經做好了安全預防措施和解決方案，比如某些安全漏洞我們可以“一鍵式”自動檢查。
區塊鏈鉛筆：在EOS社區生態中，VaaS計劃扮演一種什麼樣的角色，如何發揮作用，促進生態發展？
楊教授：在EOS社區生態中，VaaS一直在努力使其智能合約更加安全，我們將會為上線的智能合約提供安全審計服務，盡最大努力幫助智能合約開發人員查抄安全漏洞和邏輯漏洞，提高智能合約的安全性。使其在部署之前發現並解決問題，避免合約上線後出現漏洞帶來重大損失。
區塊鏈鉛筆：從整個區塊鏈行業的角度來看，未來VaaS又有著什麼樣的規劃與佈局？
楊教授：目前區塊鏈行業處於百家爭鳴的態勢，因此未來我們將為更多的區塊鏈平臺提供從智能合約開發、安全審計等一條龍服務，盡我們最大努力為區塊鏈安全貢獻一份力量。
安全固然重要，但問題不是區塊鏈所獨有，也不是與生俱來不可攻克，若以一個安全問題就斷言未來，未免有些以偏概全。
目前，EOS主網上線的工作正在有條不紊地進行著，預計今晚21:00將舉行EOS全球會議投票決定是否開放主網。雖然EOS應用及生態的未來走向我們無法得知，但我們知道的是，當社區內的所有人都齊心協力，眾志成城的時候，力量就無比的強大。而有著形式化驗證為智能合約保駕護航，無疑是給EOS和以太坊又增加了一層保障。
閱讀更多 區塊鏈戀空 的文章
