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