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)如果yf(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 判定器可以接受的计算模型，比如说电路集和约束集.Cook-Levin 理论表明这种转换理论上是可以的，因为任何程序f 都可以用图灵机来模拟，同时图灵机可以转换成布尔电路，且不会超过程序的步骤.目前可验证计算协议中编译器都是基于Fairplay和Benjamin 编译器设计的，常用的计算模型主要有电路集和约束集两种.Fairplay编译器和通常的硬件编译器不同，不能使用寄存器，没有时序逻辑，通过Fairplay Web 网站可以获取该编译器.Fairplay 可以用来把高级语言编写的程序编译成一组布尔电路集，但这种高级语言并不是通常所说的高级语言，而是一种类似Pascal或者C 语言的子集的程序语言，称为(安全函数定义)SFDL 语言.Benjamin 提出的编译器继承并改进了Fairplay 编译器，用于把高级语言表示的程序编译成一组约束集.这种编译器也引入了一种类似SFDL 的高级程序语言，称为扩展函数描述BFDL.不失一般性，本文以Benjamin 编译器为例说明从高级语言程序(C 语言为例)转化成约束集的原理和工作流程.BFDL 的语法很容易理解，很多地方都是从C和Pascal语言继承的.BFDL 语言使用C 风格的语法，是一种静态类型语言，支持类型引用：第一部分是类型声明，定义将要使用的数据类型、支持布尔型、整型、结构体和数组.
5 可验证计算协议分类
5.1 依据编译器复杂程度分类
由第3节所述，可验证计算协议主要流程包括编译处理和证明系统两个阶段，所以下文将依据协议流程对不同协议分类，并说明每种分类的特点和典型协议.
本文提到的协议中的编译处理都是直接使用Fairplay和Benjamin编译器或者对其改进后使用，生成证明系统可以接受的计算模型.依据可验证计算协议使用的编译器的复杂程度，可以分为简单编译器的可验证计算协议和复杂编译器的可验证计算协议.简单的编译器是指不支持内存随机存取的编译器，即不考虑内存概念，假设程序的输入都来源于验证者.简单编译器的可验证计算协议包括GKR、CMT、Thaler、Allspice、Pepper、Ginger、Zaatar和Pinocchio等，其中Pinocchio是第一个直接接受C语言程序的协议，而其他协议则需要先将C语言程序转化为另一种指定的高级语言比如BFDL语言，然后再转化成证明系统可以接受的计算模型.GKR使用算术电路作为计算模型，相比较之前协议使用的布尔电路减少了程序编译的开销.CMT、Thaler、Allspice、Pepper基本沿用了GKR 中的编译器，且Pepper对算术电路进行了简化，Ginger扩展了算术电路模型表示的程序种类，使得模型包含浮点数类型，不等测试，逻辑表达式，条件语句等等，因而使得模型能表示的程序更加接近于通用程序.Allspice编译器通过增加了一个静态分析器来自动确定并运行Zaatar或GKR两个协议中效率较高的一个，增加了协议的可扩展性.
复杂编译器的可验证计算协议包括Pantry和BCGTV.复杂的编译器支持内存操作，这更符合实际应用场景.Pantry中的编译器改进了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)相关的理论工具还有待于进一步改进.
一方面需要通过理论工具的研究和改进来降低验证者和证明者的开销，尤其是要把证明者的开销降低到一个合理的范围，使得协议真正能用于实际的场景中.验证者的开销可以分为固定的开销(可以分摊，通常指每个程序或者每次批处理的初始阶段的开销)和可变的开销(程序的每个实例的验证开销).研究如何降低验证者的可变开销，研究能否使用密码学操作和复杂的理论工具来降低或取消验证者初始阶段的开销.改进基于无预处理的论证系统的可验证计算协议，使得其能用于实际场景.
另一方面，研究利用理论工具来建立更加合理的计算模型，用于高效的表示通用程序，从而提高协议的效率.目前的系统要不不能很好的处理循环结构，要不就是编译的代价太高无法实用.BCGTV协议可以处理独立于数据的循环的程序，但是其对于程序转化成特殊的电路模型引入了过大的开销.BCGTV和Pantry协议可以处理包含RAM 的程序，但是Pantry协议对内存操作转换成约束集也引入了过大的开销(目前，在T 机器运行的一些计算机程序原本需要T 步，转换成由电路计算远远超过T 步).有必要改进这两种计算模型使得其既可以很好的处理循环结构和RAM，又不至于引入过大的开销.或者设计新的更加高效的计算模型来表示通用计算.
(2)在系统和编程语言方面值得研究.
针对已有的电路和约束计算模型，设计定制的高级程序语言，降低程序到计算模型的转化开销.目前，一些可验证计算协议编译处理和证明系统的工作已经有所交叉，而且很多协议在并行计算中性能更优，由于计算模型的高效转化，可以使得验证的效率提高.所以设计一整套相应的高级语言程序、计算模型、验证机器十分必要.
目前还没有协议在真实的云计算场景中测试，开发适用于云计算实际场景的支持并发、访问控制、合理结构的数据库应用的可验证计算，使得协议支持多用户数据库，才能更好的构建可信的云计算.
(3)改变协议的目标和原则，减少可验证计算
协议的限制条件，比如可验证计算协议的无条件假设，即除了密码学假设之外不做任何其他假设.如果假设多个证明者之间不能相互交互、合谋，那么多证明协议相对单证明者的开销则降低很多.实际上，如果假设两个证明者至少有一个是计算正确的，就可以使得很多协议能用于特定构造的场景中.
(4)增加安全相关的属性用于构建可信的云计算
Pinocchio、Pantry协议说明了在证明者对验证者隐藏询问信息的场景下的简单应用，还有很多地方值得研究，比如说提供隐私相关的其他安全属性，可以用来保护云计算用户的隐私.再比如说公开可验证性的特性使得任何拥有密码的用户都可以验证其可信性，这为第3方审计来保证云计算的可信性提供了良好的思路.
可验证计算协议把复杂的密码学和理论计算机科学的研究成果用于实际本身就具有里程碑的意义.基于证据的可验证计算协议是一个趋势，这不仅使理论应用于实际，而且开创了理论计算机新的研究领域.虽然可验证计算协议的性能和在云计算实际场景中的部署还有一定的距离.但是以当前的研究节奏，相信不久的将来，就会有基于证据的可验证计算协议应用到云计算的真实场景中.而且，可验证计算的潜力很大，远远不只是云计算.如果这个领域的研究性能降低到合理的范围，除了验证云计算之外，还有更大的价值.将会有新的方法来构建协议，在任何一个模块为另一个模块执行程序的场景中都可以应用.包括微观层面(micro level)，如果CPU可以验证GPU，则可以消除硬件错误;宏观层面(macro level)分布式计算将基于不同的可信假设构建.而且，随着计算能力的增加和计算成本的下降，原本无法实践的协议也可以用于实际场景中.
