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