NEST 社區開發者 YolkLi 分享 DeFi 開發中需要注意的安全問題,安比實驗室郭宇聊到智能合約安全的形式化驗證。

原文標題:《Math Show #007 - 深入淺出,如何確保你的 DeFi 資金安全》
整理:Math Show

6 月 23 日晚 7 點,麥子錢包舉辦了 Math Show 的第 7 期,有幸邀請了 NEST 社區開發者 YolkLi 和 安比實驗室 郭宇,特邀主持人鏈聞研究總監 潘致雄,帶大家「深入淺出,如何確保你的 DeFi 資金安全」,以下是當晚的精彩撰錄。

如何確保 DeFi 資金安全?我們與 NEST 開發者及安比實驗室聊了聊

主持人:想必大家對最近 DeFi 最近的火熱程度有目共睹,除了帶了的財富效應之外,大家其實最核心還是最關注「DeFi 資金」的安全性,那麼我們先請第一位嘉賓 NEST 社區開發者 YolkLi 給我們帶來的分享。

YolkLi:今晚和大家分享一下日常開發中的一些經驗。

代碼安全

智能合約的開發和傳統的開發不同,因爲區塊鏈的操作消耗和去中心化特點,代碼的質量和安全顯得更爲突出。大概有三點建議:

1、DeFi 是建立在區塊鏈上的應用,公鏈(聯盟鏈)底層邏輯或者機制的改變會對 DeFi 應用產生影響,比如 Gas 消耗由於某次改動上升了,導致某個 DeFi 的套利空間不存在了。我們需要關注區塊鏈的發展,尤其是底層的升級對 DeFi 安全性的影響。

2、區塊鏈上的操作是以交易的方式進行的,要保證交易的原子性,交易中所有的操作和影響都要在代碼邏輯的覆蓋範圍內。

3、安全審計,DeFi 面向市場前必須要經過安全審計這步,這是對用戶和投資者負責。NEST 目前也在和安比實驗室進行 NEST3.0 的審計工作。

跨合約安全

很多業務場景需要用到其他的合約接口,前段時間也出現了很多問題,比如 ERC20 的假充值,ERC 777 重入攻擊等。

合約的組合會破壞一筆交易的原子性。舉個例子:

一張「競猜」合約:轉入 1 ETH 參與競猜,正確返回 2 ETH ,錯誤 1 ETH 就損失掉了。假設競猜過程公平公正,代碼也是安全的。我們理想的邏輯是調用者轉入 1 ETH 並且返回結果,賺 1 ETH 或者損失 1 ETH。正常調用沒有問題,但是如果用另一張合約調用,並且在合約中實現「沒有返回 2 ETH 就交易失敗」的邏輯,成本只有一點 gas 費,但是永遠不會輸。在一段正常邏輯外加了一段新的邏輯,遊戲就變得不公平了。

當自己的合約內部用到多張合約組合的結構,需要明確整個交易邏輯的閉環,確保沒有額外的方法或者權限可以影響交易邏輯。

需要使用外部合約時,我們假設對方是安全的,兩張安全的合約組合後交易的安全性會發生變化,可能會變得不安全,我們需要對組合後的安全性進行分析。或者假設對方是不安全的,我們需要對調用後的邏輯進行限制,對特殊的結果特殊處理,確保自己的業務邏輯不受影響。

風險控制

DeFi 安全是個長期的工程,代碼安全是個大前提,同時爲了應對未來的安全問題,DeFi 需要有應急流程。我們需要明確知道業務中的風險點在哪,確保在緊急情況最大程度的保證所有人的資金安全。在處理緊急狀況依然需要堅持去中心化,這對去中心化的治理是個挑戰。

安全最終並不是靠某個項目方或者安全審計團隊完成的,應該是一個去中心化的方式。讓社區成員或者黑客參與到 DeFi 安全的建設中,並且給予相應的激勵。參與的人越來越多,DeFi 的發展才能越來越健壯。

主持人:感謝 YolkLi 的分享,收穫頗豐,大家可以慢慢消化,接下來有請我們安比實驗室的郭宇繼續圍繞這個話題分享。

郭宇:DeFi 是由智能合約來構建的,它的安全性包含了以下關鍵因素:

A. 底層鏈的安全型:礦工 / 黑客作惡成本與收益,當合約上的資產在不斷膨脹後,礦工作惡的動機會逐步加大,多方博弈帶來的納什均衡的轉移。

B. 合約平臺的安全性:智能合約語言是在動態變化的,編譯器也在發展,eth2 還會引入 wasm,這個動態變化過程會引入新的安全不穩定因素,並且帶來更大的攻擊面。特別是當編譯器變複雜之後,也許會有黑客攻擊編譯器的事件發生,編譯器引入的安全漏洞會更加隱蔽,更加難排查。

C. 業務本身的安全性:DeFi 跟外部金融世界是緊密聯繫的,比如外部沒有經過驗證的價格,外部的套利行爲,DeFi 和 CeFi 之間的互相關聯性而帶來的攻擊手法。

D. 第三方服務的安全性:可組合式的 DeFi 合約的可靠性,接口是否兼容,合約標準的制定比較隨意。

單純從技術角度,區塊鏈安全是前所未有的。區塊鏈項目是「全開放式」的,用戶不需要 KYC 就能任意接入,這在傳統金融中是完全不可想象的,並且系統的每一個細節都對外暴露。

安全審計是必須要做的,但這並不能從根本上解決問題,問題就是:「審計結果無法量化」。

如果審計報告上列出的 bug 越多,能證明剩下的 bug 越少嗎?這有可能是代碼質量較差,發現的 bug 多,所以隱藏的 bug 會更多。

可是,如果審計報告上列出的 bug 很少呢?也許是審計不夠深入。

其實,我認爲這都不是智能合約的終極難題,終極難題是:智能合約到底怎麼樣算是安全?

從用戶和合約開發者的角度有時候是對立的。比如有些合約有管理員權限,那麼從開發者的角度看,有管理員利於後續做一些高權限操作。但是,從用戶角度來看,管理員權限過高就意味着更大的風險。所以,當我們把「公平性」也納入到「安全性」的範疇後,這個問題會變得更加複雜。

於是,一部分區塊鏈信仰者走了一條路,那就是「治理」。

「治理」能解決問題嗎?我不確定,但是直覺上,它不能解決安全的根本問題,而且代價很高,遠超出「治理派」的估算,而我堅信的是:我們需要基於數學的信任與安全。

我想談談形式化驗證

在形式化驗證之前,需要給「安全」下一個數學定義。請注意,是數學定義,用嚴格的形式化邏輯語言來定義的定義。

凡是遇到聲稱在做形式化驗證,或者經過形式化驗證的項目,我們需要追問一句,形式化驗證了什麼?

形式化驗證的結果是一個確定性的結果,是一個數學定理!

之前看過一些項目,包括一些大廠,聲稱做形式化驗證,但是閉口不談驗證了什麼性質。

這個定理長什麼樣子呢?我舉個例子:

定理 1:對任意的環境 Env,對所有的輸入 I,程序 Env |- P(I) 運行得到一個執行行爲序列 [B0, B1, B2 ..... Bn],forall i, Safe(Bi)。

這個定理是可以完整地用數理邏輯來定義的,只是這裏我用中文,利於大家理解。

接下來,需要證明:

定理 1:對任意的環境 Env,對所有的輸入 I,程序 Env |- P(I) 運行得到一個執行行爲序列 [B0, B1, B2 ..... Bn],forall i, Safe(Bi)。

證明:

…(略)

證畢。

是不是眼熟?和我們初中做數學作業有點類似。

任何形式的形式化驗證都會得到這一個定理和證明過程,只不過證明過程有時候是「隱式」的,被一些別的定理所蘊含了,不存在一個明確的表達。

上面定理中的 forall i, Safe(Bi) , 這裏 Safe() 函數怎麼定義 可是個大學問。

一種最直觀的做法是這麼定義 Safe(X):X 不整數溢出,X 不數組越界,X 沒有重入,X ……

但是這樣大家會有疑問,這個定義包含的規則是完備的嗎?當然不可能完備,總有新的安全漏洞出現。

那麼這個 Safe() 定義靠譜嗎?當然不靠譜,但是不靠譜不等於不正確。目前的安全審計基本停留在這一層面,只是這個定義不 Sound。

主持人:所以是不是需要發展一些對於 DeFi 場景而言的形式化驗證的 best practice,以後的審計效率和安全性就能提升?

郭宇:是的。

其實,Safe() 函數的定義需要的是一個基於互模擬的數學定義,而不是規則的羅列。互模擬在「差分隱私」「多方計算」「零知識證明」「操作系統驗證」…… 等等各種形式驗證領域都有具體的定義。這裏我就不展開了,總之,要給出一個 sound 可靠的 Safe 定義在不同的領域是完全不同的,而且是最困難的。

定義好安全性之後,我們驗證的對象是什麼?這裏可以分爲模型級別驗證和代碼級別驗證。但是不管怎麼驗證,我們需要對驗證的代碼寫出「規範」,從上面的例子延伸:

Solidity 開發語言裏面有一個 方法 A(i),輸入 i,輸出 B;

形式化驗證就是,根據方法 A(i) 產生另一個方法,也輸入 i,得到 B。這就證明了方法 A 是 OK 的。

這就是在驗證一個行爲滿足規範。

那麼這個驗證過程,可以是自動化的,半自動化的,也可以是人工的。但是形式化驗證很快會面臨一個很困難的新問題:如果代碼量很大怎麼辦?如果代碼會頻繁改動怎麼辦?

這是過去二十年,形式化驗證領域的研究熱點,就是如何把代碼拆成很多的模塊,然後實現驗證的模塊化,這裏面的理論難度深不見底。

這裏我來談談最後一個形式化驗證的難題,這就是工具悖論。假如,我們把代碼驗證完了,藉助了一個工具。那麼問題來了,這個工具的安全性怎麼來保證?爲了驗證這個工具,我們又需要一個新工具。

有一類形式化驗證,會產生「Proof Term」,也就是具體的驗證過程的表達。

定理 1:對任意的環境 Env,對所有的輸入 I,程序 Env |- P(I) 運行得到一個執行行爲序列 [B0, B1, B2 ..... Bn],forall i, Safe(Bi)。

證明:

…「Proof Term」(略)

證畢。

也就是中間那個非常龐大的證明過程,它可以擺脫對驗證工具的信任依賴,類似於區塊鏈中我們不需要信任礦工一樣。我們可以藉助各種先進的驗證證明產生工具,只要他們能產生對的證明,他們本身是否安全不重要,這是一種很本質的新的去中心化技術。

形式化驗證是銀彈嗎?

並不是。

挑戰一:成本很高,需要很多的智力投入。

挑戰二:需要理論上的重大突破,提高邏輯的自動推理能力。

挑戰三:一方面我們需要更復雜的 DeFi 功能!另一方面,複雜理論的驗證方法更難。

驗證技術與技術創新存在一個賽跑,目前來看,驗證技術遠遠落後於技術的發展,Fuzzing,符號執行,人工審計,動態監控,應急預案,這些傳統的技術需要和先進形式化驗證技術一起使用。

主持人:在未來的 3-5 年內,我們有沒有可能通過 Etherscan 等區塊鏈瀏覽器上一個通過形式化驗證的標記來確認該智能合約的安全性?

郭宇:對於簡單的智能合約是很有希望的,比如 ERC20 的 token 合約 。但是對於超過 2000 行的智能合約,難度就會加大很多。其實我們不能僅關注「打勾」,而是需要看形式化驗證的那個最終定理是否是有意義的,或者說是否 sound。並且可能出現今天打了勾,明天就發現問題,需要取消,所以其實需要制定標準。這個未來需要一個社區,有專家,有用戶,有黑客,大家一起來建設,3 年有點短,5 年也許有希望,建議採取學術界的同行評議機制。

智能合約非常特殊,難度更大,傳統軟件的形式化驗證開源工具是有的,智能合約這邊其實進展很小。但是,其實目前形式化驗證的自動化能力非常弱,大家能看到的只能做到「找 bug」 這種程度,不能保證「無 bug」。

主持人:請問 NEST 預言機與 Chainlink 預言機有什麼不同?

YolkLi:NEST 價格預言機是「直接」預言機方案:通過礦工雙邊報價、驗證者喫單套利的方式在鏈上直接生成價格。通俗來講,NEST 預言機報價礦工在用真金白銀證明自己的報價,如果驗證者覺得該價格與市場價格之間有偏差,那就可以喫單套利。最終,NEST 預言機在鏈上生成的價格都是能夠代表市場公允價格的。

這種機制的亮點在於價格在鏈上可以被市場驗證。或者是分佈式驗證,任何一個人都可以成爲價格的驗證者。

Chainlink 的預言機方案需要相信 Chainlink 的節點。使用 NEST 預言機需要相信市場的驗證(共識)。

主持人:DeFi 領域的多起安全事件給整個區塊鏈行業敲響了安全的警鐘。現階段的 DeFi 不光有安全問題,還有很多其他的痛點,能否從公鏈和應用的角度,談一下對於 DeFi 迫切需要解決的有哪些問題?面對日益嚴峻的安全挑戰安比將怎樣應對?

郭宇:我覺得有兩點需要做,

第一個是:可組合性的 DeFi 的接口需要進行更細緻的分析和行爲披露,可組合性的風險還是比較大;

第二個是:智能合約安全需要一個更廣泛更積極的社區參與,可以參考 DAO。

安比的使命是探索新的技術,來提升區塊鏈系統的安全性,實現基於數學而不是基於專家權威的安全性。

主持人:2019 年以來 DeFi 市場發展火熱,據 DeFipulse 統計,當前 DeFi 市場整體鎖倉規模已突破 10 億美元,較去年同期增長 362%。那麼請問您怎麼看待 DeFi 這一熱門領域?NEST 是否有佈局去中心化金融的打算呢?

YolkLi:我非常看好 DeFi 的未來發展,這是一個數以萬億計規模的開放式金融市場。我們希望 NEST 預言機能夠給下游 DeFi 提供高度確定性的鏈上價格數據。

就 NEST 開發者小組來說,更多的是以分佈式的方式去維護好 NEST 預言機。有關 DeFi 的研發,我們也在做,而且投入了很多的精力。NEST 是個開放的預言機網絡,更重要的是吸引更多的開發者和項目方使用 NEST。

主持人:非常感謝參與今晚 Math Show #007 活動的「show」友們, 也感謝兩位嘉賓帶來的分享,想必大家對「 DeFi 資金安全」有一定的認知和了解。