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)分布式计算将基于不同的可信假设构建.而且，随着计算能力的增加和计算成本的下降，原本无法实践的协议也可以用于实际场景中.
【浅析基于可验证计算的可信云计算优秀论文】相关文章：
本文来源：http://www.010zaixian.com/shiyongwen/2297451.htm