楊霞 | 成都鏈安科技CEO，創始人，電子科技大學副教授，最早研究區塊鍊形式化驗證的專家；一直為航空航天、軍事領域提供形式化驗證服務，主持國家核高基、裝發重大軟件課題等近10項國家課題；CC國際安全標準成員、CCF區塊鏈專委會委員。
騰訊安全日前發佈的報告顯示，與加密數字貨幣有關的黑客攻擊事件，從 2013年到2018年上半年增加了約五倍，全年預計增加10倍左右。其中，僅今年上半年，黑客對加密數字貨幣的攻擊，就已經造成了20億美元的直接損失。
基於區塊鏈加密數字貨幣引發的安全問題，來源於區塊鏈自身機制安全、生態安全和使用者安全三個方面。在區塊鏈自身機制安全方面，智能合約的安全性至關重要。
據鏈安方面的數據顯示，2011年至2018年，由智能合約安全事件導致的經濟損失達12.4億美元。目前，由智能合約安全事件導致的經濟損失已經超越交易所，位列第一。
智能合約作為執行合約條款的計算機交易協議，對所有用戶都開放，導致了內部存在的安全漏洞也隨之公開暴露在黑客面前。
而且，智能合約一旦上傳即公開且不可更改，因此現在的區塊鏈項目，對於安全性的需求更加迫切。因此，在智能合約正式開始運行之前進行安全審計就顯得尤為重要。
鏈安科技創始人兼CEO楊霞表示，從目前研究來看，80%的智能合約都存在安全漏洞。在合約開發前、開發過程中和編寫完成後，整個項目週期都要保證智能合約的安全性。
在合約開發前，開發者應進行智能合約相關漏洞風險知識學習，瞭解最新的智能合約安全漏洞，避免開發的合約中存在安全隱患。
在開發過程中，Remix-IDE、truffle等編譯工具會對合約中不符合最新規範的代碼提出告警，開發者需要對告警引起重視，強烈建議開發者更改自己的代碼，以消除編譯過程中的告警。
在合約編寫完成後，需要對合約功能的完整性和安全性進行測試，確保合約邏輯實現與設計相符，確保無安全風險；最後，可以尋找專業的智能合約審計團隊進行合約審計，最大程度地減少安全隱患。
智能合約形式化驗證應用狀況
2016年9月1日，萬向區塊鏈實驗室肖風在為《區塊鏈革命》作序時曾寫道：“The Dao”事件提醒我們，應該有一個能對智能合約進行事先檢驗的科學方法，但這方面最先進的技術如形式化驗證，目前還處於理論研究階段。”可是如今形式化驗證已經被正式用於智能合約的檢驗中了，這就是技術的進步。
形式化驗證指的是用數學中的形式化方法對算法的性質進行證明或證偽。
據瞭解，一般來講，方法有兩種：
一種是模型檢測，即把系統所有可能的狀態列出來並一一進行檢驗，此種方法是全自動化的，但是隻適合小型系統；
另一種是定理證明，即首先把系統代碼標記成抽象數學模型，然後對定理進行證明，此種方法適合大型系統，但是需要首先人工將系統的運作方法轉換成驗證系統可以理解的語言。
目前區塊鏈產業中與形式化驗證相關的產品可以分為三類: VaaS平臺，公鏈和語言。
目前，主要從事智能合約形式化認證的區塊鏈安全公司主要有7家，分別是成都鏈安科技、Imandra、Certik、The Matrix、Securify.ch、Runtime Verification和Tezos。其中，從事VaaS形式化驗證平臺研發的有四家，分別是：成都鏈安科技、Certik、Securify.ch和Runtime Verification。
其中，鏈安的特色在於：提供多個區塊鏈平臺驗證工具，而不是單一地為以太坊或者EOS提供智能合約形式化驗證。
楊霞是2016年才開始接觸區塊鏈的，正趕上了著名的以太坊The Dao事件，在此之前，楊霞老師一直專注於為航空航天、軍事領域提供形式化驗證服務。
“其實那個時候真的沒有太在意。不過我有一個朋友在搞區塊鏈，他跟我說你搞形式化驗證，能不能去驗證一下智能合約的安全，比如針對Dao系統的安全事件。”楊霞回憶道，“我覺得挺有趣的就去試了一下。那時候我們還沒有自動化的工具，只能靠人工進行代碼的形式化描述，然後去證明。最後發現，形式化驗證方法應用於智能合約安全審計效果不錯。”
也許當時選擇將形式化驗證應用於區塊鏈智能合約的審計是一個偶然的機遇，但是，通過楊霞和她的團隊經過一年半左右的潛心研究研發出了自動化的智能合約安全驗證平臺VaaS。
目前，鏈安的VaaS平臺支持EOS和以太坊的智能合約的安全審計，VaaS也是全球第一個支持EOS的智能合約驗證平臺。
形式化方法像一套完備的法律
被問到如何向技術小白解釋形式化認證，楊霞表示“形式化方法就像一套完備的法律，規定了每個角色能做什麼和不能做什麼，並對角色之間的關係進行界定。類似於社會系統架構對不同角色進行分類，在承認個體天性的同時，使系統的複雜程度降低了多個維度。”
形式化驗證通過數學建模的方式，對合約進行驗證，發現合約的未知的潛在的風險。
因為是用數學證明的方式去發現問題，所以首先需要一個函數的詳細功能規範，形式化驗證就依據這個功能規範去證明實際的代碼是不是和需求一致，如果是函數的規範足夠完整並且能夠清楚無歧義的表達，那麼是可以發現針對這個被驗證的函數之前沒有發現的問題。
形式化的抽象可以從複雜的事物中抽離出本質。舉個簡單的例子，一個構造複雜的中式涼亭，經過形式化的方法抽象過後，可能只是一個分層的三角形，這就相當於一個精簡的解讀。
在驗證安全之後，通過使用可執行模型，將較高級別的抽象模型轉換為較低級別的代碼。形式化方法使智能合約的生成和執行有了規範性約束，保證了合約的可信性，使智能合約的生產過程和執行效果得到了保障。
據楊霞表示，目前，理論上講，形式化認證可以找出所有已知的和未知的智能合約安全漏洞。而實際操作中，形式化工具可以查出80%的常規漏洞，對於部分結合業務邏輯的漏洞，還需要人工複核。
智能合約小白級漏洞居多
區塊鏈行業的安全漏洞是不斷湧現的，尤其是涉及到“錢”的安全漏洞，可以使人們的數字資產瞬時歸零。目前，隨著漏洞不斷被挖出，很多數字資產投資者也陷入到了恐慌之中。
楊霞老師表示，就智能合約來講，80%都存在安全問題。
就目前看來，智能合約中還是小白級的錯誤居多，包括一些造成鉅額財產損失的漏洞。
舉個例子，2018年4 月 22 日 13 時左右BEC智能合約被爆出的整數溢出漏洞，黑客能無限印幣，在一次交易中，也就那麼幾秒鐘的事情，黑客就“無中生有”地給兩個賬戶轉了天文數字般的BEC幣，而原賬戶一分BEC幣都沒損失。一行代碼就造成了60多億人民幣的損失。
整數溢出就像是水輪車。往裡面加水，加滿之後，繼續加水，水輪車將會失衡並轉動，此時水將會被全部倒出來，並重新盛水。當變量累加到超過自身容量範圍時，將會溢出，歸零。而黑客也是利用了這一點，把運算前的數值作為轉賬金額，把運算後溢出的0作為檢測條件，從而實現繞過。
這是一個很簡單的邏輯，但是後果卻很嚴重。
同樣，之前爆出來的以太坊平臺的漏洞，短地址攻擊，以及拒絕服務攻擊等等的漏洞的邏輯也都很簡單，但是這些漏洞都造成了人們數字資產的巨大損失。
其實，這些漏洞在智能合約正式開始運行之前，都是可以通過形式化驗證的方式找出來的，並加以修復的。
鏈安採用數學的證明方式將代碼形式化描述為公式，並對其進行邏輯漏洞和安全漏洞證明，基於此原理，實現了自動化的驗證工具，能夠方便、快速地驗證出代碼的功能正確性和安全屬性。
楊霞老師表示，目前，成都鏈安科技的優勢集中體現在三個方面：
第一，我們專注只做智能合約的安全。
第二，我們在技術上有優勢，我們採用了嚴格的形式化驗證的方法，為智能合約提供更加完備的安全審計。
第三，我們率先研發了自動化的智能合約安全驗證工具VaaS，在智能合約的審計過程中，我們通過自動化工具VaaS和人工結合的方法比全人工的安全審計方式更準確、更高效。
對於未來區塊鏈安全的走向，楊霞老師表示，安全是一個持續完善的過程，沒有絕對的安全，越是複雜的軟件系統，出現安全事件的概率越高。
為了避免安全事件的發生，最好的辦法就是提高軟件開發人員的安全意識，並對智能合約在部署之前進行全面的安全審計。
我們要理智地看待區塊鏈技術的漏洞，區塊鏈作為一個新興技術，出現安全事件是可以理解的，不能因噎廢食。
閱讀更多 財鏈社 的文章
