目前，我们正在与约翰斯·霍普金斯大学（Johns Hopkins University）的Matthew Green教授共同研究通过零知识（ZK）证明创设一个可信可靠的环境，让科技企业和漏洞研究人员能够在这样的环境中无后顾之忧地沟通交流。在未来四年中，我们将推动ZK证明从理论走向实践，并面向漏洞研究人员提供可得出ZK可利用性证明的软件。此项研究隶属于美国国防部高级研究计划局（DARPA）所资助的加密验证和评估信息安全（SIEVE）项目。
近年来，ZK研究主要集中在区块链应用领域，其中参与方需要证明其交易符合公认的底层规则。而我们的研究则大幅拓宽了ZK可证明的语句种类。该项目结束后，用户将能够验证x86处理器程序的相关语句。
为什么是ZK可利用性证明？
就bug的发现和报告，软件开发者和漏洞研究人员无法达成一致。披露过多的漏洞信息会中伤第三方研究人员的收益，而披露过早则会对软件厂商的信誉造成永久的损失。各方之间的沟通往往以失败告终，同时技术产业的损失也十分惨重。
而且，在很多时候，企业不愿意接触安全团队，也不会理睬用户隐私所面临的潜在威胁。在这样的情况下，漏洞研究人员的处境十分艰难：要么在知道用户面临风险的情况下保持沉默，要么公开披露漏洞，迫使企业做出行动。如果选择了后者，研究人员则将漏洞利用路径告诉了攻击者，亲手把用户放到了砧板之上。
ZK可利用性证明将彻底颠覆了漏洞的披露方式，能够让企业能够精准地明确bug悬赏范围，让研究人员在不冒险进行公开披露情况下提交能明确证明其掌握了漏洞利用情况的证明。
设计ZK证明
通过ZK证明，验证人能够让校验人相信自己持有一段信息，同时不需要暴露信息本身。例如，Alice希望让Bob相信自己知道了某个值Y的SHA256预映射X，但是并不需要告诉Bob X具体是什么。（或许X是Alice的密码）。ZK证明最知名的工业应用或许是在ZCash等注重隐私保护的区块链领域，在此领域，用户在提交交易时，希望自己的身份、接收人的身份、交易金额都能保持匿名。为此，他们需要提交一个ZK证明，证明其交易符合区块链规则，并且发送者具有足够的资金。（请阅读Matt Green的文章了解ZK证明及相关示例。）
现在你已经知道了ZK证明的用处，但是这些算法是如何开发的呢？需要权衡哪些利弊呢？关于高效系统的开发，有三大衡量指标：验证时间（prover time）、校验时间（verifier time）和带宽（bandwidth）（即一方必须通过协议向另一方发送的数据量）。某些ZK证明不需要验证人与校验人进行交互，在此情况下，带宽仅是证明的大小。
接着，我们谈一谈目前的难点以及影响ZK证明投入实践的主要障碍。大多数传统的ZK协议要求底层语句必须首先用布尔电路（Boolean circuit）或无循环的运算电路（即组合电路）来表示。对于布尔电路，可以用AND门、NOT门和XOR门，而对于运算电路，可以用ADD门和MULT门可以想象，要想把一个要证明的语句转换成这样的电路并不容易，如果还没有简洁的数学公式，更是难上加难。例如，如果一个程序包含循环行为，那么在电路生成之前，必须先把它展开，而当程序包含数据依赖型循环时，那就无法展开了。
另外，电路尺寸也会影响到ZK协议的效率。一般情况下，验证时间与电路尺寸至少呈线性关系（通常，各个门的开销通常很大且恒定）。因此，在漏洞披露时，ZK证明需要底层漏洞能被尺寸合适的电路捕捉到。
证明可利用性
由于ZK证明一般会接收写成布尔电路的语句，因此，这里的难点在于需要布尔电路仅在漏洞利用成功时返回“true”，以此表示存在漏洞利用。
我们希望当验证人向程序中导入会造成漏洞利用的输入时，电路能够接收（accept），例如：能够让攻击者取得程序执行权限的缓冲区溢出（buffer overflow）。由于大多数二进制漏洞利用针对的是二进制（binary）和特定的处理器，因此，我们的电路必须准确地对程序的目标编译架构进行建模。最后，当程序成功运行时，以及当漏洞利用在执行过程中被触发时，我们需要一个电路来接收。
初级的方法是开发一个电路来代表目标建模处理器的“一步”（one step）。接着，我们根据要执行的程序，将容纳该程序的内存初始化；按照程序的启动时间，设置程序计数器；验证人使程序运行在自己的恶意输入上——重复处理器电路，直至程序结束，检查每一步是否均满足了漏洞利用条件。也就是说检查程序计数器是否被设置成了一个已知的“恶意”（bad）值，或被写入了一个有权限的内存地址。关于此策略的重要注意事项：在每一步均需要完整运行整个处理器电路（即便实际上只有一条指令在运行），因为单独列出一项功能会泄露相关的跟踪信息。
不幸的是，这种方法会导致电路过大，因为程序执行的每一步都需要有一个电路对核心处理器逻辑及整个RAM进行建模。即便我们把RAM限制成50 MB，对于一次漏洞利用，如果其跟踪使用了100条指令，那么产生一条相应的ZK语句会导致电路至少达到5GB。这种方法效率太低，无法用于有意义的程序。关键问题在于电路尺寸与跟踪长度和RAM大小成线性关系。为了解决这个问题，我们采用了SNARKs for C的方法，即把程序执行证明分为两部分，一部分为核心逻辑，另一部分为内存正确性。
要证明逻辑有效性，必须将处理器电路应用于程序跟踪中连续的每一对指令（sequential pair of instructions）。该电路可以验证一个寄存器状态能否合法地跟随另一寄存器状态。如果每一对状态均有效，则电路接收。不过要注意，这里的前提是内存操作是正确的。如果转移函数电路中存在一个存储器检查器，则会产生开销，此开销与所使用的RAM大小成比例。
让验证人也输入一个内存排序的执行跟踪，就能进行内存验证。如果第一个内存地址访问了一个低于第二个内存地址的内存地址（破坏了时间戳（timestamp）关系），那么这个跟踪就会在另一个跟踪之前放置一条跟踪记录。这个跟踪能让我们线性地扫描内存排序指令，确保内存访问的一致性。此方法无需根据RAM大小创建相应尺寸的电路。不过，该电路与跟踪尺寸呈线性关系，并且仅能执行基础的相等性检查（equality check），不能明确地记录每一步下的完整RAM。
最后一个要解决的问题是，验证人不受阻挠地使用与最初情况不符并且无法创建假证明的内存排序跟踪。要解决此问题，我们必须添加一个“排列检查器”（permutation checker）电路来验证我们是否确实根据内存位置对程序跟踪进行了排序。欲进一步了解相关讨论，请参见SNARKs for C论文。
建模x86
知道了如何证明ZK中存在漏洞利用，接下来我们需要把相关的处理器架构建模成布尔电路。此前已经有人对TinyRAM进行了建模，这是一种RISC架构，其目标是在ZK环境中高效运行。不幸的是，TinyRAM并未商用，而且由于漏洞利用大多依赖特定于架构的行为，因此TinyRAM不能为现实程序提供ZK可利用性证明。
我们接下来将通过建模一种相对简单且应用广泛的微处理器——MSP430进行建模，以开发ZK可利用性证明，这种简单的芯片被广泛应用于各种嵌入式系统。另外，Microcorruption CTF系统也是基于MSP430运行。我们的首要目标是针对Microcorruption受到的每一次挑战提供ZK证明。在完成此“可行性演示”后，我们会转向x86。
从简单的RISC架构过渡到复杂的CISC架构，随之而来的是各种复杂问题。对于RISC处理器的电路模型，每周期的时钟门为1至10k。另一方面，如果我们的x86处理器达到10万门级别，那么对于需要10000条指令才能完成的漏洞利用，ZK证明会达到48 GB。由于x86比MSP430复杂了几个数量级，因此即便把逻辑证明和存储器正确性证明分开，也无法天真地将其功能实现为布尔电路。
我们的解决方案基于一个显而易见的事实，即没有程序能完全用尽x86。一个程序在理论上能用到x86所支持的全部3000条指令，但实际上，大多程序只用到了几百条。我们会使用程序分析技术来判断特定二进制所需的x86最小子集，并动态地生成能够验证其正确执行能力的处理器模型。
当然，我们无法支持部分x86指令，因为这些指令实现了数据依赖型循环。例如，repz会重复后续指令，直至rcx为0。对于这样的指令，只有在运行时才能确定其实际行为，而我们的处理器电路必须是组合电路，因此无法支持此类指令。为了处理这些指令，我们会把一个静态二进制转换器（binary translator）从普通x86转成特定于我们程序的x86子集。这样的话，我们就能够处理最复杂的x86指令，而无需将其硬编码到我们的处理器电路中。
新型的bug披露模式
能够与约翰斯·霍普金斯大学以及DARPA SIEVE项目的同仁共同启动这项工作，我们倍感兴奋。我们希望得到能够从根本上颠覆漏洞披露方式的工具，以便企业能够明确其bug悬赏范围，漏洞研究人员可以安全地提交能明确证明其掌握了漏洞利用情况的证明。而且，我们还希望ZK漏洞披露能成为消费者的保护伞。研究人员可以在不公布相关漏洞的情况下，警告用户特定设备存在潜在危险，这么做是在向企业施压，逼迫他们解决本不愿解决的问题。
更广泛地说，我们想把ZK证明从学术界带入产业界，使其更贴近当今的软件、更实际。关于此技术，若您有特定用途且未在本文中未提及，我们欢迎您来函。关于ZK证明方案与电路编译器的复杂生态系统，我们积累了相应的专业知识，可为您提供帮助！
*在此我们要特别感谢Colleen Swanson和Marcella Hastings，感谢他们的校对工作，以及他们关于本文的宝贵反馈。