欄目介紹
Introduction
技術的突破是推動區塊鏈行業前進的引擎,幣安中國區塊鏈研究院與鏈聞 ChainNews 同爲密切關注區塊鏈與密碼學等領域技術發展前沿的組織,故而聯合推出「他山之石」專欄,向中文世界讀者介紹全球範圍最值得關注的區塊鏈技術進展,以及在金融等產業最新的應用分析與動態,以期爲中國的區塊鏈行業「攻玉」提供借鑑和思考。
Trail of Bits Blog
自 2012 年始,Trail of Bits 幫助全球最受矚目的組織和產品進行安全防護。 他們將高端安全性研究與現實世界中的網絡攻擊者的思想相結合,以降低安全風險並強化代碼。
*本文已取得作者授權,並由鏈聞和幣安中國區塊鏈研究院獲得中文地區翻譯首發權
目前,我們正在與約翰斯·霍普金斯大學(Johns Hopkins University)的 Matthew Green 教授共同研究通過零知識(ZK)證明創設一個可信可靠的環境,讓科技企業和漏洞研究人員能夠在這樣的環境中無後顧之憂地溝通交流。在未來四年中,我們將推動 ZK 證明從理論走向實踐,並面向漏洞研究人員提供可得出 ZK 可利用性證明的軟件。此項研究隸屬於美國國防部高級研究計劃局(DARPA)所資助的加密驗證和評估信息安全(SIEVE)項目。
近年來,ZK 研究主要集中在區塊鏈應用領域,其中參與方需要證明其交易符合公認的底層規則。而我們的研究則大幅拓寬了 ZK 可證明的語句種類。該項目結束後,用戶將能夠驗證 x86 處理器程序的相關語句。
爲什麼是 ZK 可利用性證明?
就 bug 的發現和報告,軟件開發者和漏洞研究人員無法達成一致。披露過多的漏洞信息會中傷第三方研究人員的收益,而披露過早則會對軟件廠商的信譽造成永久的損失。各方之間的溝通往往以失敗告終,同時技術產業的損失也十分慘重。
而且,在很多時候,企業不願意接觸安全團隊,也不會理睬用戶隱私所面臨的潛在威脅。在這樣的情況下,漏洞研究人員的處境十分艱難:要麼在知道用戶面臨風險的情況下保持沉默,要麼公開披露漏洞,迫使企業做出行動。如果選擇了後者,研究人員則將漏洞利用路徑告訴了攻擊者,親手把用戶放到了砧板之上。
ZK 可利用性證明將徹底顛覆了漏洞的披露方式,能夠讓企業能夠精準地明確 bug 懸賞範圍,讓研究人員在不冒險進行公開披露情況下提交能明確證明其掌握了漏洞利用情況的證明。
設計 ZK 證明
通過 ZK 證明,驗證人能夠讓校驗人相信自己持有一段信息,同時不需要暴露信息本身。例如,Alice 希望讓 Bob 相信自己知道了某個值 Y 的 SHA256 預映射 X,但是並不需要告訴 Bob X 具體是什麼。(或許 X 是 Alice 的密碼)。ZK 證明最知名的工業應用或許是在 ZCash 等注重隱私保護的區塊鏈領域,在此領域,用戶在提交交易時,希望自己的身份、接收人的身份、交易金額都能保持匿名。爲此,他們需要提交一個 ZK 證明,證明其交易符合區塊鏈規則,並且發送者具有足夠的資金。(請閱讀 Matt Green 的文章瞭解 ZK 證明及相關示例。)
現在你已經知道了 ZK 證明的用處,但是這些算法是如何開發的呢?需要權衡哪些利弊呢?關於高效系統的開發,有三大衡量指標:驗證時間(prover time)、校驗時間(verifier time)和帶寬(bandwidth)(即一方必須通過協議向另一方發送的數據量)。某些 ZK 證明不需要驗證人與校驗人進行交互,在此情況下,帶寬僅是證明的大小。
接着,我們談一談目前的難點以及影響 ZK 證明投入實踐的主要障礙。大多數傳統的 ZK 協議要求底層語句必須首先用布爾電路(Boolean circuit)或無循環的運算電路(即組合電路)來表示。對於布爾電路,可以用 AND 門、NOT 門和 XOR 門,而對於運算電路,可以用 ADD 門和 MULT 門可以想象,要想把一個要證明的語句轉換成這樣的電路並不容易,如果還沒有簡潔的數學公式,更是難上加難。例如,如果一個程序包含循環行爲,那麼在電路生成之前,必須先把它展開,而當程序包含數據依賴型循環時,那就無法展開了。
布爾電路與運算電路示例
另外,電路尺寸也會影響到 ZK 協議的效率。一般情況下,驗證時間與電路尺寸至少呈線性關係(通常,各個門的開銷通常很大且恆定)。因此,在漏洞披露時,ZK 證明需要底層漏洞能被尺寸合適的電路捕捉到。
證明可利用性
由於 ZK 證明一般會接收寫成布爾電路的語句,因此,這裏的難點在於需要布爾電路僅在漏洞利用成功時返回“true”,以此表示存在漏洞利用。
我們希望當驗證人向程序中導入會造成漏洞利用的輸入時,電路能夠接收(accept),例如:能夠讓攻擊者取得程序執行權限的緩衝區溢出(buffer overflow)。由於大多數二進制漏洞利用針對的是二進制(binary)和特定的處理器,因此,我們的電路必須準確地對程序的目標編譯架構進行建模。最後,當程序成功運行時,以及當漏洞利用在執行過程中被觸發時,我們需要一個電路來接收。
初級的方法是開發一個電路來代表目標建模處理器的“一步”(one step)。接着,我們根據要執行的程序,將容納該程序的內存初始化;按照程序的啓動時間,設置程序計數器;驗證人使程序運行在自己的惡意輸入上——重複處理器電路,直至程序結束,檢查每一步是否均滿足了漏洞利用條件。也就是說檢查程序計數器是否被設置成了一個已知的“惡意”(bad)值,或被寫入了一個有權限的內存地址。關於此策略的重要注意事項:在每一步均需要完整運行整個處理器電路(即便實際上只有一條指令在運行),因爲單獨列出一項功能會泄露相關的跟蹤信息。
不幸的是,這種方法會導致電路過大,因爲程序執行的每一步都需要有一個電路對核心處理器邏輯及整個 RAM 進行建模。即便我們把 RAM 限制成 50 MB,對於一次漏洞利用,如果其跟蹤使用了 100 條指令,那麼產生一條相應的 ZK 語句會導致電路至少達到 5GB。這種方法效率太低,無法用於有意義的程序。關鍵問題在於電路尺寸與跟蹤長度和 RAM 大小成線性關係。爲了解決這個問題,我們採用了 SNARKs for C 的方法,即把程序執行證明分爲兩部分,一部分爲核心邏輯,另一部分爲內存正確性。
要證明邏輯有效性,必須將處理器電路應用於程序跟蹤中連續的每一對指令(sequential pair of instructions)。該電路可以驗證一個寄存器狀態能否合法地跟隨另一寄存器狀態。如果每一對狀態均有效,則電路接收。不過要注意,這裏的前提是內存操作是正確的。如果轉移函數電路中存在一個存儲器檢查器,則會產生開銷,此開銷與所使用的 RAM 大小成比例。
無內存檢查處理器執行有效性
讓驗證人也輸入一個內存排序的執行跟蹤,就能進行內存驗證。如果第一個內存地址訪問了一個低於第二個內存地址的內存地址(破壞了時間戳(timestamp)關係),那麼這個跟蹤就會在另一個跟蹤之前放置一條跟蹤記錄。這個跟蹤能讓我們線性地掃描內存排序指令,確保內存訪問的一致性。此方法無需根據 RAM 大小創建相應尺寸的電路。不過,該電路與跟蹤尺寸呈線性關係,並且僅能執行基礎的相等性檢查(equality check),不能明確地記錄每一步下的完整 RAM。
檢查內存排序跟蹤
最後一個要解決的問題是,驗證人不受阻撓地使用與最初情況不符並且無法創建假證明的內存排序跟蹤。要解決此問題,我們必須添加一個“排列檢查器”(permutation checker)電路來驗證我們是否確實根據內存位置對程序跟蹤進行了排序。欲進一步瞭解相關討論,請參見 SNARKs for C 論文。
建模 x86
知道了如何證明 ZK 中存在漏洞利用,接下來我們需要把相關的處理器架構建模成布爾電路。此前已經有人對 TinyRAM 進行了建模,這是一種 RISC 架構,其目標是在 ZK 環境中高效運行。不幸的是,TinyRAM 並未商用,而且由於漏洞利用大多依賴特定於架構的行爲,因此 TinyRAM 不能爲現實程序提供 ZK 可利用性證明。
我們接下來將通過建模一種相對簡單且應用廣泛的微處理器——MSP430 進行建模,以開發 ZK 可利用性證明,這種簡單的芯片被廣泛應用於各種嵌入式系統。另外,Microcorruption CTF 系統也是基於 MSP430 運行。我們的首要目標是針對 Microcorruption 受到的每一次挑戰提供 ZK 證明。在完成此“可行性演示”後,我們會轉向 x86。
從簡單的 RISC 架構過渡到複雜的 CISC 架構,隨之而來的是各種複雜問題。對於 RISC 處理器的電路模型,每週期的時鐘門爲 1 至 10k。另一方面,如果我們的 x86 處理器達到 10 萬門級別,那麼對於需要 10000 條指令才能完成的漏洞利用,ZK 證明會達到 48 GB。由於 x86 比 MSP430 複雜了幾個數量級,因此即便把邏輯證明和存儲器正確性證明分開,也無法天真地將其功能實現爲布爾電路。
我們的解決方案基於一個顯而易見的事實,即沒有程序能完全用盡 x86。一個程序在理論上能用到 x86 所支持的全部 3000 條指令,但實際上,大多程序只用到了幾百條。我們會使用程序分析技術來判斷特定二進制所需的 x86 最小子集,並動態地生成能夠驗證其正確執行能力的處理器模型。
當然,我們無法支持部分 x86 指令,因爲這些指令實現了數據依賴型循環。例如,repz 會重複後續指令,直至 rcx 爲 0。對於這樣的指令,只有在運行時才能確定其實際行爲,而我們的處理器電路必須是組合電路,因此無法支持此類指令。爲了處理這些指令,我們會把一個靜態二進制轉換器(binary translator)從普通 x86 轉成特定於我們程序的 x86 子集。這樣的話,我們就能夠處理最複雜的 x86 指令,而無需將其硬編碼到我們的處理器電路中。
新型的 bug 披露模式
能夠與約翰斯·霍普金斯大學以及 DARPA SIEVE 項目的同仁共同啓動這項工作,我們倍感興奮。我們希望得到能夠從根本上顛覆漏洞披露方式的工具,以便企業能夠明確其 bug 懸賞範圍,漏洞研究人員可以安全地提交能明確證明其掌握了漏洞利用情況的證明。而且,我們還希望 ZK 漏洞披露能成爲消費者的保護傘。研究人員可以在不公佈相關漏洞的情況下,警告用戶特定設備存在潛在危險,這麼做是在向企業施壓,逼迫他們解決本不願解決的問題。
更廣泛地說,我們想把 ZK 證明從學術界帶入產業界,使其更貼近當今的軟件、更實際。關於此技術,若您有特定用途且未在本文中未提及,我們歡迎您來函。關於 ZK 證明方案與電路編譯器的複雜生態系統,我們積累了相應的專業知識,可爲您提供幫助!
*在此我們要特別感謝 Colleen Swanson 和 Marcella Hastings,感謝他們的校對工作,以及他們關於本文的寶貴反饋。
*“幣安區塊鏈研究院” *致力於打造基於區塊鏈技術的數字金融基礎架構與服務,並建立更開放、更包容、更安全的價值網絡生態;專注於區塊鏈技術的自主核心技術、行業應用和治理模式研究,使幣安學術研究成果走在區塊鏈科研的最前列。
我們爲從業者和開發者提供區塊鏈教育培訓認證、以及工具和資源。同時,我們將深度挖掘並投資優質生態夥伴,推動技術成果轉化,促進區塊鏈技術在實體經濟中的應用。
掃碼即可關注,獲幣安最新資訊
點“閱讀原文”查看原報告