隨著DAO系統、Parity錢包、Coincheck等區塊鏈安全問題的頻發，區塊鏈平臺特別是智能合約的安全問題成了這一新技術的發展障礙。為解決此問題，國內外的學者和研究者一致認為，嚴格的形式化驗證方法將有效提高區塊鏈生態系統的安全性。（科普下形式化驗證方法：在計算機科學領域，特別是軟件工程和硬件工程中，形式化方法是一種特殊的基於數學的技術，用於規範、開發和驗證軟件和硬件系統，以提高系統的安全性、可靠性和魯棒性。形式化方法可以形容為建立在相當廣泛的理論計算機科學基礎上的應用，特別是邏輯演算，形式語言、自動機理論、離散事件動態系統和程序的語義，還包括類型系統和代數數據類型等理論。一般這類研究主要應用於昂貴的航空、航天、軍事器材的操作系統、危險的醫療設備的程序之中。）
為此，中國具有“985”、“雙一流”雙重稱號的電子科技大學信息與軟件工程學院的楊霞副教授帶領的區塊鍊形式化驗證團隊，經過近2年的研究和努力，研製出了一套高度自動化的區塊鍊形式化驗證平臺VaaS（Verification as a Service）。該團隊由20多名具有海外知名高校（如耶魯、UCLA）留學經歷的副教授、博士、碩士組成，具有多年的形式化驗證經驗。該團隊自2013年起，為航天、國防等領域的安全關鍵軟件提供專業的形式化驗證服務。
VaaS形式化驗證平臺，採用了多種形式化驗證方法，具有驗證效率高、自動化程度高、人工參與度低、易於使用、支持多個合約開發語言、可支持大容量區塊鏈底層平臺的形式化驗證等優點。VaaS提供了針對智能合約的形式化驗證工具，極大提高了智能合約的安全性和可靠性。產品通過對合約代碼進行嚴格的安全驗證，杜絕邏輯漏洞，確保合約安全，在滿足實際應用效率需求的同時，達到有效控制漏洞風險的目的。目前，VaaS平臺已支持主流區塊鏈平臺（如以太坊等）智能合約形式化驗證，並且已與國內10多家區塊鏈行業的知名企業建立了合作關係。
近期，VaaS將重點專注於EOS區塊鏈平臺的形式化驗證工作，為EOS提供全面的形式化驗證服務，包括EOS智能合約的形式化驗證，EOS平臺底層軟件的形式化建模和驗證。未來，VaaS平臺將逐步支持其它主流區塊鏈平臺的形式化驗證工作，將為更多的區塊鏈平臺提供形式化驗證服務。
楊霞副教授的團隊已經得到分佈式資本的投資，併成立了成都鏈安科技有限公司。鏈安科技成為中國第一個專門從事區塊鏈安全的團隊，也是分佈式資本資助的唯一一個從事區塊鏈安全的公司。成都鏈安科技正在和LongHash，Cybex一起建立服務於EOS生態系統的形式化驗證社區，為EOS的安全運行保駕復航。
閱讀更多 鏈天下 的文章
