區塊鏈時代,智能合約的安全性被無限放大,一行代碼的漏洞就能導致千萬美元的損失。統計數據顯示,2011 年-2018 年間,智能合約安全事件損失金額達 12.4 億美元,佔該期間區塊鏈安全事件總損失金額的 1/3。

2018 年 3 月,一家想要保證智能合約 100% 正確的安全服務公司「Beosin 成都鏈安」,攜帶一種被應用在軍事、航空航天等領域的小衆、高門檻的驗證方式「形式化驗證」殺入區塊鏈領域。Beosin 成都鏈安創始人楊霞表示,形式化驗證並非很神祕,歸根結底,它是利用數學之美爲計算機系統做安全防護的一種嚴格、有效的方法。

如今 Beosin 成都鏈安正式迎來了它的一週歲,針對智能合約的安全問題,Beosin 成都鏈安成功研發了全球首個同時支持 ETH、EOS、Fabric、TRON 等多個區塊鏈平臺的高度自動化智能合約形式化驗證平臺,實現了「一鍵式」的形式化驗證,用數學的手段證明代碼,給智能合約提供軍事化級別的安全保護。

Beosin 成都鏈安是楊霞的第四次創業,作爲一名連續創業者,她對區塊鏈行業的未來和安全需求表達了充分的信心:「區塊鏈跟其他互聯網產業不一樣,它的安全需求更大,而且它更剛需,無論是鏈上交易也罷,數字資產也罷,用戶數據也罷,這些都不能出現安全問題,如果出現問題後果是非常嚴重的。」

Beosin 成都鏈安一週歲:利用數學之美,讓區塊鏈世界更健壯Beosin 成都鏈安創始人楊霞

在 Beosin 成都鏈安成立一週年之際,楊霞接受了鏈聞的專訪,分享了她對區塊鏈安全和形式化驗證的深度觀察和思考。以下是本次採訪實錄:

Q = 鏈聞 ChainNews
A = 楊霞,Beosin 成都鏈安聯合創始人,電子科技大學副教授

Q:您從何時開始關注到區塊鏈,能否講一講你深入區塊鏈領域的過程?

A:對區塊鏈這個概念的瞭解,是來源於我身邊的一些朋友,他們有人從 14 年、15 年就開始在區塊鏈領域工作,也給陸續我講區塊鏈方面的知識和動態。但是我當時還沒有真正的把目標轉向區塊鏈,因爲我本來一直在安全領域做研究,所以我更關注的是安全。16 年的時候,以太坊 The DAO 系統安全漏洞的的發生直接導致了 7000 萬美元的損失,可以說是這個漏洞把我的目光吸引過來。

從那個時候開始我思考能否嘗試用形式化驗證的方法避免這些漏洞的發生,尤其是我之前一直給軍事等比較關鍵的領域做形式化驗證,對於形式化驗證有足夠的信賴。因爲 The DAO 的安全事件讓我感覺到在區塊鏈領域安全問題非常大,一次漏洞就丟那麼多錢,說明風險太高。作爲安全領域的從業者和研究者,我需要不斷的找尋新的對安全有需求的領域進行探索,所以我是從 16 年開始,真正深入區塊鏈安全領域進行實踐。

注:The DAO 事件是區塊鏈歷史上的著名事件,由於智能合約的漏洞造成資金被黑客轉移。2016 年 5 月初,以太坊社區的一些成員宣佈了「The DAO」的誕生。它是作爲以太坊區塊鏈上的一種智能合約而被建造的。編碼框架是由 Slock 開源開發的。 2016 年 6 月 17 日,一名黑客在編碼上發現了漏洞,使得他可以從 The Dao 上抽走資金。在攻擊的頭幾個小時,360 萬的以太被轉出,在當時價值相當於七千萬美元。

Q:能否分享一下成立 Beosin 成都鏈安的過程?初衷和願景是什麼?

A:成立 Beosin 成都鏈安的過程是進行了很多探索的,在形式化驗證這個領域創業是一個很艱難的事,它是比較冷門、門檻比較高、比較小衆的一個領域。因爲門檻高,所以形式化驗證對於傳統互聯網的安全,實際上發展空間並不大。但是在軍事這些非常關鍵的領域,形式化驗證已經被頻繁的應用。所以對我而言,我首要思考的是從原來的應用領域,把應用的目標轉向區塊鏈,我當時第一個要考慮的問題就是用形式化驗證的方法能在區塊鏈領域做什麼,然後是怎麼做?

(鏈聞注:形式化驗證即是用數學和邏輯學的方法對代碼的安全屬性進行證明或證僞,通過判斷代碼問題,從而證明這個代碼的實現是否能滿足用戶需求。這種方法相較傳統審計代碼方法具有更高效、更安全的特點,多用於對安全係數要求較高的航空、航天等關鍵領域。)

當時可選擇的區塊鏈網絡不多,基於對這個問題的思考,我們就在以太坊上面,對以太坊的智能合約進行形式化驗證的嘗試。當時智能合約同樣也不多,我記得很清楚,我們當時找了一個 IBM 官方的捐贈合約,然後用人工的方法對其進行形式化的描述,而後進行形式化的建模,進而去證明整個流程。當時通過這份合約的形式化驗證,我們的確發現了以太坊有一個機制漏洞——send 函數沒有返回值(「unchecked-send」bug)。如果用戶習慣不好,實際上這是不安全的。這算是我們通過形式化驗證發現以太坊智能合約的第一個安全問題,也證明這個方法是有效的。

Beosin 成都鏈安一週歲:利用數學之美,讓區塊鏈世界更健壯Beosin 成都鏈安技術團隊與 Vitalik 就形式化驗證進行交流

但是這個過程中有一個問題,驗證這樣一個幾百行代碼的合約,我們就花了一週多的時間。 這說明通過用人工的方式去做效率太低了。通過人工建模,然後再去發現問題,這個過程太費時間,用這種方法做產業化服務顯然是不行的,得儘可能提高它的自動化能力。因爲我們先嚐試的是通過人工進行形式化的建模,那麼我當時就想能不能不用人工建模,而製作一個工具自動對代碼進行建模,進而轉換成形式化的語言描述,證明部分再用人工參與。

確定了這個方向,我們就朝這個目標走,也就是半自動化的目標。到目前爲止,我們已經經歷了從全人工化到半自動化到現在大部分自動化的三個階段,當半自動化功能出來之後,其實我們大部分的產品原型也陸續完備,時間也就到了 2017 年底,完成這些準備之後,分佈式資本對我們進行了投資,2018 年 3 月正式成立了 Beosin 成都鏈安。

Q:獲得投資的過程順利嗎?能否介紹一下 Beosin 成都鏈安的創始團隊,國內是否對標的項目和團隊?

A:很順利,實際上在 17 年 9 月份的時候,萬向組織了第三屆區塊鏈全球峯會,當時峯會邀請我去做了「智能合約及形式化驗證」的主題分享。當時在演講結束後反響特別好,這套方法得到了比較廣泛的認可。

目前在國內區塊鏈行業,我們還暫時沒有看到特別能夠跟我們對標的公司或者團隊。我的聯合創始人郭文生老師也是做形式化驗證的學者,我們原來是兩個不同的門派,所以 Beosin 成都鏈安相當於把兩套方法結合起來提供安全服務,加上自動化能力、安全檢測能力和先發優勢,目前還沒有明確的競爭對手。

Q:走完了從全人工化到半自動化到大部分自動化三個階段之後,2019 年的目標和計劃是什麼?

A:因爲公司成立剛好滿一年了,在這一年中,我們推出了基於形式化驗證的 VaaS (Verification as a Service)平臺,它是 Beosin 成都鏈安創立時就規劃的一個高門檻的產品,這個產品我們已經做到全球最頂級,精確度和準確率都是全球最高。在形式化驗證的基礎上,2019 年我們計劃做更多的區塊鏈安全產品,同時我們的安全服務也將進化爲全生態的,市場也將朝全球化發展,區塊鏈本來就是個全球化的產物。

(鏈聞注:VaaS 是一個智能合約安全驗證平臺,主要來檢驗智能合約的安全屬性和功能正確性,功能正確性是指智能合約的代碼實踐符合用戶的預期功能需求。)

例如我們前段時間剛剛發佈了面向 EOS 的線上智能合約開發平臺,我們爲什麼做這個事情?因爲在做形式化驗證的過程中,我們發現其實有些問題是由於編程人員的規範不夠,或者編程人員的意識不夠,或者能力不夠,或者有的是習慣不好,因此我們覺得有必要做一個專業的開發平臺。基於形式化驗證這套服務發展服務和產品生態,這就是我們 2019 年的目標。

Q:如何看待過去一段時間區塊鏈的安全形勢和區塊鏈安全領域的變化?,區塊鏈安全是否有了長足的進步?

A:還是有很大的進步。至少 2016 年的時候還沒有多少人關注區塊鏈安全,我們應該算全球最早一批把形式化驗證用到區塊鏈來的團隊,所以在我們做的時候根本沒有任何路子可尋,都不知道該怎麼做,全是自己硬着頭皮一步步走過來的。到 17 年的時候,行情開始火熱,慢慢有人在關注區塊鏈安全了,到 2018 年的時候也成立了多家區塊鏈安全公司,但現在好多公司可能都沒有聲音了,能夠堅持下來也就只有幾家。

現在畢竟是行情的低谷期,這很正常,因爲區塊鏈行業仍是很早期的產物。但是對於區塊鏈的發展我是長期有信心的。區塊鏈跟其他互聯網產業不一樣,它的安全需求更大,而且它更剛需,無論是鏈上交易也罷,數字資產也罷,用戶數據也罷,這些都不能出現安全問題,如果出現問題後果是非常嚴重的。

Q:在安全服務領域,道德是值得討論的一個話題,從事安全服務,是否需要更高的道德約束?能否講講您的理解?

A:這個問題的確是好多安全公司需要面對的問題,所以我也想提一下,這就是我們公司和其他安全服務公司不太一樣的地方,其實 Beosin 成都鏈安的定位是以防爲主,不是以攻爲主。形式化驗證是一個很好的防的方法,形式化驗證這套方法的目的是讓系統的的代碼真的安全,更安全的代碼,意味着更少被攻擊的可能性。

形式化驗證是做盾的,就好像我們原來在航空、航天、軍事領域用形式化驗證讓系統更堅固,讓代碼更安全,儘可能減少漏洞。Beosin 成都鏈安是一個以防爲主的公司,這是我們跟其他的安全服務公司不太一樣的地方,我們重點關注的是如何提升系統自身的安全能力和系統自身的健壯能力。這一點跟其他的白帽黑帽團隊是不一樣的,的確,白和黑或者白和灰,這是一念之間,這裏面有太多的誘惑了,我們防的就是黑,是通過系統自身的安全角度去防黑。

我們把這叫做從根本上出發,從開發源頭解決問題,包括我剛提到的 EOS 線上智能合約開發平臺,我們的目的就是爲開發者提供一個好用的開發平臺,對開發流程進行保護,然後再進行安全檢測。包括區塊鏈安全態勢感知系統、安全事件的預警報警、風控和反洗錢等等都是希望從系統自身的健壯性出發解決問題。

Q:Beosin 成都鏈安有行業榜樣嗎?不侷限於區塊鏈領域,爲什麼?

A:其實在 Beosin 成都鏈安成立之初就想做區塊鏈的 360,當然是不是 360 這種模式或者 360 的發展路線我們還不確定。實際上我們的第一個形式化驗證平臺就是免費的。我們面向普通用戶 to C 都是免費的,而面對企業選擇做定製化的服務,這是互聯網公司一種成熟的發展模式。