VaaS平臺已支持區(qū)塊鏈平臺智能合約的形式化驗(yàn)證

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

為此，兼具中國“985工程”與“雙一流”稱號的電子科技大學(xué)信息與軟件工程學(xué)院楊霞副教授帶領(lǐng)一支區(qū)塊鏈形式化驗(yàn)證團(tuán)隊(duì)，經(jīng)過近2年的研究和努力，研制出了一套高度自動化的區(qū)塊鏈形式化驗(yàn)證平臺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)為航天、國防等領(lǐng)域的安全關(guān)鍵軟件提供了專業(yè)的形式化驗(yàn)證服務(wù)。

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

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

目前，楊霞副教授的團(tuán)隊(duì)已經(jīng)得到分布式資本的投資，并成立了成都鏈安科技有限公司。鏈安科技因此成為中國首個專門從事區(qū)塊鏈安全的團(tuán)隊(duì)，也是分布式資本資助的唯一一個致力于區(qū)塊鏈平臺安全的公司。成都鏈安科技現(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ī)范、開發(fā)和驗(yàn)證軟件和硬件系統(tǒng)，以提高系統(tǒng)的安全性、可靠性和魯棒性。形式化方法可以形容為建立在相當(dāng)廣泛的理論計(jì)算機(jī)科學(xué)基礎(chǔ)上的應(yīng)用，特別是邏輯演算，形式語言、自動機(jī)理論、離散事件動態(tài)系統(tǒng)和程序的語義，還包括類型系統(tǒng)和代數(shù)數(shù)據(jù)類型等理論。一般這類研究主要應(yīng)用于昂貴的航空、航天、軍事器材的操作系統(tǒng)、危險(xiǎn)的醫(yī)療設(shè)備的程序之中。