鏈安科技楊霞:被用于導彈控制的形式化驗證,進軍區塊鏈安全區塊鏈
自2009年中本聰發布了《Bitcoin:A Peer-to-Peer -Eletronic System》論文后,區塊鏈的概念就逐漸在社會中普及開來。近年來隨著社會各界...
自2009年中本聰發布了《Bitcoin:A Peer-to-Peer -Eletronic System》論文后,區塊鏈的概念就逐漸在社會中普及開來。近年來隨著社會各界關注度的日益提高,區塊鏈技術的發展更是突飛猛進。
在早期,被稱為區塊鏈1.0的比特幣,它的代碼和結構體系是簡單的,這也是它能健康運行直到現在的重要原因。而隨著行業發展,越來越多的技術被運用于區塊鏈技術。不僅被稱為區塊鏈2.0的以太坊,區塊鏈3.0的EOS等主鏈依次上線,市面上種類繁多的項目更是讓人目不暇接。
野蠻生長雖然對區塊鏈技術的發展是一種好事,但與之相伴相生的區塊鏈安全問題也日益嚴重。
遠至以太坊DAO,mtgox被黑客攻擊,近至NiceHash事件,Tether黑客事件。各種對區塊鏈技術或者數字貨幣的安全漏洞事件層出不窮。根據區塊鏈安全公司CipherTrace報告,僅僅2018年上半年,黑客就竊取了價值7.31億美元的加密數字貨幣。
安全問題從來都是不可忽略的,每個行業的發展都需要一些專注于安全的公司。近日,耳朵財經(微信公眾號ID:erduocaijing)采訪了國內首家專注于區塊鏈安全的公司—鏈安科技。
很多時候,一個新興行業的發展需要來自其他成熟行業的支持,無論是技術也好、人才也好。
最近,區塊鏈圈內新出現了一家專注于智能合約安全的公司,叫做鏈安,它是國內首家專門從事區塊鏈安全的公司。由來自成都電子科技大學的楊霞教授和她的技術團隊所創立,目前已經與國內十多家區塊鏈行業的知名公司,如火幣、OKex、KuCoin等建立了長期的戰略合作。
鏈安科技的創始人楊霞,作為形式化驗證的專家,曾經為大型航空航天項目的形式化驗證服務,主持過國家核高基,裝發重大軟件等近10項國家重大課題,發表學術論文30多篇,申請20多項專利。
2016年以太坊發生了第一個安全漏洞事件。當時以太坊被爆出the DAO漏洞,這個漏洞使得攻擊者可以將theDAO資產池中的以太幣非法轉移給自己。楊霞在區塊鏈行業的一個朋友頓時想到了她在安全領域中建樹頗豐,認為如果楊教授如果能來做區塊鏈方面的安全研究一定能獲得一些成功。
“目前從數據上看,市面上起碼80%的智能合約都或多或少存在著安全問題”,楊霞說“往往幾行代碼的錯誤就會造成數十億的損失,這帶來的教訓是十分慘痛的”。
楊霞對區塊鏈技術當前的安全性是不滿意的。
于是從2016年下半年開始,那么為了保證區塊鏈代碼的安全,楊霞就聽從了朋友的建議。開始了對區塊鏈的研究,將自己在形式化驗證方面的成果,運用到了區塊鏈方面。
這種形式化驗證,相較傳統審計代碼方法,具有更高效,更安全的特點。它本身主要用于航空航天,軍事安全等領域中,之前更多的實際應用是導彈控制,戰斗機導航等對安全性和正確性要求比較高的系統之中。
形式化驗證,簡單的說,就是用數學工具進行驗證的方法,把代碼編成數學模型,從設計到實現整個流程,通過證明手段來證明代碼是完備安全的,能夠滿足期待。
因此,將它運用在區塊鏈智能合約中是非常合適的。這種先進的科技理念和技術指導,是其他行業對區塊鏈發展的強大動力。
眾所周知,和傳統的互聯網技術不同,智能合約一旦寫定上鏈后,后續出現問題則是無法更改的。這是區塊鏈技術的特點也是對區塊鏈安全技術發展的挑戰。
這對代碼的測試就有了很高的要求,在楊霞看來,和傳統測試不同的是,區塊鏈項目的測試需要的科技含量更高。傳統測試無論是白盒測試、黑盒測試,往往都需要窮盡bug。而限于人力,測試往往不能覆蓋所有可能產生的問題,這種測試方式在區塊鏈行業是很容易忽略致命的漏洞,一旦漏洞出現,又無法修復,帶來的損失將會是巨大的。
針對智能合約的安全問題,鏈安科技研發的VaaS平臺,采用了形式化驗證的形式,用數學的手段來證明代碼,給智能合約提供軍事化級別的安全保護,杜絕邏輯漏洞和安全漏洞,確保系統安全性。
“減少人工干預,更多的工作被機器完成”也是智能合約安全需要被強調的。
VaaS所提供的服務,具有快速支持多平臺的能力,近期VaaS的重點雖然是專注于為EOS提供全面的形式化驗證服務,但是未來,VaaS平臺也將逐步支持其他主流區塊鏈平臺的形式化驗證工作。
在聊到區塊鏈這個大行業整體的當前的創業氛圍時,楊霞認為,雖然現在有不少人借用區塊鏈技術來作惡,但這是一個社會問題。無論哪種技術在發展的時候都是無法避免的。區塊鏈本身依然是一個很偉大的創新。
比如最近風靡的某個區塊鏈游戲,在楊霞看來,這種類型的傳銷游戲并不是一種好的現象,對區塊鏈的發展不會起到促進的作用。雖然它的本意是諷刺目前幣圈的一些騙局。但是大家在看到它火了之后反而去爭相模仿,這在信息傳播急速的現代社會是會產生不良影響的項目。
當然除了這些利用人性,利用區塊鏈為噱頭的騙局之外,在區塊鏈基礎之上的一些技術的發展可以對整個行業是會起到促進作用,鏈安科技所提供的智能合約審計服務就是其中一個典范。
隨著各種規范的完善,代碼錯誤率降低,程序的漏洞減少,黑客攻擊的成本增加難度加大。數字貨幣的價值最終也會越來越穩定,市場也會越來越成熟。
但這都是依靠在越來越多像鏈安這樣,從技術服務角度,為區塊鏈產業的發展貢獻出自己一份力量的基礎上。
1.TMT觀察網遵循行業規范,任何轉載的稿件都會明確標注作者和來源;
2.TMT觀察網的原創文章,請轉載時務必注明文章作者和"來源:TMT觀察網",不尊重原創的行為TMT觀察網或將追究責任;
3.作者投稿可能會經TMT觀察網編輯修改或補充。