2018年初，日本第二大虛擬貨幣在線交易所Coincheck遭受到黑客攻擊，該案當時被稱為“史上最大虛擬貨幣盜竊案”，據稱損失超620億日元（約合30多億元人民幣）！最近，區塊鏈成為炙手可熱的技術，但這個人人皆知的技術卻並沒有想象中那麼安全。而成都一家公司研發的全球首個“一鍵式”智能合約自動形式化驗證工具，可一鍵查驗代碼漏洞，其檢測準確率超過97%。
楊霞接受採訪
投入
從區塊鏈安全事件中嗅到商機
今年9月，鏈財經發布數據顯示，2011-2019年累計安全損失高達80多億美元，僅2019年1-8月份，由區塊鏈安全事件引起的損失便高達33 億美元。
區塊鏈安全事件爆發率逐年增高，案值也不斷增大。如今，國家已經將區塊鏈列為重點發展的技術之一，未來區塊鏈技術將有可能應用於供應鏈金融，政務系統，司法系統，物聯網等領域，區塊鏈系統的安全問題也將更加突出，區塊鏈安全更應給予足夠的重視。
“我們要看到區塊鏈發展的機遇，同樣也要重視區塊鏈的安全問題。”楊霞作為一名已經在安全行業幹了18年的專業人士，她對於區塊鏈的安全更為關注。
2016年，區塊鏈上出現首個智能合約安全漏洞，導致5200萬美元的損失。該事件觸動了楊霞，楊霞敏銳地感覺到，智能合約安全問題不解決未來將嚴重影響區塊鏈技術的發展，她同樣也在這之中嗅到商機，“當時全球都沒有多少企業在做區塊鏈安全。”
當年，楊霞便開始投入到區塊鏈安全的研究中來。“因為任何一個區塊鏈應用程序都將包含多個智能合約程序。於是，我開始嘗試將擅長的形式化驗證技術用來解決智能合約的安全。”楊霞說，通過兩年多的努力，最終在2018年6月，全球首個“一鍵式”智能合約自動形式化驗證工具在成都誕生。
研發
形式化驗證將可能問題進行窮舉
2018年3月，一家專門從事區塊鏈安全的企業成都鏈安科技有限公司在成都註冊，公司創始人正是楊霞。
公司在成立後不久，便推出了第一款針對區塊鏈的安全檢測工具Beosin-VaaS。據瞭解，Beosin-VaaS是全球首個同時支持微眾BCOS、ETH、EOS、Fabric、ONT等多個鏈平臺的“一鍵式”智能合約自動形式化驗證工具，該驗證工具首次實現了面向智能合約的自動代碼安全檢測，可精確定位風險代碼位置並給出修改建議，檢測準確率超過97%，全球已有2萬多開發者使用了VaaS平臺。
“這個驗證工具與我之前從事安全行業有很大關係，它就是基於形式化驗證技術研發出來的。”楊霞從面向航空航天領域的安全關鍵系統的安全到如今區塊鏈安全，在她看來並沒有本質區別，只不過區塊鏈的安全面臨的挑戰更大，形態更復雜，但其根本都是為系統做好安全防護工作。提高系統自身安全能力，建立完善的安全防禦體系，是她最擅長的。
什麼是形式化驗證技術呢？
“簡單來說，就是將各種可能出現的問題進行窮舉。”據楊霞介紹，形式化驗證技術產生於上世紀七八十年代，它主要針對測試不能窮舉的情況，運用數學的手段證明代碼的安全性和功能正確性。
“傳統檢測手段，無法把可能出現的情況一一列舉進行測試，而形式化驗證它是可以窮舉的，它通過數學的手段，對代碼建立數學模型，並證明是否存在任一可能的安全問題，最終儘可能讓區塊鏈系統的代碼沒有漏洞，以預防被黑客攻擊。”楊霞說，這種技術雖然已經存在幾十年，已經廣泛應用於航空、航天、軍事等安全關鍵領域。但就像人工智能一樣，面對新的應用領域，它仍有很大的發展空間。
專家提醒
區塊鏈不是萬能的
不必為了用而用
雖然有“一鍵式”驗證技術，但你以為，區塊鏈的安全問題僅僅是驗證一下代碼就可以完成的嗎？
區塊鏈安全風險貫穿始終。“以全球最知名的以太坊鏈平臺為例，其智能合約代碼具有不可更改性，一旦部署將無法修改。如果智能合約代碼一旦有漏洞，就只能眼睜睜看著被攻擊。”楊霞說，隨著區塊鏈應用進入我國國計民生相關的各個領域，而其關鍵程序智能合約存在漏洞將嚴重影響系統的運行，甚至導致項目失敗，鏈上資產和數據全部丟失。
在運營階段，黑客會通過DDoS攻擊、漏洞入侵等方式降低交易平臺的可用性，竊取賬戶，資產等。而若智能合約存在漏洞將嚴重影響整個項目，甚至導致項目失敗。在推廣時期除了網絡攻擊，平臺還可能遭受薅羊毛等業務欺詐、山寨仿冒等釣魚欺詐。
“目前，整個區塊鏈行業還處於開發階段，不確定因素較多，沒有必要為了用而用。”楊霞認為，區塊鏈適用於物流、保險、金融、法院、供應鏈等行業，並在一定程度上能大大促使這些行業的加速發展，但在一些不必要的行業，則有可能帶來更多的風險，造成更多的麻煩。
成都商報-紅星新聞記者 閆宇恆 嚴丹
攝影記者 呂國應
閱讀更多 成都全搜索新聞網 的文章
