文| 常明星 編輯| 畢彤彤 來源| PANews
“條件漏洞、邏輯判斷錯誤、代幣授權錯誤、整型溢出漏洞、拒絕服務攻擊等數十個常見漏洞普遍存在於智能合約中。” Beosin （成都鏈安科技）的一份分析報告寫道，目前80%的智能合約存在安全問題。 而這些智能合約漏洞帶來的最直觀的危害就是經濟的莫名損失，包括造成代幣被盜、多次取款等。
2017年，多簽名錢包的智能合約被爆出現了一個極其簡單的漏洞，導致錢包被多次洗劫。第一次損失了3000萬美元，第二次損失了1.5億美金。今年四月，曾經高出美圖5倍市值的美圖關聯區塊鏈項目美鏈的代幣BEC也因智能合約漏洞，一夜被盜64億，市值幾近歸零。諸如此類的安全問題不勝枚舉，區塊鏈行業發展中的技術安全問題日益凸顯。
“區塊鏈行業想要真正站起來和走出去，時間和安全缺一不可。” Beosin聯合創始人兼CEO楊霞在接受PANews專訪時坦言。作為首家將形式化驗證技術運用到智能合約代碼安全檢測中的安全公司，楊霞帶領著Beosin團隊為區塊鏈的行業安全“保駕護航”。
形式化驗證：用數學模型來檢驗代碼
形式化驗證原本是比較小眾的驗證方式，通常被應用在軍事、航空航天等領域，對關鍵的系統進行安全驗證。楊霞表示， 形式化驗證並非很神秘，歸根結底，它也是計算機系統安全防護的一種最嚴格、有效的方法。
對智能合約進行形式化驗證時，首先會將智能合約的代碼轉換為數學公式，用數學的方式對代碼進行形式化的描述，這個過程叫做形式化建模。建模之後，則可靈活地根據客戶的需求，撰寫數學定理，然後證明代碼是否正確的滿足用戶定義的功能，從而確定智能合約代碼是否存在安全隱患，或者是否符合某些功能要求。
楊霞介紹到，Beosin （成都鏈安科技公司） 研發的VaaS自動形式化驗證平台，已經將形式化驗證的人工參與程度大幅度降低，一般的安全檢測能夠完全自動化完成，而對於一些非常複雜邏輯的代碼，人工參與度也僅有20%左右。 “目前對於常見的智能合約安全檢測已基本通過VaaS自動化檢測平台實現了全自動化，這樣做的優勢在於，一方面減少了人工操作帶來的失誤，提高了準確率，另一方面讓簡單的漏洞檢測變得更高效。” 她說。
自動化形式化驗證的過程是怎樣的？ 楊霞這樣描述，只需將要檢測的代碼導入到VaaS檢測工具中，然後點擊“開始檢測”，鏈安的VaaS自動化檢測工具就會將合約代碼中存在的漏洞以及其他問題“一網打盡”。
丟入代碼、運行代碼再到檢測出問題，這種對用戶來說及其方便的檢測程序，似乎與傳統意義上的代碼測試並無明顯區別。
對此，楊霞表示， 傳統的代碼測試只能檢驗出代碼中已表現出的漏洞，並且誤報率非常高；而形式化驗證是通過數學的角度證明代碼是否存在這些安全漏洞，更加嚴格和準確，同時藉助於部分人工參與還能檢測出智能合約代碼未表現出來的隱藏安全漏洞。 她補充說，形式化驗證還通過數學的方法為代碼構建了一種檢驗模型，因此VaaS的安全檢測的準確率可達到95%以上。
提到Beosin開發的VaaS智能合約自動形式化驗證平台，楊霞認為，Beosin作為國內首家將形式化驗證運用到智能合約漏洞檢測的公司，其開發的VaaS檢測平台憑藉高效、精準的性能“技壓群雄”。
在Beosin給出的一份VaaS平台與俄羅斯安全團隊研發的SmartDec智能合約安全審計工具、瑞士團隊研發的Securify以太坊智能合約形式化驗證漏洞掃描工具，以及美國Quantstamp團隊研發的QSP付費型自動化審計工具的《對比測試報告》中顯示， 無論是在產品的使用體驗，還是在代碼檢測的準確度（達到95%以上）和速度等方面，Beosin的VaaS平台都比同類產品要成熟和強大的多。
揭秘Beosin：兩位教授帶隊，成員90%為技術
Beosin在形式化驗證上的優勢，跟其創始陣容有著直接的關係。
創始人楊霞和郭文生分別為電子科技大學的博士後和博士，後留校任教，擔任副教授。 楊霞剛告訴PANews，她從事形式化驗證、內核安全、移動設備安全等技術的研究長達18年。並長期為航空、航天、軍事等行業提供形式化驗證的服務，還為微軟、華為、長虹等公司提供安全解決方案，主持了國家級重大安全類軟件課題近10項。 郭文生也同樣如此，他同樣在形式化驗證的領域沉浸10多年，發表過相關論文30多篇，申請的專利數也達10多項。
“我和郭教授雖都從事形式化驗證領域，但我們兩人所研究的路線不同”，楊霞補充說，“其實郭文生教授最開始比較感興趣的行業是人工智能，但我覺得區塊鏈行業對我們來說，潛力更大，於是我說服他一起創立了成都鏈安科技有限公司，將我們在形式化驗證研究的不同方法合為一體，從而研製出了同時支持ETH、EOS 、Fabric等多個區塊鏈平台的VaaS智能合約自動形式化驗證平台。並在短時間內就申請了4項專利”
2018年3月，發起成立鏈安科技其實是楊霞的第四次創業，作為一名連續創業者，她認為區塊鏈行業在未來的“不可限量”，而且，就現階段來說， 這個行業比其他任何行業都更需要優秀的安全技術。
楊霞及技術團隊與V神交流
發展至今，鏈安已擁有40餘人的團隊成員，其中90%都是專攻技術，並根據其業務範圍，分為面向行業應用的DApp開發組、安全審計組（包括鏈平台、錢包、dapp、合約等安全審計）和VaaS平台工具開發組等。除此之外，鏈安科技還與海外的一些資源建立了合作關係，包括美國Idaho大學終身教授，同是從事形式化驗證的Jim Alves-Foss和法國形式化驗證團隊等。
安全之後，看準應用開發落地
談到Beosin的未來規劃，楊霞表示，做技術的公司無論如何都要將研發安全技術產品放在首位。但未來Beosin的安全產品將面向整個區塊鏈生態，而不只是智能合約。
Beosin不僅在技術安全領域有著紮實的功底，其在區塊鏈技術開發方面也同樣“功力深厚”。
Beosin目前的業務除了智能合約安全審計、還包括錢包開發和審計、VaaS平台定制化開發、安全的Dapp開發與審計一條龍、安全的智能合約開發審計一條龍、交易所和公鏈平台安全檢測等全生態安全服務。
楊霞稱，未來Beosin發展的第一步，就是將其安全產品對應到區塊鏈生態的各個環節，而不止是專攻智能合約的安全檢測方面。第二步，就是讓區塊鏈技術被更多的企業所應用，做好區塊鏈落地應用的技術支持。
“Beosin會在未來開展一些面對行業技術落地應用的業務。因為Beosin接收到很多傳統企業想要接觸和應用區塊鏈技術的需求。但是很多企業雖然區塊鏈技術有很大的探索欲，但苦於沒有技術雄厚的公司來對接。” 楊霞也同樣憧憬這她帶領的Beosin團隊在區塊鏈應用落地方面，能有所作為。
