淺析基于可驗證計算的可信云計算優(yōu)秀論文
1 引 言
云計算作為一種新興的網(wǎng)絡(luò )計算商業(yè)服務(wù)模式,使得用戶(hù)可以隨時(shí)在遠端的云服務(wù)器存儲數據和運行程序.但這種新興的計算模式在給用戶(hù)帶來(lái)諸多便利性的同時(shí),也帶來(lái)了一些新的安全挑戰.用戶(hù)可能擔心云計算平臺本身的安全性,比如云平臺漏洞和錯誤配置、管理員的惡意行為等等,而這都可能直接導致用戶(hù)數據的完整性和隱私性受到危害,導致用戶(hù)應用程序無(wú)法正確執行.這就產(chǎn)生了一個(gè)問(wèn)題:用戶(hù)如何相信云提供商執行的程序結果是正確的?如何確保存儲在遠端的數據的完整性和私密性?檢測遠程服務(wù)器返回的結果是否正確的傳統解決方案有以下幾種:
(1)采用審計的方法,即隨機選取服務(wù)器執行的一小部分程序進(jìn)行驗證,這就可能發(fā)生錯誤執行的程序沒(méi)有被服務(wù)器驗證的情況,所以說(shuō)這種方法必須假設錯誤執行的程序的發(fā)生頻率是很小的;
(2)利用可信硬件和遠程證明來(lái)保證遠程服務(wù)器運行的程序是正確的,但是這種方法必須假設云提供商是完全可信的,由于硬件基礎設施是在云提供商的控制之下,如果云提供商內部人員惡意控制了可信硬件(如CPU、TPM),就無(wú)法保障云提供商運行的程序的機密性和可驗證性.而且還需要假設存在一個(gè)可信鏈,而運行時(shí)可信鏈的建立在可信計算領(lǐng)域依然是一個(gè)難題.事實(shí)上,在實(shí)際的云計算應用場(chǎng)景中這兩個(gè)假設通常是無(wú)法滿(mǎn)足的.在云計算場(chǎng)景中,用戶(hù)無(wú)法完全相信云提供商,即使用戶(hù)出于聲譽(yù)的考慮相信云提供商本身,也無(wú)法相信其內部管理人員;
(3)采用冗余計算的方法,用戶(hù)可以讓多個(gè)遠程服務(wù)器把相同的程序執行多次,然后檢測他們返回的結果是否一致.但這在云計算中也是行不通的,云計算中的軟硬件平臺配置通常是相同的,而這違背了冗余計算中錯誤必須是不相關(guān)的假設,且遠程服務(wù)器很容易竄通,合謀返回一個(gè)錯誤的程序執行結果.
而可證明數據持有(Provable Data Possession,PDP)方法和可恢復證明(Proof of Retrievability,POR)方法可以用來(lái)確保存儲在遠端的數據的完整性,避免云提供商刪除和篡改數據.相比PDP方法,POR除了能確保數據的完整性之外,還能確保數據的可恢復性,但是PDP和POR無(wú)法確保在云提供商端執行的程序的正確性.另一方面,基于復雜性理論的交互式證明系統(Interactive Proof system,IPs)和概率可驗證證明系統(Probabilistically Checkable Proof system,PCPs)以及密碼學(xué)理論構造的可驗證計算協(xié)議能以很高的正確率檢測出遠程服務(wù)器返回的程序執行結果是否正確并且不需要對遠程服務(wù)器(云提供商)做任何假設.可驗證計算協(xié)議致力于設計驗證者與證明者之間的協(xié)議,協(xié)議允許在計算能力上相對較弱的驗證者(如云計算中的用戶(hù))將其程序發(fā)送到一個(gè)計算能力強大的,但不可信的證明者(例如云提供商),并要求證明者執行其發(fā)送的程序.所設計的協(xié)議應確保證明者不但返回程序的執行結果給驗證者,并且使得驗證者相信這個(gè)程序執行結果是正確的.其主要目標是使得服務(wù)器在發(fā)送程序執行結果的同時(shí)提供程序正確執行的證據,而用戶(hù)驗證證據的過(guò)程必須要比用戶(hù)自己執行程序的開(kāi)銷(xiāo)小(當然有時(shí)由于資源比如存儲的限制,用戶(hù)根本無(wú)法自己執行程序,在這種情況下是指和假設用戶(hù)有足夠的資源執行程序時(shí)的開(kāi)銷(xiāo)相比要小)。
2 問(wèn)題描述和協(xié)議設計原則問(wèn)題描述:
驗證者V把程序f和輸入變量x發(fā)送給證明者P,P計算f(x),并把f(x)賦值給變量y,返回y給V,然后V 和P 以如下方式進(jìn)行交互:
(1)如果y=f(x),那么P 應該能向V 證明y的正確性,即使得V 接受y.其中,證明可以通過(guò)回答V 提出的一些問(wèn)題完成,也可以通過(guò)給V 提供一個(gè)證書(shū)完成.
(2)如果y≠f(x),V 能以很高的概率拒絕接受y.可驗證計算協(xié)議的設計必須滿(mǎn)足3個(gè)基本原則:(1)協(xié)議應該使得驗證者的開(kāi)銷(xiāo)比其在本地執行程序f(x)的開(kāi)銷(xiāo)要低,但可以允許證明者為達到協(xié)議的目標產(chǎn)生合理的開(kāi)銷(xiāo),因為提供運行程序的正確性保障本身就需要用戶(hù)付出一定的代價(jià),在云計算實(shí)際場(chǎng)景中,表現為云提供商可能會(huì )對需要提供程序正確執行證據的用戶(hù)收取額外的費用;
(2)不能假設證明者完全遵守協(xié)議,也就是說(shuō)證明者可能是惡意的,這和云計算中不能假設云提供商是完全可信的實(shí)際場(chǎng)景也是十分吻合的;
(3)f 應該是通用程序,然而在具體的協(xié)議設計中,可能需要對f 表示的程序做一些假設,從而通過(guò)限制可驗證計算協(xié)議適用的應用程序種類(lèi)使得協(xié)議的性能達到實(shí)際應用場(chǎng)景的要求,但是可驗證計算協(xié)議的設計原則依然是盡量能表示通用程序.
通常的安全保障工具比如說(shuō)病毒檢測關(guān)注的都是不正確的行為的識別和防范,可驗證計算協(xié)議則有所不同,其不關(guān)心證明者可能的不正確行為,比如犯了什么錯誤,出現了什么故障等等,而只關(guān)心其執行程序的結果是否是正確的,卻無(wú)法推測程序錯誤執行的原因.這和云計算中用戶(hù)對于程序執行的要求也是相符的.
3 協(xié)議流程和關(guān)鍵
3.1 可驗證計算協(xié)議流程
可驗證計算協(xié)議的流程主要包括編譯處理和證明系統,具體流程如圖1所示.首先是編譯處理階段,驗證者V 和證明者P 將高級語(yǔ)言(比如C 語(yǔ)言)編寫(xiě)的`程序轉換成一組布爾電路集(根據協(xié)議的不同,也可以是其他計算模型比如算術(shù)電路集或者約束集等).接下來(lái),P 和V 進(jìn)行一系列協(xié)議交互,不失一般性,這里用布爾電路集C表示程序f.V 把輸入變量x傳輸給P,P 計算C,輸出程序執行結果y和C正確執行的一組軌跡{C,x,y}給V,{C,x,y}也稱(chēng)為C的一個(gè)可滿(mǎn)足性賦值z.其中,C正確執行的一組軌跡是指C的輸入線(xiàn)路被賦值為x,輸出線(xiàn)路被賦值為f(x)時(shí),電路集中所有電路門(mén)的賦值集合.在程序執行的過(guò)程中,證明者P 獲得了正確計算電路的執行軌跡{C,x,y}.如果P 聲稱(chēng)的輸出y是不正確的,即y不等于f(x),那么對于{C,x,y},就不可能存在一個(gè)有效的執行軌跡(電路C正確計算的一個(gè)證明).因此,如果P 能夠對{C,x,y}構建一個(gè)有效的執行軌跡,那么就一定能使得驗證者V 相信它返回的結果是正確的.顯然,電路正確計算過(guò)程中的各個(gè)門(mén)的賦值本身就能說(shuō)明存在有效的執行軌跡.但是,如果需要V 依次驗證所有電路門(mén)在計算電路過(guò)程中的值,進(jìn)而確定程序是否正確執行,這個(gè)工作量和V 本地執行f 是相當的,這就違背了可驗證計算協(xié)議設計的基本原則.所以,圖中第步就需要證明者對程序執行軌跡編碼,生成一個(gè)很長(cháng)的字符串,并使得不同的執行軌跡生成的編碼在所有不同的位置的取值是不相同的.這樣,驗證者就可以通過(guò)檢查隨機選擇的編碼的特定的位置的取值,來(lái)驗證執行軌跡的有效性,進(jìn)而對返回的結果采取特定的測試來(lái)確定證明者返回的結果是否正確.
3.2 可驗證計算協(xié)議的理論依據
理解可驗證計算協(xié)議的原理和流程關(guān)鍵在于理解兩個(gè)等價(jià)關(guān)系,如3.1節所述,可驗證計算協(xié)議的流程主要包括編譯處理和證明系統.其中,編譯處理階段,編譯器完成高級語(yǔ)言程序到電路集或者約束集(可以看做方程組)等計算模型的轉化,其實(shí)現的理論依據在于等價(jià)關(guān)系:程序執行的正確性等價(jià)于電路集或者約束集可滿(mǎn)足問(wèn)題.
4 計算模型生成原理流程
為了應用IPs和PCPs理論構造可驗證計算協(xié)議,必須先把高級語(yǔ)言程序轉換成IPs和PCPs 判定器可以接受的計算模型,比如說(shuō)電路集和約束集.Cook-Levin 理論表明這種轉換理論上是可以的,因為任何程序f 都可以用圖靈機來(lái)模擬,同時(shí)圖靈機可以轉換成布爾電路,且不會(huì )超過(guò)程序的步驟.目前可驗證計算協(xié)議中編譯器都是基于Fairplay和Benjamin 編譯器設計的,常用的計算模型主要有電路集和約束集兩種.Fairplay編譯器和通常的硬件編譯器不同,不能使用寄存器,沒(méi)有時(shí)序邏輯,通過(guò)Fairplay Web 網(wǎng)站可以獲取該編譯器.Fairplay 可以用來(lái)把高級語(yǔ)言編寫(xiě)的程序編譯成一組布爾電路集,但這種高級語(yǔ)言并不是通常所說(shuō)的高級語(yǔ)言,而是一種類(lèi)似Pascal或者C 語(yǔ)言的子集的程序語(yǔ)言,稱(chēng)為(安全函數定義)SFDL 語(yǔ)言.Benjamin 提出的編譯器繼承并改進(jìn)了Fairplay 編譯器,用于把高級語(yǔ)言表示的程序編譯成一組約束集.這種編譯器也引入了一種類(lèi)似SFDL 的高級程序語(yǔ)言,稱(chēng)為擴展函數描述BFDL.不失一般性,本文以Benjamin 編譯器為例說(shuō)明從高級語(yǔ)言程序(C 語(yǔ)言為例)轉化成約束集的原理和工作流程.BFDL 的語(yǔ)法很容易理解,很多地方都是從C和Pascal語(yǔ)言繼承的.BFDL 語(yǔ)言使用C 風(fēng)格的語(yǔ)法,是一種靜態(tài)類(lèi)型語(yǔ)言,支持類(lèi)型引用:第一部分是類(lèi)型聲明,定義將要使用的數據類(lèi)型、支持布爾型、整型、結構體和數組.
5 可驗證計算協(xié)議分類(lèi)
5.1 依據編譯器復雜程度分類(lèi)
由第3節所述,可驗證計算協(xié)議主要流程包括編譯處理和證明系統兩個(gè)階段,所以下文將依據協(xié)議流程對不同協(xié)議分類(lèi),并說(shuō)明每種分類(lèi)的特點(diǎn)和典型協(xié)議.
本文提到的協(xié)議中的編譯處理都是直接使用Fairplay和Benjamin編譯器或者對其改進(jìn)后使用,生成證明系統可以接受的計算模型.依據可驗證計算協(xié)議使用的編譯器的復雜程度,可以分為簡(jiǎn)單編譯器的可驗證計算協(xié)議和復雜編譯器的可驗證計算協(xié)議.簡(jiǎn)單的編譯器是指不支持內存隨機存取的編譯器,即不考慮內存概念,假設程序的輸入都來(lái)源于驗證者.簡(jiǎn)單編譯器的可驗證計算協(xié)議包括GKR、CMT、Thaler、Allspice、Pepper、Ginger、Zaatar和Pinocchio等,其中Pinocchio是第一個(gè)直接接受C語(yǔ)言程序的協(xié)議,而其他協(xié)議則需要先將C語(yǔ)言程序轉化為另一種指定的高級語(yǔ)言比如BFDL語(yǔ)言,然后再轉化成證明系統可以接受的計算模型.GKR使用算術(shù)電路作為計算模型,相比較之前協(xié)議使用的布爾電路減少了程序編譯的開(kāi)銷(xiāo).CMT、Thaler、Allspice、Pepper基本沿用了GKR 中的編譯器,且Pepper對算術(shù)電路進(jìn)行了簡(jiǎn)化,Ginger擴展了算術(shù)電路模型表示的程序種類(lèi),使得模型包含浮點(diǎn)數類(lèi)型,不等測試,邏輯表達式,條件語(yǔ)句等等,因而使得模型能表示的程序更加接近于通用程序.Allspice編譯器通過(guò)增加了一個(gè)靜態(tài)分析器來(lái)自動(dòng)確定并運行Zaatar或GKR兩個(gè)協(xié)議中效率較高的一個(gè),增加了協(xié)議的可擴展性.
復雜編譯器的可驗證計算協(xié)議包括Pantry和BCGTV.復雜的編譯器支持內存操作,這更符合實(shí)際應用場(chǎng)景.Pantry中的編譯器改進(jìn)了Zaatar和Pinocchio使用的編譯器,結合了不可信存儲中使用的技術(shù),使用Merkle-hash樹(shù)來(lái)支持內存隨機存取.通過(guò)構建一個(gè)二叉樹(shù)來(lái)表示內存,二叉樹(shù)的每個(gè)葉節點(diǎn)存儲相應內存地址的值,每個(gè)內部節點(diǎn)存儲作用于其子節點(diǎn)的抗沖突哈希函數的值.每當驗證者通過(guò)(根節點(diǎn)值、內存地址)二元組訪(fǎng)問(wèn)一個(gè)內存地址(葉節點(diǎn))時(shí),證明者可以通過(guò)提供沿葉節點(diǎn)到根節點(diǎn)“證明路徑”的所有值來(lái)“證明”其返回值是正確的.證明者欺騙驗證者的唯一方法是通過(guò)找到哈希函數中的沖突.由于Pantry使用的抗沖突哈希函數的計算函數可以有效地表示成約束集,從而使得內存操作也可以有效的表示成約束集.如果把內存操作也看作普通的程序,就可以實(shí)現包含內存操作的程序的可驗證計算了.更重要的是,Pantry支持“遠程輸入”,這使其能更好的支持MapReduce程序,且在MapReduce程序中為了降低開(kāi)銷(xiāo)定義了GetBlock和PutBlock兩種元操作來(lái)代替構造Merklehash樹(shù)6 基于交互式證明系統的可驗證計算協(xié)議 本文首先說(shuō)明交互式證明系統是如何使驗證者V確信它接收到的程序執行結果是正確的,.假設要執行的程序是計算輸入為x 的函數f.首先,驗證者在把輸入x 和f傳輸給證明者,同時(shí)隨機選取關(guān)于輸入的低階多項式擴展函數的值(比如加權和)作為秘密s,s不依賴(lài)于要執行的程序,因此無(wú)需在輸入要執行的程序之前選取秘密s.接下來(lái),P和V 進(jìn)行一系列交互(d 輪,d 為電路層數),這些交互的目的在于V 控制并引導P從生成V0(0,0,…,0)=R0遞歸到Vd(Zd)=Rd(從一層的電路門(mén)的值的低階多項式擴展函數的某個(gè)點(diǎn)的值遞歸到下一層的電路門(mén)的值的低階多項式擴展函數的某個(gè)點(diǎn)的值,其中低階多項式擴展函數是每層的線(xiàn)性組合,如加權和),Vd是輸入x的低階多項式擴展函數,V 此時(shí)的任務(wù)就是計算Vd在特定點(diǎn)Zd的函數值,并檢測和P 的回復是否一致.在這個(gè)過(guò)程中,V 發(fā)送給P 詢(xún)問(wèn)向量Zi=(z1,z2,…,zm),P 計算Ri=Vi(Zi),用Ri回復V 的詢(xún)問(wèn).這些詢(xún)問(wèn)向量(一共d個(gè))都是相關(guān)的,V 遞歸檢測P 對所有詢(xún)問(wèn)向量的回復是否一致.V 隨機生成的詢(xún)問(wèn)向量使得P 對第一個(gè)詢(xún)問(wèn)向量的回復包含所執行的程序f的結果的聲稱(chēng)值.同樣的,P 對最后一個(gè)詢(xún)問(wèn)的回復包含一個(gè)關(guān)于V 的輸入變量的低階多項式擴展函數的某個(gè)點(diǎn)的值的聲稱(chēng)Rd.如果P 對所有向量的回復都是一致的,且聲稱(chēng)的值Rd和Rd的真實(shí)值相匹配,然后P 使得V 確信其遵守了協(xié)議,即正確的執行了程序,因此接受結果.否則,V 知道P 在某個(gè)點(diǎn)欺騙它,因此拒絕接受.
6 問(wèn)題與展望
目前可驗證計算協(xié)議還只是“玩具”系統,由于性能開(kāi)銷(xiāo)過(guò)大,仍無(wú)法真正用于通用應用程序和云計算的實(shí)際場(chǎng)景中.本文說(shuō)這些協(xié)議接近實(shí)際場(chǎng)景,是因為相對于相關(guān)理論的直接實(shí)現所產(chǎn)生的開(kāi)銷(xiāo)來(lái)說(shuō),這些協(xié)議已經(jīng)有了質(zhì)的飛躍.在特定構造的程序中,這些協(xié)議還是有意義的.而且,在某些需要犧牲性能來(lái)?yè)Q得安全性的場(chǎng)景下,比如在高確保計算場(chǎng)景中,為了掌握部署在遠端的機器的運行是否正常,通常愿意花費比較大的代價(jià).更幸運的是,現有可驗證計算協(xié)議基于性能的考慮要求證明者有大量空閑的CPU周期,驗證的程序有多個(gè)不同的實(shí)例(同一程序、不同輸入),這些和數據并行的云計算場(chǎng)景十分吻合,因而研究可驗證計算協(xié)議,對于解決引言中提出的云計算中的程序執行的可信問(wèn)題從而構建可信的云計算是有意義的.
然而,可驗證計算協(xié)議領(lǐng)域以及其構建可信云計算領(lǐng)域在以下幾個(gè)方面還有待進(jìn)一步的研究:
(1)相關(guān)的理論工具還有待于進(jìn)一步改進(jìn).
一方面需要通過(guò)理論工具的研究和改進(jìn)來(lái)降低驗證者和證明者的開(kāi)銷(xiāo),尤其是要把證明者的開(kāi)銷(xiāo)降低到一個(gè)合理的范圍,使得協(xié)議真正能用于實(shí)際的場(chǎng)景中.驗證者的開(kāi)銷(xiāo)可以分為固定的開(kāi)銷(xiāo)(可以分攤,通常指每個(gè)程序或者每次批處理的初始階段的開(kāi)銷(xiāo))和可變的開(kāi)銷(xiāo)(程序的每個(gè)實(shí)例的驗證開(kāi)銷(xiāo)).研究如何降低驗證者的可變開(kāi)銷(xiāo),研究能否使用密碼學(xué)操作和復雜的理論工具來(lái)降低或取消驗證者初始階段的開(kāi)銷(xiāo).改進(jìn)基于無(wú)預處理的論證系統的可驗證計算協(xié)議,使得其能用于實(shí)際場(chǎng)景.
另一方面,研究利用理論工具來(lái)建立更加合理的計算模型,用于高效的表示通用程序,從而提高協(xié)議的效率.目前的系統要不不能很好的處理循環(huán)結構,要不就是編譯的代價(jià)太高無(wú)法實(shí)用.BCGTV協(xié)議可以處理獨立于數據的循環(huán)的程序,但是其對于程序轉化成特殊的電路模型引入了過(guò)大的開(kāi)銷(xiāo).BCGTV和Pantry協(xié)議可以處理包含RAM 的程序,但是Pantry協(xié)議對內存操作轉換成約束集也引入了過(guò)大的開(kāi)銷(xiāo)(目前,在T 機器運行的一些計算機程序原本需要T 步,轉換成由電路計算遠遠超過(guò)T 步).有必要改進(jìn)這兩種計算模型使得其既可以很好的處理循環(huán)結構和RAM,又不至于引入過(guò)大的開(kāi)銷(xiāo).或者設計新的更加高效的計算模型來(lái)表示通用計算.
(2)在系統和編程語(yǔ)言方面值得研究.
針對已有的電路和約束計算模型,設計定制的高級程序語(yǔ)言,降低程序到計算模型的轉化開(kāi)銷(xiāo).目前,一些可驗證計算協(xié)議編譯處理和證明系統的工作已經(jīng)有所交叉,而且很多協(xié)議在并行計算中性能更優(yōu),由于計算模型的高效轉化,可以使得驗證的效率提高.所以設計一整套相應的高級語(yǔ)言程序、計算模型、驗證機器十分必要.
目前還沒(méi)有協(xié)議在真實(shí)的云計算場(chǎng)景中測試,開(kāi)發(fā)適用于云計算實(shí)際場(chǎng)景的支持并發(fā)、訪(fǎng)問(wèn)控制、合理結構的數據庫應用的可驗證計算,使得協(xié)議支持多用戶(hù)數據庫,才能更好的構建可信的云計算.
(3)改變協(xié)議的目標和原則,減少可驗證計算
協(xié)議的限制條件,比如可驗證計算協(xié)議的無(wú)條件假設,即除了密碼學(xué)假設之外不做任何其他假設.如果假設多個(gè)證明者之間不能相互交互、合謀,那么多證明協(xié)議相對單證明者的開(kāi)銷(xiāo)則降低很多.實(shí)際上,如果假設兩個(gè)證明者至少有一個(gè)是計算正確的,就可以使得很多協(xié)議能用于特定構造的場(chǎng)景中.
(4)增加安全相關(guān)的屬性用于構建可信的云計算
Pinocchio、Pantry協(xié)議說(shuō)明了在證明者對驗證者隱藏詢(xún)問(wèn)信息的場(chǎng)景下的簡(jiǎn)單應用,還有很多地方值得研究,比如說(shuō)提供隱私相關(guān)的其他安全屬性,可以用來(lái)保護云計算用戶(hù)的隱私.再比如說(shuō)公開(kāi)可驗證性的特性使得任何擁有密碼的用戶(hù)都可以驗證其可信性,這為第3方審計來(lái)保證云計算的可信性提供了良好的思路.
可驗證計算協(xié)議把復雜的密碼學(xué)和理論計算機科學(xué)的研究成果用于實(shí)際本身就具有里程碑的意義.基于證據的可驗證計算協(xié)議是一個(gè)趨勢,這不僅使理論應用于實(shí)際,而且開(kāi)創(chuàng )了理論計算機新的研究領(lǐng)域.雖然可驗證計算協(xié)議的性能和在云計算實(shí)際場(chǎng)景中的部署還有一定的距離.但是以當前的研究節奏,相信不久的將來(lái),就會(huì )有基于證據的可驗證計算協(xié)議應用到云計算的真實(shí)場(chǎng)景中.而且,可驗證計算的潛力很大,遠遠不只是云計算.如果這個(gè)領(lǐng)域的研究性能降低到合理的范圍,除了驗證云計算之外,還有更大的價(jià)值.將會(huì )有新的方法來(lái)構建協(xié)議,在任何一個(gè)模塊為另一個(gè)模塊執行程序的場(chǎng)景中都可以應用.包括微觀(guān)層面(micro level),如果CPU可以驗證GPU,則可以消除硬件錯誤;宏觀(guān)層面(macro level)分布式計算將基于不同的可信假設構建.而且,隨著(zhù)計算能力的增加和計算成本的下降,原本無(wú)法實(shí)踐的協(xié)議也可以用于實(shí)際場(chǎng)景中.
【淺析基于可驗證計算的可信云計算優(yōu)秀論文】相關(guān)文章:
云計算閱讀答案04-27
《云計算》閱讀練習題附答案07-11
用計算器計算說(shuō)課稿11-16
簡(jiǎn)便計算說(shuō)課稿11-06
時(shí)間的計算教學(xué)反思04-14
時(shí)間的計算教學(xué)反思05-10
各地云計算中心建設項目可行性研究報告10-25