近年來，隨著The DAO、Parity錢包、Coincheck等一系列區(qū)塊鏈平臺安全事件的頻繁爆發(fā)，區(qū)塊鏈平臺特別是智能合約的安全問題成為這項新技術向前發(fā)展的障礙。針對這一安全性問題，國內外研究學者一致認為，嚴格的形式化驗證方法能夠有效地提高區(qū)塊鏈生態(tài)系統(tǒng)的安全性。

為此，兼具中國“985工程”與“雙一流”稱號的電子科技大學信息與軟件工程學院楊霞副教授帶領一支區(qū)塊鏈形式化驗證團隊，經過近2年的研究和努力，研制出了一套高度自動化的區(qū)塊鏈形式化驗證平臺VaaS（Verification as a Service）。該團隊由20多名具有海外知名高校（如耶魯、UCLA）留學經歷的副教授、博士、碩士組成，具有多年的形式化驗證經驗。自2013年起，楊霞副教授所帶領的團隊也已經為航天、國防等領域的安全關鍵軟件提供了專業(yè)的形式化驗證服務。

VaaS形式化驗證平臺，采用了多種形式化驗證方法，具有驗證效率高、自動化程度高、人工參與度低、易于使用、支持多個合約開發(fā)語言、可支持大容量區(qū)塊鏈底層平臺的形式化驗證等優(yōu)點。VaaS提供了針對智能合約的形式化驗證工具，極大提高了智能合約的安全性與可靠性。產品通過對合約代碼進行嚴格的安全驗證，杜絕邏輯漏洞，確保合約安全，在滿足實際應用效率需求的同時，達到有效控制漏洞風險的目的。目前，VaaS平臺已支持主流區(qū)塊鏈平臺（如以太坊等）智能合約的形式化驗證，并且已與國內10多家區(qū)塊鏈行業(yè)的知名企業(yè)建立了合作關系。

近期，VaaS將重點專注于EOS區(qū)塊鏈平臺的形式化驗證工作，為EOS提供全面的形式化驗證服務，包括EOS智能合約的形式化驗證，EOS平臺底層軟件的形式化建模和驗證。未來，VaaS平臺將逐步支持其它主流區(qū)塊鏈平臺的形式化驗證工作，將為更多的區(qū)塊鏈平臺提供形式化驗證服務。

目前，楊霞副教授的團隊已經得到分布式資本的投資，并成立了成都鏈安科技有限公司。鏈安科技因此成為中國首個專門從事區(qū)塊鏈安全的團隊，也是分布式資本資助的唯一一個致力于區(qū)塊鏈平臺安全的公司。成都鏈安科技現(xiàn)正與LongHash、Cybex共同建立服務于EOS生態(tài)系統(tǒng)的形式化驗證社區(qū)，為EOS的安全運行保駕護航！

小科普——你知道什么是形式化驗證方法嗎？

所謂形式化驗證方法，即指在計算機科學領域，特別是軟件工程和硬件工程中，一種特殊的基于數(shù)學的技術，用于規(guī)范、開發(fā)和驗證軟件和硬件系統(tǒng)，以提高系統(tǒng)的安全性、可靠性和魯棒性。形式化方法可以形容為建立在相當廣泛的理論計算機科學基礎上的應用，特別是邏輯演算，形式語言、自動機理論、離散事件動態(tài)系統(tǒng)和程序的語義，還包括類型系統(tǒng)和代數(shù)數(shù)據(jù)類型等理論。一般這類研究主要應用于昂貴的航空、航天、軍事器材的操作系統(tǒng)、危險的醫(yī)療設備的程序之中。