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

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

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

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

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

小科普——你知道什么是形式化驗(yàn)證方法嗎？

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