【得得白話】形式化驗證：被注入新靈魂的老技術
區塊鏈行業似乎已經變得波瀾不驚了。一邊是區塊鏈概念被越來越多的人所知曉，一邊是數字貨幣市場的轉涼。雖然潮水已經退去，但在這個過程中，區塊鏈領域也取得了一些實質性的進步。其中，形式化驗證（formal verification）的應用就是重要的一個。
兩年多前，2016年9月1日，萬向區塊鏈實驗室肖風在為區塊鏈行業名著《區塊鏈革命》作序時曾寫道：“The Dao”事件提醒我們，應該有一個能對智慧合約進行事先檢驗的科學方法，但這方面最先進的技術如形式化驗證，目前還處於理論研究階段。”
但如今，形式化驗證已經被正式用於智慧合約的安全審計中了。
形式化驗證：一套用數學寫的法律
談到形式化驗證首先要介紹一下形式化方法。
成都鏈安科技CEO楊霞曾打了個形象的比方，形式化方法就像一套完備的法律，規定了每個角色能做什麼和不能做什麼，並對角色之間的關係進行界定。類似於社會系統架構對不同角色進行分類，在承認個體天性的同時，使系統的複雜程度降低了多個維度。
形式化方法最大的特點就是簡化和抽象。形式化抽象可以從複雜的事物中抽離出本質，相當於一個精簡的解讀。舉個簡單的例子，一個構造複雜的中式涼亭，經過形式化的方法抽象過後，可能只是一個分層的三角形，但這種簡化又保留了本質的屬性和特徵。
形式化抽象過的涼亭
這樣看來，形式化方法最大的意義就是簡化事物，抽離本質。
而形式化驗證，則是用數學中的形式化方法對演算法的性質進行證明或證偽，也就是用形式化的程式碼給檢測出演算法正確與否。
形式化驗證的特性是通過數學或程式碼的形式制定規範，並對程式碼進行事先檢驗。
需要明確的是，形式化驗證是一種需要和特定領域結合來發揮價值的一種技術，並不能單獨發揮價值。形式化驗證並不是一個新技術，但它卻可以被不斷應用於很多新的領域，包括區塊鏈領域。
專門為系統安全級別高的領域服務，優於傳統技術測試
其實形式化驗證最開始是被從硬體開始應用的，IBM，AMD，ATMEL，STMicro等等硬體巨頭公司都是形式化方法的使用者。另外，軍工、航天等領域也廣泛應用形式化驗證。這些領域的特點都是對系統安全的要求非常高。
早在1994年，形式化驗證就被應用於一件硬體公司了，這個公司就是我們熟悉的Intel。
1994年，Intel在奔騰CPU的測試中發現漏洞（FDIV），但考慮到90億分之一的概率非常之小，奔騰CPU還是被投入了市場。但投入後發現，有不少使用者在使用過程中發現中央處理器都不能保證完全正確的運算，導致了使用者的恐慌，Intel不得不對奔騰CPU進行了回收。
那一次，Intel損失了47.5億美金的損失，從那以後，Intel開始廣泛使用形式化驗證對其硬體產品進行檢測，但慘痛的損失無法挽回。
不得不承認，形式化驗證比單純的技術測試的效果要好很多，原因主要在於，形式化驗證可以全面地檢驗系統是否正確，雖然需要更多的時間去建模和燃燒腦細胞。但技術測試一般只是在真實的環境下進行測試，並不能檢驗出所有的漏洞，漏洞觸發的機率也不能與大量投入使用的機率劃等號。
形式化驗證很適合智慧合約
目前，形式化驗證已經在區塊鏈領域有了一些落地的應用，主要集中在智慧合約的安全驗證上。
這也是因為，智慧合約安全同樣是一個對於系統安全要求非常高的領域,完美與否，在一定程度下，直接決定了人們在區塊鏈上的資產、資料和個人隱私是否安全。
據成都鏈安科技資料顯示，2011年至2018年，由智慧合約安全事件導致的經濟損失達12.4億美元。目前，由智慧合約安全事件導致的經濟損失已經超越交易所，位列第一。智慧合約上的一個小小的漏洞，都有可能使投資者的數字資產瞬間歸零，無論是The DAO，還是Parity都是如此。
而智慧合約又有一旦執行就不可更改的特性，這也就要求智慧合約在正是執行之前就保證相對“完美”，而達到這種相對“完美”，形式化驗證不失為一個好方法，結合人工檢測，可以大程度地搜查出漏洞。形式化驗證技術的優勢在於，用傳統的測試等手段無法窮舉所有可能輸入，但一旦用數學去驗證，整個問題就簡單多了。
形式化驗證通過數學建模方法對系統進行描述，開發者可以對程式的安全性事先進行審查，排除邏輯漏洞和安全漏洞，從而保證合約的安全，可以有效彌補傳統的僅靠人工經驗查詢程式碼邏輯漏洞的缺陷。
相對於傳統的網際網路安全公司的“讓Bug展現出來”的安全測試，形式化驗證直接從程式碼自身安全形度出發，防患於未然。而這種“預防”性質的檢測正與智慧合約的不可更改性相符合。
雖然前期建模過程複雜，需要大量的人力和時間，但對於使用者卻比較友好，因為模型是事先建好的，所以形式化驗證往往操作簡單，目前建立的SaaS平臺已經可以“一鍵”搜查智慧合約中的漏洞。
但形式化驗證也並不是完美的，在一般的情況下，形式化驗證可以檢測出80%的常規漏洞，但由於很多漏洞是結合業務邏輯的，因此人工符合還是必不可少。
形式化驗證雖是軍工級別，但是也不能為區塊鏈領域檢測出所有的漏洞，漏洞日新月異，不斷被挖出，只用不斷完善驗證模型，結合人工符合以及實況監測，才能最大程度地保證安全。
目前，Imandra、Certik、The Matrix、成都鏈安、Securify.ch、Runtime Verification、Tezos等區塊鏈領域的公司，都已經開展了智慧合約的形式化認證業務，它們通過建立了VaaS平臺、公鏈、以及系統語言將形式化驗證應用於區塊鏈領域。至此，形式化驗證這個被用於硬體、軍工、航空航天的老技術又被賦予了新的靈魂。
相信未來形式化驗證會被應用於更多的領域，為更多領域服務，也能更加完善，更加智慧。而區塊鏈行業在低谷的時候也能夠繼續鑽研技術，這樣才能更加穩健地發展。