曾獲DARPA採用、融資近3000萬美元,這個中國團隊正在為區塊鏈行業建立安全標準

DeepTech深科技2019-04-17 22:09:08


你相信天底下有保證絕無漏洞的代碼嗎?你相信有一種方式可以保證讓人寫出這樣無漏洞的代碼嗎?這件事聽起來似乎太不真實,但一個由來自耶魯和哥大背景的中國團隊 CertiK,正在嘗試推出這樣的安全驗證服務,要為黑客事件頻發的區塊鏈行業,建立起安全標準。

 

CertiK 是由耶魯大學計算機系主任邵中與哥倫比亞大學計算機系教授顧榮輝聯合創立,2017 年底正式成立於紐約及硅谷,核心技術為運用形式化驗證(formal verification),為智能合約和區塊鏈應用提供安全驗證和生態安全解決方案。

 

圖|CertiK 聯合創始人顧榮輝(來源:DeepTech)

 

2018 年全球區塊鏈領域安全事件暴增 5~8 倍

 

目前,區塊鏈堪稱是風險最高、最容易發生黑客攻擊、且行業安全意識又最低的領域之一。根據不同統計,2018 年全球區塊鏈領域發生至少百起安全事件,與 2017 年相比暴增 5~8 倍。而損失總金額達 20~38 億美元之間,對比目前全球加密貨幣總市值也不過約 1700 億美元左右,這樣的安全損失比例實在高得嚇人。

 

區塊鏈的安全攻擊形式層出不窮,分層來看,從數據層、網絡層、共識層、激勵層、合約層,到應用層,都可以成為攻擊切入的途徑。其中,又以應用層攻擊最多,智能合約更被認為是區塊鏈安全事件的重災區,最經典的案例就是 2016 年“The DAO”事件,黑客利用去中心化風險投資基金“The DAO”的智能合約漏洞,盜走 360 萬枚以太幣(當時價值約 5000 萬美元),最後迫使整個以太坊採取激進的防衞措施創建硬分叉,才能挽回損失。

 

而 CertiK 截至目前,已累計為 150 家以上客户提供了安全驗證服務,其中許多是加密資產相關平台,保護了總值近 13 億美元的數字資產免受到黑客攻擊,並保持着“零事故率”的記錄。

 

其客户包含幣安、火幣、OKEX、比特大陸、以太坊基金會、量子鏈等加密貨幣與區塊鏈行業知名公司。去年 10 月,CertiK 獲得幣安旗下投資機構——幣安孵化器 Binance Labs 數百萬美元的投資。幣安孵化器 CEO 張靈(Ella Zhang)説,CertiK“解決了當今區塊鏈生態中一個關鍵痛點,也同時保護我們的交易用户,正在逐步成為交易上幣的行業標準。

 

圖|CertiK 成立一年多成績不斐(來源:CertiK)

  

而 CertiK 的可保證代碼無漏洞的安全驗證服務,其核心技術其實就是兩位聯合創始人紹中和顧榮輝,將他們在“形式化驗證”(formal verification)領域的多年研究成果,打造成 CertiKOS 防黑客操作系統,這套系統在 2016 年就曾被美國國防高級研究計劃局(DARPA)資助的”高保證網絡軍事系統(HACMS)”採用,成為該系統核心構件之一。

 

形式化驗證,讓人寫出無漏洞代碼

 

何謂形式化驗證技術?真能讓人寫出無漏洞代碼?

 

簡而言之,形式化驗證是通過數學邏輯來推理演算,從數學的角度證明一段程序、一個軟件、或一個智能合約,不存在安全漏洞。每一個證明在邏輯上都承接上一個證明。通過形式化驗證,一個這樣的程序可以像證明數學定理一樣,無論如何測試都一定會得到正確的結果。

 

顧榮輝對 DeepTech 解釋,一般安全技術通常都是設法找出可能存在的漏洞,或是在概率上保證很大程度不會出錯,但形式化驗證是希望能夠從數學上直接證明一個軟件是正確的,“是目前已知的安全等級最高的一項技術”。

 

也就是説,通過形式化驗證,在某種程度上可以保證能讓人寫出沒有漏洞的代碼。

 

“當然,這是建立在數學模型正確性的基礎上,必須依賴很多的前提和假設”,顧榮輝補充,“但如果其前提條件可以被滿足,那麼最終它能達到安全等級是高於其它技術的。

 

形式化驗證其實是從 20 世紀 60、70 年代就開始興起的研究方向,但由於對應用條件要求較高,無法處理較為複雜的軟件系統,在大多數實際案例中,形式化證明的完全實現是非常困難的。因此形式化證明一直處於技術上突破有限、也苦於找不到理想應用領域的狀態。直到 2015 年左右,紹中和顧榮輝將在形式化驗證領域多年積累研究成果,具體研發成深度規範、分層結構等技術,才得到了比較大的突破。

 

話雖如此,形式化驗證所適合應用的場景,仍偏向於代碼不是太過複雜、條件相對單純、但卻價值很高的程序。而區塊鏈正好符合這些特點,因為區塊鏈往往是用相對有限的代碼數量來對應高價值加密資產,且鏈上條件相對可控。更重要的是,因區塊鏈不可篡改,代碼漏洞修補困難,就更適合形式化驗證這樣的技術。

 

正因如此,適逢 2017 年比特幣大漲帶動區塊鏈技術發展,CertiK 快速在這一行業找到落點,推出形式化驗證平台,為包括智能合約、DApps 等所有區塊鏈生態系統組件提供安全審計服務。

 

簡單來説,CertiK 的服務是通過分層結構,對所要驗證的某個複雜系統先進行分層,將軟件模塊拆分,然後再用深度規範進行復合證明,驗證每一分層是否都符合規範。如此一來,便可同時提升安全驗證的彈性和效率,將形式化驗證應用在具體業務場景。

 

以某個穩定幣客户為例,CertiK 為其智能合約所做的是,先用標籤的形式寫下合約的規範,然後將複雜的智能合約拆分為較小的可驗證模塊,在不同的抽象層進行證明。最後再將經過證明的模塊合併起來,生成整個合約正確性的證書。

 

圖|運用深度規範保護智能合約(來源:CertiK

針對智能合約的編程語言 DeepSEA


顧榮輝分析,區塊鏈行業之所以安全事件高度頻發,一方面是因為行業安全意識普遍低落、且對安全技術缺乏認識,許多區塊鏈項目或平台並未將安全放在優先考量,不願意投資安全建設。而即便是重視安全者,也不知該如何選擇,可能付出高額費用,但是得到的安全加持非常有限。

 

另一方面,問題也出在區塊鏈行業慣用的開發工具上。顧榮輝指出,現在區塊鏈行業程序員普遍愛用 C++ 或 Python 來寫智能合約,但這些工具從安全專業的角度來看,都是非常不安全的語言。尤其是 Python,天生就不適合用來開發對安全需求很高的系統。

 

“不同的語言就像工具一樣,有不同的使用的方法,這就好像你用一個螺絲刀當鉗子來使。”顧榮輝認為,如果整個行業大量依賴這些語言來從事開發,那麼安全檢測與驗證相當於只是亡羊補牢。

 

因此,CertiK 近來推出一項新的編程語言 DeepSEA,這是一種針對智能合約的函數式智能合約編程語言,通過引入形式化驗證技術,保證智能合約的安全性。

 

據顧榮輝解釋,DeepSEA 可以説是一種“無漏洞的編譯器”,可以證明源代碼無漏洞,通過 DeepSEA-Blockchain 框架可以構建出跨平台的、可信賴的智能合約,目標是為 Hyperledger、EVM 等平台上的開發者提供一個安全可信賴的開發環境。

 

“我們的出發點是希望在源代碼級別,從語言設計上引入安全的設計理念,可以在比較早期就杜絕一些很簡單的安全錯誤”,顧榮輝説。

 

DeepSEA 推出以來,幾個月內已陸續獲得哥倫比亞-IBM 區塊鏈中心的種子基金、以太坊基金會(Ethereum Foundation)第五批科研獎金,以及量子鏈(Qtum)科研經費等。

 

圖|CertiK 團隊(來源:DeepTech

此外,顧榮輝告訴 DeepTech,正式成立剛滿一年不久的 CertiK,也已陸續融資約 3000 萬美元。在資金支持下,CertiK 團隊規模已成長至 20 餘人,包括曾是谷歌 gVisor 創始人員的研發副總裁倪兆中和曾任職國際貨幣基金組織(IMF)經濟學家的首席商務官閻開,團隊分散在紐約、西雅圖、北京、首爾等地,並將在今年持續完成更大規模擴張。

 

蜂擁而至的獎助與投資,凸顯出區塊鏈行業對於可信賴、標準化的安全建設存在迫切需求。目前,加密資產的安全環境仍然十分脆弱,如果包含 CertiK 在內的區塊鏈安全服務提供商,能夠成功使其產品被行業廣為接受,也將有望從根本上改變區塊鏈產業的生態。

 

-End-


https://hk.wxwenku.com/d/200173015